let Gc be finite strict cyclic Group; :: thesis: INT.Group (card Gc),Gc are_isomorphic
set n = card Gc;
A1: card Gc > 0 by GROUP_1:90;
consider g being Element of Gc such that
A2: for h being Element of Gc ex p being Nat st h = g |^ p by GR_CY_1:42;
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
A3: h = g |^ p by A2;
reconsider p1 = p as Integer ;
take p1 ; :: thesis: h = g |^ p1
thus h = g |^ p1 by A3; :: thesis: verum
end;
then A4: Gc = gr {g} by Th11;
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
A5: for p being Element of (INT.Group (card Gc)) holds h . p = H1(p) from FUNCT_2:sch 4();
 A6: INT.Group (card Gc) = multMagma(# (Segm (card Gc)),(addint (card Gc)) #) by A1, GR_CY_1:def 6;
A7: 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) by A6;
A8: @ j1 = j1 by A1, Def1;
@ (j * j1) = (addint (card Gc)) . (j9,j19) by A6, Def1
.= (j9 + j19) mod (card Gc) by A1, GR_CY_1:def 5
.= ((@ j) + (@ j1)) mod (card Gc) by A1, A8, Def1
.= ((@ j) + (@ j1)) - ((card Gc) * (((@ j) + (@ j1)) div (card Gc))) by A1, NEWTON:77 ;
then h . (j * j1) = g |^ (((@ j) + (@ j1)) + (- ((card Gc) * (((@ j) + (@ j1)) div (card Gc))))) by A5
.= (g |^ ((@ j) + (@ j1))) * (g |^ (- ((card Gc) * (((@ j) + (@ j1)) div (card Gc))))) by GROUP_1:63
.= (g |^ ((@ j) + (@ j1))) * ((g |^ ((card Gc) * (((@ j) + (@ j1)) div (card Gc)))) ") by GROUP_1:70
.= (g |^ ((@ j) + (@ j1))) * (((g |^ (card Gc)) |^ (((@ j) + (@ j1)) div (card Gc))) ") by GROUP_1:67
.= (g |^ ((@ j) + (@ j1))) * (((1_ Gc) |^ (((@ j) + (@ j1)) div (card Gc))) ") by GR_CY_1:29
.= (g |^ ((@ j) + (@ j1))) * ((1_ Gc) ") by GROUP_1:61
.= (g |^ ((@ j) + (@ j1))) * (1_ Gc) by GROUP_1:16
.= g |^ ((@ j) + (@ j1)) by GROUP_1:def 5
.= (g |^ (@ j)) * (g |^ (@ j1)) by GROUP_1:63
.= (h . j) * (g |^ (@ j1)) by A5
.= (h . j) * (h . j1) by A5 ;
hence h . (j * j1) = (h . j) * (h . j1) ; :: thesis: verum
end;
A9: h is one-to-one
proof
let x be set ; :: according to FUNCT_1:def 8 :: thesis: for b1 being set holds
( not x in proj1 h or not b1 in proj1 h or not h . x = h . b1 or x = b1 )
let y be set ; :: thesis: ( not x in proj1 h or not y in proj1 h or not h . x = h . y or x = y )
assume that
A10: x in dom h and
A11: y in dom h and
A12: h . x = h . y and
A13: x <> y ; :: thesis: contradiction
reconsider y9 = y as Element of (INT.Group (card Gc)) by A11, FUNCT_2:def 1;
reconsider x9 = x as Element of (INT.Group (card Gc)) by A10, FUNCT_2:def 1;
A14: g |^ (@ x9) = h . y9 by A5, A12
.= g |^ (@ y9) by A5 ;
ex p, m being Element of NAT st
( p <> m & g |^ p = g |^ m & p < card Gc & m < card Gc )
proof
set p = @ x9;
set m = @ y9;
A15: @ y9 = y9 by A1, Def1;
then A16: @ y9 < card Gc by A6, NAT_1:45;
A17: @ x9 = x9 by A1, Def1;
then @ x9 < card Gc by A6, NAT_1:45;
hence ex p, m being Element of NAT st
( p <> m & g |^ p = g |^ m & p < card Gc & m < card Gc ) by A13, A14, A17, A15, A16; :: thesis: verum
end;
then consider p, m being Element of NAT such that
A18: p <> m and
A19: g |^ p = g |^ m and
A20: p < card Gc and
A21: m < card Gc ;
A22: ex k being Element of NAT st
( k <> 0 & k < card Gc & g |^ k = 1_ Gc )
proof
now
per cases ( p < m or m < p or m = p ) by XXREAL_0:1;
case A23: 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 A23, INT_1:18;
now
per cases ( r1 > 0 or r1 = 0 ) ;
suppose A24: r1 > 0 ; :: thesis: ex k being Element of NAT st
( k <> 0 & k < card Gc & g |^ k = 1_ Gc )
set zero = 0 ;
A25: r1 < card Gc
proof
reconsider n1 = card Gc as Integer ;
m1 + (- p1) < n1 + 0 by A21, XREAL_1:10;
hence r1 < card Gc ; :: thesis: verum
end;
(g |^ m1) * (g |^ (- p1)) = g |^ (p1 + (- p1)) by A19, GROUP_1:63;
then g |^ (m1 + (- p1)) = g |^ 0 by GROUP_1:63;
hence ex k being Element of NAT st
( k <> 0 & k < card Gc & g |^ k = 1_ Gc ) by A24, A25, GROUP_1:43; :: 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 A18; :: thesis: verum
end;
end;
end;
hence ex k being Element of NAT st
( k <> 0 & k < card Gc & g |^ k = 1_ Gc ) ; :: thesis: verum
end;
case A26: m < p ; :: thesis: verum
reconsider m1 = m, p1 = p as Integer ;
reconsider r1 = p1 - m1 as Element of NAT by A26, INT_1:18;
per cases ( r1 > 0 or r1 = 0 ) ;
suppose A27: r1 > 0 ; :: thesis: ex k being Element of NAT st
( k <> 0 & k < card Gc & g |^ k = 1_ Gc )
set zero = 0 ;
A28: r1 < card Gc
proof
reconsider n1 = card Gc as Integer ;
p1 + (- m1) < n1 + 0 by A20, XREAL_1:10;
hence r1 < card Gc ; :: thesis: verum
end;
(g |^ p1) * (g |^ (- m1)) = g |^ (m1 + (- m1)) by A19, GROUP_1:63;
then g |^ (p1 + (- m1)) = g |^ 0 by GROUP_1:63;
hence ex k being Element of NAT st
( k <> 0 & k < card Gc & g |^ k = 1_ Gc ) by A27, A28, GROUP_1:43; :: 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 A18; :: thesis: verum
end;
end;
end;
end;
end;
hence ex k being Element of NAT st
( k <> 0 & k < card Gc & g |^ k = 1_ Gc ) ; :: thesis: verum
end;
( not g is being_of_order_0 & ord g = card Gc ) by A4, GR_CY_1:26, GR_CY_1:27;
hence contradiction by A22, GROUP_1:def 12; :: thesis: verum
end;
A29: dom h = the carrier of (INT.Group (card Gc)) by FUNCT_2:def 1;
A30: 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
A31: z = g |^ p by A2;
ex t being set st
( t in dom h & x = h . t )
proof
set t = p mod (card Gc);
p mod (card Gc) < card Gc by A1, NAT_D:1;
then reconsider t9 = p mod (card Gc) as Element of (INT.Group (card Gc)) by A6, NAT_1:45;
take t9 ; :: thesis: ( t9 in dom h & x = h . t9 )
A32: @ t9 = p mod (card Gc) by A1, Def1;
z = g |^ (((card Gc) * (p div (card Gc))) + (p mod (card Gc))) by A1, A31, NAT_D:2
.= (g |^ ((card Gc) * (p div (card Gc)))) * (g |^ (p mod (card Gc))) by GROUP_1:63
.= ((g |^ (card Gc)) |^ (p div (card Gc))) * (g |^ (p mod (card Gc))) by GROUP_1:67
.= ((1_ Gc) |^ (p div (card Gc))) * (g |^ (p mod (card Gc))) by GR_CY_1:29
.= (1_ Gc) * (g |^ (p mod (card Gc))) by GROUP_1:61
.= g |^ (p mod (card Gc)) by GROUP_1:def 5 ;
hence ( t9 in dom h & x = h . t9 ) by A5, A29, A32; :: thesis: verum
end;
hence x in rng h by FUNCT_1:def 5; :: thesis: verum
end;
rng h c= the carrier of Gc by RELAT_1:def 19;
then A33: rng h = the carrier of Gc by A30, XBOOLE_0:def 10;
reconsider h = h as Homomorphism of (INT.Group (card Gc)),Gc by A7, GROUP_6:def 7;
take h ; :: thesis: h is bijective
h is onto by A33, FUNCT_2:def 3;
hence h is bijective by A9, FUNCT_2:def 4; :: thesis: verum
end;
hence INT.Group (card Gc),Gc are_isomorphic by GROUP_6:def 15; :: thesis: verum