let F be Field; :: thesis: for E being FieldExtension of F
for T being non empty finite F -algebraic Subset of E holds
( FAdj (F,T) is F -normal iff for a being Element of T holds MinPoly (a,F) splits_in FAdj (F,T) )
let E be FieldExtension of F; :: thesis: for T being non empty finite F -algebraic Subset of E holds
( FAdj (F,T) is F -normal iff for a being Element of T holds MinPoly (a,F) splits_in FAdj (F,T) )
let T be non empty finite F -algebraic Subset of E; :: thesis: ( FAdj (F,T) is F -normal iff for a being Element of T holds MinPoly (a,F) splits_in FAdj (F,T) )
set V = FAdj (F,T);

A: now :: thesis: ( FAdj (F,T) is F -normal implies for a being Element of T holds MinPoly (a,F) splits_in FAdj (F,T) )

assume B: FAdj (F,T) is F -normal ; :: thesis: for a being Element of T holds MinPoly (a,F) splits_in FAdj (F,T)

now :: thesis: for a being Element of T holds MinPoly (a,F) splits_in FAdj (F,T)

let a be Element of T; :: thesis: MinPoly (a,F) splits_in FAdj (F,T)
( T is Subset of (FAdj (F,T)) & a in T ) by FIELD_6:35;
then reconsider a1 = a as Element of (FAdj (F,T)) ;
E is FAdj (F,T) -extending by FIELD_4:7;
then Ext_eval ((MinPoly (a,F)),a1) = Ext_eval ((MinPoly (a,F)),a) by FIELD_6:11
.= 0. E by FIELD_6:52
.= 0. (FAdj (F,T)) by EC_PF_1:def 1 ;
then a1 is_a_root_of MinPoly (a,F), FAdj (F,T) by FIELD_4:def 2;
hence MinPoly (a,F) splits_in FAdj (F,T) by B, FIELD_4:def 3; :: thesis: verum

end;

hence for a being Element of T holds MinPoly (a,F) splits_in FAdj (F,T) ; :: thesis: verum

end;

now :: thesis: ( ( for a being Element of T holds MinPoly (a,F) splits_in FAdj (F,T) ) implies FAdj (F,T) is F -normal )

assume BB: for a being Element of T holds MinPoly (a,F) splits_in FAdj (F,T) ; :: thesis: FAdj (F,T) is F -normal
set M = { (MinPoly (a,F)) where a is Element of T : verum } ;
set x = the Element of T;
E: MinPoly ( the Element of T,F) in { (MinPoly (a,F)) where a is Element of T : verum } ;

now :: thesis: for o being object st o in { (MinPoly (a,F)) where a is Element of T : verum } holds
o in the carrier of (Polynom-Ring F)

let o be object ; :: thesis: ( o in { (MinPoly (a,F)) where a is Element of T : verum } implies o in the carrier of (Polynom-Ring F) )
assume o in { (MinPoly (a,F)) where a is Element of T : verum } ; :: thesis: o in the carrier of (Polynom-Ring F)
then consider a being Element of T such that
F: o = MinPoly (a,F) ;
thus o in the carrier of (Polynom-Ring F) by F; :: thesis: verum

end;

then reconsider M = { (MinPoly (a,F)) where a is Element of T : verum } as non empty Subset of the carrier of (Polynom-Ring F) by E, TARSKI:def 3;
defpred S₁[ object , object ] means ex a being Element of T st
( a = $1 & $2 = MinPoly (a,F) );
E1: for a being Element of T ex y being Element of M st S₁[a,y]

proof

let a be Element of T; :: thesis: ex y being Element of M st S₁[a,y]
MinPoly (a,F) in { (MinPoly (a,F)) where a is Element of T : verum } ;
then reconsider y = MinPoly (a,F) as Element of M ;
take y ; :: thesis: S₁[a,y]
thus S₁[a,y] ; :: thesis: verum

end;

consider f being Function of T,M such that
E2: for a being Element of T holds S₁[a,f . a] from FUNCT_2:sch 3(E1);
E3: dom f = T by FUNCT_2:def 1;
rng f = M

proof

E4: now :: thesis: for o being object st o in M holds
o in rng f

let o be object ; :: thesis: ( o in M implies o in rng f )
assume o in M ; :: thesis: o in rng f
then consider a being Element of T such that
E5: o = MinPoly (a,F) ;
S₁[a,f . a] by E2;
hence o in rng f by E5, E3, FUNCT_1:def 3; :: thesis: verum

end;

now :: thesis: for o being object st o in rng f holds
o in M

let o be object ; :: thesis: ( o in rng f implies o in M )
assume o in rng f ; :: thesis: o in M
then consider a being object such that
E4: ( a in dom f & f . a = o ) by FUNCT_1:def 3;
reconsider a = a as Element of T by E4;
S₁[a,o] by E2, E4;
hence o in M ; :: thesis: verum

end;

hence rng f = M by E4, TARSKI:2; :: thesis: verum

end;

then reconsider M = M as non empty finite Subset of the carrier of (Polynom-Ring F) ;
( rng (canFS M) c= M & M c= the carrier of (Polynom-Ring F) ) by FINSEQ_1:def 4;
then ( len (canFS M) = card M & rng (canFS M) c= the carrier of (Polynom-Ring F) ) by FINSEQ_1:93;
then reconsider G = canFS M as non empty FinSequence of the carrier of (Polynom-Ring F) by FINSEQ_1:def 4;
reconsider p = Product G as Element of the carrier of (Polynom-Ring F) ;
F: ex i being Element of dom G st G . i = MinPoly ( the Element of T,F)

proof

rng (canFS M) = M by FUNCT_2:def 3;
then MinPoly ( the Element of T,F) in rng (canFS M) ;
then consider i being object such that
H: ( i in dom (canFS M) & (canFS M) . i = MinPoly ( the Element of T,F) ) by FUNCT_1:def 3;
thus ex i being Element of dom G st G . i = MinPoly ( the Element of T,F) by H; :: thesis: verum

end;

not Product G is constant

proof

now :: thesis: for i being Element of dom G holds G . i <> 0_. F

let i be Element of dom G; :: thesis: G . i <> 0_. F
H1: G . i in rng G by FUNCT_1:def 3;
rng (canFS M) c= M by FINSEQ_1:def 4;
then G . i in M by H1;
then consider a being Element of T such that
H2: G . i = MinPoly (a,F) ;
thus G . i <> 0_. F by H2; :: thesis: verum

end;

then H: deg p >= deg (MinPoly ( the Element of T,F)) by F, lemNor1deg;
deg (MinPoly ( the Element of T,F)) > 0 by RING_4:def 4;
hence not Product G is constant by H, RING_4:def 4; :: thesis: verum

end;

then reconsider p = Product G as non constant Element of the carrier of (Polynom-Ring F) ;
D: p splits_in FAdj (F,T)

proof

deg p > 0 by RING_4:def 4;
then reconsider q = p as non constant Polynomial of F by RATFUNC1:def 2;

now :: thesis: for i being Element of dom G
for p being Polynomial of F holds
( not p = G . i or p is constant or p splits_in FAdj (F,T) )

let i be Element of dom G; :: thesis: for p being Polynomial of F holds
( not p = G . i or p is constant or p splits_in FAdj (F,T) )
let p be Polynomial of F; :: thesis: ( not p = G . i or p is constant or p splits_in FAdj (F,T) )
assume D1: p = G . i ; :: thesis: ( p is constant or p splits_in FAdj (F,T) )
( rng G c= M & G . i in rng G ) by FUNCT_1:3, FINSEQ_1:def 4;
then G . i in M ;
then consider a being Element of T such that
D2: G . i = MinPoly (a,F) ;
thus ( p is constant or p splits_in FAdj (F,T) ) by D1, D2, BB; :: thesis: verum

end;

then q splits_in FAdj (F,T) by lemNor1a;
hence p splits_in FAdj (F,T) ; :: thesis: verum

end;

now :: thesis: for K being FieldExtension of F st p splits_in K & K is Subfield of FAdj (F,T) holds
K == FAdj (F,T)

let K be FieldExtension of F; :: thesis: ( p splits_in K & K is Subfield of FAdj (F,T) implies K == FAdj (F,T) )
assume E1: ( p splits_in K & K is Subfield of FAdj (F,T) ) ; :: thesis: K == FAdj (F,T)
then E2: ( F is Subfield of K & FAdj (F,T) is K -extending ) by FIELD_4:7;
then E3: Roots (K,p) = Roots ((FAdj (F,T)),p) by D, E1, FIELD_8:29;
E4: Roots ((FAdj (F,T)),p) = { a where a is Element of (FAdj (F,T)) : a is_a_root_of p, FAdj (F,T) } by FIELD_4:def 4;
E8: ( E is FAdj (F,T) -extending & K is Subfield of E ) by E1, EC_PF_1:5, FIELD_4:7;
T is Subset of K

proof

now :: thesis: for o being object st o in T holds
o in the carrier of K

let o be object ; :: thesis: ( o in T implies o in the carrier of K )
assume Y: o in T ; :: thesis: o in the carrier of K
then reconsider a = o as Element of T ;
T is Subset of (FAdj (F,T)) by FIELD_6:35;
then reconsider a1 = a as Element of (FAdj (F,T)) by Y;
rng G = M by FUNCT_2:def 3;
then MinPoly (a,F) in rng G ;
then consider i being object such that
E5: ( i in dom G & G . i = MinPoly (a,F) ) by FUNCT_1:def 3;
Ext_eval ((MinPoly (a,F)),a) = 0. E by FIELD_6:52;
then 0. E = Ext_eval (p,a) by E5, lemNor1b
.= Ext_eval (p,a1) by E8, FIELD_7:14 ;
then Ext_eval (p,a1) = 0. (FAdj (F,T)) by EC_PF_1:def 1;
then a1 is_a_root_of p, FAdj (F,T) by FIELD_4:def 2;
then a1 in Roots ((FAdj (F,T)),p) by E4;
hence o in the carrier of K by E3; :: thesis: verum

end;

hence T is Subset of K by TARSKI:def 3; :: thesis: verum

end;

then FAdj (F,T) is Subfield of K by E2, E8, FIELD_6:37;
hence K == FAdj (F,T) by E1, FIELD_7:def 2; :: thesis: verum

end;

then FAdj (F,T) is SplittingField of p by D, FIELD_8:def 1;
hence FAdj (F,T) is F -normal ; :: thesis: verum

end;

hence ( FAdj (F,T) is F -normal iff for a being Element of T holds MinPoly (a,F) splits_in FAdj (F,T) ) by A; :: thesis: verum