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, y be object ; :: according to FUNCT_1:def 4 :: 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
per cases ( p < m or m < p ) by A10, XXREAL_0:1;
suppose A15: 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;
per cases ( r1 > 0 or r1 = 0 ) ;
suppose A16: 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;
suppose A18: 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;
per cases ( r1 > 0 or r1 = 0 ) ;
suppose A19: 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 object ; :: 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