let G be strict cyclic Group; :: thesis: for H being strict Subgroup of G holds H is cyclic Group

let H be strict Subgroup of G; :: thesis: H is cyclic Group

let H be strict Subgroup of G; :: thesis: H is cyclic Group

per cases
( H = (1). G or H <> (1). G )
;

end;

suppose A1:
H <> (1). G
; :: thesis: H is cyclic Group

consider b being Element of G such that

A2: multMagma(# the carrier of G, the multF of G #) = gr {b} by GR_CY_1:def 7;

ex m being Nat st

( 0 < m & b |^ m in H & ( for j being Nat st 0 < j & b |^ j in H holds

m <= j ) )

A4: 0 < m and

A5: b |^ m in H and

A6: for j being Nat st 0 < j & b |^ j in H holds

m <= j ;

set c = b |^ m;

reconsider c = b |^ m as Element of H by A5;

for a being Element of H ex i being Integer st a = c |^ i

hence H is cyclic Group by GR_CY_2:4; :: thesis: verum

end;A2: multMagma(# the carrier of G, the multF of G #) = gr {b} by GR_CY_1:def 7;

ex m being Nat st

( 0 < m & b |^ m in H & ( for j being Nat st 0 < j & b |^ j in H holds

m <= j ) )

proof

then consider m being Nat such that
defpred S_{1}[ Nat] means ( 0 < $1 & b |^ $1 in H );

ex k being Nat st S_{1}[k]
by A1, A2, Th24;

then A3: ex k being Nat st S_{1}[k]
;

ex m being Nat st

( S_{1}[m] & ( for j being Nat st S_{1}[j] holds

m <= j ) ) from NAT_1:sch 5(A3);

hence ex m being Nat st

( 0 < m & b |^ m in H & ( for j being Nat st 0 < j & b |^ j in H holds

m <= j ) ) ; :: thesis: verum

end;ex k being Nat st S

then A3: ex k being Nat st S

ex m being Nat st

( S

m <= j ) ) from NAT_1:sch 5(A3);

hence ex m being Nat st

( 0 < m & b |^ m in H & ( for j being Nat st 0 < j & b |^ j in H holds

m <= j ) ) ; :: thesis: verum

A4: 0 < m and

A5: b |^ m in H and

A6: for j being Nat st 0 < j & b |^ j in H holds

m <= j ;

set c = b |^ m;

reconsider c = b |^ m as Element of H by A5;

for a being Element of H ex i being Integer st a = c |^ i

proof

then
H = gr {c}
by GR_CY_2:5;
let a be Element of H; :: thesis: ex i being Integer st a = c |^ i

ex t being Integer st

( b |^ t in H & b |^ t = a )

A10: b |^ t in H and

A11: b |^ t = a ;

ex r, s being Integer st

( 0 <= s & s < m & t = (m * r) + s )

A12: 0 <= s and

A13: s < m and

A14: t = (m * r) + s ;

reconsider s = s as Element of NAT by A12, INT_1:3;

A15: b |^ t = (b |^ (m * r)) * (b |^ s) by A14, GROUP_1:33

.= ((b |^ m) |^ r) * (b |^ s) by GROUP_1:35 ;

A16: (b |^ m) |^ r in H by A5, Th22;

b |^ s in H

then b |^ s = 1_ G by GROUP_1:25;

then A18: b |^ t = (b |^ m) |^ r by A15, GROUP_1:def 4;

(b |^ m) |^ r = c |^ r by GROUP_4:2;

hence ex i being Integer st a = c |^ i by A11, A18; :: thesis: verum

end;ex t being Integer st

( b |^ t in H & b |^ t = a )

proof

then consider t being Integer such that
A7:
a in G
by GROUP_2:41;

A8: a in gr {b} by A2, GROUP_2:41;

a is Element of G by A7;

then consider j1 being Integer such that

A9: a = b |^ j1 by A8, GR_CY_1:5;

b |^ j1 in H by A9;

hence ex t being Integer st

( b |^ t in H & b |^ t = a ) by A9; :: thesis: verum

end;A8: a in gr {b} by A2, GROUP_2:41;

a is Element of G by A7;

then consider j1 being Integer such that

A9: a = b |^ j1 by A8, GR_CY_1:5;

b |^ j1 in H by A9;

hence ex t being Integer st

( b |^ t in H & b |^ t = a ) by A9; :: thesis: verum

A10: b |^ t in H and

A11: b |^ t = a ;

ex r, s being Integer st

( 0 <= s & s < m & t = (m * r) + s )

proof

then consider r, s being Integer such that
take
t div m
; :: thesis: ex s being Integer st

( 0 <= s & s < m & t = (m * (t div m)) + s )

take t mod m ; :: thesis: ( 0 <= t mod m & t mod m < m & t = (m * (t div m)) + (t mod m) )

thus ( 0 <= t mod m & t mod m < m & t = (m * (t div m)) + (t mod m) ) by A4, NEWTON:64, NEWTON:65, NEWTON:66; :: thesis: verum

end;( 0 <= s & s < m & t = (m * (t div m)) + s )

take t mod m ; :: thesis: ( 0 <= t mod m & t mod m < m & t = (m * (t div m)) + (t mod m) )

thus ( 0 <= t mod m & t mod m < m & t = (m * (t div m)) + (t mod m) ) by A4, NEWTON:64, NEWTON:65, NEWTON:66; :: thesis: verum

A12: 0 <= s and

A13: s < m and

A14: t = (m * r) + s ;

reconsider s = s as Element of NAT by A12, INT_1:3;

A15: b |^ t = (b |^ (m * r)) * (b |^ s) by A14, GROUP_1:33

.= ((b |^ m) |^ r) * (b |^ s) by GROUP_1:35 ;

A16: (b |^ m) |^ r in H by A5, Th22;

b |^ s in H

proof

then
s = 0
by A6, A13;
set u = b |^ t;

set v = (b |^ m) |^ r;

A17: (((b |^ m) |^ r) ") * (b |^ t) = ((((b |^ m) |^ r) ") * ((b |^ m) |^ r)) * (b |^ s) by A15, GROUP_1:def 3

.= (1_ G) * (b |^ s) by GROUP_1:def 5

.= b |^ s by GROUP_1:def 4 ;

((b |^ m) |^ r) " in H by A16, GROUP_2:51;

hence b |^ s in H by A10, A17, GROUP_2:50; :: thesis: verum

end;set v = (b |^ m) |^ r;

A17: (((b |^ m) |^ r) ") * (b |^ t) = ((((b |^ m) |^ r) ") * ((b |^ m) |^ r)) * (b |^ s) by A15, GROUP_1:def 3

.= (1_ G) * (b |^ s) by GROUP_1:def 5

.= b |^ s by GROUP_1:def 4 ;

((b |^ m) |^ r) " in H by A16, GROUP_2:51;

hence b |^ s in H by A10, A17, GROUP_2:50; :: thesis: verum

then b |^ s = 1_ G by GROUP_1:25;

then A18: b |^ t = (b |^ m) |^ r by A15, GROUP_1:def 4;

(b |^ m) |^ r = c |^ r by GROUP_4:2;

hence ex i being Integer st a = c |^ i by A11, A18; :: thesis: verum

hence H is cyclic Group by GR_CY_2:4; :: thesis: verum