let F be Field; for E being FieldExtension of F
for G being non empty FinSequence of the carrier of (Polynom-Ring E) st ( for i being Nat st i in dom G holds
ex a being Element of F st G . i = rpoly (1,a) ) holds
Product G is Ppoly of F
let E be FieldExtension of F; for G being non empty FinSequence of the carrier of (Polynom-Ring E) st ( for i being Nat st i in dom G holds
ex a being Element of F st G . i = rpoly (1,a) ) holds
Product G is Ppoly of F
let G be non empty FinSequence of the carrier of (Polynom-Ring E); ( ( for i being Nat st i in dom G holds
ex a being Element of F st G . i = rpoly (1,a) ) implies Product G is Ppoly of F )
assume AS:
for i being Nat st i in dom G holds
ex a being Element of F st G . i = rpoly (1,a)
; Product G is Ppoly of F
F is Subfield of E
by FIELD_4:7;
then H1:
the carrier of F c= the carrier of E
by EC_PF_1:def 1;
defpred S1[ Nat] means for G being non empty FinSequence of (Polynom-Ring E) st len G = $1 & ( for i being Nat st i in dom G holds
ex a being Element of F st G . i = rpoly (1,a) ) holds
Product G is Ppoly of F;
IA:
S1[ 0 ]
;
IS:
now for k being Nat st S1[k] holds
S1[k + 1]let k be
Nat;
( S1[k] implies S1[k + 1] )assume IV:
S1[
k]
;
S1[k + 1]now for G being non empty FinSequence of (Polynom-Ring E) st len G = k + 1 & ( for i being Nat st i in dom G holds
ex a being Element of F st G . i = rpoly (1,a) ) holds
Product G is Ppoly of Flet G be non
empty FinSequence of
(Polynom-Ring E);
( len G = k + 1 & ( for i being Nat st i in dom G holds
ex a being Element of F st G . i = rpoly (1,a) ) implies Product b1 is Ppoly of F )assume A:
(
len G = k + 1 & ( for
i being
Nat st
i in dom G holds
ex
a being
Element of
F st
G . i = rpoly (1,
a) ) )
;
Product b1 is Ppoly of Fper cases
( k = 0 or k > 0 )
;
suppose S:
k = 0
;
Product b1 is Ppoly of Fthen
1
in Seg (len G)
by A;
then
1
in dom G
by FINSEQ_1:def 3;
then consider a being
Element of
F such that A0:
G . 1
= rpoly (1,
a)
by A;
H:
G = <*(rpoly (1,a))*>
by A0, A, S, FINSEQ_1:40;
reconsider b =
a as
Element of
E by H1;
rpoly (1,
a)
= rpoly (1,
b)
by FIELD_4:21;
then
rpoly (1,
a) is
Element of the
carrier of
(Polynom-Ring E)
by POLYNOM3:def 10;
then
Product G = rpoly (1,
a)
by H, GROUP_4:9;
hence
Product G is
Ppoly of
F
by RING_5:51;
verum end; suppose S:
k > 0
;
Product b1 is Ppoly of Fconsider H being
FinSequence,
y being
object such that B2:
G = H ^ <*y*>
by FINSEQ_1:46;
B2a:
rng H c= rng G
by B2, FINSEQ_1:29;
B2b:
rng G c= the
carrier of
(Polynom-Ring E)
by FINSEQ_1:def 4;
then reconsider H =
H as
FinSequence of
(Polynom-Ring E) by B2a, XBOOLE_1:1, FINSEQ_1:def 4;
B3:
len G =
(len H) + (len <*y*>)
by B2, FINSEQ_1:22
.=
(len H) + 1
by FINSEQ_1:39
;
then reconsider H =
H as non
empty FinSequence of
(Polynom-Ring E) by S, A;
reconsider q =
Product H as
Polynomial of
E by POLYNOM3:def 10;
C:
dom H c= dom G
by B2, FINSEQ_1:26;
then reconsider q1 =
Product H as
Ppoly of
F by B3, A, IV;
rng <*y*> = {y}
by FINSEQ_1:39;
then G5:
y in rng <*y*>
by TARSKI:def 1;
rng <*y*> c= rng G
by B2, FINSEQ_1:30;
then reconsider y =
y as
Element of
(Polynom-Ring E) by G5, B2b;
dom <*y*> = {1}
by FINSEQ_1:2, FINSEQ_1:def 8;
then
1
in dom <*y*>
by TARSKI:def 1;
then B6:
G . (k + 1) =
<*y*> . 1
by B2, B3, A, FINSEQ_1:def 7
.=
y
by FINSEQ_1:def 8
;
dom G = Seg (k + 1)
by A, FINSEQ_1:def 3;
then consider a being
Element of
F such that B9:
y = rpoly (1,
a)
by A, B6, FINSEQ_1:4;
reconsider b =
a as
Element of
E by H1;
reconsider y1 =
rpoly (1,
b) as
Element of
(Polynom-Ring E) by POLYNOM3:def 10;
B8:
rpoly (1,
b)
= rpoly (1,
a)
by FIELD_4:21;
B7:
rpoly (1,
a) is
Ppoly of
F
by RING_5:51;
Product G =
(Product H) * y
by B2, GROUP_4:6
.=
q *' (rpoly (1,b))
by B8, B9, POLYNOM3:def 10
.=
q1 *' (rpoly (1,a))
by B8, FIELD_4:17
;
hence
Product G is
Ppoly of
F
by B7, RING_5:52;
verum end; end; hence
S1[
k + 1]
;
verum end;
I:
for k being Nat holds S1[k]
from NAT_1:sch 2(IA, IS);
consider n being Nat such that
J:
len G = n
;
thus
Product G is Ppoly of F
by I, J, AS; verum