let F be Field; :: thesis: for E being FieldExtension of F
for a being Element of E holds
( a is F -algebraic iff FAdj (F,{a}) is F -finite )
let E be FieldExtension of F; :: thesis: for a being Element of E holds
( a is F -algebraic iff FAdj (F,{a}) is F -finite )
let a be Element of E; :: thesis: ( a is F -algebraic iff FAdj (F,{a}) is F -finite )

now :: thesis: ( FAdj (F,{a}) is F -finite implies a is F -algebraic )

assume AS: FAdj (F,{a}) is F -finite ; :: thesis: a is F -algebraic
then reconsider n = deg ((FAdj (F,{a})),F) as Element of NAT by ORDINAL1:def 12;
H: n = dim (VecSp ((FAdj (F,{a})),F)) by FIELD_4:def 7;

per cases ( ex i, j being Element of NAT st
( i < j & j <= n & a |^ i = a |^ j ) or for i, j being Element of NAT holds
( not i < j or not j <= n or not a |^ i = a |^ j ) ) ;

suppose ex i, j being Element of NAT st
( i < j & j <= n & a |^ i = a |^ j ) ; :: thesis: a is F -algebraic

then consider i, j being Element of NAT such that
U: ( i < j & j <= n & a |^ i = a |^ j ) ;
set p1 = <%(0. F),(1. F)%> `^ j;
set p2 = <%(0. F),(1. F)%> `^ i;
set p = (<%(0. F),(1. F)%> `^ j) - (<%(0. F),(1. F)%> `^ i);

now :: thesis: not (<%(0. F),(1. F)%> `^ j) - (<%(0. F),(1. F)%> `^ i) = 0_. F

assume (<%(0. F),(1. F)%> `^ j) - (<%(0. F),(1. F)%> `^ i) = 0_. F ; :: thesis: contradiction
then 0. F = ((<%(0. F),(1. F)%> `^ j) - (<%(0. F),(1. F)%> `^ i)) . j
.= ((<%(0. F),(1. F)%> `^ j) . j) - ((<%(0. F),(1. F)%> `^ i) . j) by POLYNOM3:27
.= (1. F) - ((<%(0. F),(1. F)%> `^ i) . j) by help1
.= (1. F) - (0. F) by U, help2 ;
hence contradiction ; :: thesis: verum

end;

then reconsider p = (<%(0. F),(1. F)%> `^ j) - (<%(0. F),(1. F)%> `^ i) as non zero Polynomial of F by UPROOTS:def 5;

per cases ( i = 0 or not i is zero ) ;

suppose T: i = 0 ; :: thesis: a is F -algebraic

then W: a |^ i = 1_ E by BINOM:8;
Ext_eval (p,a) = (Ext_eval ((<%(0. F),(1. F)%> `^ j),a)) - (Ext_eval ((<%(0. F),(1. F)%> `^ i),a)) by exevalminus2
.= (Ext_eval ((<%(0. F),(1. F)%> `^ j),a)) - (Ext_eval ((1_. F),a)) by T, POLYNOM5:15
.= (Ext_eval ((<%(0. F),(1. F)%> `^ j),a)) - (1. E) by FIELD_4:23
.= (a |^ j) - (1. E) by U, help3
.= 0. E by W, U, RLVECT_1:15 ;
hence a is F -algebraic by alg00; :: thesis: verum

end;

suppose T: not i is zero ; :: thesis: a is F -algebraic

Ext_eval (p,a) = (Ext_eval ((<%(0. F),(1. F)%> `^ j),a)) - (Ext_eval ((<%(0. F),(1. F)%> `^ i),a)) by exevalminus2
.= (a |^ j) - (Ext_eval ((<%(0. F),(1. F)%> `^ i),a)) by U, help3
.= (a |^ j) - (a |^ i) by T, help3
.= 0. E by U, RLVECT_1:15 ;
hence a is F -algebraic by alg00; :: thesis: verum

end;

end;

end;

suppose U: for i, j being Element of NAT holds
( not i < j or not j <= n or not a |^ i = a |^ j ) ; :: thesis: a is F -algebraic

set M = { (a |^ i) where i is Element of NAT : i <= n } ;
set V = VecSp ((FAdj (F,{a})),F);
X: {a} is Subset of (FAdj (F,{a})) by FAt;
a in {a} by TARSKI:def 1;
then reconsider a1 = a as Element of (FAdj (F,{a})) by X;
I: { (a |^ i) where i is Element of NAT : i <= n } c= the carrier of (VecSp ((FAdj (F,{a})),F))

proof

now :: thesis: for o being object st o in { (a |^ i) where i is Element of NAT : i <= n } holds
o in the carrier of (VecSp ((FAdj (F,{a})),F))

let o be object ; :: thesis: ( o in { (a |^ i) where i is Element of NAT : i <= n } implies o in the carrier of (VecSp ((FAdj (F,{a})),F)) )
assume o in { (a |^ i) where i is Element of NAT : i <= n } ; :: thesis: o in the carrier of (VecSp ((FAdj (F,{a})),F))
then consider i being Element of NAT such that
H: ( o = a |^ i & i <= n ) ;
I: the carrier of (VecSp ((FAdj (F,{a})),F)) = the carrier of (FAdj (F,{a})) by FIELD_4:def 6;
FAdj (F,{a}) is Subring of E by FIELD_5:12;
then a |^ i = a1 |^ i by pr5;
hence o in the carrier of (VecSp ((FAdj (F,{a})),F)) by H, I; :: thesis: verum

end;

hence { (a |^ i) where i is Element of NAT : i <= n } c= the carrier of (VecSp ((FAdj (F,{a})),F)) ; :: thesis: verum

end;

{ (a |^ i) where i is Element of NAT : i <= n } is finite

proof

deffunc H₁( Nat) -> Element of the carrier of E = a |^ $1;
defpred S₁[ Nat] means $1 <= n;
D: { H₁(i) where i is Nat : ( i <= n & S₁[i] ) } is finite from FINSEQ_1:sch 6();

E: now :: thesis: for o being object st o in { H₁(i) where i is Nat : ( i <= n & S₁[i] ) } holds
o in { (a |^ i) where i is Element of NAT : i <= n }

let o be object ; :: thesis: ( o in { H₁(i) where i is Nat : ( i <= n & S₁[i] ) } implies o in { (a |^ i) where i is Element of NAT : i <= n } )
assume o in { H₁(i) where i is Nat : ( i <= n & S₁[i] ) } ; :: thesis: o in { (a |^ i) where i is Element of NAT : i <= n }
then consider i being Nat such that
E1: ( o = a |^ i & i <= n & i <= n ) ;
i is Element of NAT by ORDINAL1:def 12;
hence o in { (a |^ i) where i is Element of NAT : i <= n } by E1; :: thesis: verum

end;

now :: thesis: for o being object st o in { (a |^ i) where i is Element of NAT : i <= n } holds
o in { H₁(i) where i is Nat : ( i <= n & S₁[i] ) }

let o be object ; :: thesis: ( o in { (a |^ i) where i is Element of NAT : i <= n } implies o in { H₁(i) where i is Nat : ( i <= n & S₁[i] ) } )
assume o in { (a |^ i) where i is Element of NAT : i <= n } ; :: thesis: o in { H₁(i) where i is Nat : ( i <= n & S₁[i] ) }
then consider i being Element of NAT such that
E1: ( o = a |^ i & i <= n ) ;
thus o in { H₁(i) where i is Nat : ( i <= n & S₁[i] ) } by E1; :: thesis: verum

end;

hence { (a |^ i) where i is Element of NAT : i <= n } is finite by D, E, TARSKI:2; :: thesis: verum

end;

then reconsider M = { (a |^ i) where i is Element of NAT : i <= n } as finite Subset of (VecSp ((FAdj (F,{a})),F)) by I;
card M = n + 1

proof

set m = n + 1;
defpred S₁[ object , object ] means ex x being Element of Seg (n + 1) ex y being Element of NAT st
( $1 = x & y = x - 1 & $2 = a |^ y );
B1: for x, y1, y2 being object st x in Seg (n + 1) & S₁[x,y1] & S₁[x,y2] holds
y1 = y2 ;

B2: now :: thesis: for x being object st x in Seg (n + 1) holds
ex y being object st S₁[x,y]

let x be object ; :: thesis: ( x in Seg (n + 1) implies ex y being object st S₁[x,y] )
assume B3: x in Seg (n + 1) ; :: thesis: ex y being object st S₁[x,y]
then reconsider i = x as Element of Seg (n + 1) ;
1 <= i by B3, FINSEQ_1:1;
then reconsider z = i - 1 as Element of NAT by INT_1:3;
thus ex y being object st S₁[x,y] :: thesis: verum

proof

take a |^ z ; :: thesis: S₁[x,a |^ z]
thus S₁[x,a |^ z] ; :: thesis: verum

end;

end;

consider f being Function such that
C: ( dom f = Seg (n + 1) & ( for x being object st x in Seg (n + 1) holds
S₁[x,f . x] ) ) from FUNCT_1:sch 2(B1, B2);

A1: 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 i being Element of NAT such that
A2: ( o = a |^ i & i <= n ) ;
A3: ( 0 + 1 <= i + 1 & i + 1 <= n + 1 ) by A2, XREAL_1:6;
then reconsider x = i + 1 as Element of Seg (n + 1) by FINSEQ_1:1;
A4: x in Seg (n + 1) by FINSEQ_1:1, A3;
S₁[x,f . x] by C, FINSEQ_1:1, A3;
hence o in rng f by A4, C, A2, 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 u being object such that
A2: ( u in dom f & o = f . u ) by FUNCT_1:def 3;
S₁[u,f . u] by C, A2;
then consider x being Element of Seg (n + 1), y being Element of NAT such that
A3: ( u = x & y = x - 1 & f . x = a |^ y ) ;
n + 1 in Seg (n + 1) by FINSEQ_1:3;
then ( 1 <= x & x <= n + 1 ) by FINSEQ_1:1;
then y < ((n + 1) - 1) + 1 by A3, XREAL_1:9, NAT_1:13;
then y <= n by NAT_1:13;
hence o in M by A2, A3; :: thesis: verum

end;

then A: rng f = M by A1, TARSKI:2;

now :: thesis: f is one-to-one

assume not f is one-to-one ; :: thesis: contradiction
then consider x1, x2 being object such that
A1: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 & x1 <> x2 ) ;
consider n1 being Element of Seg (n + 1), y1 being Element of NAT such that
A2: ( x1 = n1 & y1 = n1 - 1 & f . x1 = a |^ y1 ) by A1, C;
consider n2 being Element of Seg (n + 1), y2 being Element of NAT such that
A3: ( x2 = n2 & y2 = n2 - 1 & f . x2 = a |^ y2 ) by A1, C;
( n1 <= n + 1 & n2 <= n + 1 ) by C, A1, FINSEQ_1:1;
then A4: ( y1 < ((n + 1) - 1) + 1 & y2 < ((n + 1) - 1) + 1 ) by A3, A2, XREAL_1:9, NAT_1:13;
A5: y1 <> y2 by A1, A2, A3;
A6: ( y1 <= n & y2 <= n ) by A4, NAT_1:13;

per cases ( y1 < y2 or y1 > y2 ) by A5, XXREAL_0:1;

suppose y1 < y2 ; :: thesis: contradiction

hence contradiction by U, A1, A2, A3, A6; :: thesis: verum

end;

suppose y1 > y2 ; :: thesis: contradiction

hence contradiction by U, A1, A2, A3, A6; :: thesis: verum

end;

end;

end;

then card M = card (Seg (n + 1)) by A, C, CARD_1:70
.= n + 1 by FINSEQ_1:57 ;
hence card M = n + 1 ; :: thesis: verum

end;

then card M > n by NAT_1:13;
then M is linearly-dependent by H, AS, lemlin;
then consider l being Linear_Combination of M such that
D1: ( Sum l = 0. (VecSp ((FAdj (F,{a})),F)) & Carrier l <> {} ) by VECTSP_7:def 1;
set z = the Element of Carrier l;
consider v being Element of (VecSp ((FAdj (F,{a})),F)) such that
D2: ( the Element of Carrier l = v & l . v <> 0. F ) by D1, VECTSP_6:1;
H1: M = { (a1 |^ i) where i is Element of NAT : i <= n }

proof

V: FAdj (F,{a}) is Subring of E by FIELD_5:12;

A: now :: thesis: for o being object st o in M holds
o in { (a1 |^ i) where i is Element of NAT : i <= n }

let o be object ; :: thesis: ( o in M implies o in { (a1 |^ i) where i is Element of NAT : i <= n } )
assume o in M ; :: thesis: o in { (a1 |^ i) where i is Element of NAT : i <= n }
then consider i being Element of NAT such that
B: ( o = a |^ i & i <= n ) ;
a |^ i = a1 |^ i by V, pr5;
hence o in { (a1 |^ i) where i is Element of NAT : i <= n } by B; :: thesis: verum

end;

now :: thesis: for o being object st o in { (a1 |^ i) where i is Element of NAT : i <= n } holds
o in M

let o be object ; :: thesis: ( o in { (a1 |^ i) where i is Element of NAT : i <= n } implies o in M )
assume o in { (a1 |^ i) where i is Element of NAT : i <= n } ; :: thesis: o in M
then consider i being Element of NAT such that
B: ( o = a1 |^ i & i <= n ) ;
a |^ i = a1 |^ i by V, pr5;
hence o in M by B; :: thesis: verum

end;

hence M = { (a1 |^ i) where i is Element of NAT : i <= n } by A, TARSKI:2; :: thesis: verum

end;

H2: for i, j being Element of NAT st i < j & j <= n holds
a1 |^ i <> a1 |^ j

proof

let i, j be Element of NAT ; :: thesis: ( i < j & j <= n implies a1 |^ i <> a1 |^ j )
assume W: ( i < j & j <= n ) ; :: thesis: a1 |^ i <> a1 |^ j
V: FAdj (F,{a}) is Subring of E by FIELD_5:12;
assume a1 |^ i = a1 |^ j ; :: thesis: contradiction
then a |^ i = a1 |^ j by V, pr5
.= a |^ j by V, pr5 ;
hence contradiction by W, U; :: thesis: verum

end;

I: E is FAdj (F,{a}) -extending by FIELD_4:7;
Carrier l c= M by VECTSP_6:def 4;
then the Element of Carrier l in M by D1;
then consider i being Element of NAT such that
D3: ( the Element of Carrier l = a |^ i & i <= n ) ;
FAdj (F,{a}) is Subring of E by FIELD_5:12;
then D3a: a |^ i = a1 |^ i by pr5;
consider pM being Polynomial of F such that
D4a: ( deg pM <= n & ( for i being Element of NAT st i <= n holds
pM . i = l . (a1 |^ i) ) ) by lembasx2;
pM . i <> 0. F by D3a, D3, D2, D4a;
then pM <> 0_. F ;
then reconsider pM = pM as non zero Polynomial of F by UPROOTS:def 5;
reconsider pMC = pM as Element of the carrier of (Polynom-Ring F) by POLYNOM3:def 10;
Ext_eval (pMC,a) = Ext_eval (pMC,a1) by I, lemma7
.= 0. (VecSp ((FAdj (F,{a})),F)) by H1, H2, D1, D4a, lembasx1
.= 0. (FAdj (F,{a})) by FIELD_4:def 6
.= 0. E by dFA ;
hence a is F -algebraic by alg00; :: thesis: verum

end;

end;

end;

hence ( a is F -algebraic iff FAdj (F,{a}) is F -finite ) ; :: thesis: verum