let F be commutative Skew-Field; :: thesis: for G being Subgroup of MultGroup F
for a, b being Element of G
for n being Nat st G is finite & 0 < n & ord a = n & b |^ n = 1_ G holds
b is Element of (gr {a})
let G be Subgroup of MultGroup F; :: thesis: for a, b being Element of G
for n being Nat st G is finite & 0 < n & ord a = n & b |^ n = 1_ G holds
b is Element of (gr {a})
let a, b be Element of G; :: thesis: for n being Nat st G is finite & 0 < n & ord a = n & b |^ n = 1_ G holds
b is Element of (gr {a})
let n be Nat; :: thesis: ( G is finite & 0 < n & ord a = n & b |^ n = 1_ G implies b is Element of (gr {a}) )
assume A1: ( G is finite & 0 < n & ord a = n & b |^ n = 1_ G ) ; :: thesis: b is Element of (gr {a})
assume A2: b is not Element of (gr {a}) ; :: thesis: contradiction
A3: the carrier of G c= the carrier of (MultGroup F) by GROUP_2:def 5;
reconsider L = F as non empty unital doubleLoopStr ;
consider f being Polynomial of F such that
A4: ( deg f = n & ( for x, xn being Element of F
for xz being Element of G st x = xz & xn = xz |^ n holds
eval f,x = xn - (1. F) ) ) by A1, LM0X62a;
A5: for x being Element of G st x |^ n = 1_ G holds
x in Roots f

proof

let x1 be Element of G; :: thesis: ( x1 |^ n = 1_ G implies x1 in Roots f )
assume A6: x1 |^ n = 1_ G ; :: thesis: x1 in Roots f
x1 in the carrier of G ;
then x1 in the carrier of (MultGroup F) by A3;
then x1 in NonZero F by UNIROOTS:def 1;
then reconsider x3 = x1 as Element of F ;
A7: 1_ F = 1_ (MultGroup F) by UNIROOTS:20;
then A8: x1 |^ n = 1. F by GROUP_2:53, A6;
reconsider x2 = x1 |^ n as Element of F by GROUP_2:53, A6, A7;
eval f,x3 = x2 - (1. F) by A4
.= 0. F by RLVECT_1:28, A8 ;
then x3 is_a_root_of f by POLYNOM5:def 6;
hence x1 in Roots f by POLYNOM5:def 9; :: thesis: verum

end;

A9: the carrier of (gr {a}) c= Roots f

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of (gr {a}) or x in Roots f )
assume A10: x in the carrier of (gr {a}) ; :: thesis: x in Roots f
the carrier of (gr {a}) c= the carrier of G by GROUP_2:def 5;
then reconsider x1 = x as Element of G by A10;
x1 in gr {a} by A10, STRUCT_0:def 5;
then consider j being Integer such that
A11: x1 = a |^ j by GR_CY_1:25;
x1 |^ n = a |^ (j * n) by GROUP_1:67, A11
.= (a |^ n) |^ j by GROUP_1:67
.= (1_ G) |^ j by A1, GROUP_1:82
.= 1_ G by GROUP_1:61 ;
hence x in Roots f by A5; :: thesis: verum

end;

reconsider RF = Roots f as finite set by INT_7:27, A4;
consider m, n0 being Element of NAT such that
A12: ( n0 = deg f & m = card (Roots f) & m <= n0 ) by INT_7:27, A4;
reconsider gra = gr {a} as finite Group by A1;
A13: n = card gra by GR_CY_1:27, A1
.= card the carrier of (gr {a}) ;
b in Roots f by A1, A5;
then {b} c= Roots f by ZFMISC_1:37;
then A14: the carrier of (gr {a}) \/ {b} c= Roots f by A9, XBOOLE_1:8;
reconsider XX = the carrier of (gr {a}) as finite set by A13;
A15: card (the carrier of (gr {a}) \/ {b}) = card (XX \/ {b})
.= n0 + 1 by A4, A12, A13, CARD_2:54, A2 ;
card (n0 + 1) c= card m by CARD_1:27, A14, A15, A12;
then n0 + 1 <= m by NAT_1:41;
hence contradiction by NAT_1:16, A12, XXREAL_0:2; :: thesis: verum