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

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

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

A13:
the carrier of (gr {a}) c= Roots f
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;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

proof

b in Roots f
by A4, A9;
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;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

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