:: GR_CY_2 semantic presentation

begin


theorem :: GR_CY_2:1
for G being Group
for a, b being Element of G
for k being Element of NAT st ord a > 1 & a = b |^ k holds
k <> 0
proof
let G be Group; ::_thesis: for a, b being Element of G
for k being Element of NAT st ord a > 1 & a = b |^ k holds
k <> 0
let a, b be Element of G; ::_thesis: for k being Element of NAT st ord a > 1 & a = b |^ k holds
k <> 0
let k be Element of NAT ; ::_thesis: ( ord a > 1 & a = b |^ k implies k <> 0 )
assume that
A1: ord a > 1 and
A2: ( a = b |^ k & k = 0 ) ; ::_thesis: contradiction
 a = 1_ G by A2, GROUP_1:25;
hence  contradiction by A1, GROUP_1:42; ::_thesis: verum
end;

theorem Th2: :: GR_CY_2:2
for G being Group
for a being Element of G holds a in gr {a}
proof
let G be Group; ::_thesis: for a being Element of G holds a in gr {a}
let a be Element of G; ::_thesis: a in gr {a}
 ex i being Integer st a = a |^ i
proof
reconsider i = 1 as Integer ;
take  i ; ::_thesis: a = a |^ i
thus  a = a |^ i by GROUP_1:26; ::_thesis: verum
end;
hence  a in gr {a} by GR_CY_1:5; ::_thesis: verum
end;

theorem Th3: :: GR_CY_2:3
for G being Group
for G1 being Subgroup of G
for a being Element of G
for a1 being Element of G1 st a = a1 holds
gr {a} = gr {a1}
proof
let G be Group; ::_thesis: for G1 being Subgroup of G
for a being Element of G
for a1 being Element of G1 st a = a1 holds
gr {a} = gr {a1}
let G1 be Subgroup of G; ::_thesis: for a being Element of G
for a1 being Element of G1 st a = a1 holds
gr {a} = gr {a1}
let a be Element of G; ::_thesis: for a1 being Element of G1 st a = a1 holds
gr {a} = gr {a1}
let a1 be Element of G1; ::_thesis: ( a = a1 implies gr {a} = gr {a1} )
reconsider Gr = gr {a1} as Subgroup of G by GROUP_2:56;
assume A1: a = a1 ; ::_thesis: gr {a} = gr {a1}
A2: for b being Element of G st b in Gr holds
b in gr {a}
proof
let b be Element of G; ::_thesis: ( b in Gr implies b in gr {a} )
assume A3: b in Gr ; ::_thesis: b in gr {a}
then  b in G1 by GROUP_2:40;
then reconsider b1 = b as Element of G1 by STRUCT_0:def_5;
consider i being Integer such that
A4: b1 = a1 |^ i by A3, GR_CY_1:5;
 b = a |^ i by A1, A4, GROUP_4:2;
hence  b in gr {a} by GR_CY_1:5; ::_thesis: verum
end;
 for b being Element of G st b in gr {a} holds
b in Gr
proof
let b be Element of G; ::_thesis: ( b in gr {a} implies b in Gr )
assume  b in gr {a} ; ::_thesis: b in Gr
then consider i being Integer such that
A5: b = a |^ i by GR_CY_1:5;
 b = a1 |^ i by A1, A5, GROUP_4:2;
hence  b in Gr by GR_CY_1:5; ::_thesis: verum
end;
hence  gr {a} = gr {a1} by A2, GROUP_2:60; ::_thesis: verum
end;

theorem Th4: :: GR_CY_2:4
for G being Group
for a being Element of G holds gr {a} is cyclic Group
proof
let G be Group; ::_thesis: for a being Element of G holds gr {a} is cyclic Group
let a be Element of G; ::_thesis: gr {a} is cyclic Group
 ex a1 being Element of (gr {a}) st gr {a} = gr {a1}
proof
 a in gr {a} by Th2;
then reconsider a1 = a as Element of (gr {a}) by STRUCT_0:def_5;
take  a1 ; ::_thesis: gr {a} = gr {a1}
thus  gr {a} = gr {a1} by Th3; ::_thesis: verum
end;
hence  gr {a} is cyclic Group by GR_CY_1:def_7; ::_thesis: verum
end;

theorem Th5: :: GR_CY_2:5
for G being strict Group
for b being Element of G holds
( ( for a being Element of G ex i being Integer st a = b |^ i ) iff G = gr {b} )
proof
let G be strict Group; ::_thesis: for b being Element of G holds
( ( for a being Element of G ex i being Integer st a = b |^ i ) iff G = gr {b} )
let b be Element of G; ::_thesis: ( ( for a being Element of G ex i being Integer st a = b |^ i ) iff G = gr {b} )
thus  ( ( for a being Element of G ex i being Integer st a = b |^ i ) implies G = gr {b} ) ::_thesis: ( G = gr {b} implies for a being Element of G ex i being Integer st a = b |^ i )
proof
assume A1: for a being Element of G ex i being Integer st a = b |^ i ; ::_thesis: G = gr {b}
 for a being Element of G holds a in gr {b}
proof
let a be Element of G; ::_thesis: a in gr {b}
 ex i being Integer st a = b |^ i by A1;
hence  a in gr {b} by GR_CY_1:5; ::_thesis: verum
end;
hence  G = gr {b} by GROUP_2:62; ::_thesis: verum
end;
assume A2: G = gr {b} ; ::_thesis: for a being Element of G ex i being Integer st a = b |^ i
let a be Element of G; ::_thesis: ex i being Integer st a = b |^ i
 a in gr {b} by A2, STRUCT_0:def_5;
hence  ex i being Integer st a = b |^ i by GR_CY_1:5; ::_thesis: verum
end;

theorem Th6: :: GR_CY_2:6
for G being finite strict Group
for b being Element of G holds
( ( for a being Element of G ex p being Element of NAT st a = b |^ p ) iff G = gr {b} )
proof
let G be finite strict Group; ::_thesis: for b being Element of G holds
( ( for a being Element of G ex p being Element of NAT st a = b |^ p ) iff G = gr {b} )
let b be Element of G; ::_thesis: ( ( for a being Element of G ex p being Element of NAT st a = b |^ p ) iff G = gr {b} )
reconsider n1 = card G as Integer ;
thus  ( ( for a being Element of G ex p being Element of NAT st a = b |^ p ) implies G = gr {b} ) ::_thesis: ( G = gr {b} implies for a being Element of G ex p being Element of NAT st a = b |^ p )
proof
assume A1: for a being Element of G ex p being Element of NAT st a = b |^ p ; ::_thesis: G = gr {b}
 for a being Element of G ex i being Integer st a = b |^ i
proof
let a be Element of G; ::_thesis: ex i being Integer st a = b |^ i
consider p being Element of NAT  such that
A2: a = b |^ p by A1;
reconsider p1 = p as Integer ;
take  p1 ; ::_thesis: a = b |^ p1
thus  a = b |^ p1 by A2; ::_thesis: verum
end;
hence  G = gr {b} by Th5; ::_thesis: verum
end;
assume A3: G = gr {b} ; ::_thesis: for a being Element of G ex p being Element of NAT st a = b |^ p
let a be Element of G; ::_thesis: ex p being Element of NAT st a = b |^ p
consider i being Integer such that
A4: a = b |^ i by A3, Th5;
reconsider p = i mod n1 as Element of NAT by INT_1:3, NEWTON:64;
take  p ; ::_thesis: a = b |^ p
a = b |^ (((i div n1) * n1) + (i mod n1)) by A4, NEWTON:66
.= (b |^ ((i div n1) * n1)) * (b |^ (i mod n1)) by GROUP_1:33
.= ((b |^ (i div n1)) |^ (card G)) * (b |^ (i mod n1)) by GROUP_1:35
.= (1_ G) * (b |^ (i mod n1)) by GR_CY_1:9
.= b |^ (i mod n1) by GROUP_1:def_4 ;
hence  a = b |^ p ; ::_thesis: verum
end;

theorem Th7: :: GR_CY_2:7
for G being strict Group
for a being Element of G st G is finite & G = gr {a} holds
for G1 being strict Subgroup of G ex p being Element of NAT st G1 = gr {(a |^ p)}
proof
let G be strict Group; ::_thesis: for a being Element of G st G is finite & G = gr {a} holds
for G1 being strict Subgroup of G ex p being Element of NAT st G1 = gr {(a |^ p)}
let a be Element of G; ::_thesis: ( G is finite & G = gr {a} implies for G1 being strict Subgroup of G ex p being Element of NAT st G1 = gr {(a |^ p)} )
assume that
A1: G is finite and
A2: G = gr {a} ; ::_thesis: for G1 being strict Subgroup of G ex p being Element of NAT st G1 = gr {(a |^ p)}
let G1 be strict Subgroup of G; ::_thesis: ex p being Element of NAT st G1 = gr {(a |^ p)}
 G is cyclic Group by A2, GR_CY_1:def_7;
then  G1 is cyclic Group by A1, GR_CY_1:20;
then consider b being Element of G1 such that
A3: G1 = gr {b} by GR_CY_1:def_7;
reconsider b1 = b as Element of G by GROUP_2:42;
consider p being Element of NAT  such that
A4: b1 = a |^ p by A1, A2, Th6;
take  p ; ::_thesis: G1 = gr {(a |^ p)}
thus  G1 = gr {(a |^ p)} by A3, A4, Th3; ::_thesis: verum
end;

theorem Th8: :: GR_CY_2:8
for n, p, s being Element of NAT
for G being finite Group
for a being Element of G st G = gr {a} & card G = n & n = p * s holds
ord (a |^ p) = s
proof
let n, p, s be Element of NAT ; ::_thesis: for G being finite Group
for a being Element of G st G = gr {a} & card G = n & n = p * s holds
ord (a |^ p) = s
let G be finite Group; ::_thesis: for a being Element of G st G = gr {a} & card G = n & n = p * s holds
ord (a |^ p) = s
let a be Element of G; ::_thesis: ( G = gr {a} & card G = n & n = p * s implies ord (a |^ p) = s )
assume that
A1: G = gr {a} and
A2: card G = n and
A3: n = p * s ; ::_thesis: ord (a |^ p) = s
A4: ( not a |^ p is being_of_order_0 & s <> 0 ) by A2, A3, GR_CY_1:6;
A5: p <> 0 by A2, A3;
A6: for k being Nat st (a |^ p) |^ k = 1_ G & k <> 0 holds
s <= k
proof
let k be Nat; ::_thesis: ( (a |^ p) |^ k = 1_ G & k <> 0 implies s <= k )
assume that
A7: (a |^ p) |^ k = 1_ G and
A8: ( k <> 0 & s > k ) ; ::_thesis: contradiction
A9: a |^ (p * k) = 1_ G by A7, GROUP_1:35;
A10: ( ord a = n & not a is being_of_order_0 ) by A1, A2, GR_CY_1:6, GR_CY_1:7;
 ( p * s > p * k & p * k <> 0 ) by A5, A8, XCMPLX_1:6, XREAL_1:68;
hence  contradiction by A3, A10, A9, GROUP_1:def_11; ::_thesis: verum
end;
(a |^ p) |^ s = a |^ n by A3, GROUP_1:35
.= 1_ G by A2, GR_CY_1:9 ;
hence  ord (a |^ p) = s by A4, A6, GROUP_1:def_11; ::_thesis: verum
end;

theorem Th9: :: GR_CY_2:9
for G being Group
for a being Element of G
for s, k being Element of NAT st s divides k holds
a |^ k in gr {(a |^ s)}
proof
let G be Group; ::_thesis: for a being Element of G
for s, k being Element of NAT st s divides k holds
a |^ k in gr {(a |^ s)}
let a be Element of G; ::_thesis: for s, k being Element of NAT st s divides k holds
a |^ k in gr {(a |^ s)}
let s, k be Element of NAT ; ::_thesis: ( s divides k implies a |^ k in gr {(a |^ s)} )
assume  s divides k ; ::_thesis: a |^ k in gr {(a |^ s)}
then consider p being Nat such that
A1: k = s * p by NAT_D:def_3;
 ex i being Integer st a |^ k = (a |^ s) |^ i
proof
reconsider p9 = p as Integer ;
take  p9 ; ::_thesis: a |^ k = (a |^ s) |^ p9
thus  a |^ k = (a |^ s) |^ p9 by A1, GROUP_1:35; ::_thesis: verum
end;
hence  a |^ k in gr {(a |^ s)} by GR_CY_1:5; ::_thesis: verum
end;

theorem Th10: :: GR_CY_2:10
for s, k being Element of NAT
for G being finite Group
for a being Element of G st card (gr {(a |^ s)}) = card (gr {(a |^ k)}) & a |^ k in gr {(a |^ s)} holds
gr {(a |^ s)} = gr {(a |^ k)}
proof
let s, k be Element of NAT ; ::_thesis: for G being finite Group
for a being Element of G st card (gr {(a |^ s)}) = card (gr {(a |^ k)}) & a |^ k in gr {(a |^ s)} holds
gr {(a |^ s)} = gr {(a |^ k)}
let G be finite Group; ::_thesis: for a being Element of G st card (gr {(a |^ s)}) = card (gr {(a |^ k)}) & a |^ k in gr {(a |^ s)} holds
gr {(a |^ s)} = gr {(a |^ k)}
let a be Element of G; ::_thesis: ( card (gr {(a |^ s)}) = card (gr {(a |^ k)}) & a |^ k in gr {(a |^ s)} implies gr {(a |^ s)} = gr {(a |^ k)} )
assume A1: card (gr {(a |^ s)}) = card (gr {(a |^ k)}) ; ::_thesis: ( not a |^ k in gr {(a |^ s)} or gr {(a |^ s)} = gr {(a |^ k)} )
assume  a |^ k in gr {(a |^ s)} ; ::_thesis: gr {(a |^ s)} = gr {(a |^ k)}
then reconsider h = a |^ k as Element of (gr {(a |^ s)}) by STRUCT_0:def_5;
 card (gr {h}) = card (gr {(a |^ s)}) by A1, Th3;
hence  gr {(a |^ s)} = gr {h} by GROUP_2:73
.= gr {(a |^ k)} by Th3 ;
::_thesis: verum
end;

theorem Th11: :: GR_CY_2:11
for n, p, k being Element of NAT
for G being finite Group
for G1 being Subgroup of G
for a being Element of G st card G = n & G = gr {a} & card G1 = p & G1 = gr {(a |^ k)} holds
n divides k * p
proof
let n, p, k be Element of NAT ; ::_thesis: for G being finite Group
for G1 being Subgroup of G
for a being Element of G st card G = n & G = gr {a} & card G1 = p & G1 = gr {(a |^ k)} holds
n divides k * p
let G be finite Group; ::_thesis: for G1 being Subgroup of G
for a being Element of G st card G = n & G = gr {a} & card G1 = p & G1 = gr {(a |^ k)} holds
n divides k * p
let G1 be Subgroup of G; ::_thesis: for a being Element of G st card G = n & G = gr {a} & card G1 = p & G1 = gr {(a |^ k)} holds
n divides k * p
let a be Element of G; ::_thesis: ( card G = n & G = gr {a} & card G1 = p & G1 = gr {(a |^ k)} implies n divides k * p )
assume that
A1: card G = n and
A2: G = gr {a} and
A3: card G1 = p and
A4: G1 = gr {(a |^ k)} ; ::_thesis: n divides k * p
set z = k * p;
consider m, l being Nat such that
A5: k * p = (n * m) + l and
A6: l < n by A1, NAT_1:17;
 l = 0
proof
 a |^ k in gr {(a |^ k)} by Th2;
then reconsider h = a |^ k as Element of G1 by A4, STRUCT_0:def_5;
assume A7: l <> 0 ; ::_thesis: contradiction
a |^ (k * p) = (a |^ k) |^ p by GROUP_1:35
.= h |^ p by GROUP_4:1
.= 1_ G1 by A3, GR_CY_1:9
.= 1_ G by GROUP_2:44 ;
then A8: 1_ G = (a |^ (n * m)) * (a |^ l) by A5, GROUP_1:33
.= ((a |^ n) |^ m) * (a |^ l) by GROUP_1:35
.= ((1_ G) |^ m) * (a |^ l) by A1, GR_CY_1:9
.= (1_ G) * (a |^ l) by GROUP_1:31
.= a |^ l by GROUP_1:def_4 ;
 ( not a is being_of_order_0 & ord a = n ) by A1, A2, GR_CY_1:6, GR_CY_1:7;
hence  contradiction by A6, A7, A8, GROUP_1:def_11; ::_thesis: verum
end;
hence  n divides k * p by A5, NAT_D:def_3; ::_thesis: verum
end;

theorem :: GR_CY_2:12
for n, k being Element of NAT
for G being finite strict Group
for a being Element of G st G = gr {a} & card G = n holds
( G = gr {(a |^ k)} iff k gcd n = 1 )
proof
let n, k be Element of NAT ; ::_thesis: for G being finite strict Group
for a being Element of G st G = gr {a} & card G = n holds
( G = gr {(a |^ k)} iff k gcd n = 1 )
let G be finite strict Group; ::_thesis: for a being Element of G st G = gr {a} & card G = n holds
( G = gr {(a |^ k)} iff k gcd n = 1 )
let a be Element of G; ::_thesis: ( G = gr {a} & card G = n implies ( G = gr {(a |^ k)} iff k gcd n = 1 ) )
assume that
A1: G = gr {a} and
A2: card G = n ; ::_thesis: ( G = gr {(a |^ k)} iff k gcd n = 1 )
A3: ( G = gr {(a |^ k)} implies k gcd n = 1 )
proof
set d = k gcd n;
assume that
A4: G = gr {(a |^ k)} and
A5: k gcd n <> 1 ; ::_thesis: contradiction
 k gcd n divides n by NAT_D:def_5;
then consider p being Nat such that
A6: n = (k gcd n) * p by NAT_D:def_3;
A7: p <> 0 by A2, A6;
A8: p <> n
proof
assume  p = n ; ::_thesis: contradiction
then  (k gcd n) * p = p * 1 by A6;
hence  contradiction by A5, A2, A6, XCMPLX_1:5; ::_thesis: verum
end;
 k gcd n divides k by NAT_D:def_5;
then consider l being Nat such that
A9: k = (k gcd n) * l by NAT_D:def_3;
A10: not a |^ k is being_of_order_0 by GR_CY_1:6;
(a |^ k) |^ p = a |^ ((l * (k gcd n)) * p) by A9, GROUP_1:35
.= a |^ (n * l) by A6
.= (a |^ n) |^ l by GROUP_1:35
.= (1_ G) |^ l by A2, GR_CY_1:9
.= 1_ G by GROUP_1:31 ;
then A11: ord (a |^ k) <= p by A7, A10, GROUP_1:def_11;
 p divides n by A6, NAT_D:def_3;
then  p <= n by A2, NAT_D:7;
then  p < n by A8, XXREAL_0:1;
hence  contradiction by A2, A4, A11, GR_CY_1:7; ::_thesis: verum
end;
 ( k gcd n = 1 implies G = gr {(a |^ k)} )
proof
assume  k gcd n = 1 ; ::_thesis: G = gr {(a |^ k)}
then consider i, i1 being Integer such that
A12: (i * k) + (i1 * n) = 1 by A2, NEWTON:67;
 for b being Element of G holds b in gr {(a |^ k)}
proof
let b be Element of G; ::_thesis: b in gr {(a |^ k)}
 b in G by STRUCT_0:def_5;
then consider i0 being Integer such that
A13: b = a |^ i0 by A1, GR_CY_1:5;
A14: i0 = ((k * i) + (n * i1)) * i0 by A12
.= ((k * i) * i0) + ((n * i1) * i0) ;
 ex i2 being Integer st b = (a |^ k) |^ i2
proof
take  i * i0 ; ::_thesis: b = (a |^ k) |^ (i * i0)
b = (a |^ ((k * i) * i0)) * (a |^ (n * (i1 * i0))) by A13, A14, GROUP_1:33
.= (a |^ ((k * i) * i0)) * ((a |^ n) |^ (i1 * i0)) by GROUP_1:35
.= (a |^ ((k * i) * i0)) * ((1_ G) |^ (i1 * i0)) by A2, GR_CY_1:9
.= (a |^ ((k * i) * i0)) * (1_ G) by GROUP_1:31
.= a |^ (k * (i * i0)) by GROUP_1:def_4
.= (a |^ k) |^ (i * i0) by GROUP_1:35 ;
hence  b = (a |^ k) |^ (i * i0) ; ::_thesis: verum
end;
hence  b in gr {(a |^ k)} by GR_CY_1:5; ::_thesis: verum
end;
hence  G = gr {(a |^ k)} by GROUP_2:62; ::_thesis: verum
end;
hence  ( G = gr {(a |^ k)} iff k gcd n = 1 ) by A3; ::_thesis: verum
end;

theorem Th13: :: GR_CY_2:13
for Gc being cyclic Group
for H being Subgroup of Gc
for g being Element of Gc st Gc = gr {g} & g in H holds
multMagma(# the carrier of Gc, the multF of Gc #) = multMagma(# the carrier of H, the multF of H #)
proof
let Gc be cyclic Group; ::_thesis: for H being Subgroup of Gc
for g being Element of Gc st Gc = gr {g} & g in H holds
multMagma(# the carrier of Gc, the multF of Gc #) = multMagma(# the carrier of H, the multF of H #)
let H be Subgroup of Gc; ::_thesis: for g being Element of Gc st Gc = gr {g} & g in H holds
multMagma(# the carrier of Gc, the multF of Gc #) = multMagma(# the carrier of H, the multF of H #)
let g be Element of Gc; ::_thesis: ( Gc = gr {g} & g in H implies multMagma(# the carrier of Gc, the multF of Gc #) = multMagma(# the carrier of H, the multF of H #) )
assume that
A1: Gc = gr {g} and
A2: g in H ; ::_thesis: multMagma(# the carrier of Gc, the multF of Gc #) = multMagma(# the carrier of H, the multF of H #)
reconsider g9 = g as Element of H by A2, STRUCT_0:def_5;
 gr {g9} is Subgroup of H ;
then  gr {g} is Subgroup of H by Th3;
hence  multMagma(# the carrier of Gc, the multF of Gc #) = multMagma(# the carrier of H, the multF of H #) by A1, GROUP_2:55; ::_thesis: verum
end;

theorem Th14: :: GR_CY_2:14
for Gc being cyclic Group
for g being Element of Gc st Gc = gr {g} holds
( Gc is finite iff ex i, i1 being Integer st
( i <> i1 & g |^ i = g |^ i1 ) )
proof
let Gc be cyclic Group; ::_thesis: for g being Element of Gc st Gc = gr {g} holds
( Gc is finite iff ex i, i1 being Integer st
( i <> i1 & g |^ i = g |^ i1 ) )
let g be Element of Gc; ::_thesis: ( Gc = gr {g} implies ( Gc is finite iff ex i, i1 being Integer st
( i <> i1 & g |^ i = g |^ i1 ) ) )
assume A1: Gc = gr {g} ; ::_thesis: ( Gc is finite iff ex i, i1 being Integer st
( i <> i1 & g |^ i = g |^ i1 ) )
A2: ( ex i, i1 being Integer st
( i <> i1 & g |^ i = g |^ i1 ) implies Gc is finite )
proof
given i, i1 being Integer such that A3: i <> i1 and
A4: g |^ i = g |^ i1 ; ::_thesis: Gc is finite
now__::_thesis:_Gc_is_finite
percases ( i < i1 or i1 < i ) by A3, XXREAL_0:1;
supposeA5: i < i1 ; ::_thesis: Gc is finite
set r = i1 - i;
 i1 > i + 0 by A5;
then A6: i1 - i > 0 by XREAL_1:20;
then reconsider m = i1 - i as Element of NAT by INT_1:3;
 (g |^ i1) * (g |^ (- i)) = (g |^ i) * ((g |^ i) ") by A4, GROUP_1:36;
then  (g |^ i1) * (g |^ (- i)) = 1_ Gc by GROUP_1:def_5;
then A7: g |^ (i1 + (- i)) = 1_ Gc by GROUP_1:33;
A8: for i2 being Integer ex n being Element of NAT st
( g |^ i2 = g |^ n & n >= 0 & n < i1 - i )
proof
let i2 be Integer; ::_thesis: ex n being Element of NAT st
( g |^ i2 = g |^ n & n >= 0 & n < i1 - i )
reconsider m = i2 mod (i1 - i) as Element of NAT by A6, INT_1:3, NEWTON:64;
take  m ; ::_thesis: ( g |^ i2 = g |^ m & m >= 0 & m < i1 - i )
g |^ i2 = g |^ (((i2 div (i1 - i)) * (i1 - i)) + (i2 mod (i1 - i))) by A6, NEWTON:66
.= (g |^ ((i1 - i) * (i2 div (i1 - i)))) * (g |^ (i2 mod (i1 - i))) by GROUP_1:33
.= ((1_ Gc) |^ (i2 div (i1 - i))) * (g |^ (i2 mod (i1 - i))) by A7, GROUP_1:35
.= (1_ Gc) * (g |^ (i2 mod (i1 - i))) by GROUP_1:31
.= g |^ (i2 mod (i1 - i)) by GROUP_1:def_4 ;
hence  ( g |^ i2 = g |^ m & m >= 0 & m < i1 - i ) by A6, NEWTON:65; ::_thesis: verum
end;
 ex F being FinSequence st rng F = the carrier of Gc
proof
deffunc H1( Nat) ->  Element of the carrier of Gc = g |^ $1;
consider F being FinSequence such that
A9: len F = m and
A10: for p being Nat st p in dom F holds
F . p = H1(p) from FINSEQ_1:sch_2();
A11: dom F = Seg m by A9, FINSEQ_1:def_3;
A12: the carrier of Gc c= rng F
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in the carrier of Gc or y in rng F )
assume  y in the carrier of Gc ; ::_thesis: y in rng F
then reconsider a = y as Element of Gc ;
 a in Gc by STRUCT_0:def_5;
then A13: ex i2 being Integer st a = g |^ i2 by A1, GR_CY_1:5;
 ex n being Element of NAT st
( n in dom F & F . n = a )
proof
consider n being Element of NAT  such that
A14: a = g |^ n and
 n >= 0 and
A15: n < i1 - i by A8, A13;
percases ( n = 0 or n > 0 ) ;
supposeA16: n = 0 ; ::_thesis: ex n being Element of NAT st
( n in dom F & F . n = a )
A17: m >= 0 + 1 by A6, NAT_1:13;
then A18: m in Seg m by FINSEQ_1:1;
A19: m in dom F by A11, A17, FINSEQ_1:1;
 a = g |^ m by A7, A14, A16, GROUP_1:25;
then  F . m = a by A10, A11, A18;
hence  ex n being Element of NAT st
( n in dom F & F . n = a ) by A19; ::_thesis: verum
end;
suppose n > 0 ; ::_thesis: ex n being Element of NAT st
( n in dom F & F . n = a )
then A20: n >= 0 + 1 by NAT_1:13;
then  n in Seg m by A15, FINSEQ_1:1;
then A21: F . n = a by A10, A11, A14;
 n in dom F by A11, A15, A20, FINSEQ_1:1;
hence  ex n being Element of NAT st
( n in dom F & F . n = a ) by A21; ::_thesis: verum
end;
end;
end;
hence  y in rng F by FUNCT_1:def_3; ::_thesis: verum
end;
take  F ; ::_thesis: rng F = the carrier of Gc
A22: for y being set st y in rng F holds
ex n being Element of NAT st y = g |^ n
proof
let y be set ; ::_thesis: ( y in rng F implies ex n being Element of NAT st y = g |^ n )
assume  y in rng F ; ::_thesis: ex n being Element of NAT st y = g |^ n
then consider x being set  such that
A23: x in dom F and
A24: F . x = y by FUNCT_1:def_3;
reconsider n = x as Element of NAT by A23;
take  n ; ::_thesis: y = g |^ n
thus  y = g |^ n by A10, A23, A24; ::_thesis: verum
end;
 rng F c= the carrier of Gc
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng F or y in the carrier of Gc )
assume  y in rng F ; ::_thesis: y in the carrier of Gc
then  ex n being Element of NAT st y = g |^ n by A22;
hence  y in the carrier of Gc ; ::_thesis: verum
end;
hence  rng F = the carrier of Gc by A12, XBOOLE_0:def_10; ::_thesis: verum
end;
hence  Gc is finite ; ::_thesis: verum
end;
supposeA25: i1 < i ; ::_thesis: Gc is finite
set r = i - i1;
 i > i1 + 0 by A25;
then A26: i - i1 > 0 by XREAL_1:20;
then reconsider m = i - i1 as Element of NAT by INT_1:3;
 (g |^ i) * (g |^ (- i1)) = (g |^ i1) * ((g |^ i1) ") by A4, GROUP_1:36;
then  (g |^ i) * (g |^ (- i1)) = 1_ Gc by GROUP_1:def_5;
then A27: g |^ (i + (- i1)) = 1_ Gc by GROUP_1:33;
A28: for i2 being Integer ex n being Element of NAT st
( g |^ i2 = g |^ n & n >= 0 & n < i - i1 )
proof
let i2 be Integer; ::_thesis: ex n being Element of NAT st
( g |^ i2 = g |^ n & n >= 0 & n < i - i1 )
reconsider m = i2 mod (i - i1) as Element of NAT by A26, INT_1:3, NEWTON:64;
take  m ; ::_thesis: ( g |^ i2 = g |^ m & m >= 0 & m < i - i1 )
g |^ i2 = g |^ (((i2 div (i - i1)) * (i - i1)) + (i2 mod (i - i1))) by A26, NEWTON:66
.= (g |^ ((i - i1) * (i2 div (i - i1)))) * (g |^ (i2 mod (i - i1))) by GROUP_1:33
.= ((1_ Gc) |^ (i2 div (i - i1))) * (g |^ (i2 mod (i - i1))) by A27, GROUP_1:35
.= (1_ Gc) * (g |^ (i2 mod (i - i1))) by GROUP_1:31
.= g |^ (i2 mod (i - i1)) by GROUP_1:def_4 ;
hence  ( g |^ i2 = g |^ m & m >= 0 & m < i - i1 ) by A26, NEWTON:65; ::_thesis: verum
end;
 ex F being FinSequence st rng F = the carrier of Gc
proof
deffunc H1( Nat) ->  Element of the carrier of Gc = g |^ $1;
consider F being FinSequence such that
A29: len F = m and
A30: for p being Nat st p in dom F holds
F . p = H1(p) from FINSEQ_1:sch_2();
A31: dom F = Seg m by A29, FINSEQ_1:def_3;
A32: the carrier of Gc c= rng F
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in the carrier of Gc or y in rng F )
assume  y in the carrier of Gc ; ::_thesis: y in rng F
then reconsider a = y as Element of Gc ;
 a in Gc by STRUCT_0:def_5;
then A33: ex i2 being Integer st a = g |^ i2 by A1, GR_CY_1:5;
 ex n being Element of NAT st
( n in dom F & F . n = a )
proof
consider n being Element of NAT  such that
A34: a = g |^ n and
 n >= 0 and
A35: n < i - i1 by A28, A33;
percases ( n = 0 or n > 0 ) ;
supposeA36: n = 0 ; ::_thesis: ex n being Element of NAT st
( n in dom F & F . n = a )
A37: m >= 0 + 1 by A26, NAT_1:13;
then A38: m in Seg m by FINSEQ_1:1;
A39: m in dom F by A31, A37, FINSEQ_1:1;
 a = g |^ m by A27, A34, A36, GROUP_1:25;
then  F . m = a by A30, A31, A38;
hence  ex n being Element of NAT st
( n in dom F & F . n = a ) by A39; ::_thesis: verum
end;
suppose n > 0 ; ::_thesis: ex n being Element of NAT st
( n in dom F & F . n = a )
then A40: n >= 0 + 1 by NAT_1:13;
then  n in Seg m by A35, FINSEQ_1:1;
then A41: F . n = a by A30, A31, A34;
 n in dom F by A31, A35, A40, FINSEQ_1:1;
hence  ex n being Element of NAT st
( n in dom F & F . n = a ) by A41; ::_thesis: verum
end;
end;
end;
hence  y in rng F by FUNCT_1:def_3; ::_thesis: verum
end;
take  F ; ::_thesis: rng F = the carrier of Gc
A42: for y being set st y in rng F holds
ex n being Element of NAT st y = g |^ n
proof
let y be set ; ::_thesis: ( y in rng F implies ex n being Element of NAT st y = g |^ n )
assume  y in rng F ; ::_thesis: ex n being Element of NAT st y = g |^ n
then consider x being set  such that
A43: x in dom F and
A44: F . x = y by FUNCT_1:def_3;
reconsider n = x as Element of NAT by A43;
take  n ; ::_thesis: y = g |^ n
thus  y = g |^ n by A30, A43, A44; ::_thesis: verum
end;
 rng F c= the carrier of Gc
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng F or y in the carrier of Gc )
assume  y in rng F ; ::_thesis: y in the carrier of Gc
then  ex n being Element of NAT st y = g |^ n by A42;
hence  y in the carrier of Gc ; ::_thesis: verum
end;
hence  rng F = the carrier of Gc by A32, XBOOLE_0:def_10; ::_thesis: verum
end;
hence  Gc is finite ; ::_thesis: verum
end;
end;
end;
hence  Gc is finite ; ::_thesis: verum
end;
 ( Gc is finite implies ex i, i1 being Integer st
( i <> i1 & g |^ i = g |^ i1 ) )
proof
assume  Gc is finite ; ::_thesis: ex i, i1 being Integer st
( i <> i1 & g |^ i = g |^ i1 )
then reconsider Gc = Gc as finite cyclic Group ;
reconsider z = 0 , i0 = card Gc as Integer ;
A45: g |^ z = 1_ Gc by GROUP_1:25
.= g |^ i0 by GR_CY_1:9 ;
thus  ex i, i1 being Integer st
( i <> i1 & g |^ i = g |^ i1 ) by A45; ::_thesis: verum
end;
hence  ( Gc is finite iff ex i, i1 being Integer st
( i <> i1 & g |^ i = g |^ i1 ) ) by A2; ::_thesis: verum
end;

registration
let n be non zero Nat;
cluster  ->  natural for Element of the carrier of (INT.Group n);
coherence
 for b1 being Element of (INT.Group n) holds b1 is natural ;
end;

theorem Th15: :: GR_CY_2:15
for Gc being finite strict cyclic Group holds INT.Group (card Gc),Gc are_isomorphic
proof
let Gc be finite strict cyclic Group; ::_thesis: INT.Group (card Gc),Gc are_isomorphic
set n = card Gc;
consider g being Element of Gc such that
A1: for h being Element of Gc ex p being Nat st h = g |^ p by GR_CY_1:18;
 for h being Element of Gc ex i being Integer st h = g |^ i
proof
let h be Element of Gc; ::_thesis: ex i being Integer st h = g |^ i
consider p being Nat such that
A2: h = g |^ p by A1;
reconsider p1 = p as Integer ;
take  p1 ; ::_thesis: h = g |^ p1
thus  h = g |^ p1 by A2; ::_thesis: verum
end;
then A3: Gc = gr {g} by Th5;
 ex h being Homomorphism of (INT.Group (card Gc)),Gc st h is bijective
proof
deffunc H1( Element of (INT.Group (card Gc))) ->  Element of the carrier of Gc = g |^ $1;
consider h being Function of the carrier of (INT.Group (card Gc)), the carrier of Gc such that
A4: for p being Element of (INT.Group (card Gc)) holds h . p = H1(p) from FUNCT_2:sch_4();
A5: for j, j1 being Element of (INT.Group (card Gc)) holds h . (j * j1) = (h . j) * (h . j1)
proof
let j, j1 be Element of (INT.Group (card Gc)); ::_thesis: h . (j * j1) = (h . j) * (h . j1)
reconsider j9 = j, j19 = j1 as Element of Segm (card Gc) ;
j * j1 = (j + j1) mod (card Gc) by GR_CY_1:def_4
.= (j + j1) - ((card Gc) * ((j + j1) div (card Gc))) by NEWTON:63 ;
then h . (j * j1) = g |^ ((j + j1) + (- ((card Gc) * ((j + j1) div (card Gc))))) by A4
.= (g |^ (j + j1)) * (g |^ (- ((card Gc) * ((j + j1) div (card Gc))))) by GROUP_1:33
.= (g |^ (j + j1)) * ((g |^ ((card Gc) * ((j + j1) div (card Gc)))) ") by GROUP_1:36
.= (g |^ (j + j1)) * (((g |^ (card Gc)) |^ ((j + j1) div (card Gc))) ") by GROUP_1:35
.= (g |^ (j + j1)) * (((1_ Gc) |^ ((j + j1) div (card Gc))) ") by GR_CY_1:9
.= (g |^ (j + j1)) * ((1_ Gc) ") by GROUP_1:31
.= (g |^ (j + j1)) * (1_ Gc) by GROUP_1:8
.= g |^ (j + j1) by GROUP_1:def_4
.= (g |^ j) * (g |^ j1) by GROUP_1:33
.= (h . j) * (g |^ j1) by A4
.= (h . j) * (h . j1) by A4 ;
hence  h . (j * j1) = (h . j) * (h . j1) ; ::_thesis: verum
end;
A6: h is one-to-one
proof
let x be set ; :: according to FUNCT_1:def_4 ::_thesis: for b1 being set holds
( not x in dom h or not b1 in dom h or not h . x = h . b1 or x = b1 )
let y be set ; ::_thesis: ( not x in dom h or not y in dom h or not h . x = h . y or x = y )
assume that
A7: x in dom h and
A8: y in dom h and
A9: h . x = h . y and
A10: x <> y ; ::_thesis: contradiction
reconsider m = y as Element of (INT.Group (card Gc)) by A8, FUNCT_2:def_1;
reconsider p = x as Element of (INT.Group (card Gc)) by A7, FUNCT_2:def_1;
A11: g |^ p = h . m by A4, A9
.= g |^ m by A4 ;
reconsider p = p, m = m as Element of NAT by ORDINAL1:def_12;
A12: p < card Gc by NAT_1:44;
A13: m < card Gc by NAT_1:44;
A14: ex k being Element of NAT st
( k <> 0 & k < card Gc & g |^ k = 1_ Gc )
proof
percases ( p < m or m < p ) by A10, XXREAL_0:1;
supposeA15: p < m ; ::_thesis: ex k being Element of NAT st
( k <> 0 & k < card Gc & g |^ k = 1_ Gc )
reconsider m1 = m, p1 = p as Integer ;
reconsider r1 = m1 - p1 as Element of NAT by A15, INT_1:5;
percases ( r1 > 0 or r1 = 0 ) ;
supposeA16: r1 > 0 ; ::_thesis: ex k being Element of NAT st
( k <> 0 & k < card Gc & g |^ k = 1_ Gc )
set z = 0 ;
A17: r1 < card Gc
proof
reconsider n1 = card Gc as Integer ;
 m1 + (- p1) < n1 + 0 by A13, XREAL_1:8;
hence  r1 < card Gc ; ::_thesis: verum
end;
 (g |^ m1) * (g |^ (- p1)) = g |^ (p1 + (- p1)) by A11, GROUP_1:33;
then  g |^ (m1 + (- p1)) = g |^ 0 by GROUP_1:33;
hence  ex k being Element of NAT st
( k <> 0 & k < card Gc & g |^ k = 1_ Gc ) by A16, A17, GROUP_1:25; ::_thesis: verum
end;
suppose r1 = 0 ; ::_thesis: ex k being Element of NAT st
( k <> 0 & k < card Gc & g |^ k = 1_ Gc )
hence  ex k being Element of NAT st
( k <> 0 & k < card Gc & g |^ k = 1_ Gc ) by A10; ::_thesis: verum
end;
end;
end;
supposeA18: m < p ; ::_thesis: ex k being Element of NAT st
( k <> 0 & k < card Gc & g |^ k = 1_ Gc )
reconsider m1 = m, p1 = p as Integer ;
reconsider r1 = p1 - m1 as Element of NAT by A18, INT_1:5;
percases ( r1 > 0 or r1 = 0 ) ;
supposeA19: r1 > 0 ; ::_thesis: ex k being Element of NAT st
( k <> 0 & k < card Gc & g |^ k = 1_ Gc )
set z = 0 ;
A20: r1 < card Gc
proof
reconsider n1 = card Gc as Integer ;
 p1 + (- m1) < n1 + 0 by A12, XREAL_1:8;
hence  r1 < card Gc ; ::_thesis: verum
end;
 (g |^ p1) * (g |^ (- m1)) = g |^ (m1 + (- m1)) by A11, GROUP_1:33;
then  g |^ (p1 + (- m1)) = g |^ 0 by GROUP_1:33;
hence  ex k being Element of NAT st
( k <> 0 & k < card Gc & g |^ k = 1_ Gc ) by A19, A20, GROUP_1:25; ::_thesis: verum
end;
suppose r1 = 0 ; ::_thesis: ex k being Element of NAT st
( k <> 0 & k < card Gc & g |^ k = 1_ Gc )
hence  ex k being Element of NAT st
( k <> 0 & k < card Gc & g |^ k = 1_ Gc ) by A10; ::_thesis: verum
end;
end;
end;
end;
end;
 ( not g is being_of_order_0 & ord g = card Gc ) by A3, GR_CY_1:6, GR_CY_1:7;
hence  contradiction by A14, GROUP_1:def_11; ::_thesis: verum
end;
A21: dom h = the carrier of (INT.Group (card Gc)) by FUNCT_2:def_1;
A22: the carrier of Gc c= rng h
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of Gc or x in rng h )
assume  x in the carrier of Gc ; ::_thesis: x in rng h
then reconsider z = x as Element of Gc ;
consider p being Nat such that
A23: z = g |^ p by A1;
set t = p mod (card Gc);
 p mod (card Gc) < card Gc by NAT_D:1;
then reconsider t9 = p mod (card Gc) as Element of (INT.Group (card Gc)) by NAT_1:44;
z = g |^ (((card Gc) * (p div (card Gc))) + (p mod (card Gc))) by A23, NAT_D:2
.= (g |^ ((card Gc) * (p div (card Gc)))) * (g |^ (p mod (card Gc))) by GROUP_1:33
.= ((g |^ (card Gc)) |^ (p div (card Gc))) * (g |^ (p mod (card Gc))) by GROUP_1:35
.= ((1_ Gc) |^ (p div (card Gc))) * (g |^ (p mod (card Gc))) by GR_CY_1:9
.= (1_ Gc) * (g |^ (p mod (card Gc))) by GROUP_1:31
.= g |^ (p mod (card Gc)) by GROUP_1:def_4 ;
then  ( t9 in dom h & x = h . t9 ) by A4, A21;
hence  x in rng h by FUNCT_1:def_3; ::_thesis: verum
end;
 rng h c= the carrier of Gc by RELAT_1:def_19;
then A24: rng h = the carrier of Gc by A22, XBOOLE_0:def_10;
reconsider h = h as Homomorphism of (INT.Group (card Gc)),Gc by A5, GROUP_6:def_6;
take  h ; ::_thesis: h is bijective
 h is onto by A24, FUNCT_2:def_3;
hence  h is bijective by A6, FUNCT_2:def_4; ::_thesis: verum
end;
hence  INT.Group (card Gc),Gc are_isomorphic by GROUP_6:def_11; ::_thesis: verum
end;

theorem :: GR_CY_2:16
for Gc being strict cyclic Group st Gc is infinite holds
INT.Group ,Gc are_isomorphic
proof
let Gc be strict cyclic Group; ::_thesis: ( Gc is infinite implies INT.Group ,Gc are_isomorphic )
consider g being Element of Gc such that
A1: for h being Element of Gc ex i being Integer st h = g |^ i by GR_CY_1:17;
assume A2: Gc is infinite ; ::_thesis: INT.Group ,Gc are_isomorphic
 ex h being Homomorphism of INT.Group,Gc st h is bijective
proof
deffunc H1( Element of INT.Group) ->  Element of the carrier of Gc = g |^ (@' $1);
consider h being Function of the carrier of INT.Group, the carrier of Gc such that
A3: for j1 being Element of INT.Group holds h . j1 = H1(j1) from FUNCT_2:sch_4();
A4: Gc = gr {g} by A1, Th5;
A5: h is one-to-one
proof
let x be set ; :: according to FUNCT_1:def_4 ::_thesis: for b1 being set holds
( not x in dom h or not b1 in dom h or not h . x = h . b1 or x = b1 )
let y be set ; ::_thesis: ( not x in dom h or not y in dom h or not h . x = h . y or x = y )
assume that
A6: x in dom h and
A7: y in dom h and
A8: h . x = h . y and
A9: x <> y ; ::_thesis: contradiction
reconsider y9 = y as Element of INT.Group by A7, FUNCT_2:def_1;
reconsider x9 = x as Element of INT.Group by A6, FUNCT_2:def_1;
g |^ (@' x9) = h . y9 by A3, A8
.= g |^ (@' y9) by A3 ;
hence  contradiction by A2, A4, A9, Th14; ::_thesis: verum
end;
A10: dom h = the carrier of INT.Group by FUNCT_2:def_1;
A11: the carrier of Gc c= rng h
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of Gc or x in rng h )
assume  x in the carrier of Gc ; ::_thesis: x in rng h
then reconsider z = x as Element of Gc ;
consider i being Integer such that
A12: z = g |^ i by A1;
reconsider i9 = i as Element of INT.Group by INT_1:def_2;
 i = @' i9 ;
then  x = h . i9 by A3, A12;
hence  x in rng h by A10, FUNCT_1:def_3; ::_thesis: verum
end;
 rng h c= the carrier of Gc by RELAT_1:def_19;
then A13: rng h = the carrier of Gc by A11, XBOOLE_0:def_10;
 for j, j1 being Element of INT.Group holds h . (j * j1) = (h . j) * (h . j1)
proof
let j, j1 be Element of INT.Group; ::_thesis: h . (j * j1) = (h . j) * (h . j1)
 @' (j * j1) = (@' j) + (@' j1) ;
then h . (j * j1) = g |^ ((@' j) + (@' j1)) by A3
.= (g |^ (@' j)) * (g |^ (@' j1)) by GROUP_1:33
.= (h . j) * (g |^ (@' j1)) by A3
.= (h . j) * (h . j1) by A3 ;
hence  h . (j * j1) = (h . j) * (h . j1) ; ::_thesis: verum
end;
then reconsider h = h as Homomorphism of INT.Group,Gc by GROUP_6:def_6;
take  h ; ::_thesis: h is bijective
 h is onto by A13, FUNCT_2:def_3;
hence  h is bijective by A5, FUNCT_2:def_4; ::_thesis: verum
end;
hence  INT.Group ,Gc are_isomorphic by GROUP_6:def_11; ::_thesis: verum
end;

theorem Th17: :: GR_CY_2:17
for Gc, Hc being finite strict cyclic Group st card Hc = card Gc holds
Hc,Gc are_isomorphic
proof
let Gc, Hc be finite strict cyclic Group; ::_thesis: ( card Hc = card Gc implies Hc,Gc are_isomorphic )
set p = card Hc;
assume  card Hc = card Gc ; ::_thesis: Hc,Gc are_isomorphic
then A1: INT.Group (card Hc),Gc are_isomorphic by Th15;
 INT.Group (card Hc),Hc are_isomorphic by Th15;
hence  Hc,Gc are_isomorphic by A1, GROUP_6:67; ::_thesis: verum
end;

theorem Th18: :: GR_CY_2:18
for p being Element of NAT
for F, G being finite strict Group st card F = p & card G = p & p is prime holds
F,G are_isomorphic
proof
let p be Element of NAT ; ::_thesis: for F, G being finite strict Group st card F = p & card G = p & p is prime holds
F,G are_isomorphic
let F, G be finite strict Group; ::_thesis: ( card F = p & card G = p & p is prime implies F,G are_isomorphic )
assume that
A1: ( card F = p & card G = p ) and
A2: p is prime ; ::_thesis: F,G are_isomorphic
 ( F is cyclic Group & G is cyclic Group ) by A1, A2, GR_CY_1:21;
hence  F,G are_isomorphic by A1, Th17; ::_thesis: verum
end;

theorem :: GR_CY_2:19
for F, G being finite strict Group st card F = 2 & card G = 2 holds
F,G are_isomorphic by Th18, INT_2:28;

theorem :: GR_CY_2:20
for G being finite strict Group st card G = 2 holds
for H being strict Subgroup of G holds
( H = (1). G or H = G ) by GR_CY_1:12, INT_2:28;

theorem :: GR_CY_2:21
for G being finite strict Group st card G = 2 holds
G is cyclic Group by GR_CY_1:21, INT_2:28;

theorem :: GR_CY_2:22
for n being Element of NAT
for G being finite strict Group st G is cyclic & card G = n holds
for p being Element of NAT st p divides n holds
ex G1 being strict Subgroup of G st
( card G1 = p & ( for G2 being strict Subgroup of G st card G2 = p holds
G2 = G1 ) )
proof
let n be Element of NAT ; ::_thesis: for G being finite strict Group st G is cyclic & card G = n holds
for p being Element of NAT st p divides n holds
ex G1 being strict Subgroup of G st
( card G1 = p & ( for G2 being strict Subgroup of G st card G2 = p holds
G2 = G1 ) )
let G be finite strict Group; ::_thesis: ( G is cyclic & card G = n implies for p being Element of NAT st p divides n holds
ex G1 being strict Subgroup of G st
( card G1 = p & ( for G2 being strict Subgroup of G st card G2 = p holds
G2 = G1 ) ) )
assume that
A1: G is cyclic and
A2: card G = n ; ::_thesis: for p being Element of NAT st p divides n holds
ex G1 being strict Subgroup of G st
( card G1 = p & ( for G2 being strict Subgroup of G st card G2 = p holds
G2 = G1 ) )
let p be Element of NAT ; ::_thesis: ( p divides n implies ex G1 being strict Subgroup of G st
( card G1 = p & ( for G2 being strict Subgroup of G st card G2 = p holds
G2 = G1 ) ) )
assume A3: p divides n ; ::_thesis: ex G1 being strict Subgroup of G st
( card G1 = p & ( for G2 being strict Subgroup of G st card G2 = p holds
G2 = G1 ) )
 ex G1 being strict Subgroup of G st
( card G1 = p & ( for G2 being strict Subgroup of G st card G2 = p holds
G2 = G1 ) )
proof
consider s being Nat such that
A4: n = p * s by A3, NAT_D:def_3;
consider a being Element of G such that
A5: G = gr {a} by A1, GR_CY_1:def_7;
take  gr {(a |^ s)} ; ::_thesis: ( card (gr {(a |^ s)}) = p & ( for G2 being strict Subgroup of G st card G2 = p holds
G2 = gr {(a |^ s)} ) )
A6: s in NAT by ORDINAL1:def_12;
then A7: ord (a |^ s) = p by A2, A5, A4, Th8;
then A8: card (gr {(a |^ s)}) = p by GR_CY_1:7;
 for G2 being strict Subgroup of G st card G2 = p holds
G2 = gr {(a |^ s)}
proof
let G2 be strict Subgroup of G; ::_thesis: ( card G2 = p implies G2 = gr {(a |^ s)} )
assume A9: card G2 = p ; ::_thesis: G2 = gr {(a |^ s)}
consider k being Element of NAT  such that
A10: G2 = gr {(a |^ k)} by A5, Th7;
 n divides k * p by A2, A5, A9, A10, Th11;
then consider m being Nat such that
A11: k * p = n * m by NAT_D:def_3;
 ex l being Nat st k = s * l
proof
take  m ; ::_thesis: k = s * m
reconsider p1 = p as Integer ;
A12: p <> 0 by A2, A4;
 ((1 / p1) * p1) * k = (1 / p1) * ((p1 * s) * m) by A4, A11, XCMPLX_1:4;
then  1 * k = ((p1 * (1 / p1)) * s) * m by A12, XCMPLX_1:106;
then  k = (1 * s) * m by A12, XCMPLX_1:106;
hence  k = s * m ; ::_thesis: verum
end;
then  s divides k by NAT_D:def_3;
hence  G2 = gr {(a |^ s)} by A6, A8, A9, A10, Th9, Th10; ::_thesis: verum
end;
hence  ( card (gr {(a |^ s)}) = p & ( for G2 being strict Subgroup of G st card G2 = p holds
G2 = gr {(a |^ s)} ) ) by A7, GR_CY_1:7; ::_thesis: verum
end;
hence  ex G1 being strict Subgroup of G st
( card G1 = p & ( for G2 being strict Subgroup of G st card G2 = p holds
G2 = G1 ) ) ; ::_thesis: verum
end;

theorem :: GR_CY_2:23
for Gc being cyclic Group
for g being Element of Gc st Gc = gr {g} holds
for G being Group
for f being Homomorphism of G,Gc st g in Image f holds
f is onto
proof
let Gc be cyclic Group; ::_thesis: for g being Element of Gc st Gc = gr {g} holds
for G being Group
for f being Homomorphism of G,Gc st g in Image f holds
f is onto
let g be Element of Gc; ::_thesis: ( Gc = gr {g} implies for G being Group
for f being Homomorphism of G,Gc st g in Image f holds
f is onto )
assume A1: Gc = gr {g} ; ::_thesis: for G being Group
for f being Homomorphism of G,Gc st g in Image f holds
f is onto
let G be Group; ::_thesis: for f being Homomorphism of G,Gc st g in Image f holds
f is onto
let f be Homomorphism of G,Gc; ::_thesis: ( g in Image f implies f is onto )
assume  g in Image f ; ::_thesis: f is onto
then  Image f = Gc by A1, Th13;
hence  f is onto by GROUP_6:57; ::_thesis: verum
end;

theorem Th24: :: GR_CY_2:24
for Gc being finite strict cyclic Group st ex k being Element of NAT st card Gc = 2 * k holds
ex g1 being Element of Gc st
( ord g1 = 2 & ( for g2 being Element of Gc st ord g2 = 2 holds
g1 = g2 ) )
proof
let Gc be finite strict cyclic Group; ::_thesis: ( ex k being Element of NAT st card Gc = 2 * k implies ex g1 being Element of Gc st
( ord g1 = 2 & ( for g2 being Element of Gc st ord g2 = 2 holds
g1 = g2 ) ) )
set n = card Gc;
given k being Element of NAT  such that A1: card Gc = 2 * k ; ::_thesis: ex g1 being Element of Gc st
( ord g1 = 2 & ( for g2 being Element of Gc st ord g2 = 2 holds
g1 = g2 ) )
consider g being Element of Gc such that
A2: Gc = gr {g} by GR_CY_1:def_7;
A3: ord g = card Gc by A2, GR_CY_1:7;
take  g |^ k ; ::_thesis: ( ord (g |^ k) = 2 & ( for g2 being Element of Gc st ord g2 = 2 holds
g |^ k = g2 ) )
A4: (g |^ k) |^ 2 = g |^ (card Gc) by A1, GROUP_1:35
.= 1_ Gc by GR_CY_1:9 ;
A5: k <> 0 by A1;
A6: for p being Nat st (g |^ k) |^ p = 1_ Gc & p <> 0 holds
2 <= p
proof
let p be Nat; ::_thesis: ( (g |^ k) |^ p = 1_ Gc & p <> 0 implies 2 <= p )
assume that
A7: (g |^ k) |^ p = 1_ Gc and
A8: ( p <> 0 & 2 > p ) ; ::_thesis: contradiction
A9: ( not g is being_of_order_0 & 1_ Gc = g |^ (k * p) ) by A7, GROUP_1:35, GR_CY_1:6;
 ( card Gc > k * p & k * p <> 0 ) by A1, A5, A8, XCMPLX_1:6, XREAL_1:68;
hence  contradiction by A3, A9, GROUP_1:def_11; ::_thesis: verum
end;
 not g |^ k is being_of_order_0 by GR_CY_1:6;
hence  ord (g |^ k) = 2 by A4, A6, GROUP_1:def_11; ::_thesis: for g2 being Element of Gc st ord g2 = 2 holds
g |^ k = g2
let g2 be Element of Gc; ::_thesis: ( ord g2 = 2 implies g |^ k = g2 )
consider k1 being Element of NAT  such that
A10: g2 = g |^ k1 by A2, Th6;
assume that
A11: ord g2 = 2 and
A12: g |^ k <> g2 ; ::_thesis: contradiction
now__::_thesis:_contradiction
A13: not g is being_of_order_0 by GR_CY_1:6;
consider t, t1 being Nat such that
A14: k1 = (k * t) + t1 and
A15: t1 < k by A5, NAT_1:17;
A16: 2 * t1 < card Gc by A1, A15, XREAL_1:68;
 t1 <> 0
proof
assume  t1 = 0 ; ::_thesis: contradiction
then A17: g |^ k1 = g |^ (k * ((2 * (t div 2)) + (t mod 2))) by A14, NAT_D:2
.= g |^ (((k * 2) * (t div 2)) + (k * (t mod 2)))
.= (g |^ ((k * 2) * (t div 2))) * (g |^ (k * (t mod 2))) by GROUP_1:33
.= ((g |^ (k * 2)) |^ (t div 2)) * (g |^ (k * (t mod 2))) by GROUP_1:35
.= ((1_ Gc) |^ (t div 2)) * (g |^ (k * (t mod 2))) by A4, GROUP_1:35
.= (1_ Gc) * (g |^ (k * (t mod 2))) by GROUP_1:31
.= g |^ (k * (t mod 2)) by GROUP_1:def_4 ;
percases ( t mod 2 = 0 or t mod 2 = 1 ) by NAT_D:12;
suppose t mod 2 = 0 ; ::_thesis: contradiction
then  g |^ k1 = 1_ Gc by A17, GROUP_1:25;
hence  contradiction by A11, A10, GROUP_1:42; ::_thesis: verum
end;
suppose t mod 2 = 1 ; ::_thesis: contradiction
hence  contradiction by A12, A10, A17; ::_thesis: verum
end;
end;
end;
then A18: 2 * t1 <> 0 ;
1_ Gc = (g |^ k1) |^ 2 by A11, A10, GROUP_1:41
.= g |^ (((k * t) + t1) * 2) by A14, GROUP_1:35
.= g |^ (((card Gc) * t) + (t1 * 2)) by A1
.= (g |^ ((card Gc) * t)) * (g |^ (t1 * 2)) by GROUP_1:33
.= ((g |^ (ord g)) |^ t) * (g |^ (t1 * 2)) by A3, GROUP_1:35
.= ((1_ Gc) |^ t) * (g |^ (t1 * 2)) by GROUP_1:41
.= (1_ Gc) * (g |^ (t1 * 2)) by GROUP_1:31
.= g |^ (2 * t1) by GROUP_1:def_4 ;
hence  contradiction by A3, A18, A16, A13, GROUP_1:def_11; ::_thesis: verum
end;
hence  contradiction ; ::_thesis: verum
end;

registration
let G be Group;
cluster center G ->  normal ;
coherence
 center G is normal by GROUP_5:78;
end;

theorem :: GR_CY_2:25
for Gc being finite strict cyclic Group st ex k being Element of NAT st card Gc = 2 * k holds
ex H being Subgroup of Gc st
( card H = 2 & H is cyclic Group )
proof
let Gc be finite strict cyclic Group; ::_thesis: ( ex k being Element of NAT st card Gc = 2 * k implies ex H being Subgroup of Gc st
( card H = 2 & H is cyclic Group ) )
set n = card Gc;
assume  ex k being Element of NAT st card Gc = 2 * k ; ::_thesis: ex H being Subgroup of Gc st
( card H = 2 & H is cyclic Group )
then consider g1 being Element of Gc such that
A1: ord g1 = 2 and
 for g2 being Element of Gc st ord g2 = 2 holds
g1 = g2 by Th24;
take  gr {g1} ; ::_thesis: ( card (gr {g1}) = 2 & gr {g1} is cyclic Group )
thus  ( card (gr {g1}) = 2 & gr {g1} is cyclic Group ) by A1, Th4, GR_CY_1:7; ::_thesis: verum
end;

theorem Th26: :: GR_CY_2:26
for F being Group
for G being strict Group
for g being Homomorphism of G,F st G is cyclic holds
Image g is cyclic
proof
let F be Group; ::_thesis: for G being strict Group
for g being Homomorphism of G,F st G is cyclic holds
Image g is cyclic
let G be strict Group; ::_thesis: for g being Homomorphism of G,F st G is cyclic holds
Image g is cyclic
let g be Homomorphism of G,F; ::_thesis: ( G is cyclic implies Image g is cyclic )
assume  G is cyclic ; ::_thesis: Image g is cyclic
then consider a being Element of G such that
A1: G = gr {a} by GR_CY_1:def_7;
 ex f1 being Element of (Image g) st Image g = gr {f1}
proof
 g . a in Image g by GROUP_6:45;
then reconsider f = g . a as Element of (Image g) by STRUCT_0:def_5;
take  f ; ::_thesis: Image g = gr {f}
 for d being Element of (Image g) ex i being Integer st d = f |^ i
proof
let d be Element of (Image g); ::_thesis: ex i being Integer st d = f |^ i
 d in Image g by STRUCT_0:def_5;
then consider b being Element of G such that
A2: d = g . b by GROUP_6:45;
 b in gr {a} by A1, STRUCT_0:def_5;
then consider i being Integer such that
A3: b = a |^ i by GR_CY_1:5;
take  i ; ::_thesis: d = f |^ i
d = (g . a) |^ i by A2, A3, GROUP_6:37
.= f |^ i by GROUP_4:2 ;
hence  d = f |^ i ; ::_thesis: verum
end;
hence  Image g = gr {f} by Th5; ::_thesis: verum
end;
hence  Image g is cyclic by GR_CY_1:def_7; ::_thesis: verum
end;

theorem :: GR_CY_2:27
for G, F being strict Group st G,F are_isomorphic & G is cyclic holds
F is cyclic
proof
let G, F be strict Group; ::_thesis: ( G,F are_isomorphic & G is cyclic implies F is cyclic )
assume that
A1: G,F are_isomorphic and
A2: G is cyclic ; ::_thesis: F is cyclic
consider h being Homomorphism of G,F such that
A3: h is bijective by A1, GROUP_6:def_11;
 h is onto by A3, FUNCT_2:def_4;
then  Image h = F by GROUP_6:57;
hence  F is cyclic by A2, Th26; ::_thesis: verum
end;