gr_cy_2.miz

    begin

    reserve F,G for Group;

    reserve G1 for Subgroup of G;

    reserve Gc for cyclic Group;

    reserve H for Subgroup of Gc;

    reserve f for Homomorphism of G, Gc;

    reserve a,b for Element of G;

    reserve g for Element of Gc;

    reserve a1 for Element of G1;

    reserve k,m,n,p,s for Element of NAT ;

    reserve i0,i,i1,i2 for Integer;

    reserve j,j1 for Element of INT.Group ;

    reserve x,y,t for set;

    theorem :: GR_CY_2:1

    ( ord a) > 1 & a = (b |^ k) implies k <> 0

    proof

      assume that

       A1: ( ord a) > 1 and

       A2: a = (b |^ k) & k = 0 ;

      a = ( 1_ G) by A2, GROUP_1: 25;

      hence contradiction by A1, GROUP_1: 42;

    end;

    theorem :: GR_CY_2:2



     Th2: a in ( gr {a})

    proof

      ex i st a = (a |^ i)

      proof

        reconsider i = 1 as Integer;

        take i;

        thus thesis by GROUP_1: 26;

      end;

      hence thesis by GR_CY_1: 5;

    end;

    theorem :: GR_CY_2:3



     Th3: a = a1 implies ( gr {a}) = ( gr {a1})

    proof

      reconsider Gr = ( gr {a1}) as Subgroup of G by GROUP_2: 56;

      assume

       A1: a = a1;



       A2: for b holds b in Gr implies b in ( gr {a})

      proof

        let b;

        assume

         A3: b in Gr;

        then b in G1 by GROUP_2: 40;

        then

        reconsider b1 = b as Element of G1 by STRUCT_0:def 5;

        consider i such that

         A4: b1 = (a1 |^ i) by A3, GR_CY_1: 5;

        b = (a |^ i) by A1, A4, GROUP_4: 2;

        hence thesis by GR_CY_1: 5;

      end;

      for b holds b in ( gr {a}) implies b in Gr

      proof

        let b;

        assume b in ( gr {a});

        then

        consider i such that

         A5: b = (a |^ i) by GR_CY_1: 5;

        b = (a1 |^ i) by A1, A5, GROUP_4: 2;

        hence thesis by GR_CY_1: 5;

      end;

      hence thesis by A2, GROUP_2: 60;

    end;

    theorem :: GR_CY_2:4



     Th4: ( gr {a}) is cyclic Group

    proof

      ex a1 be 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;

        thus thesis by Th3;

      end;

      hence thesis by GR_CY_1:def 7;

    end;

    theorem :: GR_CY_2:5



     Th5: for G be strict Group, b be Element of G holds (for a be Element of G holds ex i st a = (b |^ i)) iff G = ( gr {b})

    proof

      let G be strict Group;

      let b be Element of G;

      thus (for a be Element of G holds ex i st a = (b |^ i)) implies G = ( gr {b})

      proof

        assume

         A1: for a be Element of G holds ex i st a = (b |^ i);

        for a be Element of G holds a in ( gr {b})

        proof

          let a be Element of G;

          ex i st a = (b |^ i) by A1;

          hence thesis by GR_CY_1: 5;

        end;

        hence thesis by GROUP_2: 62;

      end;

      assume

       A2: G = ( gr {b});

      let a be Element of G;

      a in ( gr {b}) by A2, STRUCT_0:def 5;

      hence thesis by GR_CY_1: 5;

    end;

    theorem :: GR_CY_2:6



     Th6: for G be strict finite Group, b be Element of G holds (for a be Element of G holds ex p st a = (b |^ p)) iff G = ( gr {b})

    proof

      let G be strict finite Group, b be Element of G;

      reconsider n1 = ( card G) as Integer;

      thus (for a be Element of G holds ex p st a = (b |^ p)) implies G = ( gr {b})

      proof

        assume

         A1: for a be Element of G holds ex p st a = (b |^ p);

        for a be Element of G holds ex i st a = (b |^ i)

        proof

          let a be Element of G;

          consider p such that

           A2: a = (b |^ p) by A1;

          reconsider p1 = p as Integer;

          take p1;

          thus thesis by A2;

        end;

        hence thesis by Th5;

      end;

      assume

       A3: G = ( gr {b});

      let a be Element of G;

      consider i 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;

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

    end;

    theorem :: GR_CY_2:7



     Th7: for G be strict Group, a be Element of G holds G is finite & G = ( gr {a}) implies for G1 be strict Subgroup of G holds ex p st G1 = ( gr {(a |^ p)})

    proof

      let G be strict Group, a be Element of G;

      assume that

       A1: G is finite and

       A2: G = ( gr {a});

      let G1 be strict Subgroup of G;

      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 be 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 such that

       A4: b1 = (a |^ p) by A1, A2, Th6;

      take p;

      thus thesis by A3, A4, Th3;

    end;

    theorem :: GR_CY_2:8



     Th8: for G be finite Group, a be Element of G holds G = ( gr {a}) & ( card G) = n & n = (p * s) implies ( ord (a |^ p)) = s

    proof

      let G be finite Group, a be Element of G;

      assume that

       A1: G = ( gr {a}) and

       A2: ( card G) = n and

       A3: n = (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 be Nat st ((a |^ p) |^ k) = ( 1_ G) & k <> 0 holds s <= k

      proof

        let k be Nat;

        assume that

         A7: ((a |^ p) |^ k) = ( 1_ G) and

         A8: k <> 0 & s > k;



         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;

      end;

      ((a |^ p) |^ s) = (a |^ n) by A3, GROUP_1: 35

      .= ( 1_ G) by A2, GR_CY_1: 9;

      hence thesis by A4, A6, GROUP_1:def 11;

    end;

    theorem :: GR_CY_2:9



     Th9: s divides k implies (a |^ k) in ( gr {(a |^ s)})

    proof

      assume s divides k;

      then

      consider p be Nat such that

       A1: k = (s * p) by NAT_D:def 3;

      ex i st (a |^ k) = ((a |^ s) |^ i)

      proof

        reconsider p9 = p as Integer;

        take p9;

        thus thesis by A1, GROUP_1: 35;

      end;

      hence thesis by GR_CY_1: 5;

    end;

    theorem :: GR_CY_2:10



     Th10: for G be finite Group, a be Element of G holds ( card ( gr {(a |^ s)})) = ( card ( gr {(a |^ k)})) & (a |^ k) in ( gr {(a |^ s)}) implies ( gr {(a |^ s)}) = ( gr {(a |^ k)})

    proof

      let G be finite Group, a be Element of G;

      assume

       A1: ( card ( gr {(a |^ s)})) = ( card ( gr {(a |^ k)}));

      assume (a |^ k) in ( gr {(a |^ s)});

      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;

    end;

    theorem :: GR_CY_2:11



     Th11: for G be finite Group, G1 be Subgroup of G, a be Element of G holds ( card G) = n & G = ( gr {a}) & ( card G1) = p & G1 = ( gr {(a |^ k)}) implies n divides (k * p)

    proof

      let G be finite Group, G1 be Subgroup of G, a be Element of G;

      assume that

       A1: ( card G) = n and

       A2: G = ( gr {a}) and

       A3: ( card G1) = p and

       A4: G1 = ( gr {(a |^ k)});

      set z = (k * p);

      consider m,l be Nat such that

       A5: z = ((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 ;

        (a |^ z) = ((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;

      end;

      hence thesis by A5, NAT_D:def 3;

    end;

    theorem :: GR_CY_2:12

    for G be strict finite Group, a be Element of G holds G = ( gr {a}) & ( card G) = n implies (G = ( gr {(a |^ k)}) iff (k gcd n) = 1)

    proof

      let G be strict finite Group, a be Element of G;

      assume that

       A1: G = ( gr {a}) and

       A2: ( card G) = n;



       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;

        d divides n by NAT_D:def 5;

        then

        consider p be Nat such that

         A6: n = (d * p) by NAT_D:def 3;



         A7: p <> 0 by A2, A6;



         A8: p <> n

        proof

          assume p = n;

          then (d * p) = (p * 1) by A6;

          hence contradiction by A5, A2, A6, XCMPLX_1: 5;

        end;

        d divides k by NAT_D:def 5;

        then

        consider l be Nat such that

         A9: k = (d * 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 * d) * 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;

      end;

      (k gcd n) = 1 implies G = ( gr {(a |^ k)})

      proof

        assume (k gcd n) = 1;

        then

        consider i, i1 such that

         A12: ((i * k) + (i1 * n)) = 1 by NEWTON: 67;

        for b be Element of G holds b in ( gr {(a |^ k)})

        proof

          let b be Element of G;

          b in G by STRUCT_0:def 5;

          then

          consider i0 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 st b = ((a |^ k) |^ i2)

          proof

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

          end;

          hence thesis by GR_CY_1: 5;

        end;

        hence thesis by GROUP_2: 62;

      end;

      hence thesis by A3;

    end;

    theorem :: GR_CY_2:13



     Th13: Gc = ( gr {g}) & g in H implies the multMagma of Gc = the multMagma of H

    proof

      assume that

       A1: Gc = ( gr {g}) and

       A2: g in 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 thesis by A1, GROUP_2: 55;

    end;

    theorem :: GR_CY_2:14



     Th14: Gc = ( gr {g}) implies (Gc is finite iff ex i, i1 st i <> i1 & (g |^ i) = (g |^ i1))

    proof

      assume

       A1: Gc = ( gr {g});



       A2: (ex i, i1 st i <> i1 & (g |^ i) = (g |^ i1)) implies Gc is finite

      proof

        given i, i1 such that

         A3: i <> i1 and

         A4: (g |^ i) = (g |^ i1);

        now

          per cases by A3, XXREAL_0: 1;

            suppose

             A5: i < i1;

            set r = (i1 - i);

            i1 > (i + 0 ) by A5;

            then

             A6: (i1 - i) > 0 by XREAL_1: 20;

            then

            reconsider m = r 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 holds ex n st (g |^ i2) = (g |^ n) & n >= 0 & n < (i1 - i)

            proof

              let i2;

              reconsider m = (i2 mod r) as Element of NAT by A6, INT_1: 3, NEWTON: 64;

              take m;

              (g |^ i2) = (g |^ (((i2 div r) * r) + (i2 mod r))) by A6, NEWTON: 66

              .= ((g |^ (r * (i2 div r))) * (g |^ (i2 mod r))) by GROUP_1: 33

              .= ((( 1_ Gc) |^ (i2 div r)) * (g |^ (i2 mod r))) by A7, GROUP_1: 35

              .= (( 1_ Gc) * (g |^ (i2 mod r))) by GROUP_1: 31

              .= (g |^ (i2 mod r)) by GROUP_1:def 4;

              hence thesis by A6, NEWTON: 65;

            end;

            ex F be FinSequence st ( rng F) = the carrier of Gc

            proof

              deffunc F( Nat) = (g |^ $1);

              consider F be FinSequence such that

               A9: ( len F) = m and

               A10: for p be Nat holds p in ( dom F) implies (F . p) = F(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 object;

                assume y in the carrier of Gc;

                then

                reconsider a = y as Element of Gc;

                a in Gc by STRUCT_0:def 5;

                then

                 A13: ex i2 st a = (g |^ i2) by A1, GR_CY_1: 5;

                ex n st n in ( dom F) & (F . n) = a

                proof

                  consider n such that

                   A14: a = (g |^ n) and n >= 0 and

                   A15: n < (i1 - i) by A8, A13;

                  per cases ;

                    suppose

                     A16: n = 0 ;



                     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 thesis by A19;

                  end;

                    suppose n > 0 ;

                    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 thesis by A21;

                  end;

                end;

                hence thesis by FUNCT_1:def 3;

              end;

              take F;



               A22: for y st y in ( rng F) holds ex n st y = (g |^ n)

              proof

                let y;

                assume y in ( rng F);

                then

                consider x be object 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;

                thus thesis by A10, A23, A24;

              end;

              ( rng F) c= the carrier of Gc

              proof

                let y be object;

                assume y in ( rng F);

                then ex n st y = (g |^ n) by A22;

                hence thesis;

              end;

              hence thesis by A12, XBOOLE_0:def 10;

            end;

            hence thesis;

          end;

            suppose

             A25: i1 < i;

            set r = (i - i1);

            i > (i1 + 0 ) by A25;

            then

             A26: (i - i1) > 0 by XREAL_1: 20;

            then

            reconsider m = r 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 holds ex n st (g |^ i2) = (g |^ n) & n >= 0 & n < (i - i1)

            proof

              let i2;

              reconsider m = (i2 mod r) as Element of NAT by A26, INT_1: 3, NEWTON: 64;

              take m;

              (g |^ i2) = (g |^ (((i2 div r) * r) + (i2 mod r))) by A26, NEWTON: 66

              .= ((g |^ (r * (i2 div r))) * (g |^ (i2 mod r))) by GROUP_1: 33

              .= ((( 1_ Gc) |^ (i2 div r)) * (g |^ (i2 mod r))) by A27, GROUP_1: 35

              .= (( 1_ Gc) * (g |^ (i2 mod r))) by GROUP_1: 31

              .= (g |^ (i2 mod r)) by GROUP_1:def 4;

              hence thesis by A26, NEWTON: 65;

            end;

            ex F be FinSequence st ( rng F) = the carrier of Gc

            proof

              deffunc F( Nat) = (g |^ $1);

              consider F be FinSequence such that

               A29: ( len F) = m and

               A30: for p be Nat holds p in ( dom F) implies (F . p) = F(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 object;

                assume y in the carrier of Gc;

                then

                reconsider a = y as Element of Gc;

                a in Gc by STRUCT_0:def 5;

                then

                 A33: ex i2 st a = (g |^ i2) by A1, GR_CY_1: 5;

                ex n st n in ( dom F) & (F . n) = a

                proof

                  consider n such that

                   A34: a = (g |^ n) and n >= 0 and

                   A35: n < (i - i1) by A28, A33;

                  per cases ;

                    suppose

                     A36: n = 0 ;



                     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 thesis by A39;

                  end;

                    suppose n > 0 ;

                    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 thesis by A41;

                  end;

                end;

                hence thesis by FUNCT_1:def 3;

              end;

              take F;



               A42: for y st y in ( rng F) holds ex n st y = (g |^ n)

              proof

                let y;

                assume y in ( rng F);

                then

                consider x be object 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;

                thus thesis by A30, A43, A44;

              end;

              ( rng F) c= the carrier of Gc

              proof

                let y be object;

                assume y in ( rng F);

                then ex n st y = (g |^ n) by A42;

                hence thesis;

              end;

              hence thesis by A32, XBOOLE_0:def 10;

            end;

            hence thesis;

          end;

        end;

        hence thesis;

      end;

      Gc is finite implies ex i, i1 st i <> i1 & (g |^ i) = (g |^ i1)

      proof

        assume Gc is finite;

        then

        reconsider 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 thesis by A45;

      end;

      hence thesis by A2;

    end;

    registration

      let n be non zero Nat;

      cluster -> natural for Element of ( INT.Group n);

      coherence ;

    end

    theorem :: GR_CY_2:15



     Th15: for Gc be strict finite cyclic Group holds (( INT.Group ( card Gc)),Gc) are_isomorphic

    proof

      let Gc be strict finite cyclic Group;

      set n = ( card Gc);

      consider g be Element of Gc such that

       A1: for h be Element of Gc holds ex p be Nat st h = (g |^ p) by GR_CY_1: 18;

      for h be Element of Gc holds ex i st h = (g |^ i)

      proof

        let h be Element of Gc;

        consider p be Nat such that

         A2: h = (g |^ p) by A1;

        reconsider p1 = p as Integer;

        take p1;

        thus thesis by A2;

      end;

      then

       A3: Gc = ( gr {g}) by Th5;

      ex h be Homomorphism of ( INT.Group n), Gc st h is bijective

      proof

        deffunc F( Element of ( INT.Group n)) = (g |^ $1);

        consider h be Function of the carrier of ( INT.Group n), the carrier of Gc such that

         A4: for p be Element of ( INT.Group n) holds (h . p) = F(p) from FUNCT_2:sch 4;



         A5: for j,j1 be Element of ( INT.Group n) holds (h . (j * j1)) = ((h . j) * (h . j1))

        proof

          let j,j1 be Element of ( INT.Group n);

          reconsider j9 = j, j19 = j1 as Element of ( Segm n);

          (j * j1) = ((j + j1) mod n) by GR_CY_1:def 4

          .= ((j + j1) - (n * ((j + j1) div n))) by NEWTON: 63;



          then (h . (j * j1)) = (g |^ ((j + j1) + ( - (n * ((j + j1) div n))))) by A4

          .= ((g |^ (j + j1)) * (g |^ ( - (n * ((j + j1) div n))))) by GROUP_1: 33

          .= ((g |^ (j + j1)) * ((g |^ (n * ((j + j1) div n))) " )) by GROUP_1: 36

          .= ((g |^ (j + j1)) * (((g |^ n) |^ ((j + j1) div n)) " )) by GROUP_1: 35

          .= ((g |^ (j + j1)) * ((( 1_ Gc) |^ ((j + j1) div n)) " )) 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 thesis;

        end;



         A6: h is one-to-one

        proof

          let x,y be object;

          assume that

           A7: x in ( dom h) and

           A8: y in ( dom h) and

           A9: (h . x) = (h . y) and

           A10: x <> y;

          reconsider m = y as Element of ( INT.Group n) by A8, FUNCT_2:def 1;

          reconsider p = x as Element of ( INT.Group n) by A7, FUNCT_2:def 1;



           A11: (g |^ p) = (h . m) by A4, A9

          .= (g |^ m) by A4;

          reconsider p, m as Element of NAT by ORDINAL1:def 12;



           A12: p < n by NAT_1: 44;



           A13: m < n by NAT_1: 44;



           A14: ex k st k <> 0 & k < n & (g |^ k) = ( 1_ Gc)

          proof

            per cases by A10, XXREAL_0: 1;

              suppose

               A15: p < m;

              reconsider m1 = m, p1 = p as Integer;

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

              per cases ;

                suppose

                 A16: r1 > 0 ;

                set z = 0 ;



                 A17: r1 < n

                proof

                  reconsider n1 = n as Integer;

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

                  hence thesis;

                end;

                ((g |^ m1) * (g |^ ( - p1))) = (g |^ (p1 + ( - p1))) by A11, GROUP_1: 33;

                then (g |^ (m1 + ( - p1))) = (g |^ z) by GROUP_1: 33;

                hence thesis by A16, A17, GROUP_1: 25;

              end;

                suppose r1 = 0 ;

                hence thesis by A10;

              end;

            end;

              suppose

               A18: m < p;

              reconsider m1 = m, p1 = p as Integer;

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

              per cases ;

                suppose

                 A19: r1 > 0 ;

                set z = 0 ;



                 A20: r1 < n

                proof

                  reconsider n1 = n as Integer;

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

                  hence thesis;

                end;

                ((g |^ p1) * (g |^ ( - m1))) = (g |^ (m1 + ( - m1))) by A11, GROUP_1: 33;

                then (g |^ (p1 + ( - m1))) = (g |^ z) by GROUP_1: 33;

                hence thesis by A19, A20, GROUP_1: 25;

              end;

                suppose r1 = 0 ;

                hence thesis by A10;

              end;

            end;

          end;

           not g is being_of_order_0 & ( ord g) = n by A3, GR_CY_1: 6, GR_CY_1: 7;

          hence contradiction by A14, GROUP_1:def 11;

        end;



         A21: ( dom h) = the carrier of ( INT.Group n) by FUNCT_2:def 1;



         A22: the carrier of Gc c= ( rng h)

        proof

          let x be object;

          assume x in the carrier of Gc;

          then

          reconsider z = x as Element of Gc;

          consider p be Nat such that

           A23: z = (g |^ p) by A1;

          set t = (p mod n);

          t < n by NAT_D: 1;

          then

          reconsider t9 = t as Element of ( INT.Group n) by NAT_1: 44;

          z = (g |^ ((n * (p div n)) + (p mod n))) by A23, NAT_D: 2

          .= ((g |^ (n * (p div n))) * (g |^ (p mod n))) by GROUP_1: 33

          .= (((g |^ n) |^ (p div n)) * (g |^ (p mod n))) by GROUP_1: 35

          .= ((( 1_ Gc) |^ (p div n)) * (g |^ (p mod n))) by GR_CY_1: 9

          .= (( 1_ Gc) * (g |^ (p mod n))) by GROUP_1: 31

          .= (g |^ (p mod n)) by GROUP_1:def 4;

          then t9 in ( dom h) & x = (h . t9) by A4, A21;

          hence thesis by FUNCT_1:def 3;

        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 as Homomorphism of ( INT.Group n), Gc by A5, GROUP_6:def 6;

        take h;

        h is onto by A24, FUNCT_2:def 3;

        hence thesis by A6, FUNCT_2:def 4;

      end;

      hence thesis by GROUP_6:def 11;

    end;

    theorem :: GR_CY_2:16

    for Gc be strict cyclic Group st Gc is infinite holds ( INT.Group ,Gc) are_isomorphic

    proof

      let Gc be strict cyclic Group;

      consider g be Element of Gc such that

       A1: for h be Element of Gc holds ex i st h = (g |^ i) by GR_CY_1: 17;

      assume

       A2: Gc is infinite;

      ex h be Homomorphism of INT.Group , Gc st h is bijective

      proof

        deffunc F( Element of INT.Group ) = (g |^ ( @' $1));

        consider h be Function of the carrier of INT.Group , the carrier of Gc such that

         A3: for j1 be Element of INT.Group holds (h . j1) = F(j1) from FUNCT_2:sch 4;



         A4: Gc = ( gr {g}) by A1, Th5;



         A5: h is one-to-one

        proof

          let x,y be object;

          assume that

           A6: x in ( dom h) and

           A7: y in ( dom h) and

           A8: (h . x) = (h . y) and

           A9: x <> y;

          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;

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

          assume x in the carrier of Gc;

          then

          reconsider z = x as Element of Gc;

          consider i 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 thesis by A10, FUNCT_1:def 3;

        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 holds (h . (j * j1)) = ((h . j) * (h . j1))

        proof

          let j, 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 thesis;

        end;

        then

        reconsider h as Homomorphism of INT.Group , Gc by GROUP_6:def 6;

        take h;

        h is onto by A13, FUNCT_2:def 3;

        hence thesis by A5, FUNCT_2:def 4;

      end;

      hence thesis by GROUP_6:def 11;

    end;

    theorem :: GR_CY_2:17



     Th17: for Gc,Hc be strict finite cyclic Group st ( card Hc) = ( card Gc) holds (Hc,Gc) are_isomorphic

    proof

      let Gc,Hc be strict finite cyclic Group;

      set p = ( card Hc);

      assume ( card Hc) = ( card Gc);

      then

       A1: (( INT.Group p),Gc) are_isomorphic by Th15;

      (( INT.Group p),Hc) are_isomorphic by Th15;

      hence thesis by A1, GROUP_6: 67;

    end;

    theorem :: GR_CY_2:18



     Th18: for F,G be strict finite Group st ( card F) = p & ( card G) = p & p is prime holds (F,G) are_isomorphic

    proof

      let F,G be strict finite Group;

      assume that

       A1: ( card F) = p & ( card G) = p and

       A2: p is prime;

      F is cyclic Group & G is cyclic Group by A1, A2, GR_CY_1: 21;

      hence thesis by A1, Th17;

    end;

    theorem :: GR_CY_2:19

    for F,G be strict finite 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 be strict finite Group holds ( card G) = 2 implies for H be 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 be strict finite Group st ( card G) = 2 holds G is cyclic Group by GR_CY_1: 21, INT_2: 28;

    theorem :: GR_CY_2:22

    for G be strict finite Group st G is cyclic & ( card G) = n holds for p st p divides n holds ex G1 be strict Subgroup of G st ( card G1) = p & for G2 be strict Subgroup of G st ( card G2) = p holds G2 = G1

    proof

      let G be strict finite Group;

      assume that

       A1: G is cyclic and

       A2: ( card G) = n;

      let p such that

       A3: p divides n;

      ex G1 be strict Subgroup of G st ( card G1) = p & for G2 be strict Subgroup of G st ( card G2) = p holds G2 = G1

      proof

        consider s be Nat such that

         A4: n = (p * s) by A3, NAT_D:def 3;

        consider a be Element of G such that

         A5: G = ( gr {a}) by A1;

        take ( 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 be strict Subgroup of G st ( card G2) = p holds G2 = ( gr {(a |^ s)})

        proof

          let G2 be strict Subgroup of G such that

           A9: ( card G2) = p;

          consider k such that

           A10: G2 = ( gr {(a |^ k)}) by A5, Th7;

          n divides (k * p) by A2, A5, A9, A10, Th11;

          then

          consider m be Nat such that

           A11: (k * p) = (n * m) by NAT_D:def 3;

          ex l be Nat st k = (s * l)

          proof

            take 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 thesis;

          end;

          then s divides k by NAT_D:def 3;

          hence thesis by A6, A8, A9, A10, Th9, Th10;

        end;

        hence thesis by A7, GR_CY_1: 7;

      end;

      hence thesis;

    end;

    theorem :: GR_CY_2:23

    Gc = ( gr {g}) implies for G, f holds g in ( Image f) implies f is onto

    proof

      assume

       A1: Gc = ( gr {g});

      let G, f;

      assume g in ( Image f);

      then ( Image f) = Gc by A1, Th13;

      hence thesis by GROUP_6: 57;

    end;

    theorem :: GR_CY_2:24



     Th24: for Gc be strict finite cyclic Group st (ex k st ( card Gc) = (2 * k)) holds ex g1 be Element of Gc st ( ord g1) = 2 & for g2 be Element of Gc st ( ord g2) = 2 holds g1 = g2

    proof

      let Gc be strict finite cyclic Group;

      set n = ( card Gc);

      given k such that

       A1: n = (2 * k);

      consider g be Element of Gc such that

       A2: Gc = ( gr {g}) by GR_CY_1:def 7;



       A3: ( ord g) = n by A2, GR_CY_1: 7;

      take (g |^ k);



       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 be Nat st ((g |^ k) |^ p) = ( 1_ Gc) & p <> 0 holds 2 <= p

      proof

        let p be Nat;

        assume that

         A7: ((g |^ k) |^ p) = ( 1_ Gc) and

         A8: p <> 0 & 2 > p;



         A9: not g is being_of_order_0 & ( 1_ Gc) = (g |^ (k * p)) by A7, GROUP_1: 35, GR_CY_1: 6;

        n > (k * p) & (k * p) <> 0 by A1, A5, A8, XCMPLX_1: 6, XREAL_1: 68;

        hence contradiction by A3, A9, GROUP_1:def 11;

      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;

      let g2 be Element of Gc;

      consider k1 be Element of NAT such that

       A10: g2 = (g |^ k1) by A2, Th6;

      assume that

       A11: ( ord g2) = 2 and

       A12: (g |^ k) <> g2;

      now



         A13: not g is being_of_order_0 by GR_CY_1: 6;

        consider t,t1 be Nat such that

         A14: k1 = ((k * t) + t1) and

         A15: t1 < k by A5, NAT_1: 17;



         A16: (2 * t1) < n by A1, A15, XREAL_1: 68;

        t1 <> 0

        proof

          assume t1 = 0 ;



          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;

          per cases by NAT_D: 12;

            suppose (t mod 2) = 0 ;

            then (g |^ k1) = ( 1_ Gc) by A17, GROUP_1: 25;

            hence contradiction by A11, A10, GROUP_1: 42;

          end;

            suppose (t mod 2) = 1;

            hence contradiction by A12, A10, A17;

          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 |^ ((n * t) + (t1 * 2))) by A1

        .= ((g |^ (n * 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;

      end;

      hence thesis;

    end;

    registration

      let G;

      cluster ( center G) -> normal;

      coherence by GROUP_5: 78;

    end

    theorem :: GR_CY_2:25

    for Gc be strict finite cyclic Group st ex k st ( card Gc) = (2 * k) holds ex H be Subgroup of Gc st ( card H) = 2 & H is cyclic Group

    proof

      let Gc be strict finite cyclic Group;

      set n = ( card Gc);

      assume ex k st n = (2 * k);

      then

      consider g1 be Element of Gc such that

       A1: ( ord g1) = 2 and for g2 be Element of Gc st ( ord g2) = 2 holds g1 = g2 by Th24;

      take ( gr {g1});

      thus thesis by A1, Th4, GR_CY_1: 7;

    end;

    theorem :: GR_CY_2:26



     Th26: for G be strict Group holds for g be Homomorphism of G, F st G is cyclic holds ( Image g) is cyclic

    proof

      let G be strict Group;

      let g be Homomorphism of G, F;

      assume G is cyclic;

      then

      consider a be Element of G such that

       A1: G = ( gr {a});

      ex f1 be 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;

        for d be Element of ( Image g) holds ex i st d = (f |^ i)

        proof

          let d be Element of ( Image g);

          d in ( Image g) by STRUCT_0:def 5;

          then

          consider b be 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 such that

           A3: b = (a |^ i) by GR_CY_1: 5;

          take i;

          d = ((g . a) |^ i) by A2, A3, GROUP_6: 37

          .= (f |^ i) by GROUP_4: 2;

          hence thesis;

        end;

        hence thesis by Th5;

      end;

      hence thesis;

    end;

    theorem :: GR_CY_2:27

    for G,F be strict Group st (G,F) are_isomorphic & G is cyclic holds F is cyclic

    proof

      let G,F be strict Group;

      assume that

       A1: (G,F) are_isomorphic and

       A2: G is cyclic;

      consider h be 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 thesis by A2, Th26;

    end;