let F be Field; :: thesis: for E being FieldExtension of F
for a being F -algebraic Element of E holds card (Base a) = deg (MinPoly (a,F))
let E be FieldExtension of F; :: thesis: for a being F -algebraic Element of E holds card (Base a) = deg (MinPoly (a,F))
let a be F -algebraic Element of E; :: thesis: card (Base a) = deg (MinPoly (a,F))
set ma = MinPoly (a,F);
set m = deg (MinPoly (a,F));
defpred S1[ object , object ] means ex x being Element of Seg (deg (MinPoly (a,F))) 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 (deg (MinPoly (a,F))) & S1[x,y1] & S1[x,y2] holds
y1 = y2 ;
B2: now :: thesis: for x being object st x in Seg (deg (MinPoly (a,F))) holds
ex y being object st S1[x,y]
let x be object ; :: thesis: ( x in Seg (deg (MinPoly (a,F))) implies ex y being object st S1[x,y] )
assume B3: x in Seg (deg (MinPoly (a,F))) ; :: thesis: ex y being object st S1[x,y]
then reconsider n = x as Element of Seg (deg (MinPoly (a,F))) ;
1 <= n by B3, FINSEQ_1:1;
then reconsider z = n - 1 as Element of NAT by INT_1:3;
thus ex y being object st S1[x,y] :: thesis: verum
proof
take a |^ z ; :: thesis: S1[x,a |^ z]
thus S1[x,a |^ z] ; :: thesis: verum
end;
end;
consider f being Function such that
C: ( dom f = Seg (deg (MinPoly (a,F))) & ( for x being object st x in Seg (deg (MinPoly (a,F))) holds
S1[x,f . x] ) ) from FUNCT_1:sch 2(B1, B2);
A1: now :: thesis: for o being object st o in Base a holds
o in rng f
let o be object ; :: thesis: ( o in Base a implies o in rng f )
assume o in Base a ; :: thesis: o in rng f
then consider n being Element of NAT such that
A2: ( o = a |^ n & n < deg (MinPoly (a,F)) ) ;
A3: ( 0 + 1 <= n + 1 & n + 1 <= deg (MinPoly (a,F)) ) by A2, INT_1:7;
then reconsider x = n + 1 as Element of Seg (deg (MinPoly (a,F))) by FINSEQ_1:1;
A4: x in Seg (deg (MinPoly (a,F))) by FINSEQ_1:1, A3;
S1[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 Base a
let o be object ; :: thesis: ( o in rng f implies o in Base a )
assume o in rng f ; :: thesis: o in Base a
then consider u being object such that
A2: ( u in dom f & o = f . u ) by FUNCT_1:def 3;
S1[u,f . u] by C, A2;
then consider x being Element of Seg (deg (MinPoly (a,F))), y being Element of NAT such that
A3: ( u = x & y = x - 1 & f . x = a |^ y ) ;
not deg (MinPoly (a,F)) <= 0 by RING_4:def 4;
then deg (MinPoly (a,F)) in Seg (deg (MinPoly (a,F))) by FINSEQ_1:3;
then ( 1 <= x & x <= deg (MinPoly (a,F)) ) by FINSEQ_1:1;
then y < ((deg (MinPoly (a,F))) - 1) + 1 by A3, XREAL_1:9, NAT_1:13;
hence o in Base a by A2, A3; :: thesis: verum
end;
then A: rng f = Base a 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 (deg (MinPoly (a,F))), 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 (deg (MinPoly (a,F))), y2 being Element of NAT such that
A3: ( x2 = n2 & y2 = n2 - 1 & f . x2 = a |^ y2 ) by A1, C;
( n1 <= deg (MinPoly (a,F)) & n2 <= deg (MinPoly (a,F)) ) by C, A1, FINSEQ_1:1;
then ( (y1 + 1) - 1 <= (deg (MinPoly (a,F))) - 1 & (y2 + 1) - 1 <= (deg (MinPoly (a,F))) - 1 ) by A3, A2, XREAL_1:9;
then A4: ( y1 < ((deg (MinPoly (a,F))) - 1) + 1 & y2 < ((deg (MinPoly (a,F))) - 1) + 1 ) by NAT_1:13;
A5: y1 <> y2 by A1, A2, A3;
per cases ( y1 < y2 or y1 > y2 ) by A5, XXREAL_0:1;
end;
end;
then card (Base a) = card (Seg (deg (MinPoly (a,F)))) by A, C, CARD_1:70
.= deg (MinPoly (a,F)) by FINSEQ_1:57 ;
hence card (Base a) = deg (MinPoly (a,F)) ; :: thesis: verum