gr_cy_1.miz



    begin

    reserve i1 for Element of INT ;

    reserve j1,j2,j3 for Integer;

    reserve p,s,k,n for Nat;

    reserve x,y,xp,yp for set;

    reserve G for Group;

    reserve a,b for Element of G;

    reserve F for FinSequence of G;

    reserve I for FinSequence of INT ;

    

     Lm1: for n holds x in ( Segm n) implies x is Element of NAT ;

    definition

      :: original: addint

      redefine

      :: GR_CY_1:def1

      func addint means for i1,i2 be Element of INT holds (it . (i1,i2)) = ( addreal . (i1,i2));

      compatibility

      proof

        let b be BinOp of INT ;

        hereby

          assume

           A1: b = addint ;

          let i1,i2 be Element of INT ;

          

          thus (b . (i1,i2)) = (i1 + i2) by A1, BINOP_2:def 20

          .= ( addreal . (i1,i2)) by BINOP_2:def 9;

        end;

        assume

         A2: for i1,i2 be Element of INT holds (b . (i1,i2)) = ( addreal . (i1,i2));

        now

          let i1,i2 be Element of INT ;

          

          thus (b . (i1,i2)) = ( addreal . (i1,i2)) by A2

          .= (i1 + i2) by BINOP_2:def 9

          .= ( addint . (i1,i2)) by BINOP_2:def 20;

        end;

        hence b = addint ;

      end;

    end

    theorem :: GR_CY_1:1

    for i1 st i1 = 0 holds i1 is_a_unity_wrt addint by BINOP_2: 4, SETWISEO: 14;

    theorem :: GR_CY_1:2

    

     Th2: ( Sum I) = ( addint $$ I)

    proof

      set g = addint , h = addcomplex ;

      set i = ( [#] (I,( the_unity_wrt g)));

      ( rng I) c= COMPLEX by NUMBERS: 11;

      then

      reconsider f = I as FinSequence of COMPLEX by FINSEQ_1:def 4;

      set j = ( [#] (f,( the_unity_wrt h)));

      consider n be Nat such that

       A1: ( dom f) = ( Seg n) by FINSEQ_1:def 2;

      

       A2: (g $$ I) = (g $$ (( finSeg n),i)) & (h $$ f) = (h $$ (( finSeg n),j)) by A1, SETWOP_2:def 2;

      defpred P[ Nat] means (g $$ (( finSeg $1),i)) = (h $$ (( finSeg $1),j));

      

       A3: for k be Nat st P[k] holds P[(k + 1)]

      proof

        let k be Nat;

        assume

         A4: P[k];

        set b = (g $$ (( finSeg k),i));

        set a = (i . (k + 1));

        

         A5: not (k + 1) in ( Seg k) by FINSEQ_3: 8;

        (g $$ (( finSeg (k + 1)),i)) = (g $$ ((( finSeg k) \/ {.(k + 1).}),i)) by FINSEQ_1: 9

        .= (g . (b,a)) by A5, SETWOP_2: 2

        .= (b + a) by BINOP_2:def 20

        .= (h . ((h $$ (( finSeg k),j)),(j . (k + 1)))) by A4, BINOP_2: 1, BINOP_2: 4, BINOP_2:def 3

        .= (h $$ ((( finSeg k) \/ {.(k + 1).}),j)) by A5, SETWOP_2: 2

        .= (h $$ (( finSeg (k + 1)),j)) by FINSEQ_1: 9;

        hence thesis;

      end;

      

       A6: ( Seg 0 ) = ( {}. NAT );

      

      then (g $$ (( finSeg 0 ),( [#] (I,( the_unity_wrt g))))) = ( the_unity_wrt h) by BINOP_2: 1, BINOP_2: 4, SETWISEO: 31

      .= (h $$ (( finSeg 0 ),( [#] (f,( the_unity_wrt h))))) by A6, SETWISEO: 31;

      then

       A7: P[ 0 ];

      for k be Nat holds P[k] from NAT_1:sch 2( A7, A3);

      then (g $$ I) = (h $$ f) by A2;

      hence thesis by RVSUM_1:def 10;

    end;

    definition

      let I;

      :: original: Sum

      redefine

      :: GR_CY_1:def2

      func Sum (I) -> Element of INT equals ( addint $$ I);

      coherence

      proof

        ( Sum I) = ( addint $$ I) by Th2;

        hence thesis;

      end;

      compatibility by Th2;

    end

    theorem :: GR_CY_1:3

    

     Th3: ( Sum ( <*> INT )) = 0 by BINOP_2: 4, FINSOP_1: 10;

    

     Lm2: ( Product ((( len ( <*> INT )) |-> a) |^ ( <*> INT ))) = (a |^ ( Sum ( <*> INT )))

    proof

      (( <*> the carrier of G) |^ ( <*> INT )) = ( <*> the carrier of G) by GROUP_4: 21;

      

      then ( Product ((( len ( <*> INT )) |-> a) |^ ( <*> INT ))) = ( 1_ G) by GROUP_4: 8

      .= (a |^ ( Sum ( <*> INT ))) by Th3, GROUP_1: 25;

      hence thesis;

    end;

    

     Lm3: for I be FinSequence of INT holds for w be Element of INT st ( Product ((( len I) |-> a) |^ I)) = (a |^ ( Sum I)) holds ( Product ((( len (I ^ <*w*>)) |-> a) |^ (I ^ <*w*>))) = (a |^ ( Sum (I ^ <*w*>)))

    proof

      let I;

      let w be Element of INT ;

      assume

       A1: ( Product ((( len I) |-> a) |^ I)) = (a |^ ( Sum I));

      

       A2: ( len (( len I) |-> a)) = ( len I) by CARD_1:def 7;

      

       A3: ( len <*a*>) = 1 by FINSEQ_1: 40

      .= ( len <*w*>) by FINSEQ_1: 40;

      ( Product ((( len (I ^ <*w*>)) |-> a) |^ (I ^ <*w*>))) = ( Product (((( len I) + 1) |-> a) |^ (I ^ <*w*>))) by FINSEQ_2: 16

      .= ( Product (((( len I) |-> a) ^ <*a*>) |^ (I ^ <*w*>))) by FINSEQ_2: 60

      .= ( Product (((( len I) |-> a) |^ I) ^ ( <*a*> |^ <*w*>))) by A2, A3, GROUP_4: 19

      .= (( Product ((( len I) |-> a) |^ I)) * ( Product ( <*a*> |^ <*( @ ( @ w))*>))) by GROUP_4: 5

      .= (( Product ((( len I) |-> a) |^ I)) * ( Product <*(a |^ ( @ w))*>)) by GROUP_4: 22

      .= ((a |^ ( Sum I)) * (a |^ ( @ w))) by A1, FINSOP_1: 11

      .= (a |^ (( Sum I) + ( @ w))) by GROUP_1: 33

      .= (a |^ ( Sum (I ^ <*w*>))) by RVSUM_1: 74;

      hence thesis;

    end;

    theorem :: GR_CY_1:4

    

     Th4: for I be FinSequence of INT holds ( Product ((( len I) |-> a) |^ I)) = (a |^ ( Sum I))

    proof

      defpred P[ FinSequence of INT ] means ( Product ((( len $1) |-> a) |^ $1)) = (a |^ ( Sum $1));

      

       A1: for p be FinSequence of INT holds for x be Element of INT st P[p] holds P[(p ^ <*x*>)] by Lm3;

      

       A2: P[( <*> INT )] by Lm2;

      for p be FinSequence of INT holds P[p] from FINSEQ_2:sch 2( A2, A1);

      hence thesis;

    end;

    theorem :: GR_CY_1:5

    

     Th5: b in ( gr {a}) iff ex j1 st b = (a |^ j1)

    proof

      

       A1: (ex j1 st b = (a |^ j1)) implies b in ( gr {a})

      proof

        given j1 such that

         A2: b = (a |^ j1);

        consider n be Nat such that

         A3: j1 = n or j1 = ( - n) by INT_1: 2;

        per cases by A3;

          suppose

           A4: j1 = n;

          ex F, I st ( len F) = ( len I) & ( rng F) c= {a} & ( Product (F |^ I)) = b

          proof

            take F = (n |-> a);

            

             A5: ( len F) = n by CARD_1:def 7

            .= ( len (n |-> ( @ 1))) by CARD_1:def 7;

            ( Product (F |^ (n |-> ( @ 1)))) = ( Product (F |^ (( len F) |-> ( @ 1)))) by CARD_1:def 7

            .= ( Product (n |-> a)) by GROUP_4: 25

            .= b by A2, A4, GROUP_4: 12;

            hence thesis by A5, FUNCOP_1: 13;

          end;

          hence thesis by GROUP_4: 28;

        end;

          suppose j1 = ( - n);

          

          then

           A6: (b " ) = (a |^ ( - ( - n))) by A2, GROUP_1: 36

          .= (a |^ n);

          ex F, I st ( len F) = ( len I) & ( rng F) c= {a} & ( Product (F |^ I)) = (b " )

          proof

            take F = (n |-> a);

            

             A7: ( len F) = n by CARD_1:def 7

            .= ( len (n |-> ( @ 1))) by CARD_1:def 7;

            ( Product (F |^ (n |-> ( @ 1)))) = ( Product (F |^ (( len F) |-> ( @ 1)))) by CARD_1:def 7

            .= ( Product (n |-> a)) by GROUP_4: 25

            .= (b " ) by A6, GROUP_4: 12;

            hence thesis by A7, FUNCOP_1: 13;

          end;

          then (b " ) in ( gr {a}) by GROUP_4: 28;

          then ((b " ) " ) in ( gr {a}) by GROUP_2: 51;

          hence thesis;

        end;

      end;

      b in ( gr {a}) implies ex j1 st b = (a |^ j1)

      proof

        assume b in ( gr {a});

        then

        consider F, I such that

         A8: ( len F) = ( len I) and

         A9: ( rng F) c= {a} and

         A10: ( Product (F |^ I)) = b by GROUP_4: 28;

        take ( Sum I);

        

         A11: for p be Nat st p in ( dom F) holds (F . p) = ((( len F) |-> a) . p)

        proof

          let p be Nat;

          

           A12: ( dom F) = ( Seg ( len F)) by FINSEQ_1:def 3;

          assume

           A13: p in ( dom F);

          then (F . p) in ( rng F) by FUNCT_1:def 3;

          

          then (F . p) = a by A9, TARSKI:def 1

          .= ((( len F) |-> a) . p) by A12, A13, FUNCOP_1: 7;

          hence thesis;

        end;

        ( dom (( len F) |-> a)) = ( Seg ( len F)) by FUNCOP_1: 13

        .= ( dom F) by FINSEQ_1:def 3;

        

        then b = ( Product ((( len I) |-> a) |^ I)) by A8, A10, A11, FINSEQ_1: 13

        .= (a |^ ( Sum I)) by Th4;

        hence thesis;

      end;

      hence thesis by A1;

    end;

    theorem :: GR_CY_1:6

    

     Th6: for G be finite Group, a be Element of G holds not a is being_of_order_0

    proof

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

      ex n st n <> 0 & (a |^ n) = ( 1_ G)

      proof

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

        consider F be FinSequence such that

         A1: ( len F) = (( card G) + 1) and

         A2: for p be Nat st p in ( dom F) holds (F . p) = F(p) from FINSEQ_1:sch 2;

        

         A3: ( dom F) = ( Seg (( card G) + 1)) by A1, FINSEQ_1:def 3;

        

         A4: for y st y in ( rng F) holds ex n st y = (a |^ n)

        proof

          let y;

          assume y in ( rng F);

          then

          consider x be object such that

           A5: x in ( dom F) and

           A6: (F . x) = y by FUNCT_1:def 3;

          reconsider n = x as Element of NAT by A5;

          take n;

          thus thesis by A2, A5, A6;

        end;

        for x be object holds x in ( rng F) implies x in the carrier of G

        proof

          let y be object;

          assume y in ( rng F);

          then ex n st y = (a |^ n) by A4;

          hence thesis;

        end;

        then ( rng F) c= the carrier of G;

        then

        reconsider F9 = F as Function of ( Seg (( card G) + 1)), the carrier of G by A3, FUNCT_2:def 1, RELSET_1: 4;

        

         A7: ( card G) < (( card G) + 1) by XREAL_1: 29;

        ( card ( Segm ( card G))) = ( card the carrier of G) & ( card ( Seg (( card G) + 1))) = ( card ( Segm (( card G) + 1))) by FINSEQ_1: 55;

        then ( card the carrier of G) in ( card ( Seg (( card G) + 1))) by A7, NAT_1: 41;

        then

        consider x,y be object such that

         A8: x in ( Seg (( card G) + 1)) and

         A9: y in ( Seg (( card G) + 1)) and

         A10: x <> y and

         A11: (F9 . x) = (F9 . y) by FINSEQ_4: 65;

        reconsider p = x, n = y as Element of NAT by A8, A9;

        per cases by A10, XXREAL_0: 1;

          suppose

           A12: n > p;

          then

          reconsider t = (n - p) as Element of NAT by INT_1: 5;

          take t;

          (F9 . p) = (a |^ p) by A2, A3, A8;

          then (a |^ n) = (a |^ p) by A2, A3, A9, A11;

          then (a |^ (n + ( - p))) = ((a |^ p) * (a |^ ( - p))) by GROUP_1: 33;

          then (a |^ t) = (a |^ (p + ( - p))) by GROUP_1: 33;

          hence thesis by A12, GROUP_1: 25;

        end;

          suppose

           A13: p > n;

          then

          reconsider t = (p - n) as Element of NAT by INT_1: 5;

          take t;

          (F9 . p) = (a |^ p) by A2, A3, A8;

          then (a |^ n) = (a |^ p) by A2, A3, A9, A11;

          then (a |^ (p + ( - n))) = ((a |^ n) * (a |^ ( - n))) by GROUP_1: 33;

          then (a |^ t) = (a |^ (n + ( - n))) by GROUP_1: 33;

          hence thesis by A13, GROUP_1: 25;

        end;

      end;

      hence thesis;

    end;

    theorem :: GR_CY_1:7

    

     Th7: for G be finite Group, a be Element of G holds ( ord a) = ( card ( gr {a}))

    proof

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

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

      consider F be FinSequence such that

       A1: ( len F) = ( ord a) and

       A2: for p be Nat st p in ( dom F) holds (F . p) = F(p) from FINSEQ_1:sch 2;

      

       A3: ( dom F) = ( Seg ( ord a)) by A1, FINSEQ_1:def 3;

      

       A4: for y st y in ( rng F) holds ex n st y = (a |^ n)

      proof

        let y;

        assume y in ( rng F);

        then

        consider x be object such that

         A5: x in ( dom F) and

         A6: (F . x) = y by FUNCT_1:def 3;

        reconsider n = x as Element of NAT by A5;

        take n;

        thus thesis by A2, A5, A6;

      end;

      for x be object st x in ( rng F) holds x in the carrier of ( gr {a})

      proof

        let y be object;

        assume y in ( rng F);

        then ex n st y = (a |^ n) by A4;

        then y in ( gr {a}) by Th5;

        hence thesis;

      end;

      then

       A7: ( rng F) c= the carrier of ( gr {a});

       not a is being_of_order_0 by Th6;

      then

       A8: ( ord a) <> 0 by GROUP_1:def 11;

      

       A9: ex x st x in ( dom F) & (F . x) = a

      proof

        set x9 = 1;

        (( ord a) + x9) > ( 0 + x9) by A8, XREAL_1: 6;

        then ( ord a) >= x9 by NAT_1: 13;

        then

         A10: x9 in ( dom F) by A3;

        

        then (F . x9) = (a |^ x9) by A2

        .= a by GROUP_1: 26;

        hence thesis by A10;

      end;

      then

       A11: a in ( rng F) by FUNCT_1:def 3;

      the carrier of ( gr {a}) c= ( rng F)

      proof

        ex H be strict Subgroup of G st the carrier of H = ( rng F)

        proof

          reconsider car = ( rng F) as non empty set by A9, FUNCT_1:def 3;

          the carrier of ( gr {a}) c= the carrier of G by GROUP_2:def 5;

          then

           A12: car c= the carrier of G by A7;

          ( dom the multF of G) = [:the carrier of G, the carrier of G:] by FUNCT_2:def 1;

          then

           A13: ( dom (the multF of G || car)) = [:car, car:] by A12, RELAT_1: 62, ZFMISC_1: 96;

          for y be object st y in ( rng (the multF of G || car)) holds y in car

          proof

            let y be object;

            set f = (the multF of G || car);

            assume y in ( rng f);

            then

            consider x be object such that

             A14: x in ( dom f) and

             A15: (f . x) = y by FUNCT_1:def 3;

            consider xp,yp be object such that

             A16: [xp, yp] = x by A13, A14, RELAT_1:def 1;

            yp in car by A13, A14, A16, ZFMISC_1: 87;

            then

            consider s such that

             A17: yp = (a |^ s) by A4;

            xp in car by A13, A14, A16, ZFMISC_1: 87;

            then

            consider p such that

             A18: xp = (a |^ p) by A4;

            

             A19: ex x st x in ( dom F) & (F . x) = (a |^ (p + s))

            proof

              set t = ((p + s) mod ( ord a));

              

               A20: t < ( ord a) by A8, NAT_D: 1;

              per cases ;

                suppose

                 A21: t = 0 ;

                take ( ord a);

                (a |^ (p + s)) = (a |^ ((( ord a) * ((p + s) div ( ord a))) + ((p + s) mod ( ord a)))) by A8, NAT_D: 2

                .= ((a |^ (( ord a) * ((p + s) div ( ord a)))) * (a |^ ((p + s) mod ( ord a)))) by GROUP_1: 33

                .= (((a |^ ( ord a)) |^ ((p + s) div ( ord a))) * (a |^ ((p + s) mod ( ord a)))) by GROUP_1: 35

                .= ((( 1_ G) |^ ((p + s) div ( ord a))) * (a |^ ((p + s) mod ( ord a)))) by GROUP_1: 41

                .= (( 1_ G) * (a |^ ((p + s) mod ( ord a)))) by GROUP_1: 31

                .= (a |^ 0 ) by A21, GROUP_1:def 4

                .= ( 1_ G) by GROUP_1: 25

                .= (a |^ ( ord a)) by GROUP_1: 41

                .= (F . ( ord a)) by A2, A3, A8, FINSEQ_1: 3;

                hence thesis by A3, A8, FINSEQ_1: 3;

              end;

                suppose t > 0 ;

                then (t + 1) > ( 0 + 1) by XREAL_1: 6;

                then t >= 1 by NAT_1: 13;

                then

                 A22: t in ( dom F) by A3, A20;

                take t;

                (a |^ (p + s)) = (a |^ ((( ord a) * ((p + s) div ( ord a))) + ((p + s) mod ( ord a)))) by A8, NAT_D: 2

                .= ((a |^ (( ord a) * ((p + s) div ( ord a)))) * (a |^ ((p + s) mod ( ord a)))) by GROUP_1: 33

                .= (((a |^ ( ord a)) |^ ((p + s) div ( ord a))) * (a |^ ((p + s) mod ( ord a)))) by GROUP_1: 35

                .= ((( 1_ G) |^ ((p + s) div ( ord a))) * (a |^ ((p + s) mod ( ord a)))) by GROUP_1: 41

                .= (( 1_ G) * (a |^ ((p + s) mod ( ord a)))) by GROUP_1: 31

                .= (a |^ ((p + s) mod ( ord a))) by GROUP_1:def 4;

                hence thesis by A2, A22;

              end;

            end;

            y = ((a |^ p) * (a |^ s)) by A14, A15, A16, A18, A17, FUNCT_1: 47

            .= (a |^ (p + s)) by GROUP_1: 33;

            hence thesis by A19, FUNCT_1:def 3;

          end;

          then ( rng (the multF of G || car)) c= car;

          then

          reconsider op = (the multF of G || car) as BinOp of car by A13, FUNCT_2:def 1, RELSET_1: 4;

          set H = multMagma (# car, op #);

          

           A23: for f,g be Element of H, f9,g9 be Element of G st f = f9 & g = g9 holds (f9 * g9) = (f * g)

          proof

            let f,g be Element of H;

            let f9,g9 be Element of G;

            

             A24: (f * g) = ((the multF of G || car) . [f, g]);

            assume f = f9 & g = g9;

            hence thesis by A24, FUNCT_1: 49;

          end;

          

           A25: ex e be Element of H st for h be Element of H holds (h * e) = h & (e * h) = h & ex g be Element of H st (h * g) = e & (g * h) = e

          proof

            ex x st x in ( dom F) & (F . x) = (a |^ ( ord a))

            proof

              set x9 = ( ord a);

              (F . x9) = (a |^ x9) by A2, A3, A8, FINSEQ_1: 3;

              hence thesis by A3, A8, FINSEQ_1: 3;

            end;

            then (a |^ ( ord a)) in car by FUNCT_1:def 3;

            then

            reconsider e = ( 1_ G) as Element of H by GROUP_1: 41;

            take e;

            for h be Element of H holds (h * e) = h & (e * h) = h & ex g be Element of H st (h * g) = e & (g * h) = e

            proof

              let h be Element of H;

              reconsider h9 = h as Element of G by A12;

              (h * e) = (h9 * ( 1_ G)) by A23

              .= h9 by GROUP_1:def 4;

              hence (h * e) = h;

              (e * h) = (( 1_ G) * h9) by A23

              .= h9 by GROUP_1:def 4;

              hence (e * h) = h;

              thus ex g be Element of H st (h * g) = e & (g * h) = e

              proof

                ex n st h = (a |^ n) & 1 <= n & ( ord a) >= n

                proof

                  consider x be object such that

                   A26: x in ( dom F) and

                   A27: (F . x) = h by FUNCT_1:def 3;

                  reconsider n = x as Element of NAT by A26;

                  take n;

                  thus thesis by A2, A3, A26, A27, FINSEQ_1: 1;

                end;

                then

                consider n such that

                 A28: h = (a |^ n) and

                 A29: ( ord a) >= n;

                ex x st x in ( dom F) & (F . x) = (a |^ (( ord a) - n))

                proof

                  per cases by A29, XXREAL_0: 1;

                    suppose

                     A30: ( ord a) = n;

                    set x = ( ord a);

                    (F . x) = (a |^ x) by A2, A3, A8, FINSEQ_1: 3

                    .= ( 1_ G) by GROUP_1: 41

                    .= (a |^ (( ord a) - n)) by A30, GROUP_1: 25;

                    hence thesis by A3, A8, FINSEQ_1: 3;

                  end;

                    suppose

                     A31: ( ord a) > n;

                    then

                    reconsider x = (( ord a) - n) as Element of NAT by INT_1: 5;

                    take x;

                    x in ( Seg ( ord a))

                    proof

                      set r1 = ( ord a);

                      r1 <= (r1 + n) by NAT_1: 11;

                      then

                       A32: x <= r1 by XREAL_1: 20;

                      (r1 - n) > (n - n) by A31, XREAL_1: 9;

                      then x >= ( 0 + 1) by NAT_1: 13;

                      hence thesis by A32;

                    end;

                    hence thesis by A2, A3;

                  end;

                end;

                then

                reconsider g = (a |^ (( ord a) - n)) as Element of H by FUNCT_1:def 3;

                

                 A33: (n + (( ord a) - n)) = ( ord a);

                

                 A34: (g * h) = ((a |^ (( ord a) - n)) * (a |^ n)) by A23, A28

                .= (a |^ ( ord a)) by A33, GROUP_1: 33

                .= e by GROUP_1: 41;

                (h * g) = ((a |^ n) * (a |^ (( ord a) - n))) by A23, A28

                .= (a |^ ( ord a)) by A33, GROUP_1: 33

                .= e by GROUP_1: 41;

                hence thesis by A34;

              end;

            end;

            hence thesis;

          end;

          for f,g,h be Element of H holds ((f * g) * h) = (f * (g * h))

          proof

            let f,g,h be Element of H;

            reconsider f9 = f, g9 = g, h9 = h as Element of G by A12;

            

             A35: (g * h) = (g9 * h9) by A23;

            (f9 * g9) = (f * g) by A23;

            

            then ((f * g) * h) = ((f9 * g9) * h9) by A23

            .= (f9 * (g9 * h9)) by GROUP_1:def 3

            .= (f * (g * h)) by A23, A35;

            hence thesis;

          end;

          then

          reconsider H1 = H as Group by A25, GROUP_1: 1;

          the carrier of ( gr {a}) c= the carrier of G by GROUP_2:def 5;

          then the carrier of H1 c= the carrier of G by A7;

          then H1 is Subgroup of G by GROUP_2:def 5;

          hence thesis;

        end;

        then

        consider H be strict Subgroup of G such that

         A36: the carrier of H = ( rng F);

         {a} c= the carrier of H by A11, A36, ZFMISC_1: 31;

        then ( gr {a}) is Subgroup of H by GROUP_4:def 4;

        hence thesis by A36, GROUP_2:def 5;

      end;

      then

       A37: ( rng F) = the carrier of ( gr {a}) by A7, XBOOLE_0:def 10;

      reconsider So = ( Seg ( ord a)) as finite set;

      set ca = the carrier of ( gr {a});

      F is one-to-one

      proof

        let x,y be object;

        assume that

         A38: x in ( dom F) and

         A39: y in ( dom F) and

         A40: (F . x) = (F . y) and

         A41: x <> y;

        reconsider s = y as Element of NAT by A39;

        reconsider p = x as Element of NAT by A38;

        

         A42: (F . p) = (a |^ p) & (F . s) = (a |^ s) by A2, A38, A39;

        reconsider s9 = s, p9 = p, z = ( ord a) as Real;

        per cases ;

          suppose p <= s;

          then

          reconsider r1 = (s - p) as Element of NAT by INT_1: 5;

          p > 0 by A3, A38, FINSEQ_1: 1;

          then

           A43: z < (z + p9) by XREAL_1: 29;

          s9 <= z by A3, A39, FINSEQ_1: 1;

          then s9 < (z + p9) by A43, XXREAL_0: 2;

          then

           A44: (s9 - p9) < ((z + p9) - p9) by XREAL_1: 9;

          ( 1_ G) = ((a |^ s) * ((a |^ p) " )) by A40, A42, GROUP_1:def 5;

          then (a |^ 0 ) = ((a |^ s) * ((a |^ p) " )) by GROUP_1: 25;

          then (a |^ 0 ) = ((a |^ s) * (a |^ ( - p))) by GROUP_1: 36;

          then (a |^ 0 ) = (a |^ (s + ( - p))) by GROUP_1: 33;

          then

           A45: ( 1_ G) = (a |^ r1) by GROUP_1: 25;

          r1 <> 0 & not a is being_of_order_0 by A41, Th6;

          hence thesis by A45, A44, GROUP_1:def 11;

        end;

          suppose s <= p;

          then

          reconsider r2 = (p - s) as Element of NAT by INT_1: 5;

          s > 0 by A3, A39, FINSEQ_1: 1;

          then

           A46: z < (z + s9) by XREAL_1: 29;

          p9 <= z by A3, A38, FINSEQ_1: 1;

          then p9 < (z + s9) by A46, XXREAL_0: 2;

          then

           A47: (p9 - s9) < ((z + s9) - s9) by XREAL_1: 9;

          ( 1_ G) = ((a |^ p) * ((a |^ s) " )) by A40, A42, GROUP_1:def 5;

          then (a |^ 0 ) = ((a |^ p) * ((a |^ s) " )) by GROUP_1: 25;

          then (a |^ 0 ) = ((a |^ p) * (a |^ ( - s))) by GROUP_1: 36;

          then (a |^ 0 ) = (a |^ (p + ( - s))) by GROUP_1: 33;

          then

           A48: ( 1_ G) = (a |^ r2) by GROUP_1: 25;

          r2 <> 0 & not a is being_of_order_0 by A41, Th6;

          hence thesis by A48, A47, GROUP_1:def 11;

        end;

      end;

      then (( Seg ( ord a)),the carrier of ( gr {a})) are_equipotent by A3, A37, WELLORD2:def 4;

      then ( card So) = ( card ca) by CARD_1: 5;

      hence thesis by FINSEQ_1: 57;

    end;

    theorem :: GR_CY_1:8

    

     Th8: for G be finite Group, a be Element of G holds ( ord a) divides ( card G)

    proof

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

      ( ord a) = ( card ( gr {a})) by Th7;

      hence thesis by GROUP_2: 148;

    end;

    theorem :: GR_CY_1:9

    

     Th9: for G be finite Group, a be Element of G holds (a |^ ( card G)) = ( 1_ G)

    proof

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

      ( ord a) divides ( card G) by Th8;

      then

      consider t be Nat such that

       A1: ( card G) = (( ord a) * t) by NAT_D:def 3;

      (a |^ ( card G)) = ((a |^ ( ord a)) |^ t) by A1, GROUP_1: 35

      .= (( 1_ G) |^ t) by GROUP_1: 41

      .= ( 1_ G) by GROUP_1: 31;

      hence thesis;

    end;

    theorem :: GR_CY_1:10

    

     Th10: for G be finite Group, a be Element of G holds ((a |^ n) " ) = (a |^ (( card G) - (n mod ( card G))))

    proof

      let G be finite Group;

      let a be Element of G;

      set q = ( card G);

      set p9 = (n mod q);

      (n mod q) <= q by NAT_D: 1;

      then

      reconsider q9 = (q - (n mod q)) as Element of NAT by INT_1: 5;

      ((a |^ n) * (a |^ (q - (n mod q)))) = (a |^ (n + q9)) by GROUP_1: 33

      .= (a |^ (((q * (n div q)) + (n mod q)) + q9)) by NAT_D: 2

      .= (a |^ (((q * (n div q)) + q) + (( - p9) + p9)))

      .= ((a |^ ((q * (n div q)) + q)) * (a |^ (( - p9) + p9))) by GROUP_1: 33

      .= ((a |^ ((q * (n div q)) + q)) * ((a |^ ( - p9)) * (a |^ p9))) by GROUP_1: 33

      .= ((a |^ ((q * (n div q)) + q)) * (((a |^ p9) " ) * (a |^ p9))) by GROUP_1: 36

      .= ((a |^ ((q * (n div q)) + q)) * ( 1_ G)) by GROUP_1:def 5

      .= (a |^ (q * ((n div q) + 1))) by GROUP_1:def 4

      .= ((a |^ q) |^ ((n div q) + 1)) by GROUP_1: 35

      .= (( 1_ G) |^ ((n div q) + 1)) by Th9

      .= ( 1_ G) by GROUP_1: 31;

      hence thesis by GROUP_1: 12;

    end;

    registration

      let G be associative non empty multMagma;

      cluster the multMagma of G -> associative;

      coherence by BINOP_1:def 3;

    end

    registration

      let G be Group;

      cluster the multMagma of G -> Group-like;

      coherence

      proof

        set H = the multMagma of G;

        reconsider e = ( 1_ G) as Element of H;

        take e;

        let h be Element of H;

        reconsider h9 = h as Element of G;

        

        thus (h * e) = (h9 * ( 1_ G))

        .= h by GROUP_1:def 4;

        

        thus (e * h) = (( 1_ G) * h9)

        .= h by GROUP_1:def 4;

        reconsider g = (h9 " ) as Element of H;

        take g;

        

        thus (h * g) = (h9 * (h9 " ))

        .= e by GROUP_1:def 5;

        

        thus (g * h) = ((h9 " ) * h9)

        .= e by GROUP_1:def 5;

      end;

    end

    theorem :: GR_CY_1:11

    

     Th11: for G be strict finite Group st ( card G) > 1 holds ex a be Element of G st a <> ( 1_ G)

    proof

      let G be strict finite Group;

      assume that

       A1: ( card G) > 1 and

       A2: for a be Element of G holds a = ( 1_ G);

      for a be Element of G holds a in ( (1). G)

      proof

        let a be Element of G;

        a = ( 1_ G) by A2;

        then a in {( 1_ G)} by TARSKI:def 1;

        then a in the carrier of ( (1). G) by GROUP_2:def 7;

        hence thesis;

      end;

      then the multMagma of G = ( (1). G) by GROUP_2: 62;

      hence contradiction by A1, GROUP_2: 69;

    end;

    theorem :: GR_CY_1:12

    for G be strict finite Group st ( card G) = p & p is prime holds for H be strict Subgroup of G holds H = ( (1). G) or H = G

    proof

      let G be strict finite Group;

      assume that

       A1: ( card G) = p and

       A2: p is prime;

      let H be strict Subgroup of G;

      ( card H) divides p by A1, GROUP_2: 148;

      then ( card H) = 1 or ( card H) = p by A2, INT_2:def 4;

      hence thesis by A1, GROUP_2: 70, GROUP_2: 73;

    end;

    definition

      :: GR_CY_1:def3

      func INT.Group -> non empty strict multMagma equals multMagma (# INT , addint #);

      coherence ;

    end

    registration

      cluster INT.Group -> associative Group-like;

      coherence

      proof

        set G = INT.Group ;

        reconsider e = 0 as Element of G by INT_1:def 2;

        thus for h,g,f be Element of G holds ((h * g) * f) = (h * (g * f))

        proof

          let h,g,f be Element of G;

          reconsider A = h, B = g, C = f as Integer;

          

           A1: (g * f) = (B + C) by BINOP_2:def 20;

          (h * g) = (A + B) by BINOP_2:def 20;

          

          hence ((h * g) * f) = ((A + B) + C) by BINOP_2:def 20

          .= (A + (B + C))

          .= (h * (g * f)) by A1, BINOP_2:def 20;

        end;

        take e;

        let h be Element of G;

        reconsider A = h as Integer;

        ( - A) in INT by INT_1:def 2;

        then

        reconsider g = ( - A) as Element of G;

        

        thus (h * e) = (A + 0 ) by BINOP_2:def 20

        .= h;

        

        thus (e * h) = ( 0 + A) by BINOP_2:def 20

        .= h;

        take g;

        

        thus (h * g) = (A + ( - A)) by BINOP_2:def 20

        .= e;

        

        thus (g * h) = (( - A) + A) by BINOP_2:def 20

        .= e;

      end;

    end

    registration

      cluster the carrier of INT.Group -> integer-membered;

      coherence ;

    end

    registration

      let a,b be Element of INT.Group ;

      identify a + b with a * b;

      compatibility by BINOP_2:def 20;

    end

    registration

      let n be natural Number;

      cluster ( Segm n) -> natural-membered;

      coherence ;

    end

    definition

      let n be natural Number;

      :: GR_CY_1:def4

      func addint (n) -> BinOp of ( Segm n) means

      : Def4: for k,l be Element of ( Segm n) holds (it . (k,l)) = ((k + l) mod n);

      existence

      proof

        reconsider n as non zero Nat by A1, TARSKI: 1;

        defpred P[ Nat, Nat, set] means $3 = (($1 + $2) mod n);

        

         A2: for k,l be Element of ( Segm n) holds ex c be Element of ( Segm n) st P[k, l, c]

        proof

          let k,l be Element of ( Segm n);

          ((k + l) mod n) < n by NAT_D: 1;

          then

          reconsider c = ((k + l) mod n) as Element of ( Segm n) by NAT_1: 44;

          take c;

          thus thesis;

        end;

        ex o be BinOp of ( Segm n) st for a,b be Element of ( Segm n) holds P[a, b, (o . (a,b))] from BINOP_1:sch 3( A2);

        hence thesis;

      end;

      uniqueness

      proof

        let i1,i2 be BinOp of ( Segm n) such that

         A3: for k,l be Element of ( Segm n) holds (i1 . (k,l)) = ((k + l) mod n) and

         A4: for k,l be Element of ( Segm n) holds (i2 . (k,l)) = ((k + l) mod n);

        for k,l be Element of ( Segm n) holds (i1 . (k,l)) = (i2 . (k,l))

        proof

          let k,l be Element of ( Segm n);

          

          thus (i1 . (k,l)) = ((k + l) mod n) by A3

          .= (i2 . (k,l)) by A4;

        end;

        hence thesis;

      end;

    end

    definition

      let n be non zero Nat;

      :: GR_CY_1:def5

      func INT.Group (n) -> non empty strict multMagma equals multMagma (# ( Segm n), ( addint n) #);

      coherence ;

    end

    registration

      let n be non zero Nat;

      cluster ( INT.Group n) -> finite associative Group-like;

      coherence

      proof

        set G = ( INT.Group n);

        thus the carrier of ( INT.Group n) is finite;

        reconsider e = 0 as Element of G by NAT_1: 44;

        thus for h,g,f be Element of G holds ((h * g) * f) = (h * (g * f))

        proof

          let h,g,f be Element of G;

          reconsider A = h, B = g, C = f as Element of ( Segm n);

          

           A1: (g * f) = ((B + C) mod n) by Def4;

          (h * g) = ((A + B) mod n) by Def4;

          

          hence ((h * g) * f) = ((((A + B) mod n) + C) mod n) by Def4

          .= (((A + B) + C) mod n) by NAT_D: 22

          .= ((A + (B + C)) mod n)

          .= ((A + ((B + C) mod n)) mod n) by NAT_D: 22

          .= (h * (g * f)) by A1, Def4;

        end;

        take e;

        let h be Element of G;

        reconsider A = h as Element of ( Segm n);

        

         A2: A < n by NAT_1: 44;

        then

        consider p be Nat such that

         A3: n = (A + p) by NAT_1: 10;

        

        thus (h * e) = ((A + 0 ) mod n) by Def4

        .= h by A2, NAT_D: 24;

        

        thus (e * h) = (( 0 + A) mod n) by Def4

        .= h by A2, NAT_D: 24;

        (p mod n) < n by NAT_D: 1;

        then

        reconsider g = (p mod n) as Element of G by NAT_1: 44;

        reconsider B = g as Element of ( Segm n);

        take g;

        

         A4: p <= n by A3, NAT_1: 12;

        thus (h * g) = e

        proof

          per cases by A4, XXREAL_0: 1;

            suppose

             A5: p = n;

            (h * g) = ((A + B) mod n) by Def4

            .= (( 0 * n) mod n) by A3, A5, NAT_D: 25

            .= e by NAT_D: 13;

            hence thesis;

          end;

            suppose

             A6: p < n;

            (h * g) = ((A + B) mod n) by Def4

            .= (n mod n) by A3, A6, NAT_D: 24

            .= e by NAT_D: 25;

            hence thesis;

          end;

        end;

        thus (g * h) = e

        proof

          per cases by A4, XXREAL_0: 1;

            suppose p = n;

            

            then (g * h) = (((n mod n) + 0 ) mod n) by A3, Def4

            .= (( 0 * n) mod n) by NAT_D: 25

            .= e by NAT_D: 13;

            hence thesis;

          end;

            suppose

             A7: p < n;

            (g * h) = ((A + B) mod n) by Def4

            .= (n mod n) by A3, A7, NAT_D: 24

            .= e by NAT_D: 25;

            hence thesis;

          end;

        end;

      end;

    end

    theorem :: GR_CY_1:13

    

     Th13: ( 1_ INT.Group ) = 0

    proof

      reconsider e = 0 as Element of INT.Group by INT_1:def 2;

      for h be Element of INT.Group holds (h * e) = h & (e * h) = h;

      hence thesis by GROUP_1: 4;

    end;

    theorem :: GR_CY_1:14

    

     Th14: for n be non zero Nat holds ( 1_ ( INT.Group n)) = 0

    proof

      let n be non zero Nat;

      reconsider e = 0 as Element of ( Segm n) by NAT_1: 44;

      reconsider e as Element of ( INT.Group n);

      for h be Element of ( INT.Group n) holds (h * e) = h & (e * h) = h

      proof

        let h be Element of ( INT.Group n);

        reconsider A = h as Element of ( Segm n);

        reconsider A as Element of NAT ;

        

         A1: A < n by NAT_1: 44;

        

         A2: (e * h) = (( 0 + A) mod n) by Def4

        .= h by A1, NAT_D: 24;

        (h * e) = ((A + 0 ) mod n) by Def4

        .= h by A1, NAT_D: 24;

        hence thesis by A2;

      end;

      hence thesis by GROUP_1: 4;

    end;

    definition

      let h be Integer;

      :: GR_CY_1:def6

      func @' h -> Element of INT.Group equals h;

      coherence by INT_1:def 2;

    end

    theorem :: GR_CY_1:15

    

     Th15: for h be Element of INT.Group holds (h " ) = ( - h)

    proof

      let h be Element of INT.Group ;

      ( - h) in INT by INT_1:def 2;

      then

      reconsider g = ( - h) as Element of INT.Group ;

      (h * g) = ( 1_ INT.Group ) by Th13;

      hence thesis by GROUP_1: 12;

    end;

    

     Lm4: (( @' 1) |^ k) = k

    proof

      defpred P[ Nat] means (( @' 1) |^ $1) = $1;

      

       A1: for k st P[k] holds P[(k + 1)]

      proof

        let k;

        assume (( @' 1) |^ k) = k;

        then ((( @' 1) |^ k) * ( @' 1)) = (k + 1);

        hence thesis by GROUP_1: 34;

      end;

      

       A2: P[ 0 ] by Th13, GROUP_1: 25;

      for k holds P[k] from NAT_1:sch 2( A2, A1);

      hence thesis;

    end;

    theorem :: GR_CY_1:16

    

     Th16: j1 = (( @' 1) |^ j1)

    proof

      consider k be Nat such that

       A1: j1 = k or j1 = ( - k) by INT_1: 2;

      per cases by A1;

        suppose j1 = k;

        hence thesis by Lm4;

      end;

        suppose

         A2: j1 = ( - k);

        reconsider k9 = k as Integer;

        reconsider k9 as Element of INT.Group by INT_1:def 2;

        (( @' 1) |^ j1) = ((( @' 1) |^ k) " ) by A2, GROUP_1: 36

        .= (k9 " ) by Lm4

        .= j1 by A2, Th15;

        hence thesis;

      end;

    end;

    

     Lm5: INT.Group = ( gr {( @' 1)})

    proof

      reconsider h = 1 as Element of INT by INT_1:def 2;

      reconsider h as Element of INT.Group ;

      for G1 be Subgroup of INT.Group st {h} c= the carrier of G1 holds ( (Omega). INT.Group ) is Subgroup of G1

      proof

        let G1 be Subgroup of INT.Group ;

        assume

         A1: {h} c= the carrier of G1;

        the carrier of ( (Omega). INT.Group ) c= the carrier of G1

        proof

          h in {h} by TARSKI:def 1;

          then

          reconsider h99 = h as Element of G1 by A1;

          let x be object;

          assume that

           A2: x in the carrier of ( (Omega). INT.Group ) and

           A3: not x in the carrier of G1;

          reconsider x9 = x as Integer by A2;

          (h99 |^ x9) in the carrier of G1 & (h99 |^ x9) = (h |^ x9) by GROUP_4: 2;

          hence contradiction by A3, Th16;

        end;

        hence thesis by GROUP_2: 57;

      end;

      then for G1 be strict Subgroup of INT.Group st {h} c= the carrier of G1 holds ( (Omega). INT.Group ) is Subgroup of G1;

      hence thesis by GROUP_4:def 4;

    end;

    definition

      let IT be Group;

      :: GR_CY_1:def7

      attr IT is cyclic means

      : Def7: ex a be Element of IT st the multMagma of IT = ( gr {a});

    end

    registration

      cluster strict cyclic for Group;

      existence by Def7, Lm5;

    end

    registration

      let G be Group;

      cluster ( (1). G) -> cyclic;

      coherence

      proof

        ( 1_ G) in {( 1_ G)} by TARSKI:def 1;

        then

        reconsider PG = ( 1_ G) as Element of ( (1). G) by GROUP_2:def 7;

        take PG;

        for G1 be Subgroup of ( (1). G) st {PG} c= the carrier of G1 holds ( (Omega). ( (1). G)) is Subgroup of G1

        proof

          let G1 be Subgroup of ( (1). G);

          assume {PG} c= the carrier of G1;

          then the carrier of ( (Omega). ( (1). G)) c= the carrier of G1 by GROUP_2:def 7;

          hence thesis by GROUP_2: 57;

        end;

        then for G1 be strict Subgroup of ( (1). G) st {PG} c= the carrier of G1 holds ( (Omega). ( (1). G)) is Subgroup of G1;

        hence thesis by GROUP_4:def 4;

      end;

    end

    registration

      cluster strict finite cyclic for Group;

      existence

      proof

        take ( (1). the Group);

        thus thesis;

      end;

    end

    theorem :: GR_CY_1:17

    

     Th17: G is cyclic Group iff ex a be Element of G st for b be Element of G holds ex j1 st b = (a |^ j1)

    proof

      thus G is cyclic Group implies ex a be Element of G st for b be Element of G holds ex j1 st b = (a |^ j1)

      proof

        assume G is cyclic Group;

        then

        consider a be Element of G such that

         A1: the multMagma of G = ( gr {a}) by Def7;

        take a;

        for b be Element of G holds ex j1 st b = (a |^ j1) by A1, Th5, STRUCT_0:def 5;

        hence thesis;

      end;

      given a be Element of G such that

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

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

      proof

        let b be Element of G;

        ex j1 st b = (a |^ j1) by A2;

        hence thesis by Th5;

      end;

      then the multMagma of G = ( gr {a}) by GROUP_2: 62;

      hence thesis by Def7;

    end;

    theorem :: GR_CY_1:18

    

     Th18: for G be finite Group holds G is cyclic iff ex a be Element of G st for b be Element of G holds ex n st b = (a |^ n)

    proof

      let G be finite Group;

      thus G is cyclic implies ex a be Element of G st for b be Element of G holds ex n st b = (a |^ n)

      proof

        assume G is cyclic;

        then

        consider a be Element of G such that

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

        take a;

        let b be Element of G;

        consider j2 such that

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

        consider n be Nat such that

         A3: j2 = n or j2 = ( - n) by INT_1: 2;

        per cases by A3;

          suppose j2 = n;

          hence thesis by A2;

        end;

          suppose

           A4: j2 = ( - n);

          (n mod ( card G)) <= ( card G) by NAT_D: 1;

          then

          reconsider q9 = (( card G) - (n mod ( card G))) as Element of NAT by INT_1: 5;

          take q9;

          b = ((a |^ n) " ) by A2, A4, GROUP_1: 36

          .= (a |^ q9) by Th10;

          hence thesis;

        end;

      end;

      given a be Element of G such that

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

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

      proof

        let b be Element of G;

        consider n such that

         A6: b = (a |^ n) by A5;

        reconsider n as Integer;

        take n;

        thus thesis by A6;

      end;

      hence thesis by Th17;

    end;

    theorem :: GR_CY_1:19

    

     Th19: for G be finite Group holds (G is cyclic iff ex a be Element of G st ( ord a) = ( card G))

    proof

      let G be finite Group;

      thus G is cyclic implies ex a be Element of G st ( ord a) = ( card G)

      proof

        reconsider H = the multMagma of G as Group;

        assume G is cyclic;

        then

        consider a be Element of G such that

         A1: the multMagma of G = ( gr {a});

        take a;

        ( ord a) = ( card H) by A1, Th7;

        hence thesis;

      end;

      given a be Element of G such that

       A2: ( ord a) = ( card G);

      ex a be Element of G st the multMagma of G = ( gr {a})

      proof

        consider a be Element of G such that

         A3: ( ord a) = ( card G) by A2;

        take a;

        ( card ( gr {a})) = ( card G) by A3, Th7;

        hence thesis by GROUP_2: 73;

      end;

      hence thesis;

    end;

    theorem :: GR_CY_1:20

    for G be finite Group, H be strict Subgroup of G st G is cyclic holds H is cyclic

    proof

      let G be finite Group, H be strict Subgroup of G;

      

       A1: ( card H) >= 1 by GROUP_1: 45;

      assume G is cyclic;

      then

      consider a be Element of G such that

       A2: for b be Element of G holds ex n st b = (a |^ n) by Th18;

      per cases by A1, XXREAL_0: 1;

        suppose ( card H) = 1;

        then H = ( (1). G) by GROUP_2: 70;

        hence thesis;

      end;

        suppose

         A3: ( card H) > 1;

        defpred P[ Nat] means $1 > 0 & (a |^ $1) is Element of H;

        consider h be Element of H such that

         A4: h <> ( 1_ H) by A3, Th11;

        h is Element of G by GROUP_2: 42;

        then

        consider n such that

         A5: h = (a |^ n) by A2;

        n <> 0

        proof

          assume n = 0 ;

          

          then h = ( 1_ G) by A5, GROUP_1: 25

          .= ( 1_ H) by GROUP_2: 44;

          hence contradiction by A4;

        end;

        then

         A6: ex n be Nat st P[n] by A5;

        ex h1 be Element of H st for b be Element of H holds ex s st b = (h1 |^ s)

        proof

          ex k be Nat st P[k] & for n be Nat st P[n] holds k <= n from NAT_1:sch 5( A6);

          then

          consider n be Nat such that

           A7: n > 0 and

           A8: (a |^ n) is Element of H and

           A9: for k be Nat st k > 0 & (a |^ k) is Element of H holds n <= k;

          consider h1 be Element of H such that

           A10: h1 = (a |^ n) by A8;

          take h1;

          for b be Element of H holds ex s st b = (h1 |^ s)

          proof

            let b be Element of H;

            b is Element of G by GROUP_2: 42;

            then

            consider p such that

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

            consider s,r be Nat such that

             A12: p = ((n * s) + r) and

             A13: r < n by A7, NAT_1: 17;

            reconsider s, r as Element of NAT by ORDINAL1:def 12;

            take s;

            r = 0

            proof

              (h1 |^ s) = ((a |^ n) |^ s) by A10, GROUP_4: 1;

              

              then ((h1 |^ s) " ) = (((a |^ n) |^ s) " ) by GROUP_2: 48

              .= ((a |^ (n * s)) " ) by GROUP_1: 35;

              then

              reconsider g = ((a |^ (n * s)) " ) as Element of H;

              reconsider b = (a |^ p) as Element of H by A11;

              (a |^ p) = ((a |^ (n * s)) * (a |^ r)) by A12, GROUP_1: 33;

              

              then (((a |^ (n * s)) " ) * (a |^ p)) = ((((a |^ (n * s)) " ) * (a |^ (n * s))) * (a |^ r)) by GROUP_1:def 3

              .= (( 1_ G) * (a |^ r)) by GROUP_1:def 5

              .= (a |^ r) by GROUP_1:def 4;

              then

               A14: (g * b) = (a |^ r) by GROUP_2: 43;

              assume r <> 0 ;

              hence contradiction by A9, A13, A14;

            end;

            

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

            .= (h1 |^ s) by A10, GROUP_4: 1;

            hence thesis by A11;

          end;

          hence thesis;

        end;

        hence thesis by Th18;

      end;

    end;

    theorem :: GR_CY_1:21

    for G be strict finite Group st ( card G) is prime holds G is cyclic

    proof

      let G be strict finite Group;

      assume

       A1: ( card G) is prime;

      set p = ( card G);

      ex a be Element of G st ( ord a) = p

      proof

        assume

         A2: for a be Element of G holds ( ord a) <> p;

         A3:

        now

          let a be Element of G;

          ( ord a) divides p by Th8;

          then ( ord a) = 1 or ( ord a) = p by A1, INT_2:def 4;

          hence ( ord a) = 1 by A2;

        end;

        for x be object holds x in the carrier of G implies x in the carrier of ( (1). G)

        proof

          let x be object;

          assume x in the carrier of G;

          then

          reconsider x9 = x as Element of G;

          ( ord x9) = 1 by A3;

          then x9 = ( 1_ G) by GROUP_1: 43;

          then x9 in {( 1_ G)} by TARSKI:def 1;

          hence thesis by GROUP_2:def 7;

        end;

        then the carrier of G c= the carrier of ( (1). G);

        then G = ( (1). G) by GROUP_2: 61;

        then ( card G) = 1 by GROUP_2: 69;

        hence contradiction by A1, INT_2:def 4;

      end;

      hence thesis by Th19;

    end;

    theorem :: GR_CY_1:22

    

     Th22: for n be non zero Nat holds ex g be Element of ( INT.Group n) st for b be Element of ( INT.Group n) holds ex j1 st b = (g |^ j1)

    proof

      let n be non zero Nat;

      ( 0 + 1) < (n + 1) by XREAL_1: 6;

      then

       A1: n >= 1 by NAT_1: 13;

      now

        per cases by A1, XXREAL_0: 1;

          suppose n = 1;

          

          then the carrier of ( INT.Group n) = {( 1_ ( INT.Group n))} by Th14, CARD_1: 49

          .= the carrier of ( (1). ( INT.Group n)) by GROUP_2:def 7;

          then ( INT.Group n) = ( (1). ( INT.Group n)) by GROUP_2: 61;

          hence thesis by Th17;

        end;

          suppose n > 1;

          then

          reconsider g9 = 1 as Element of ( Segm n) by NAT_1: 44;

          reconsider g = g9 as Element of ( INT.Group n);

          for b be Element of ( INT.Group n) holds ex j1 st b = (g |^ j1)

          proof

            let b be Element of ( INT.Group n);

            reconsider b9 = b as Element of NAT by Lm1;

            defpred P[ Nat] means (g |^ $1) = ($1 mod n);

            

             A2: b9 < n by NAT_1: 44;

            

             A3: for k st P[k] holds P[(k + 1)]

            proof

              let k;

              assume

               A4: (g |^ k) = (k mod n);

              (k mod n) < n by NAT_D: 1;

              then

              reconsider e = (k mod n) as Element of ( Segm n) by NAT_1: 44;

              (g |^ (k + 1)) = ((g |^ k) * (g |^ 1)) by GROUP_1: 33

              .= ((g |^ k) * g) by GROUP_1: 26

              .= ((e + g9) mod n) by A4, Def4

              .= ((k + 1) mod n) by NAT_D: 22;

              hence thesis;

            end;

            (g |^ 0 ) = ( 1_ ( INT.Group n)) by GROUP_1: 25

            .= 0 by Th14

            .= ( 0 mod n) by NAT_D: 26;

            then

             A5: P[ 0 ];

            for k holds P[k] from NAT_1:sch 2( A5, A3);

            

            then

             A6: (g |^ b9) = (b9 mod n)

            .= b by A2, NAT_D: 24;

            reconsider b9 as Integer;

            take b9;

            thus thesis by A6;

          end;

          hence thesis;

        end;

      end;

      hence thesis;

    end;

    registration

      cluster cyclic -> commutative for Group;

      coherence

      proof

        let G;

        assume

         A1: G is cyclic;

        for a,b be Element of G holds (a * b) = (b * a)

        proof

          let a,b be Element of G;

          ex e be Element of G st ex j2 st a = (e |^ j2) & ex j3 st b = (e |^ j3)

          proof

            consider e be Element of G such that

             A2: for d be Element of G holds ex j3 st d = (e |^ j3) by A1, Th17;

            take e;

            (ex j2 st a = (e |^ j2)) & ex j3 st b = (e |^ j3) by A2;

            hence thesis;

          end;

          then

          consider e be Element of G, j2, j3 such that

           A3: a = (e |^ j2) & b = (e |^ j3);

          (a * b) = (e |^ (j3 + j2)) by A3, GROUP_1: 33

          .= (b * a) by A3, GROUP_1: 33;

          hence thesis;

        end;

        hence thesis;

      end;

    end

    theorem :: GR_CY_1:23

     INT.Group = ( gr {( @' 1)}) by Lm5;

    registration

      cluster INT.Group -> cyclic;

      coherence by Lm5;

    end

    registration

      let n be non zero Nat;

      cluster ( INT.Group n) -> cyclic;

      coherence

      proof

        ex g be Element of ( INT.Group n) st for b be Element of ( INT.Group n) holds ex j1 st b = (g |^ j1) by Th22;

        hence thesis by Th17;

      end;

    end