let F be Field; for p being non constant Element of the carrier of (Polynom-Ring F)
for U being FieldExtension of F
for E being b2 -extending FieldExtension of F st p splits_in E holds
( p splits_in U iff for a being Element of E st a is_a_root_of p,E holds
a in U )
let p be non constant Element of the carrier of (Polynom-Ring F); for U being FieldExtension of F
for E being b1 -extending FieldExtension of F st p splits_in E holds
( p splits_in U iff for a being Element of E st a is_a_root_of p,E holds
a in U )
let U be FieldExtension of F; for E being U -extending FieldExtension of F st p splits_in E holds
( p splits_in U iff for a being Element of E st a is_a_root_of p,E holds
a in U )
let E be U -extending FieldExtension of F; ( p splits_in E implies ( p splits_in U iff for a being Element of E st a is_a_root_of p,E holds
a in U ) )
assume
p splits_in E
; ( p splits_in U iff for a being Element of E st a is_a_root_of p,E holds
a in U )
then consider aE being non zero Element of E, qE being Ppoly of E such that
B:
p = aE * qE
by FIELD_4:def 5;
reconsider aqE = aE * qE as Element of the carrier of (Polynom-Ring E) by POLYNOM3:def 10;
consider GE being non empty FinSequence of the carrier of (Polynom-Ring E) such that
C:
( qE = Product GE & ( for i being Nat st i in dom GE holds
ex a being Element of E st GE . i = rpoly (1,a) ) )
by RING_5:def 4;
D:
now for x being Element of E st x is_a_root_of p,E holds
ex i being Nat st
( i in dom GE & GE . i = rpoly (1,x) )let x be
Element of
E;
( x is_a_root_of p,E implies ex i being Nat st
( i in dom GE & GE . i = rpoly (1,x) ) )assume
x is_a_root_of p,
E
;
ex i being Nat st
( i in dom GE & GE . i = rpoly (1,x) )then 0. E =
Ext_eval (
p,
x)
by FIELD_4:def 2
.=
eval (
aqE,
x)
by B, FIELD_4:26
.=
aE * (eval (qE,x))
by POLYNOM5:30
;
then
eval (
qE,
x)
= 0. E
by VECTSP_2:def 1;
hence
ex
i being
Nat st
(
i in dom GE &
GE . i = rpoly (1,
x) )
by C, RATFUNC1:12;
verum end;
U is Subfield of E
by FIELD_4:7;
then H1:
the carrier of U c= the carrier of E
by EC_PF_1:def 1;
reconsider p0 = p as Element of the carrier of (Polynom-Ring F) ;
p is Polynomial of E
by FIELD_4:8;
then reconsider p1 = p as Element of the carrier of (Polynom-Ring E) by POLYNOM3:def 10;
A:
now ( p splits_in U implies for a being Element of E st a is_a_root_of p,E holds
a in U )assume
p splits_in U
;
for a being Element of E st a is_a_root_of p,E holds
a in Uthen consider a being non
zero Element of
U,
q being
Ppoly of
U such that A1:
p = a * q
by FIELD_4:def 5;
consider GU being non
empty FinSequence of the
carrier of
(Polynom-Ring U) such that A4:
(
q = Product GU & ( for
i being
Nat st
i in dom GU holds
ex
a being
Element of
U st
GU . i = rpoly (1,
a) ) )
by RING_5:def 4;
reconsider q1 =
q as
Ppoly of
E by lemmapp;
reconsider b =
a as
Element of
E by H1;
A2:
U is
Subfield of
E
by FIELD_4:7;
now for x being Element of E st x is_a_root_of p,E holds
x in the carrier of Ulet x be
Element of
E;
( x is_a_root_of p,E implies x in the carrier of U )assume
x is_a_root_of p,
E
;
x in the carrier of Uthen consider j being
Nat such that B3:
(
j in dom GE &
GE . j = rpoly (1,
x) )
by D;
qE = q
by A1, B, lemma2d;
then consider i being
Nat such that G:
(
i in dom GU &
GU . i = rpoly (1,
x) )
by B3, A4, C, lemma2u;
reconsider v =
rpoly (1,
x) as
Element of the
carrier of
(Polynom-Ring U) by G, PARTFUN1:4;
U is
Subring of
E
by A2, FIELD_5:12;
then - (v . 0) =
- ((rpoly (1,x)) . 0)
by FIELD_6:17
.=
- (- ((power E) . (x,(1 + 0))))
by HURWITZ:25
.=
- (- (((power E) . (x,0)) * x))
by GROUP_1:def 7
.=
- (- ((1_ E) * x))
by GROUP_1:def 7
.=
x
;
hence
x in the
carrier of
U
;
verum end; hence
for
a being
Element of
E st
a is_a_root_of p,
E holds
a in U
;
verum end;
X:
( aE * qE is Element of the carrier of (Polynom-Ring E) & p is Element of the carrier of (Polynom-Ring F) )
by POLYNOM3:def 10;
now ( ( for a being Element of E st a is_a_root_of p,E holds
a in U ) implies p splits_in U )assume AS:
for
a being
Element of
E st
a is_a_root_of p,
E holds
a in U
;
p splits_in Unow for i being Nat st i in dom GE holds
ex b being Element of U st GE . i = rpoly (1,b)let i be
Nat;
( i in dom GE implies ex b being Element of U st GE . i = rpoly (1,b) )assume E:
i in dom GE
;
ex b being Element of U st GE . i = rpoly (1,b)then consider c being
Element of
E such that F:
GE . i = rpoly (1,
c)
by C;
eval (
qE,
c)
= 0. E
by E, F, C, RATFUNC1:12;
then
eval (
(aE * qE),
c)
= aE * (0. E)
by RING_5:7;
then
Ext_eval (
p,
c)
= 0. E
by X, B, FIELD_4:26;
then
c in U
by AS, FIELD_4:def 2;
then reconsider b =
c as
Element of
U ;
rpoly (1,
c)
= rpoly (1,
b)
by FIELD_4:21;
hence
ex
b being
Element of
U st
GE . i = rpoly (1,
b)
by F;
verum end; then reconsider qU =
qE as
Ppoly of
U by C, u8;
I3:
aE =
LC (aE * qE)
by u6
.=
LC p
by B, lemma2e
;
U is
Subring of
E
by FIELD_4:def 1;
then I4:
0. U = 0. E
by C0SP1:def 3;
F is
Subring of
U
by FIELD_4:def 1;
then
the
carrier of
F c= the
carrier of
U
by C0SP1:def 3;
then reconsider aU =
aE as non
zero Element of
U by I3, I4, STRUCT_0:def 12;
I2:
aU | U = aE | E
by FIELD_6:23;
aU * qU =
(aU | U) *' qU
by poly1
.=
(aE | E) *' qE
by I2, FIELD_4:17
.=
aE * qE
by poly1
;
hence
p splits_in U
by B, FIELD_4:def 5;
verum end;
hence
( p splits_in U iff for a being Element of E st a is_a_root_of p,E holds
a in U )
by A; verum