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 that
A1: G is finite and
A2: 0 < n and
A3: ord a = n and
A4: b |^ n = 1_ G ; :: thesis: b is Element of (gr {a})
consider f being Polynomial of F such that
A5: deg f = n and
A6: 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 A2, Lm10;
assume A7: b is not Element of (gr {a}) ; :: thesis: contradiction
A8: the carrier of G c= the carrier of (MultGroup F) by GROUP_2:def 5;
A9: 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 )
A10: 1_ F = 1_ (MultGroup F) by UNIROOTS:17;
x1 in the carrier of (MultGroup F) by A8;
then x1 in NonZero F by UNIROOTS:def 1;
then reconsider x3 = x1 as Element of F ;
assume A11: x1 |^ n = 1_ G ; :: thesis: x1 in Roots f
then A12: x1 |^ n = 1. F by A10, GROUP_2:44;
reconsider x2 = x1 |^ n as Element of F by A11, A10, GROUP_2:44;
eval (f,x3) = x2 - (1. F) by A6
.= 0. F by A12, RLVECT_1:15 ;
then x3 is_a_root_of f by POLYNOM5:def 7;
hence x1 in Roots f by POLYNOM5:def 10; :: thesis: verum

end;

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

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of (gr {a}) or x in Roots f )
assume A14: 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 A14;
x1 in gr {a} by A14;
then consider j being Integer such that
A15: x1 = a |^ j by GR_CY_1:5;
x1 |^ n = a |^ (j * n) by A15, GROUP_1:35
.= (a |^ n) |^ j by GROUP_1:35
.= (1_ G) |^ j by A3, GROUP_1:41
.= 1_ G by GROUP_1:31 ;
hence x in Roots f by A9; :: thesis: verum

end;

b in Roots f by A4, A9;
then {b} c= Roots f by ZFMISC_1:31;
then A16: the carrier of (gr {a}) \/ {b} c= Roots f by A13, XBOOLE_1:8;
reconsider gra = gr {a} as finite Group by A1;
A17: n = card gra by A1, A3, GR_CY_1:7
.= card the carrier of (gr {a}) ;
then reconsider XX = the carrier of (gr {a}) as finite set ;
consider m, n0 being Element of NAT such that
A18: n0 = deg f and
A19: m = card (Roots f) and
A20: m <= n0 by A5, INT_7:27;
card ( the carrier of (gr {a}) \/ {b}) = card (XX \/ {b})
.= n0 + 1 by A7, A5, A18, A17, CARD_2:41 ;
then card (Segm (n0 + 1)) c= card (Segm m) by A19, A16, CARD_1:11;
then n0 + 1 <= m by NAT_1:40;
hence contradiction by A20, NAT_1:16, XXREAL_0:2; :: thesis: verum