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

ex h being Homomorphism of (INT.Group (card Gc)),Gc st h is bijective

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

then A3:
Gc = gr {g}
by Th5;
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;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

ex h being Homomorphism of (INT.Group (card Gc)),Gc st h is bijective

proof

hence
INT.Group (card Gc),Gc are_isomorphic
by GROUP_6:def 11; :: thesis: verum
deffunc H_{1}( 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 = H_{1}(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)

A22: the carrier of Gc c= rng h

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;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 = H

A5: for j, j1 being Element of (INT.Group (card Gc)) holds h . (j * j1) = (h . j) * (h . j1)

proof

A6:
h is one-to-one
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;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

proof

A21:
dom h = the carrier of (INT.Group (card Gc))
by FUNCT_2:def 1;
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 )

hence contradiction by A14, GROUP_1:def 11; :: thesis: verum

end;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
end;

( not g is being_of_order_0 & ord g = card Gc )
by A3, GR_CY_1:6, GR_CY_1:7;per cases
( p < m or m < p )
by A10, XXREAL_0:1;

end;

suppose A15:
p < m
; :: thesis: ex k being Element of NAT st

( k <> 0 & k < card Gc & g |^ k = 1_ Gc )

( 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;

end;reconsider r1 = m1 - p1 as Element of NAT by A15, INT_1:5;

per cases
( r1 > 0 or r1 = 0 )
;

end;

suppose A16:
r1 > 0
; :: thesis: ex k being Element of NAT st

( k <> 0 & k < card Gc & g |^ k = 1_ Gc )

( k <> 0 & k < card Gc & g |^ k = 1_ Gc )

set z = 0 ;

A17: r1 < card Gc

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;A17: r1 < card Gc

proof

(g |^ m1) * (g |^ (- p1)) = g |^ (p1 + (- p1))
by A11, GROUP_1:33;
reconsider n1 = card Gc as Integer ;

m1 + (- p1) < n1 + 0 by A13, XREAL_1:8;

hence r1 < card Gc ; :: thesis: verum

end;m1 + (- p1) < n1 + 0 by A13, XREAL_1:8;

hence r1 < card Gc ; :: thesis: verum

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

suppose A18:
m < p
; :: thesis: ex k being Element of NAT st

( k <> 0 & k < card Gc & g |^ k = 1_ Gc )

( 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;

end;reconsider r1 = p1 - m1 as Element of NAT by A18, INT_1:5;

per cases
( r1 > 0 or r1 = 0 )
;

end;

suppose A19:
r1 > 0
; :: thesis: ex k being Element of NAT st

( k <> 0 & k < card Gc & g |^ k = 1_ Gc )

( k <> 0 & k < card Gc & g |^ k = 1_ Gc )

set z = 0 ;

A20: r1 < card Gc

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;A20: r1 < card Gc

proof

(g |^ p1) * (g |^ (- m1)) = g |^ (m1 + (- m1))
by A11, GROUP_1:33;
reconsider n1 = card Gc as Integer ;

p1 + (- m1) < n1 + 0 by A12, XREAL_1:8;

hence r1 < card Gc ; :: thesis: verum

end;p1 + (- m1) < n1 + 0 by A12, XREAL_1:8;

hence r1 < card Gc ; :: thesis: verum

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

hence contradiction by A14, GROUP_1:def 11; :: thesis: verum

A22: the carrier of Gc c= rng h

proof

rng h c= the carrier of Gc
by RELAT_1:def 19;
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;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

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