let F be Field; :: thesis: for E being FieldExtension of F holds
( E is F -finite iff ex T being finite F -algebraic Subset of E st E == FAdj (F,T) )
let E be FieldExtension of F; :: thesis: ( E is F -finite iff ex T being finite F -algebraic Subset of E st E == FAdj (F,T) )
defpred S₁[ Nat] means for F being Field
for E being FieldExtension of F st deg (E,F) = $1 holds
ex T being finite b₁ -algebraic Subset of E st E == FAdj (F,T);

IA: now :: thesis: for F being Field
for E being FieldExtension of F st deg (E,F) = 1 holds
ex T being finite b₁ -algebraic Subset of E st E == FAdj (F,T)

let F be Field; :: thesis: for E being FieldExtension of F st deg (E,F) = 1 holds
ex T being finite F -algebraic Subset of E st E == FAdj (F,T)
let E be FieldExtension of F; :: thesis: ( deg (E,F) = 1 implies ex T being finite F -algebraic Subset of E st E == FAdj (F,T) )
assume deg (E,F) = 1 ; :: thesis: ex T being finite F -algebraic Subset of E st E == FAdj (F,T)
then A: F == E by str1a;
{} c= the carrier of E ;
then reconsider T = {} as finite Subset of E ;
T is F -algebraic ;
then reconsider T = T as finite F -algebraic Subset of E ;
{} c= the carrier of F ;
then FAdj (F,T) == F by Th1;
then E == FAdj (F,T) by A;
hence ex T being finite F -algebraic Subset of E st E == FAdj (F,T) ; :: thesis: verum

end;

IS: now :: thesis: for k being Nat st k >= 1 & ( for n being Nat st n >= 1 & n < k holds
S₁[n] ) holds
S₁[k]

let k be Nat; :: thesis: ( k >= 1 & ( for n being Nat st n >= 1 & n < k holds
S₁[n] ) implies S₁[k] )
assume AS: ( k >= 1 & ( for n being Nat st n >= 1 & n < k holds
S₁[n] ) ) ; :: thesis: S₁[k]

now :: thesis: for F being Field
for E being FieldExtension of F st deg (E,F) = k holds
ex T being finite b₁ -algebraic Subset of E st E == FAdj (F,T)

let F be Field; :: thesis: for E being FieldExtension of F st deg (E,F) = k holds
ex T being finite b₂ -algebraic Subset of b₃ st b₃ == FAdj (T,b₄)
let E be FieldExtension of F; :: thesis: ( deg (E,F) = k implies ex T being finite b₁ -algebraic Subset of b₂ st b₂ == FAdj (T,b₃) )
assume Z: deg (E,F) = k ; :: thesis: ex T being finite b₁ -algebraic Subset of b₂ st b₂ == FAdj (T,b₃)
then VecSp (E,F) is finite-dimensional by FIELD_4:def 7;
then reconsider K = E as F -finite FieldExtension of F by FIELD_4:def 8;

per cases ( k = 1 or k > 1 ) by AS, XXREAL_0:1;

suppose k = 1 ; :: thesis: ex T being finite b₁ -algebraic Subset of b₂ st b₂ == FAdj (T,b₃)

hence ex T being finite F -algebraic Subset of E st E == FAdj (F,T) by Z, IA; :: thesis: verum

end;

suppose B0: k > 1 ; :: thesis: ex T being finite b₁ -algebraic Subset of b₂ st b₂ == FAdj (T,b₃)

now :: thesis: not for a being Element of K holds a in the carrier of F

assume B1: for a being Element of K holds a in the carrier of F ; :: thesis: contradiction
for o being object holds
( o in the carrier of E iff o in the carrier of F )

proof

let o be object ; :: thesis: ( o in the carrier of E iff o in the carrier of F )

now :: thesis: ( o in the carrier of F implies o in the carrier of E )

assume B: o in the carrier of F ; :: thesis: o in the carrier of E
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;
hence o in the carrier of E by B; :: thesis: verum

end;

hence ( o in the carrier of E iff o in the carrier of F ) by B1; :: thesis: verum

end;

hence contradiction by Z, B0, quah1, TARSKI:2; :: thesis: verum

end;

then consider a being Element of K such that
C1: not a in the carrier of F ;
set p = MinPoly (a,F);
C2: {a} is F -algebraic ;
C3: ( deg ((FAdj (F,{a})),F) <= k & deg ((FAdj (F,{a})),F) > 1 )

proof

K is FAdj (F,{a}) -extending by FIELD_4:7;
hence deg ((FAdj (F,{a})),F) <= k by Z, FIELD_5:15; :: thesis: deg ((FAdj (F,{a})),F) > 1
C5: {a} is Subset of the carrier of (FAdj (F,{a})) by FIELD_6:35;
a in {a} by TARSKI:def 1;
then C6: a in the carrier of (FAdj (F,{a})) by C5;
(deg ((FAdj (F,{a})),F)) + 1 > 0 + 1 by XREAL_1:6;
then deg ((FAdj (F,{a})),F) >= 1 by NAT_1:13;
hence deg ((FAdj (F,{a})),F) > 1 by C6, C1, quah1, XXREAL_0:1; :: thesis: verum

end;

deg (MinPoly (a,F)) = deg ((FAdj (F,{a})),F) by FIELD_6:67;

per cases then ( deg (MinPoly (a,F)) = k or deg (MinPoly (a,F)) < k ) by C3, XXREAL_0:1;

suppose deg (MinPoly (a,F)) = k ; :: thesis: ex T being finite b₁ -algebraic Subset of b₂ st b₂ == FAdj (T,b₃)

then K == FAdj (F,{a}) by Z, ft1;
hence ex T being finite F -algebraic Subset of E st E == FAdj (F,T) by C2; :: thesis: verum

end;

suppose deg (MinPoly (a,F)) < k ; :: thesis: ex T being finite b₁ -algebraic Subset of b₂ st b₂ == FAdj (T,b₃)

set K = FAdj (F,{a});
reconsider E1 = E as F -extending FAdj (F,{a}) -finite FieldExtension of F by alg0, FIELD_4:7;
reconsider j = deg (E1,(FAdj (F,{a}))) as Element of NAT by ORDINAL1:def 12;
( j >= 1 & j < k )

proof

j + 1 > 0 + 1 by XREAL_1:6;
hence j >= 1 by NAT_1:13; :: thesis: j < k
D7: k = (deg (E1,(FAdj (F,{a})))) * (deg ((FAdj (F,{a})),F)) by Z, degmult;
D6: j <= k by D7, NAT_1:24;

now :: thesis: not j = k

assume j = k ; :: thesis: contradiction
then k / k = (k * (deg ((FAdj (F,{a})),F))) / k by Z, degmult
.= (k / k) * (deg ((FAdj (F,{a})),F)) ;
then k / k = 1 * (deg ((FAdj (F,{a})),F)) by B0, XCMPLX_1:60;
hence contradiction by C3, XCMPLX_1:60; :: thesis: verum

end;

hence j < k by D6, XXREAL_0:1; :: thesis: verum

end;

then consider T1 being finite FAdj (F,{a}) -algebraic Subset of E1 such that
D3: E1 == FAdj ((FAdj (F,{a})),T1) by AS;
reconsider T = T1 as Subset of E ;
reconsider a1 = a as Element of E ;
for b being Element of E1 st b in T \/ {a} holds
b is F -algebraic ;
then reconsider T2 = {a1} \/ T as F -algebraic Subset of E by defTalg;
FAdj ((FAdj (F,{a})),T1) = FAdj (F,T2) by ug1;
hence ex T being finite F -algebraic Subset of E st E == FAdj (F,T) by D3; :: thesis: verum

end;

end;

end;

end;

end;

hence S₁[k] ; :: thesis: verum

end;

I: for k being Nat st k >= 1 holds
S₁[k] from NAT_1:sch 9(IS);

A: now :: thesis: ( E is F -finite implies ex T being finite F -algebraic Subset of E st E == FAdj (F,T) )

assume E is F -finite ; :: thesis: ex T being finite F -algebraic Subset of E st E == FAdj (F,T)
then reconsider k = deg (E,F) as Element of NAT by ORDINAL1:def 12;
k >= 0 + 1 by NAT_1:13;
hence ex T being finite F -algebraic Subset of E st E == FAdj (F,T) by I; :: thesis: verum

end;

now :: thesis: ( ex T being finite F -algebraic Subset of E st E == FAdj (F,T) implies E is F -finite )

assume ex T being finite F -algebraic Subset of E st E == FAdj (F,T) ; :: thesis: E is F -finite
then consider T being finite F -algebraic Subset of E such that
B0: E == FAdj (F,T) ;
VecSp ((FAdj (F,T)),F) is finite-dimensional by FIELD_4:def 8;
then VecSp (E,F) is finite-dimensional by B0, str12;
hence E is F -finite by FIELD_4:def 8; :: thesis: verum

end;

hence ( E is F -finite iff ex T being finite F -algebraic Subset of E st E == FAdj (F,T) ) by A; :: thesis: verum