let F be infinite Field; :: thesis:
let E be F -finite FieldExtension of F; :: thesis:
consider T being finite F -algebraic Subset of E such that
A: E == FAdj (F,T) by FIELD_7:37;

assume AS: IntermediateFields (E,F) is finite ; :: thesis:

let E be F -finite FieldExtension of F; :: thesis:
assume AS: IntermediateFields (E,F) is finite ; :: thesis:
let T be finite F -algebraic Subset of E; :: thesis:
assume H0: ( card T = 2 & E == FAdj (F,T) ) ; :: thesis:
then consider a, b being object such that
H1: ( a <> b & T = {a,b} ) by CARD_2:60;
( a in {a,b} & b in {a,b} ) by TARSKI:def 2;
then reconsider a = a, b = b as Element of E by H1;
ex x, y being Element of F st
( x <> y & FAdj (F,{(a + ((@ (x,E)) * b))}) = FAdj (F,{(a + ((@ (y,E)) * b))}) & FAdj (F,{(a + ((@ (x,E)) * b))}) is Subfield of E )

proof

set I = IntermediateFields (E,F);
defpred S₁[ object , object ] means ex z being Element of F st
( $1 = z & $2 = FAdj (F,{(a + ((@ (z,E)) * b))}) );
C1: for z being Element of F ex y being Element of IntermediateFields (E,F) st S₁[z,y]

proof

let z be Element of F; :: thesis:
F is Subfield of FAdj (F,{(a + ((@ (z,E)) * b))}) by FIELD_6:36;
then reconsider U = FAdj (F,{(a + ((@ (z,E)) * b))}) as Element of IntermediateFields (E,F) by defY;
thus ex y being Element of IntermediateFields (E,F) st S₁[z,y] :: thesis:

proof

take U ; :: thesis:
thus S₁[z,U] ; :: thesis:

end;

consider f being Function of F,(IntermediateFields (E,F)) such that
C2: for z being Element of F holds S₁[z,f . z] from FUNCT_2:sch 3(C1);
C3: dom f is infinite by FUNCT_2:def 1;
rng f c= IntermediateFields (E,F) ;
then not f is one-to-one by AS, C3, CARD_1:59;
then consider x, y being object such that
C4: ( x in the carrier of F & y in the carrier of F & f . x = f . y & x <> y ) by FUNCT_2:19;
reconsider x = x, y = y as Element of F by C4;
take x ; :: thesis:
take y ; :: thesis:
thus x <> y by C4; :: thesis:
( S₁[x,f . x] & S₁[y,f . y] ) by C2;
hence FAdj (F,{(a + ((@ (x,E)) * b))}) = FAdj (F,{(a + ((@ (y,E)) * b))}) by C4; :: thesis:
thus FAdj (F,{(a + ((@ (x,E)) * b))}) is Subfield of E ; :: thesis:

end;

then consider x, y being Element of F such that
H2: ( x <> y & FAdj (F,{(a + ((@ (x,E)) * b))}) = FAdj (F,{(a + ((@ (y,E)) * b))}) & FAdj (F,{(a + ((@ (x,E)) * b))}) is Subfield of E ) ;
H3: b in FAdj (F,{(a + ((@ (x,E)) * b))})

proof

F is Subfield of FAdj (F,{(a + ((@ (x,E)) * b))}) by FIELD_6:36;
then the carrier of F c= the carrier of (FAdj (F,{(a + ((@ (x,E)) * b))})) by EC_PF_1:def 1;
then reconsider x1 = x, y1 = y as Element of (FAdj (F,{(a + ((@ (x,E)) * b))})) ;
( {(a + ((@ (x,E)) * b))} is Subset of (FAdj (F,{(a + ((@ (x,E)) * b))})) & a + ((@ (x,E)) * b) in {(a + ((@ (x,E)) * b))} ) by FIELD_6:35, TARSKI:def 1;
then reconsider u = a + ((@ (x,E)) * b) as Element of (FAdj (F,{(a + ((@ (x,E)) * b))})) ;
( {(a + ((@ (y,E)) * b))} is Subset of (FAdj (F,{(a + ((@ (y,E)) * b))})) & a + ((@ (y,E)) * b) in {(a + ((@ (y,E)) * b))} ) by FIELD_6:35, TARSKI:def 1;
then reconsider v = a + ((@ (y,E)) * b) as Element of (FAdj (F,{(a + ((@ (x,E)) * b))})) by H2;
H6: (@ (x,E)) - (@ (y,E)) <> 0. E

proof

H7: x - y <> 0. F by H2, RLVECT_1:21;
H8: F is Subring of E by FIELD_4:def 1;
H9: ( x = @ (x,E) & y = @ (y,E) ) by FIELD_7:def 4;
- y = - (@ (y,E)) by H8, FIELD_6:17, FIELD_7:def 4;
then (@ (x,E)) - (@ (y,E)) = x - y by H8, H9, FIELD_6:15;
hence (@ (x,E)) - (@ (y,E)) <> 0. E by H7, H8, C0SP1:def 3; :: thesis:

end;

(a + ((@ (x,E)) * b)) - (a + ((@ (y,E)) * b)) = ((a + ((@ (x,E)) * b)) - a) - ((@ (y,E)) * b) by RLVECT_1:27
.= ((((@ (x,E)) * b) + a) + (- a)) + (- ((@ (y,E)) * b))
.= ((((@ (x,E)) * b) + a) + (- ((@ (y,E)) * b))) + (- a) by RLVECT_1:def 3
.= ((((@ (x,E)) * b) + (- ((@ (y,E)) * b))) + a) + (- a) by RLVECT_1:def 3
.= (((@ (x,E)) * b) - ((@ (y,E)) * b)) + (a + (- a)) by RLVECT_1:def 3
.= (((@ (x,E)) * b) + ((- (@ (y,E))) * b)) + (a + (- a)) by VECTSP_1:9
.= (((@ (x,E)) + (- (@ (y,E)))) * b) + (a + (- a)) by VECTSP_1:def 3
.= (((@ (x,E)) + (- (@ (y,E)))) * b) + (0. E) by RLVECT_1:5 ;
then H7: ((a + ((@ (x,E)) * b)) - (a + ((@ (y,E)) * b))) * (((@ (x,E)) - (@ (y,E))) ") = b * (((@ (x,E)) + (- (@ (y,E)))) * (((@ (x,E)) - (@ (y,E))) ")) by GROUP_1:def 3
.= b * (1. E) by H6, VECTSP_1:def 10 ;
H8: FAdj (F,{(a + ((@ (x,E)) * b))}) is Subring of E by FIELD_5:12;
H9: x1 = @ (x,E) by FIELD_7:def 4;
- y1 = - (@ (y,E)) by H8, FIELD_6:17, FIELD_7:def 4;
then H11: x1 - y1 = (@ (x,E)) - (@ (y,E)) by H8, H9, FIELD_6:15;
not (@ (x,E)) - (@ (y,E)) is zero by H6;
then H12: (x1 - y1) " = ((@ (x,E)) - (@ (y,E))) " by H11, FIELD_6:18;
- v = - (a + ((@ (y,E)) * b)) by H8, FIELD_6:17;
then u - v = (a + ((@ (x,E)) * b)) - (a + ((@ (y,E)) * b)) by H8, FIELD_6:15;
then (u - v) * ((x1 - y1) ") = ((a + ((@ (x,E)) * b)) - (a + ((@ (y,E)) * b))) * (((@ (x,E)) - (@ (y,E))) ") by H12, H8, FIELD_6:16;
hence b in FAdj (F,{(a + ((@ (x,E)) * b))}) by H7; :: thesis:

end;

H4: a in FAdj (F,{(a + ((@ (x,E)) * b))})

proof

F is Subfield of FAdj (F,{(a + ((@ (x,E)) * b))}) by FIELD_6:36;
then the carrier of F c= the carrier of (FAdj (F,{(a + ((@ (x,E)) * b))})) by EC_PF_1:def 1;
then reconsider y1 = y as Element of (FAdj (F,{(a + ((@ (x,E)) * b))})) ;
( {(a + ((@ (y,E)) * b))} is Subset of (FAdj (F,{(a + ((@ (y,E)) * b))})) & a + ((@ (y,E)) * b) in {(a + ((@ (y,E)) * b))} ) by FIELD_6:35, TARSKI:def 1;
then reconsider v = a + ((@ (y,E)) * b) as Element of (FAdj (F,{(a + ((@ (x,E)) * b))})) by H2;
reconsider b1 = b as Element of (FAdj (F,{(a + ((@ (x,E)) * b))})) by H3;
H5: (a + ((@ (y,E)) * b)) - ((@ (y,E)) * b) = a + (((@ (y,E)) * b) + (- ((@ (y,E)) * b))) by RLVECT_1:def 3
.= a + (0. E) by RLVECT_1:5 ;
H6: FAdj (F,{(a + ((@ (x,E)) * b))}) is Subring of E by FIELD_5:12;
y1 = @ (y,E) by FIELD_7:def 4;
then (@ (y,E)) * b = y1 * b1 by H6, FIELD_6:16;
then - ((@ (y,E)) * b) = - (y1 * b1) by H6, FIELD_6:17;
then v + (- (y1 * b1)) = (a + ((@ (y,E)) * b)) - ((@ (y,E)) * b) by H6, FIELD_6:15;
hence a in FAdj (F,{(a + ((@ (x,E)) * b))}) by H5; :: thesis:

end;

now :: thesis:

let o be object ; :: thesis:
assume o in {a,b} ; :: thesis:

per cases by TARSKI:def 2;

suppose o = a ; :: thesis:

hence o in the carrier of (FAdj (F,{(a + ((@ (x,E)) * b))})) by H4; :: thesis:

end;

suppose o = b ; :: thesis:

hence o in the carrier of (FAdj (F,{(a + ((@ (x,E)) * b))})) by H3; :: thesis:

end;

then H5: {a,b} c= the carrier of (FAdj (F,{(a + ((@ (x,E)) * b))})) ;
H6: F is Subfield of FAdj (F,{(a + ((@ (x,E)) * b))}) by FIELD_6:36;
E is FieldExtension of FAdj (F,{(a + ((@ (x,E)) * b))}) by FIELD_4:7;
then FAdj (F,{a,b}) is FieldExtension of FAdj (F,{(a + ((@ (x,E)) * b))}) by H0, H1, FIELD_13:11;
then FAdj (F,{(a + ((@ (x,E)) * b))}) == FAdj (F,{a,b}) by H6, H5, FIELD_6:37, FIELD_4:7;
hence ex p being Element of E st FAdj (F,{p}) = FAdj (F,T) by H1; :: thesis:

end;

defpred S₁[ Nat] means for E being F -finite FieldExtension of F st IntermediateFields (E,F) is finite holds
for T being finite F -algebraic Subset of E st card T = $1 & E == FAdj (F,T) holds
ex p being Element of E st FAdj (F,{p}) = FAdj (F,T);
I: for k being Nat st ( for n being Nat st n < k holds
S₁[n] ) holds
S₁[k]

proof

let k be Nat; :: thesis:
assume B0: for n being Nat st n < k holds
S₁[n] ; :: thesis:
( k <= 2 implies not not k = 0 & ... & not k = 2 ) ;

per cases ;

suppose B1: k = 0 ; :: thesis:

now :: thesis:

let E be F -finite FieldExtension of F; :: thesis:
let T be finite F -algebraic Subset of E; :: thesis:
assume ( card T = k & E == FAdj (F,T) ) ; :: thesis:
then T c= the carrier of F by B1;
then B2: FAdj (F,T) == F by FIELD_7:3;
reconsider F1 = F as FieldExtension of F by FIELD_4:6;
set a = the F -algebraic Element of F1;
F is Subfield of E by FIELD_4:7;
then the carrier of F c= the carrier of E by EC_PF_1:def 1;
then reconsider a1 = the F -algebraic Element of F1 as Element of E ;
B3: FAdj (F,{a1}) = FAdj (F,{ the F -algebraic Element of F1}) by FIELD_10:9;
FAdj (F,{ the F -algebraic Element of F1}) == F by FIELD_7:3;
hence ex p being Element of E st FAdj (F,{p}) = FAdj (F,T) by B2, B3; :: thesis:

end;

hence S₁[k] ; :: thesis:

end;

suppose B1: k = 1 ; :: thesis:

now :: thesis:

let E be F -finite FieldExtension of F; :: thesis:
let T be finite F -algebraic Subset of E; :: thesis:
assume ( card T = k & E == FAdj (F,T) ) ; :: thesis:
then consider a being object such that
B2: T = {a} by B1, CARD_2:42;
a in T by B2, TARSKI:def 1;
then reconsider a1 = a as Element of E ;
FAdj (F,{a1}) = FAdj (F,T) by B2;
hence ex p being Element of E st FAdj (F,{p}) = FAdj (F,T) ; :: thesis:

end;

hence S₁[k] ; :: thesis:

end;

suppose k = 2 ; :: thesis:

hence S₁[k] by H; :: thesis:

end;

suppose B1: k > 2 ; :: thesis:

now :: thesis:

let E be F -finite FieldExtension of F; :: thesis:
assume AS: IntermediateFields (E,F) is finite ; :: thesis:
let T be finite F -algebraic Subset of E; :: thesis:
assume B2: ( card T = k & E == FAdj (F,T) ) ; :: thesis:
set a = the Element of T;
( T <> {} & T c= the carrier of E ) by B1, B2;
then reconsider a = the Element of T as Element of E ;
reconsider T1 = T \ {a} as finite F -algebraic Subset of E ;
reconsider k1 = k - 1 as Nat by B1;

now :: thesis:

let o be object ; :: thesis:
assume o in {a} ; :: thesis:
then ( o = a & T <> {} ) by B1, B2, TARSKI:def 1;
hence o in T ; :: thesis:

end;

then {a} c= T ;
then B6: T = T \/ {a} by XBOOLE_1:12
.= T1 \/ {a} by XBOOLE_1:39 ;
a in {a} by TARSKI:def 1;
then not a in T1 by XBOOLE_0:def 5;
then B9: card T = (card T1) + 1 by B6, CARD_2:41;
set E1 = FAdj (F,T1);
reconsider T2 = T1 as finite F -algebraic Subset of (FAdj (F,T1)) by FIELD_6:35;
B11: E is FAdj (F,T1) -extending by FIELD_4:7;
then B12: IntermediateFields ((FAdj (F,T1)),F) c= IntermediateFields (E,F) by simp2;
B10: FAdj (F,T2) = FAdj (F,T1) by B11, FIELD_13:19;
then consider q1 being Element of (FAdj (F,T1)) such that
B8: FAdj (F,{q1}) = FAdj (F,T2) by B12, AS, B0, B2, B9, NAT_1:19;
the carrier of (FAdj (F,T1)) c= the carrier of E by EC_PF_1:def 1;
then reconsider q = q1 as Element of E ;
B4: FAdj (F,T) = FAdj (F,({q} \/ {a})) by B6, B8, B10, B11, FIELD_13:19, simp1
.= FAdj (F,{q,a}) by ENUMSET1:1 ;

per cases ;

suppose q = a ; :: thesis:

then {q,a} = {a} by ENUMSET1:29;
hence ex p being Element of E st FAdj (F,{p}) = FAdj (F,T) by B4; :: thesis:

end;

suppose q <> a ; :: thesis:

then card {q,a} = 2 by CARD_2:57;
hence ex p being Element of E st FAdj (F,{p}) = FAdj (F,T) by H, B4, B2, AS; :: thesis:

end;

hence S₁[k] ; :: thesis:

end;

J: for n being Nat holds S₁[n] from NAT_1:sch 4(I);
consider n being Nat such that
K: card T = n ;
consider p being Element of E such that
L: FAdj (F,{p}) = FAdj (F,T) by AS, A, J, K;
thus E is F -simple by A, L; :: thesis:

end;

now :: thesis:

assume E is F -simple ; :: thesis:
then consider a being Element of E such that
C0: E == FAdj (F,{a}) ;
set I = IntermediateFields (E,F);
defpred S₁[ object , object ] means ex F1 being Field ex K being FieldExtension of F1 ex E1 being b₁ -extending FieldExtension of F1 ex a1 being b₂ -algebraic Element of E1 st
( F1 = F & E1 = E & a1 = a & $1 = K & $2 = MinPoly (a1,K) );
C1: for z being Element of IntermediateFields (E,F) ex y being Element of (Polynom-Ring E) st S₁[z,y]

proof

let z be Element of IntermediateFields (E,F); :: thesis:
consider K being strict Field such that
C2: ( K = z & F is Subfield of K & K is Subfield of E ) by defY;
reconsider K = K as FieldExtension of F by C2, FIELD_4:7;
reconsider E1 = E as F -extending FieldExtension of F by C2, FIELD_4:7;
reconsider a1 = a as K -algebraic Element of E1 ;
thus ex y being Element of (Polynom-Ring E) st S₁[z,y] :: thesis:

proof

E is FieldExtension of K by C2, FIELD_4:7;
then the carrier of (Polynom-Ring K) c= the carrier of (Polynom-Ring E) by FIELD_4:10;
then reconsider y = MinPoly (a1,K) as Element of (Polynom-Ring E) ;
take y ; :: thesis:
thus S₁[z,y] by C2; :: thesis:

end;

consider f being Function of (IntermediateFields (E,F)),(Polynom-Ring E) such that
C2: for z being Element of IntermediateFields (E,F) holds S₁[z,f . z] from FUNCT_2:sch 3(C1);
C3: for K being FieldExtension of F
for E1 being FieldExtension of K
for a1 being b₁ -algebraic Element of E1 st K is strict & E1 = E & a1 = a holds
f . K = MinPoly (a1,K)

proof

let K be FieldExtension of F; :: thesis:
let E1 be FieldExtension of K; :: thesis:
let a1 be K -algebraic Element of E1; :: thesis:
assume C4: ( K is strict & E1 = E & a1 = a ) ; :: thesis:
( F is Subfield of K & K is Subfield of E1 ) by FIELD_4:7;
then K is Element of IntermediateFields (E,F) by C4, simp3;
then S₁[K,f . K] by C2;
then consider F1 being Field, K1 being FieldExtension of F1, E2 being F1 -extending FieldExtension of F1, a2 being K1 -algebraic Element of E2 such that
C5: ( F1 = F & E2 = E & a2 = a & K1 = K & f . K1 = MinPoly (a2,K1) ) ;
thus f . K = MinPoly (a1,K) by C4, C5; :: thesis:

end;

C4: f is one-to-one

proof

now :: thesis:

let x, y be object ; :: thesis:
assume C5: ( x in IntermediateFields (E,F) & y in IntermediateFields (E,F) & f . x = f . y ) ; :: thesis:
then consider Kx being strict Field such that
C6: ( Kx = x & F is Subfield of Kx & Kx is Subfield of E ) by defY;
consider Ky being strict Field such that
C7: ( Ky = y & F is Subfield of Ky & Ky is Subfield of E ) by C5, defY;
reconsider Kx = Kx as FieldExtension of F by C6, FIELD_4:7;
reconsider Eh = E as Kx -extending FieldExtension of F by C6, FIELD_4:7;
Eh is F -finite ;
then reconsider Kx = Kx as F -finite FieldExtension of F by FIELD_7:31;
reconsider Ky = Ky as FieldExtension of F by C7, FIELD_4:7;
reconsider Eh = E as Ky -extending FieldExtension of F by C7, FIELD_4:7;
Eh is F -finite ;
then reconsider Ky = Ky as F -finite FieldExtension of F by FIELD_7:31;
reconsider Ex = E as F -extending F -finite FieldExtension of F by C6, FIELD_4:7;
reconsider Ey = E as F -extending F -finite FieldExtension of F by C7, FIELD_4:7;
reconsider ax = a as Kx -algebraic Element of Ex ;
reconsider ay = a as Ky -algebraic Element of Ey ;
( the carrier of (Polynom-Ring Kx) c= the carrier of (Polynom-Ring Ex) & the carrier of (Polynom-Ring Ky) c= the carrier of (Polynom-Ring Ey) ) by FIELD_4:10;
then reconsider p1 = MinPoly (ax,Kx), p2 = MinPoly (ay,Ky) as Element of the carrier of (Polynom-Ring E) ;
C8: ( Kx == FAdj (F,(Coeff (MinPoly (ax,Kx)))) & Ky == FAdj (F,(Coeff (MinPoly (ay,Ky)))) ) by C0, simpmainhelp;
C9: p1 = f . Ky by C5, C6, C7, C3
.= p2 by C3 ;
C10: ( Coeff p1 = Coeff (MinPoly (ax,Kx)) & Coeff p2 = Coeff (MinPoly (ay,Ky)) ) by co;
then FAdj (F,(Coeff (MinPoly (ax,Kx)))) = FAdj (F,(Coeff p2)) by C9, FIELD_13:19
.= FAdj (F,(Coeff (MinPoly (ay,Ky)))) by C10, FIELD_13:19 ;
hence x = y by C6, C7, C8; :: thesis:

end;

hence f is one-to-one by FUNCT_2:19; :: thesis:

end;

the carrier of (Polynom-Ring F) c= the carrier of (Polynom-Ring E) by FIELD_4:10;
then reconsider q = MinPoly (a,F) as Element of the carrier of (Polynom-Ring E) ;
q <> 0_. F ;
then q <> 0_. E by FIELD_4:12;
then reconsider q = q as non zero Element of the carrier of (Polynom-Ring E) by UPROOTS:def 5;
C5: for p being Element of the carrier of (Polynom-Ring E) st p in rng f holds
p divides q

proof

let o be Element of the carrier of (Polynom-Ring E); :: thesis:
assume o in rng f ; :: thesis:
then consider x being object such that
C7: ( x in IntermediateFields (E,F) & o = f . x ) by FUNCT_2:11;
reconsider x = x as Element of IntermediateFields (E,F) by C7;
S₁[x,f . x] by C2;
then consider F1 being Field, K1 being FieldExtension of F1, E2 being F1 -extending FieldExtension of F1, a2 being K1 -algebraic Element of E2 such that
C8: ( F1 = F & E2 = E & a2 = a & K1 = x & f . K1 = MinPoly (a2,K1) ) ;
the carrier of (Polynom-Ring F) c= the carrier of (Polynom-Ring K1) by C8, FIELD_4:10;
then reconsider pF = MinPoly (a,F) as Element of the carrier of (Polynom-Ring K1) ;
Ext_eval (pF,a) = Ext_eval ((MinPoly (a,F)),a) by C8, FIELD_8:6
.= 0. E by FIELD_6:52 ;
then consider r being Polynomial of K1 such that
B: (MinPoly (a2,K1)) *' r = pF by C8, FIELD_6:53, RING_4:1;
C: r is Element of the carrier of (Polynom-Ring K1) by POLYNOM3:def 10;
the carrier of (Polynom-Ring K1) c= the carrier of (Polynom-Ring E) by C8, FIELD_4:10;
then reconsider q2 = MinPoly (a2,K1), r2 = r as Element of the carrier of (Polynom-Ring E) by C;
q2 *' r2 = (MinPoly (a2,K1)) *' r by C8, FIELD_4:17;
hence o divides q by C8, C7, B, RING_4:1; :: thesis:

end;

now :: thesis:

let o be object ; :: thesis:
assume C6: o in rng f ; :: thesis:
then consider x being object such that
C7: ( x in IntermediateFields (E,F) & o = f . x ) by FUNCT_2:11;
reconsider x = x as Element of IntermediateFields (E,F) by C7;
S₁[x,f . x] by C2;
then consider F1 being Field, K1 being FieldExtension of F1, E2 being F1 -extending FieldExtension of F1, a2 being K1 -algebraic Element of E2 such that
C8: ( F1 = F & E2 = E & a2 = a & K1 = x & f . K1 = MinPoly (a2,K1) ) ;
the carrier of (Polynom-Ring K1) c= the carrier of (Polynom-Ring E) by C8, FIELD_4:10;
then reconsider p = MinPoly (a2,K1) as Element of the carrier of (Polynom-Ring E) ;
C9: K1 is Subfield of E by C8, FIELD_4:7;
LC p = LC (MinPoly (a2,K1)) by C8, FIELD_8:5
.= 1. K1 by RATFUNC1:def 7
.= 1. E by C9, EC_PF_1:def 1 ;
then reconsider p = p as monic Element of the carrier of (Polynom-Ring E) by RATFUNC1:def 7;
p divides q by C8, C7, C6, C5;
hence o in { p where p is monic Element of the carrier of (Polynom-Ring E) : p divides q } by C8, C7; :: thesis:

end;

then rng f c= MonicDivisors q ;
then dom f is finite by C4, CARD_1:59;
hence IntermediateFields (E,F) is finite by FUNCT_2:def 1; :: thesis:

end;

hence ( E is F -simple iff IntermediateFields (E,F) is finite ) by B; :: thesis: