let F be Field; :: thesis: for E being FieldExtension of F
for a being F -algebraic Element of E
for n being Nat st n = card { f where f is F -fixing Automorphism of (FAdj (F,{a})) : verum } holds
n <= card (Roots ((FAdj (F,{a})),(MinPoly (a,F))))
let E be FieldExtension of F; :: thesis: for a being F -algebraic Element of E
for n being Nat st n = card { f where f is F -fixing Automorphism of (FAdj (F,{a})) : verum } holds
n <= card (Roots ((FAdj (F,{a})),(MinPoly (a,F))))
let a be F -algebraic Element of E; :: thesis: for n being Nat st n = card { f where f is F -fixing Automorphism of (FAdj (F,{a})) : verum } holds
n <= card (Roots ((FAdj (F,{a})),(MinPoly (a,F))))
let n be Nat; :: thesis: ( n = card { f where f is F -fixing Automorphism of (FAdj (F,{a})) : verum } implies n <= card (Roots ((FAdj (F,{a})),(MinPoly (a,F)))) )
assume AS: n = card { f where f is F -fixing Automorphism of (FAdj (F,{a})) : verum } ; :: thesis: n <= card (Roots ((FAdj (F,{a})),(MinPoly (a,F))))
then reconsider M = { f where f is F -fixing Automorphism of (FAdj (F,{a})) : verum } as finite set ;
set K = FAdj (F,{a});
set d = card (Roots ((FAdj (F,{a})),(MinPoly (a,F))));
set f = id (FAdj (F,{a}));

now :: thesis: for b being Element of F holds (id (FAdj (F,{a}))) . b = b

let b be Element of F; :: thesis: (id (FAdj (F,{a}))) . b = b
F is Subfield of FAdj (F,{a}) by FIELD_4:7;
then the carrier of F c= the carrier of (FAdj (F,{a})) by EC_PF_1:def 1;
then reconsider c = b as Element of (FAdj (F,{a})) ;
thus (id (FAdj (F,{a}))) . b = c
.= b ; :: thesis: verum

end;

then reconsider f = id (FAdj (F,{a})) as F -fixing Automorphism of (FAdj (F,{a})) by FIELD_8:def 2;
set M1 = M \ {f};
( a in {a} & {a} is Subset of (FAdj (F,{a})) ) by TARSKI:def 1, FIELD_6:35;
then reconsider a1 = a as Element of (FAdj (F,{a})) ;

per cases ( M \ {f} = {} or M \ {f} <> {} ) ;

suppose A: M \ {f} = {} ; :: thesis: n <= card (Roots ((FAdj (F,{a})),(MinPoly (a,F))))

f in M ;
then B: {f} c= M by TARSKI:def 1;
C: M c= {f} by A, XBOOLE_0:def 5;
D: E is FAdj (F,{a}) -extending by FIELD_4:7;
0. (FAdj (F,{a})) = 0. E by FIELD_6:def 6
.= Ext_eval ((MinPoly (a,F)),a) by FIELD_6:52
.= Ext_eval ((MinPoly (a,F)),a1) by D, FIELD_6:11 ;
then a1 is_a_root_of MinPoly (a,F), FAdj (F,{a}) by FIELD_4:def 2;
then a1 in { b where b is Element of (FAdj (F,{a})) : b is_a_root_of MinPoly (a,F), FAdj (F,{a}) } ;
then a1 in Roots ((FAdj (F,{a})),(MinPoly (a,F))) by FIELD_4:def 4;
then card (Roots ((FAdj (F,{a})),(MinPoly (a,F)))) >= 0 + 1 by INT_1:7;
hence n <= card (Roots ((FAdj (F,{a})),(MinPoly (a,F)))) by C, AS, B, XBOOLE_0:def 10, CARD_2:42; :: thesis: verum

end;

suppose M \ {f} <> {} ; :: thesis: n <= card (Roots ((FAdj (F,{a})),(MinPoly (a,F))))

then reconsider M1 = M \ {f} as non empty finite set ;

now :: thesis: not n > card (Roots ((FAdj (F,{a})),(MinPoly (a,F))))

assume AS1: n > card (Roots ((FAdj (F,{a})),(MinPoly (a,F)))) ; :: thesis: contradiction
f in M ;
then ( {f} c= M & card {f} = 1 ) by TARSKI:def 1, CARD_2:42;
then card M1 = n - 1 by AS, CARD_2:44;
then B: card M1 >= ((card (Roots ((FAdj (F,{a})),(MinPoly (a,F))))) - 1) + 1 by AS1, XREAL_1:9, INT_1:7;
D: f . a1 in Roots ((FAdj (F,{a})),(MinPoly (a,F))) by ID2a;
set M2 = { x where x is Element of (FAdj (F,{a})) : ex g being F -fixing Automorphism of (FAdj (F,{a})) st
( g in M1 & g . a = x ) } ;
F: { x where x is Element of (FAdj (F,{a})) : ex g being F -fixing Automorphism of (FAdj (F,{a})) st
( g in M1 & g . a = x ) } c= Roots ((FAdj (F,{a})),(MinPoly (a,F)))

proof

now :: thesis: for o being object st o in { x where x is Element of (FAdj (F,{a})) : ex g being F -fixing Automorphism of (FAdj (F,{a})) st
( g in M1 & g . a = x ) } holds
o in Roots ((FAdj (F,{a})),(MinPoly (a,F)))

let o be object ; :: thesis: ( o in { x where x is Element of (FAdj (F,{a})) : ex g being F -fixing Automorphism of (FAdj (F,{a})) st
( g in M1 & g . a = x ) } implies o in Roots ((FAdj (F,{a})),(MinPoly (a,F))) )
assume o in { x where x is Element of (FAdj (F,{a})) : ex g being F -fixing Automorphism of (FAdj (F,{a})) st
( g in M1 & g . a = x ) } ; :: thesis: o in Roots ((FAdj (F,{a})),(MinPoly (a,F)))
then consider x being Element of (FAdj (F,{a})) such that
F1: ( x = o & ex g being F -fixing Automorphism of (FAdj (F,{a})) st
( g in M1 & g . a = x ) ) ;
thus o in Roots ((FAdj (F,{a})),(MinPoly (a,F))) by F1, ID2a; :: thesis: verum

end;

hence { x where x is Element of (FAdj (F,{a})) : ex g being F -fixing Automorphism of (FAdj (F,{a})) st
( g in M1 & g . a = x ) } c= Roots ((FAdj (F,{a})),(MinPoly (a,F))) ; :: thesis: verum

end;

then reconsider M2 = { x where x is Element of (FAdj (F,{a})) : ex g being F -fixing Automorphism of (FAdj (F,{a})) st
( g in M1 & g . a = x ) } as finite set ;
M2 <> {}

proof

set x = the Element of M1;
M1 c= M ;
then the Element of M1 in M ;
then consider g being F -fixing Automorphism of (FAdj (F,{a})) such that
G4: the Element of M1 = g ;
g . a1 in { x where x is Element of (FAdj (F,{a})) : ex g being F -fixing Automorphism of (FAdj (F,{a})) st
( g in M1 & g . a = x ) } by G4;
hence M2 <> {} ; :: thesis: verum

end;

then reconsider M2 = M2 as non empty finite set ;

now :: thesis: Roots ((FAdj (F,{a})),(MinPoly (a,F))) c= M2

assume not Roots ((FAdj (F,{a})),(MinPoly (a,F))) c= M2 ; :: thesis: contradiction
then M2 c< Roots ((FAdj (F,{a})),(MinPoly (a,F))) by F, XBOOLE_0:def 8;
then K2: card M2 < card M1 by B, XXREAL_0:2, CARD_2:48;
ex h being Function of M1,M2 st
for g being F -fixing Automorphism of (FAdj (F,{a})) st g in M1 holds
h . g = g . a

proof

defpred S₁[ object , object ] means ex g being F -fixing Automorphism of (FAdj (F,{a})) st
( $1 = g & g in M1 & $2 = g . a );

A: now :: thesis: for x being Element of M1 ex y being Element of M2 st S₁[x,y]

let x be Element of M1; :: thesis: ex y being Element of M2 st S₁[x,y]
M1 c= M ;
then x in M ;
then consider g1 being F -fixing Automorphism of (FAdj (F,{a})) such that
A1: x = g1 ;
thus ex y being Element of M2 st S₁[x,y] :: thesis: verum

proof

g1 . a1 in { x where x is Element of (FAdj (F,{a})) : ex g being F -fixing Automorphism of (FAdj (F,{a})) st
( g in M1 & g . a = x ) } by A1;
then reconsider y = g1 . a1 as Element of M2 ;
take y ; :: thesis: S₁[x,y]
thus S₁[x,y] by A1; :: thesis: verum

end;

end;

consider h being Function of M1,M2 such that
B: for x being Element of M1 holds S₁[x,h . x] from FUNCT_2:sch 3(A);

now :: thesis: for g being F -fixing Automorphism of (FAdj (F,{a})) st g in M1 holds
h . g = g . a

let g be F -fixing Automorphism of (FAdj (F,{a})); :: thesis: ( g in M1 implies h . g = g . a )
assume g in M1 ; :: thesis: h . g = g . a
then S₁[g,h . g] by B;
hence h . g = g . a ; :: thesis: verum

end;

hence ex h being Function of M1,M2 st
for g being F -fixing Automorphism of (FAdj (F,{a})) st g in M1 holds
h . g = g . a ; :: thesis: verum

end;

then consider h being Function of M1,M2 such that
G1: for g being F -fixing Automorphism of (FAdj (F,{a})) st g in M1 holds
h . g = g . a ;
K3: ( dom h = M1 & rng h c= M2 ) by FUNCT_2:def 1, RELAT_1:def 19;
reconsider M3 = rng h as finite set ;
card M3 <= card M2 by RELAT_1:def 19, NAT_1:43;
then not h is one-to-one by K3, K2, CARD_1:70;
then consider x1, x2 being object such that
G2: ( x1 in M1 & x2 in M1 & h . x1 = h . x2 & x1 <> x2 ) by FUNCT_2:19;
x1 in M by G2;
then consider g1 being F -fixing Automorphism of (FAdj (F,{a})) such that
G4: x1 = g1 ;
x2 in M by G2;
then consider g2 being F -fixing Automorphism of (FAdj (F,{a})) such that
G5: x2 = g2 ;
g1 . a = h . g1 by G1, G2, G4
.= g2 . a by G1, G2, G4, G5 ;
hence contradiction by ID, G2, G4, G5; :: thesis: verum

end;

then M2 = Roots ((FAdj (F,{a})),(MinPoly (a,F))) by F, XBOOLE_0:def 10;
then consider x being Element of (FAdj (F,{a})) such that
E: ( x = f . a1 & ex g being F -fixing Automorphism of (FAdj (F,{a})) st
( g in M1 & g . a = x ) ) by D;
consider g being F -fixing Automorphism of (FAdj (F,{a})) such that
A: ( g in M1 & g . a = f . a1 ) by E;
( f in M1 & f in {f} ) by A, ID, TARSKI:def 1;
hence contradiction by XBOOLE_0:def 5; :: thesis: verum

end;

hence n <= card (Roots ((FAdj (F,{a})),(MinPoly (a,F)))) ; :: thesis: verum

end;

end;