The Mizar article:

Cyclic Groups and Some of Their Properties --- Part I

by
Dariusz Surowik

Received November 22, 1991

Copyright (c) 1991 Association of Mizar Users

MML identifier: GR_CY_1
[ MML identifier index ]


environ

 vocabulary INT_1, REALSET1, FINSEQ_1, NAT_1, ORDINAL2, ARYTM, BINOP_1,
      FUNCT_1, VECTSP_1, QC_LANG1, SETWISEO, RLVECT_1, FINSEQ_2, GROUP_1,
      GROUP_4, RELAT_1, ARYTM_1, FUNCOP_1, FINSET_1, CARD_1, GROUP_2, TARSKI,
      ARYTM_3, FILTER_0, RLSUB_1, GRAPH_1, GR_CY_1, CARD_3;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL2, ORDINAL1, NUMBERS,
      XCMPLX_0, XREAL_0, RELAT_1, FUNCT_1, REAL_1, FUNCT_2, SETWISEO, CARD_1,
      FINSET_1, BINOP_1, DOMAIN_1, INT_1, INT_2, NAT_1, RLVECT_1, GROUP_2,
      STRUCT_0, VECTSP_1, GROUP_1, GROUP_4, FUNCOP_1, FINSOP_1, SETWOP_2,
      FINSEQ_1;
 constructors WELLORD2, REAL_1, SETWISEO, DOMAIN_1, NAT_1, FUNCSDOM, GROUP_4,
      FINSOP_1, NAT_LAT, MEMBERED, XBOOLE_0;
 clusters SUBSET_1, FUNCT_1, CARD_1, INT_1, GROUP_1, GROUP_2, RELSET_1,
      STRUCT_0, FINSEQ_1, ARYTM_3, XREAL_0, MEMBERED, ZFMISC_1, XBOOLE_0,
      ORDINAL2;
 requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM;
 definitions GROUP_1, SETWISEO, FUNCT_1, BINOP_1, VECTSP_1, TARSKI;
 theorems AXIOMS, BINOP_1, INT_1, INT_2, NAT_1, REAL_1, FINSEQ_1, FINSEQ_2,
      FINSEQ_4, VECTSP_1, ZFMISC_1, FUNCT_2, FUNCOP_1, GROUP_1, GROUP_2,
      GROUP_4, TARSKI, FUNCT_1, CARD_1, WELLORD2, RLVECT_1, FINSOP_1, RELSET_1,
      XREAL_0, ORDINAL2, XBOOLE_0, XBOOLE_1, SQUARE_1, RELAT_1, XCMPLX_0,
      XCMPLX_1;
 schemes BINOP_1, NAT_1, FINSEQ_1, FINSEQ_2;

begin

 reserve i1,i2,i3 for Element of INT;
 reserve j1,j2,j3 for Integer;
 reserve p,s,r,g,k,n,m,q,t 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 the carrier of G;
 reserve I for FinSequence of INT;

     :::::::::::::::::::::::::::::::::::::::::::::::::::::::
     ::    Some properties of modulo function             ::
     :::::::::::::::::::::::::::::::::::::::::::::::::::::::

theorem Th1:
 m mod n = (n*k + m) mod n
 proof
  per cases by NAT_1:18;
  suppose A1: n > 0;
     m mod n = t implies (n*k + m) mod n = t
   proof
    assume m mod n = t;
    then consider q such that A2: m = n * q + t & t < n by A1,NAT_1:def 2;
      ex g st n*k + m = n*g + t & t < n
      proof
       take k + q;
         n*k + m = (n*k + n*q) + t & t < n by A2,XCMPLX_1:1;
       hence thesis by XCMPLX_1:8;
      end;
    hence thesis by NAT_1:def 2;
   end;
 hence thesis;
 suppose n = 0;
 hence thesis;
end;

theorem Th2:
 (p+s) mod n = ((p mod n)+s) mod n
 proof
  per cases by NAT_1:18;
  suppose n > 0;
  then (p + s) mod n = (n*(p div n) + (p mod n) + s) mod n by NAT_1:47
                .=(n*(p div n) + ((p mod n) + s)) mod n by XCMPLX_1:1
                .=((p mod n) + s) mod n by Th1;
   hence thesis;
   suppose
A1:  n = 0;
   hence (p+s) mod n = 0 by NAT_1:def 2
     .= ((p mod n)+s) mod n by A1,NAT_1:def 2;
 end;

theorem
  (p+s) mod n = (p + ( s mod n)) mod n by Th2;

theorem Th4:
 k < n implies k mod n = k
 proof
  assume A1:k<n;
     ex p st k=n*p + k & k<n
   proof
      k=n*0 + k;
    hence thesis by A1;
   end;
  hence thesis by NAT_1:def 2;
 end;

theorem Th5:
 n mod n = 0
 proof
  per cases by NAT_1:18;
  suppose A1:n>0;
    ex p st n=n*p +0 & 0<n
   proof
      n=n*1+0;
    hence thesis by A1;
   end;
  hence thesis by NAT_1:def 2;
  suppose n = 0;
  hence thesis by NAT_1:def 2;
 end;

theorem Th6:
 0 = 0 mod n
  proof
      n = 0 or n > 0 by NAT_1:18;
    hence thesis by Th4,NAT_1:def 2;
  end;

definition let n be natural number such that A1:n > 0;
 func Segm (n) -> non empty Subset of NAT equals
:Def1:  {p: p<n};
coherence
proof
 set X={p:p<n};
   0 in X by A1;
 then reconsider X as non empty set;
   X c= NAT
  proof
     for x holds x in X implies x in NAT
    proof
     let x be set;
     assume x in X;
     then ex p being Element of NAT st p=x & p<n;
     hence thesis;
    end;
   hence thesis by TARSKI:def 3;
 end;
 hence thesis;
 end;
end;

Lm1:
 for n st n > 0 holds x in Segm (n) implies x is Nat;

canceled 3;

theorem Th10:
 for n,s being natural number st n > 0 holds s in Segm (n) iff s < n
 proof
  let n,s be natural number;
  assume A1: n>0;
A2: s is Nat by ORDINAL2:def 21;
    s in { p : p<n } iff ex p st s=p & p<n;
  hence thesis by A1,A2,Def1;
 end;

canceled;

theorem
  for n being natural number st n > 0 holds 0 in Segm (n) by Th10;

theorem Th13:
 Segm (1) = {0}
 proof
    now let x;
  thus x in Segm(1) implies x in { 0 }
    proof assume A1:x in Segm(1);
       Segm(1) = { p : p < 1 } by Def1;
     then consider p such that
     A2:x = p & (p < 1) by A1;
       p < 0 + 1 by A2;
     then p <= 0 by NAT_1:38;
     then p = 0 by NAT_1:18;
     hence thesis by A2,TARSKI:def 1;
    end;
    assume x in { 0 };
    then x = 0 by TARSKI:def 1;
    hence x in Segm(1) by Th10;
    end;
  hence Segm(1) = { 0 } by TARSKI:2;
end;

       :::::::::::::::::::::::::::::::::::::::::::::::::::::
       ::              Definition addint                  ::
       :::::::::::::::::::::::::::::::::::::::::::::::::::::

definition
 func addint -> BinOp of INT means:
Def2: for i1,i2 being Element of INT holds
 it.(i1,i2) = addreal.(i1,i2);
existence
proof
 defpred P[Element of INT, Element of INT,set] means $3 = addreal.($1,$2);
A1:for i1,i2 being Element of INT ex c being Element of INT st P[i1,i2,c]
 proof
  let i1,i2 be Element of INT;
  reconsider i1' = i1, i2' = i2 as Integer;
  reconsider c = i1'+i2' as Element of INT by INT_1:12;
  take c;
    i1 is Element of REAL & i2 is Element of REAL by XREAL_0:def 1;
  hence thesis by VECTSP_1:def 4;
 end;
  ex B being BinOp of INT st for i1,i2 being Element of INT holds
   P[i1,i2,B.(i1,i2)] from BinOpEx(A1);
  hence thesis;
end;
uniqueness
proof
 let f1,f2 be BinOp of INT such that
 A2:for i1,i2 being Element of INT holds
   f1.(i1,i2)=addreal.(i1,i2) and
 A3:for i1,i2 being Element of INT holds
   f2.(i1,i2)=addreal.(i1,i2);
  for i1,i2 being Element of INT holds f1.(i1,i2)=f2.(i1,i2)
proof
 let i1,i2 be Element of INT;
 thus f1.(i1,i2)=addreal.(i1,i2) by A2 .=f2.(i1,i2) by A3;
end;
hence thesis by BINOP_1:2;
end;
end;

theorem Th14:
 for j1,j2 holds addint.(j1,j2)=j1+j2
 proof
  let j1,j2;
  reconsider j1'=j1,j2'=j2 as Element of INT by INT_1:12;
A1:j1 is Element of REAL & j2 is Element of REAL by XREAL_0:def 1;
  thus addint.(j1,j2)=addreal.(j1',j2') by Def2
                      .=j1+j2 by A1,VECTSP_1:def 4;
 end;

theorem Th15:
 for i1 st i1 = 0 holds i1 is_a_unity_wrt addint
proof
let i1;
assume A1:i1=0;
 A2: for i2 holds addint.(i1,i2) = i2
 proof let i2;
  reconsider e=i1 as Integer;
    addint.(e,i2) =addint.(e,@i2) by GROUP_4:def 2
               .= e +@i2 by Th14
               .= i2 by A1,GROUP_4:def 2;
  hence thesis;
end;
   for i2 holds addint.(i2,i1) = i2
  proof
   let i2;
   reconsider e=i1 as Integer;
     addint.(i2,e) =addint.(@i2,e)by GROUP_4:def 2
                .= @i2 + e by Th14
                .= i2 by A1,GROUP_4:def 2;
   hence thesis;
  end;
 hence i1 is_a_unity_wrt addint by A2,BINOP_1:11;
end;

theorem Th16:
 the_unity_wrt addint = 0
proof
 reconsider zero=0 as Element of INT by INT_1:12;
   zero is_a_unity_wrt addint by Th15;
hence thesis by BINOP_1:def 8;
end;

theorem Th17:
 addint has_a_unity
 proof reconsider O = 0 as Element of INT by INT_1:12;
 take O; thus thesis by Th15;
 end;

theorem
   addint is commutative
 proof let i1,i2;
  thus addint.(i1,i2) = addint.(@i1,i2) by GROUP_4:def 2
                     .= addint.(@i1,@i2) by GROUP_4:def 2
                     .= @i2 + (@i1) by Th14
                     .= addint.(@i2,@i1) by Th14
                     .= addint.(i2,@i1) by GROUP_4:def 2
                     .= addint.(i2,i1) by GROUP_4:def 2;
 end;

theorem
   addint is associative
 proof let i1,i2,i3;
  thus addint.(i1,addint.(i2,i3))
      = addint.(@i1,addint.(i2,i3)) by GROUP_4:def 2
     .= addint.(@i1,addint.(@i2,i3)) by GROUP_4:def 2
     .= addint.(@i1,addint.(@i2,@i3)) by GROUP_4:def 2
     .= addint.(@i1,@i2+@i3) by Th14
     .= @i1+(@i2+@i3) by Th14
     .= @i1+@i2+@i3 by XCMPLX_1:1
     .= addint.((@i1+@i2),@i3) by Th14
     .= addint.(addint.(@i1,@i2),@i3) by Th14
     .= addint.(addint.(@i1,@i2),i3) by GROUP_4:def 2
     .= addint.(addint.(@i1,i2),i3) by GROUP_4:def 2
     .= addint.(addint.(i1,i2),i3) by GROUP_4:def 2;
 end;

definition let F be FinSequence of INT;
 func Sum(F) -> Integer equals
:Def3:  addint $$ F;
  coherence;
end;

theorem Th20:
 Sum(I^<*i1*>) =Sum I +@i1
 proof
  thus Sum(I^<*i1*>) = addint $$ (I^<*i1*>) by Def3
                 .= addint.(addint $$ I,i1) by Th17,FINSOP_1:5
                 .= addint.(Sum I,i1) by Def3
                 .= addint.(Sum I,@i1) by GROUP_4:def 2
                 .= Sum I + @i1 by Th14;
   end;

theorem
   Sum <*i1*> = i1
 proof set F = <*i1*>;
  thus Sum F = addint $$ F by Def3 .= i1 by FINSOP_1:12;
 end;

theorem Th22:
 Sum (<*> INT) = 0
 proof set F = <*> INT;
   thus Sum F = addint $$ F by Def3
          .= 0 by Th16,Th17,FINSOP_1:11;
 end;

Lm2: Product(((len(<*> INT)) |->a)|^(<*> INT))=a|^Sum(<*> INT)
 proof
  A1:(<*> the carrier of G)|^(<*> INT)=<*> the carrier of G by GROUP_4:27;
  len(<*> INT)|->a =0 |-> a by FINSEQ_1:32 .=<*> the carrier of G by FINSEQ_2:
72
;
       then Product((len(<*> INT)|->a)|^(<*> INT))=1.G by A1,GROUP_4:11 .=
a|^(Sum(<*> INT)) by Th22,GROUP_1:59;
 hence thesis;
end;

Lm3: for I being FinSequence of INT for w being 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;
 A1:@(@w) =@(w) by GROUP_4:def 2 .=w by GROUP_4:def 2;
 assume A2:Product(((len I)|->a)|^I)=a|^Sum I;
 A3:len((len I) |->a) =len I by FINSEQ_2:69;
 A4:len <*a*> = 1 by FINSEQ_1:57 .= len <*w*> by FINSEQ_1:57;
   Product(((len (I^<*w*>))|->a)|^(I^<*w*>))
     =Product(((len I+1)|->a)|^(I^<*w*>)) by FINSEQ_2:19
    .= Product((((len I)|->a)^<*a*>)|^(I^<*w*>)) by FINSEQ_2:74
    .= Product((((len I)|->a)|^I)^(<*a*>|^<*w*>)) by A3,A4,GROUP_4:25
    .= Product((((len I)|->a)|^I))*Product(<*a*>|^<*@(@w)*>) by A1,GROUP_4:8
    .= Product((((len I)|->a)|^I))*Product(<*a|^(@w)*>) by GROUP_4:28
    .= (a|^Sum I)*(a|^(@w)) by A2,GROUP_4:12
    .= a|^(Sum I+@w) by GROUP_1:63
    .= a|^Sum(I^<*w*>) by Th20;
  hence thesis;
end;

canceled;

theorem Th24:
 for I being 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: P[<*> INT] by Lm2;
 A2: for p being FinSequence of INT for x being Element of INT
      st P[p] holds P[p^<*x*>] by Lm3;
 for p being FinSequence of INT holds P[p] from IndSeqD(A1,A2);
 hence thesis;
end;

    :::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
    ::          Finite groups and their some properties              ::
    :::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

theorem Th25:
 b in gr {a} iff ex j1 st b=a|^j1
proof
 A1:b in gr {a} implies ex j1 st b=a|^j1
  proof
   assume b in gr {a};
   then consider F,I such that A2: len F = len I and
   A3: rng F c= {a} and A4: Product(F |^ I ) = b by GROUP_4:37;
A5:dom ((len F) |-> a) = Seg len F by FINSEQ_2:68
                      .= dom F by FINSEQ_1:def 3;
     for p st p in dom F holds F.p = ((len F)|-> a).p
    proof
     let p;
A6:  dom F = Seg len F by FINSEQ_1:def 3;
     assume A7: p in dom F;
     then F.p in rng F by FUNCT_1:def 5;
     then F.p = a by A3,TARSKI:def 1 .= ((len F)|-> a).p by A6,A7,FINSEQ_2:70;
     hence thesis;
    end;
   then A8: b= Product(((len I) |-> a)|^I) by A2,A4,A5,FINSEQ_1:17
           .= a|^Sum I by Th24;
   take Sum I;
 thus thesis by A8;
end;
   (ex j1 st b=a|^j1) implies b in gr {a}
  proof
   given j1 such that A9: b =a|^j1;
   consider n such that A10: j1 = n or j1 = -n by INT_1:8;
  now per cases by A10;
 suppose A11:j1=n;
      ex F,I st len F = len I & rng F c= {a} & Product(F |^ I) = b
    proof
     take F =(n |-> a);
     A12: len F = n by FINSEQ_2:69 .= len(n |->@ 1) by FINSEQ_2:69;
       F = Seg n --> a by FINSEQ_2:def 2;
     then A13: rng F c= {a} by FUNCOP_1:19;
        Product(F|^(n |->@ 1)) = Product(F|^(len F |->@ 1)) by FINSEQ_2:69
               .=Product(n |-> a) by GROUP_4:31
               .=b by A9,A11,GROUP_4:15;
     hence thesis by A12,A13;
     end;
   hence thesis by GROUP_4:37;
suppose j1 = -n;
     then A14: b"=a|^(-(-n)) by A9,GROUP_1:70 .= a|^n;
       ex F,I st len F = len I & rng F c= {a} & Product(F |^ I) = b"
      proof
       take F =(n |-> a);
       A15: len F = n by FINSEQ_2:69 .= len(n |->@ 1) by FINSEQ_2:69;
         F = Seg n --> a by FINSEQ_2:def 2;
       then A16: rng F c= {a} by FUNCOP_1:19;
          Product(F|^(n |->@ 1)) = Product(F|^(len F |->@ 1)) by FINSEQ_2:69
                 .=Product(n |-> a) by GROUP_4:31 .= b" by A14,GROUP_4:15;
       hence thesis by A15,A16;
     end;
  then b" in gr {a} by GROUP_4:37;
  then b"" in gr {a} by GROUP_2:60;
  hence thesis by GROUP_1:19;
 end;
hence thesis;
end;
hence thesis by A1;
end;

theorem Th26:
 G is finite implies a is_not_of_order_0
  proof
    assume A1:G is finite;
    ex n st n<> 0 & a|^n = 1.G
   proof
    deffunc F(Nat) = a|^$1;
    consider F being FinSequence such that A2: len F = ord G +1 and
    A3: for p st p in Seg (ord G +1) holds F.p = F(p) from SeqLambda;
    A4: dom F = Seg (ord G + 1) by A2,FINSEQ_1:def 3;
    A5: 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 such that A6: x in dom F and A7: F.x=y by FUNCT_1:def 5;
       reconsider n=x as Nat by A6;
       take n;
       thus thesis by A3,A4,A6,A7;
      end;
     rng F c= the carrier of G
    proof
       for x holds x in rng F implies x in the carrier of G
       proof
        let y;
        assume y in rng F;
        then ex n st y= a|^n by A5;
        hence thesis;
       end;
      hence thesis by TARSKI:def 3;
    end;
then reconsider F'=F as Function of Seg (ord G +1),the carrier of G by A4,
FUNCT_2:def 1,RELSET_1:11;
  consider c being finite set such that
A8: c = the carrier of G & ord G = card c by A1,GROUP_1:def 14;
A9:Card ord G = Card the carrier of G by A8,CARD_1:def 11;
A10:Card Seg(ord G+1) = Card (ord G +1) by FINSEQ_1:76;
  ord G < ord G +1 by REAL_1:69;
then Card the carrier of G <` Card Seg (ord G +1) by A9,A10,CARD_1:73;
then consider x,y such that A11:x in Seg (ord G +1) and A12:y in
 Seg (ord G +1)
                and A13:x <> y and A14: F'.x = F'.y by FINSEQ_4:80;
reconsider p=x,n=y as Nat by A11,A12;
   now per cases by A13,REAL_1:def 5;
  suppose A15: n>p;
           then reconsider t = n-p as Nat by INT_1:18;
           reconsider e=0 as Integer;
           take t;
           A16: t <>0 by A15,SQUARE_1:11;
              F'.p =a|^p by A3,A11;
           then a|^n=a|^p by A3,A12,A14;
           then a|^(n+-p)=a|^p *a|^(-p) by GROUP_1:64;
           then a|^(n+-p)=a|^(p+-p) by GROUP_1:64;
           then a|^t =a|^(p+-p) by XCMPLX_0:def 8;
           then a|^t=a|^e by XCMPLX_0:def 6;
           then a|^t=1.G by GROUP_1:59;
      hence thesis by A16;
   suppose A17: p>n;
            then reconsider t = p-n as Nat by INT_1:18;
            take t;
            reconsider e=0 as Integer;
            A18: t <>0 by A17,SQUARE_1:11;
               F'.p =a|^p by A3,A11;
            then a|^n=a|^p by A3,A12,A14;
            then a|^(p+-n)=a|^n *a|^(-n) by GROUP_1:64;
            then a|^(p+-n)=a|^(n+-n) by GROUP_1:64;
            then a|^t =a|^(n+-n) by XCMPLX_0:def 8;
            then a|^t=a|^e by XCMPLX_0:def 6;
            then a|^t=1.G by GROUP_1:59;
      hence thesis by A18;
    end;
   hence thesis;
  end;
 hence thesis by GROUP_1:def 10;
end;

theorem Th27:
 G is finite implies ord a = ord gr {a}
 proof
  assume A1:G is finite;
  then A2:gr {a} is finite by GROUP_2:48;
  deffunc F(Nat) = a|^$1;
  consider F being FinSequence such that A3: len F = ord a and
  A4:  for p st p in Seg ord a holds F.p = F(p) from SeqLambda;
  A5: dom F = Seg ord a by A3,FINSEQ_1:def 3;
    a is_not_of_order_0 by A1,Th26;
  then A6:ord a <> 0 by GROUP_1:def 11;
  then A7:ord a >0 by NAT_1:19;
   A8: a in rng F
    proof
        ex x st x in dom F & F.x=a
        proof
         set x'=1;
         A9:x' in dom F
           proof
              (ord a)+x' > 0+x' by A7,REAL_1:53;
            then (ord a) >= x' by NAT_1:38;
            hence thesis by A5,FINSEQ_1:3;
           end;
         then F.x'=a|^x' by A4,A5 .=a by GROUP_1:44;
         hence thesis by A9;
        end;
     hence thesis by FUNCT_1:def 5;
   end;
A10: rng F = the carrier of gr {a}
 proof
   A11: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 such that A12: x in dom F and A13: F.x=y by FUNCT_1:def 5
;
      reconsider n=x as Nat by A12;
      take n;
      thus thesis by A4,A5,A12,A13;
     end;
A14: rng F c= the carrier of gr {a}
    proof
       for x holds x in rng F implies x in the carrier of gr {a}
      proof
       let y;
       assume y in rng F;
       then consider n such that A15:y= a|^n by A11;
         y in gr {a} by A15,Th25;
       hence thesis by RLVECT_1:def 1;
      end;
     hence thesis by TARSKI:def 3;
   end;
  the carrier of gr {a} c= rng F
 proof
    ex H being strict Subgroup of G st the carrier of H = rng F
   proof
     reconsider car=rng F as non empty set by A8;
     A16:dom(the mult of G)=
     [:the carrier of G,the carrier of G:] by FUNCT_2:def 1;
       the carrier of gr {a} c= the carrier of G by GROUP_2:def 5;
     then A17: car c= the carrier of G by A14,XBOOLE_1:1;
     then [:car,car:] c= [:the carrier of G,the carrier of G:] by ZFMISC_1:119
;
 then A18:dom((the mult of G)|[:car,car:])=[:car,car:] by A16,RELAT_1:91;
       rng((the mult of G)|[:car,car:]) c= car
       proof
           for y st y in rng((the mult of G)|[:car,car:]) holds y in car
            proof
              set f=(the mult of G)|[:car,car:];
              let y;
              assume y in rng(f);
              then consider x such that A19:x in dom(f) and
              A20: f.x=y by FUNCT_1:def 5;
              consider xp,yp such that A21:[xp,yp]=x
               by A18,A19,ZFMISC_1:102;
                xp in car by A18,A19,A21,ZFMISC_1:106;
              then consider p such that A22:  xp = a|^p by A11;
                yp in car by A18,A19,A21,ZFMISC_1:106;
              then consider s such that A23:  yp = a|^s by A11;
              A24:  y = (the mult of G).[a|^p,a|^s]
                        by A19,A20,A21,A22,A23,FUNCT_1:70
                      .= (the mult of G).(a|^p,a|^s) by BINOP_1:def 1
                      .= a|^p*(a|^s) by VECTSP_1:def 10
                      .= a|^(p+s) by GROUP_1:48;
                a|^(p+s) in car
               proof
                  ex x st x in dom F & F.x=a|^(p+s)
                 proof
                    per cases by NAT_1:18;
                     suppose A25:p+s=0;
                          A26:ord a in dom F by A5,A6,FINSEQ_1:5;
                          A27:a|^(p+s)=1.G by A25,GROUP_1:43
                          .= a|^(ord a) by GROUP_1:82 .= F.ord a by A4,A5,A26;
                          take ord a;
                       thus thesis by A5,A6,A27,FINSEQ_1:5;
                     suppose p+s>0;
                     thus thesis
                      proof
                           set t=(p+s) mod (ord a);
                           A28:t < ord a by A7,NAT_1:46;
                        now per cases by NAT_1:18;
                         suppose A29:t=0;
                              A30:ord a in dom F by A5,A6,FINSEQ_1:5;
  A31:a|^(p+s)=a|^((ord a)*((p+s) div (ord a)) + ((p+s) mod (ord a))) by A7,
NAT_1:47
    .=a|^((ord a)*((p+s) div (ord a)))*(a|^ ((p+s) mod (ord a))) by GROUP_1:48
    .=a|^(ord a)|^((p+s) div (ord a))*(a|^ ((p+s) mod (ord a))) by GROUP_1:50
    .=(1.G)|^((p+s) div (ord a))*(a|^ ((p+s) mod (ord a))) by GROUP_1:82
    .=(1.G) *(a|^ ((p+s) mod (ord a))) by GROUP_1:42
    .=a|^0 by A29,GROUP_1:def 4 .= 1.G by GROUP_1:43
    .= a|^(ord a) by GROUP_1:82 .= F.ord a by A4,A5,A30;
     take x = ord a;
     thus x in dom F & F.x=a|^(p+s) by A5,A6,A31,FINSEQ_1:5;
                          suppose t>0;
                             then t+1 > 0+1 by REAL_1:53;
                             then A32:t >= 1 by NAT_1:38;
                             take x = t;
                             A33:t in dom F by A5,A28,A32,FINSEQ_1:3;
    a|^(p+s)=a|^((ord a)*((p+s) div (ord a)) + ((p+s) mod (ord a))) by A7,NAT_1
:47
    .=a|^((ord a)*((p+s) div (ord a))) *(a|^ ((p+s) mod (ord a))) by GROUP_1:48
    .=a|^(ord a)|^((p+s) div (ord a)) *(a|^ ((p+s) mod (ord a))) by GROUP_1:50
    .=(1.G)|^((p+s) div (ord a)) *(a|^ ((p+s) mod (ord a))) by GROUP_1:82
    .=(1.G) *(a|^ ((p+s) mod (ord a))) by GROUP_1:42
    .=a|^ ((p+s) mod (ord a)) by GROUP_1:def 4;
         hence x in dom F & F.x=a|^(p+s) by A4,A5,A33;
       end;
   hence thesis;
         end;
            thus thesis;
                    end;
       hence thesis by FUNCT_1:def 5;
     end;
   hence thesis by A24;
   end;
hence thesis by TARSKI:def 3;
  end;
 then reconsider op=(the mult of G)|[:car,car:] as BinOp of car by A18,FUNCT_2:
def 1,RELSET_1:11;
 set H=HGrStr(#car,op#);
   H is Group
 proof
A34: for f,g being Element of H ,
        f',g' being Element of G
    st f = f' & g = g' holds f'*g' = f*g
 proof
  let f,g be Element of H;
  let f' ,g' be Element of G;
  assume A35: f = f' & g =g';
  set A = [:car,car:];
  A36:f*g = ((the mult of G) | A).(f,g) by VECTSP_1:def 10
       .= ((the mult of G) | A).[f,g] by BINOP_1:def 1;
    f'*g' = (the mult of G).(f',g') by VECTSP_1:def 10
         .= (the mult of G).[f',g'] by BINOP_1:def 1;
  hence thesis by A35,A36,FUNCT_1:72;
  end;

 A37:for f,g,h being Element of H holds (f * g) * h = f * (g * h
)
 proof
  let f,g,h be Element of H;
  reconsider f'=f as Element of G by A17,TARSKI:def 3;
  reconsider g'=g as Element of G by A17,TARSKI:def 3;
  reconsider h'=h as Element of G by A17,TARSKI:def 3;
  A38:  f'*g' = f*g by A34;
  A39:  g * h = g' * h' by A34;
    (f*g)*h =(f'*g')*h' by A34,A38 .= f'*(g'*h') by VECTSP_1:def 16
 .=f*(g*h) by A34,A39;
  hence thesis;
 end;
    ex e being Element of H st
    for h being Element of H holds
     h * e = h & e * h = h &
     ex g being Element of H st h * g = e & g * h = e
     proof
        a|^(ord a) in car
       proof
          ex x st x in dom F & F.x=a|^(ord a)
          proof
           set x'=(ord a);
           A40: x' in Seg ord a by A6,FINSEQ_1:5;
           then F.x'=a|^x' by A4;
           hence thesis by A5,A40;
          end;
        hence thesis by FUNCT_1:def 5;
     end;
 then reconsider e=1.G as Element of H by GROUP_1:82;
 take e;
   for h being Element of H holds
 h * e = h & e * h = h &
 ex g being Element of H st h * g = e & g * h = e
  proof
   let h be Element of H;
   reconsider h'=h as Element of G by A17,TARSKI:def 3;
   thus h * e = h
    proof
       h*e = h' *(1.G) by A34 .= h' by GROUP_1:def 4;
     hence thesis;
    end;
   thus e * h = h
    proof
       e*h = (1.G)*h' by A34 .= h' by GROUP_1:def 4;
     hence thesis;
    end;
   thus ex g being 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 such that A41: x in dom F and A42: F.x=h by FUNCT_1:def 5;
        reconsider n=x as Nat by A41;
        take n;
        thus thesis by A4,A5,A41,A42,FINSEQ_1:3;
       end;
     then consider n such that A43:h=a|^n and A44: ord a >= n;
       a|^(ord a - n) in car
      proof
         ex x st x in dom F & F.x =a|^(ord a - n)
        proof
          per cases by A44,REAL_1:def 5;
              suppose ord a = n;
                   then A45: ord a - n =0 by XCMPLX_1:14;
                   set x = ord a;
                   A46: x in dom F by A5,A6,FINSEQ_1:5;
                   then F.x=a|^x by A4,A5 .= 1.G by GROUP_1:82
                   .= a|^(ord a - n) by A45,GROUP_1:43;
                  hence thesis by A46;
              suppose A47:ord a > n;
                      then reconsider x = ord a - n as Nat by INT_1:18;
                      take x;
                       x in Seg ord a
                        proof
                         reconsider r1=ord a ,r2=n as Real;
                         A48:x >= 1
                          proof
                             r1 - r2 > r2 -r2 by A47,REAL_1:54;
                           then r1-r2 > 0 by XCMPLX_1:14;
                           then x >= 0 +1 by NAT_1:38;
                           hence x >= 1;
                          end;
                        x <= ord a
                        proof
                           r1 <= r1 + r2 by NAT_1:29;
                         hence thesis by REAL_1:86;
                        end;
                      hence thesis by A48,FINSEQ_1:3;
                     end;
                hence thesis by A3,A4,FINSEQ_1:def 3;
          end;
        hence thesis by FUNCT_1:def 5;
      end;
       then reconsider g =a|^(ord a - n) as Element of H;
       A49:n+(ord a-n) =ord a
        proof
         reconsider n'=n ,z = ord a as Integer;
         reconsider n''=n' ,z' =z as Real;
           n+(ord a-n) = (z' + n'') - n'' by XCMPLX_1:29
         .= z' + (n'' - n'') by XCMPLX_1:29 .= z'+0 by XCMPLX_1:14
         .= z';
         hence thesis;
       end;
     A50: h * g = e
       proof
           h * g =a|^n *(a|^(ord a - n)) by A34,A43
               .=a|^(ord a) by A49,GROUP_1:64
               .= e by GROUP_1:82;
           hence thesis;
       end;
       g * h = e
        proof
           g * h =a|^(ord a - n) * (a|^n) by A34,A43
               .=a|^(ord a) by A49,GROUP_1:65
               .= e by GROUP_1:82;
           hence thesis;
        end;
       hence thesis by A50;
           end;
            thus thesis;
           end;
     hence thesis;
           end;
 hence thesis by A37,GROUP_1:5;
 end;
then reconsider H1=H as Group;
  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 A14,XBOOLE_1:1;
then H1 is Subgroup of G by GROUP_2:def 5;
hence thesis;
end;
then consider H being strict Subgroup of G such that
A51: the carrier of H = rng F;
  {a} c= the carrier of H by A8,A51,ZFMISC_1:37;
then gr {a} is Subgroup of H by GROUP_4:def 5;
hence the carrier of gr {a} c= rng F by A51,GROUP_2:def 5;
end;
hence thesis by A14,XBOOLE_0:def 10;
end;
  F is one-to-one
 proof
  let x,y;
  assume that A52: x in dom F and A53: y in dom F and A54: F.x = F.y
             and A55:x<>y;
  reconsider p=x as Nat by A52;
  reconsider s=y as Nat by A53;
  reconsider s'=s,p'=p,z= ord a as Real;
  A56:F.p=a|^p by A4,A5,A52;
  A57:F.s=a|^s by A4,A5,A53;
   per cases;
       suppose A58:p<=s;
         then A59:p<s by A55,REAL_1:def 5;
         reconsider r1=s-p as Nat by A58,INT_1:18;
         A60: r1=s+-p by XCMPLX_0:def 8;
           1.G=a|^s*(a|^p)" by A54,A56,A57,GROUP_1:def 5;
         then a|^0=a|^s*(a|^p)" by GROUP_1:43;
         then a|^0=a|^s*(a|^(-p)) by GROUP_1:71;
         then a|^0=a|^(s+(-p)) by GROUP_1:64;
         then A61:1.G=a|^r1 by A60,GROUP_1:43;
         A62: r1 <> 0 by A59,SQUARE_1:11;
         A63:p >0
          proof
              p>=1 by A5,A52,FINSEQ_1:3;
            hence thesis by AXIOMS:22;
          end;
         A64:r1 < ord a
            proof
             A65: s'<=z by A5,A53,FINSEQ_1:3;
               z<z+p' by A63,REAL_1:69;
             then s'<z+p' by A65,AXIOMS:22;
             then s'-p'<z+p'-p' by REAL_1:54;
             then s'-p'<z+p'+-p' by XCMPLX_0:def 8;
             then s'-p'<z+(p'+-p') by XCMPLX_1:1;
             then s'-p'<z+0 by XCMPLX_0:def 6;
             hence thesis;
            end;
           a is_not_of_order_0 by A1,Th26;
       hence thesis by A61,A62,A64,GROUP_1:def 11;
   suppose A66:s<=p;
        then A67:s<p by A55,REAL_1:def 5;
        reconsider r2=p-s as Nat by A66,INT_1:18;
        A68: r2=p+-s by XCMPLX_0:def 8;
          1.G=a|^p*(a|^s)" by A54,A56,A57,GROUP_1:def 5;
        then a|^0=a|^p*(a|^s)" by GROUP_1:43;
        then a|^0=a|^p*(a|^(-s)) by GROUP_1:71;
        then a|^0=a|^(p+(-s)) by GROUP_1:64;
        then A69:1.G=a|^r2 by A68,GROUP_1:43;
        A70: r2 <> 0 by A67,SQUARE_1:11;
        A71:s >0
         proof
             s>=1 by A5,A53,FINSEQ_1:3;
           hence thesis by AXIOMS:22;
         end;
       A72:r2 < ord a
         proof
          A73: p'<=z by A5,A52,FINSEQ_1:3;
            z<z+s' by A71,REAL_1:69;
          then p'<z+s' by A73,AXIOMS:22;
          then p'-s'<z+s'-s' by REAL_1:54;
          then p'-s'<z+s'+-s' by XCMPLX_0:def 8;
          then p'-s'<z+(s'+-s') by XCMPLX_1:1;
          then p'-s'<z+0 by XCMPLX_0:def 6;
          hence thesis;
         end;
        a is_not_of_order_0 by A1,Th26;
     hence thesis by A69,A70,A72,GROUP_1:def 11;
end;
then A74: Seg ord a,the carrier of gr {a} are_equipotent by A5,A10,WELLORD2:def
4;
   consider ca being finite set such that
A75: ca = the carrier of gr {a} & ord gr {a} = card ca by A2,GROUP_1:def 14;
    reconsider So = Seg ord a as finite set;
      card So = card ca by A74,A75,CARD_1:21;
hence thesis by A75,FINSEQ_1:78;
end;

theorem Th28:
 G is finite implies ord a divides ord G
proof
 assume A1: G is finite;
 then ord a = ord gr {a} by Th27;
 hence ord a divides ord G by A1,GROUP_2:178;
end;

theorem Th29:
 G is finite implies a|^ord G = 1.G
proof
 assume G is finite;
 then ord a divides ord G by Th28;
 then consider t being Nat such that
 A1: ord G = ord a * t by NAT_1:def 3;
   a|^ord G = a |^ ord a |^ t by A1,GROUP_1:50
         .= (1.G) |^ t by GROUP_1:82 .= 1.G by GROUP_1:42;
 hence thesis;
end;

theorem Th30:
 G is finite implies (a|^n)" = a|^(ord G - (n mod ord G))
  proof
   assume A1: G is finite;
   set q = ord G;
   set p'=n mod q;
     q >=1 by A1,GROUP_1:90;
   then A2: q > 0 by AXIOMS:22;
   then n mod q <=q by NAT_1:46;
   then reconsider q'=q -( n mod q) as Nat by INT_1:18;
     a|^n*(a|^(q-(n mod q)))=a|^(n+q') by GROUP_1:48
   .= a|^((q*(n div q)+(n mod q))+q') by A2,NAT_1:47
   .= a|^(q*(n div q)+(q'+(n mod q))) by XCMPLX_1:1
   .= a|^(q*(n div q)+((q +(-(n mod q)))+(n mod q))) by XCMPLX_0:def 8
   .= a|^(q*(n div q)+(q +(-p'+p'))) by XCMPLX_1:1
   .= a|^(q*(n div q)+q +(-p'+p')) by XCMPLX_1:1
   .= a|^(q*(n div q)+q)*(a|^(-p'+p')) by GROUP_1:64
   .= a|^(q*(n div q)+q)*(a|^(-p')*(a|^p')) by GROUP_1:65
   .= a|^(q*(n div q)+q)*((a|^p')"*(a|^p')) by GROUP_1:71
   .= a|^(q*(n div q)+q)*(1.G) by GROUP_1:def 5
   .= a|^(q*(n div q)+q*1) by GROUP_1:def 4
   .= a|^(q*(n div q+1)) by XCMPLX_1:8
   .= a|^q|^(n div q+1) by GROUP_1:50
   .= (1.G)|^(n div q+1) by A1,Th29
   .= 1.G by GROUP_1:42;
   hence thesis by GROUP_1:20;
  end;

theorem Th31:
 for G being strict Group holds
  ord G > 1 implies ex a being Element of G st a <> 1.G
  proof let G be strict Group;
   assume that A1: ord G > 1 and
   A2: for a being Element of G holds a = 1.G;
    for a being 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 by RLVECT_1:def 1;
     end;
   then G = (1).G by GROUP_2:71;
   hence contradiction by A1,GROUP_2:81;
 end;

theorem
   for G being strict Group holds
  G is finite & ord G = p & p is prime implies
   for H being strict Subgroup of G holds H = (1).G or H = G
 proof let G be strict Group;
  assume that A1: G is finite and A2: ord G = p and A3: p is prime;
  let H be strict Subgroup of G;
  A4:H is finite by A1,GROUP_2:48;
    ord H divides p by A1,A2,GROUP_2:178;
  then ord H = 1 or ord H = p by A3,INT_2:def 5;
  hence thesis by A1,A2,A4,GROUP_2:82,85;
 end;

theorem Th33:
 HGrStr(#INT,addint#) is associative Group-like
  proof
   set G = HGrStr (# INT, addint #);
   A1: now let h,g be Element of G, A,B be Integer;
   assume h = A & g = B;
   hence h * g = addint.(A,B) by VECTSP_1:def 10 .= A + B by Th14;
 end;
 thus for h,g,f being 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 by INT_1:12;
     A2: h * g = A + B by A1;
     A3: g * f = B + C by A1;
 thus (h * g) * f = A + B + C by A1,A2
                 .= A + (B + C) by XCMPLX_1:1
                 .= h * (g * f) by A1,A3;
   end;
  reconsider e=0 as Element of G by INT_1:12;
  take e;
  let h be Element of G;
  reconsider A = h as Integer by INT_1:12;
  thus h * e = A + 0 by A1
            .= h;
  thus e * h = 0 + A by A1
            .= h;
  reconsider g = - A as Element of G by INT_1:12;
  take g;
  thus h * g = A + (- A) by A1
            .= e by XCMPLX_0:def 6;
  thus g * h = (- A) + A by A1
             .= e by XCMPLX_0:def 6;
  end;

 definition
 func INT.Group -> strict Group equals :
 Def4: HGrStr(#INT,addint#);
       coherence by Th33;
 end;

definition let n such that A1:n > 0;
 func addint(n) -> BinOp of Segm(n) means
 :Def5: for k,l being Element of Segm(n) holds
  it.(k,l) = (k+l) mod n;
 existence
  proof
    defpred P[Element of Segm n,Element of Segm n,set] means
      $3 = ($1+$2) mod n;
    A2: for k,l being Element of Segm(n) ex c being Element of Segm(n) st
      P[k,l,c]
       proof
       let k,l be Element of Segm(n);
       reconsider k'=k,l'=l as Nat;
          ((k'+l') mod n) < n by A1,NAT_1:46;
        then reconsider c = (k'+l') mod n as Element of Segm(n) by A1,Th10;
       take c;
       thus thesis;
       end;
       ex o being BinOp of Segm n st
         for a,b being Element of Segm n holds
           P[a,b,o.(a,b)] from BinOpEx(A2);
       hence thesis;
         end;
 uniqueness
   proof
        let i1,i2 be BinOp of Segm(n) such that
      A3:for k,l being Element of Segm(n) holds
        i1.(k,l)=((k+l) mod n) and
      A4:for k,l being Element of Segm(n) holds
        i2.(k,l)=((k+l) mod n);
        for k,l being 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 by BINOP_1:2;
         end;
end;

theorem Th34:
 for n st n > 0 holds HGrStr(#Segm(n),addint(n)#) is associative Group-like
  proof
   let n;
   assume A1:n>0;
   set G = HGrStr (# Segm(n), addint(n) #);
   A2: now let h,g be Element of G, A,B be Element of Segm(n);
   assume h = A & g = B;
   hence h * g = (addint(n)).(A,B) by VECTSP_1:def 10
              .= (A + B) mod n by A1,Def5;
   end;
   thus for h,g,f being 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);
     A3: h * g = (A + B) mod n by A2;
     A4: g * f = (B + C) mod n by A2;
     thus (h * g) * f = (((A + B) mod n) + C) mod n by A2,A3
                     .= ((A + B) + C) mod n by Th2
                     .=(A + (B + C)) mod n by XCMPLX_1:1
                     .=(A + ((B + C) mod n)) mod n by Th2
                     .= h * (g * f) by A2,A4;
     end;
    reconsider e=0 as Element of G by A1,Th10;
    take e;
    let h be Element of G;
    reconsider A = h as Element of Segm(n);
reconsider A as Nat;
    A5:A < n by A1,Th10;
  thus h * e = (A + 0) mod n by A2
            .= h by A5,Th4;
  thus e * h = (0 + A) mod n by A2
              .= h by A5,Th4;
consider p such that A6: n=A+p by A5,NAT_1:28;
A7:     p <= n by A6,NAT_1:37;
       (p mod n) < n by A1,NAT_1:46;
     then reconsider g = p mod n as Element of G by A1,Th10;
     take g;
     reconsider B=g as Element of Segm(n);
 thus h * g =e
    proof
       now per cases by A7,REAL_1:def 5;
       suppose A8:p = n;
             then n + 0 =A + n by A6;
             then A9:A = 0 by XCMPLX_1:2;
               h * g = (A +B) mod n by A2
                  .= (0 * n) mod n by A8,A9,Th5
                  .= e by GROUP_4:101;
                hence thesis;
       suppose A10:p < n;
              h * g = (A +B) mod n by A2
                 .= n mod n by A6,A10,Th4
                 .= e by Th5;
             hence thesis;
           end;
         hence thesis;
        end;
thus g * h = e
  proof
     now per cases by A7,REAL_1:def 5;
      suppose A11:p = n;
            then n + 0 =A + n by A6;
            then A = 0 by XCMPLX_1:2;
            then g * h = (n mod n + 0) mod n by A2,A11
                  .= (0 * n) mod n by Th5
                  .= e by GROUP_4:101;
                  hence thesis;
      suppose A12:p < n;
                  g * h = (A + B) mod n by A2
                     .=n mod n by A6,A12,Th4
                     .= e by Th5;
                hence thesis;
             end;
         hence thesis;
      end;
    end;

definition let n such that A1: n > 0;
 func INT.Group(n) -> strict Group equals
:Def6: HGrStr(#Segm(n),addint(n)#);
coherence by A1,Th34;
end;

theorem Th35:
 1.INT.Group = 0
  proof
  A1: now let h,g be Element of INT.Group, A,B be Integer;
  assume h = A & g = B;
  hence h * g = addint.(A,B) by Def4,VECTSP_1:def 10
             .= A + B by Th14;
  end;
  reconsider e = 0 as Element of INT by INT_1:12;
  reconsider e as Element of INT.Group by Def4;
     for h being Element of INT.Group holds h * e = h & e * h =
h
   proof
    let h be Element of INT.Group;
    reconsider A = h as Integer by Def4,INT_1:12;
    A2: h * e = A + 0 by A1
             .= h;
          e * h = 0 + A by A1
               .= h;
    hence thesis by A2;
    end;
 hence thesis by GROUP_1:10;
 end;

theorem Th36:
 for n st n>0 holds 1.INT.Group(n) = 0
  proof
   let n;
   assume A1: n>0;
   then A2: INT.Group(n) = HGrStr(#Segm(n),addint(n)#) by Def6;

   A3: now let h,g be Element of INT.Group(n),
              A,B be Element of Segm(n);
   assume h = A & g = B;
   hence h * g = (addint(n)).(A,B) by A2,VECTSP_1:def 10
              .= (A + B) mod n by A1,Def5;
   end;
   reconsider e = 0 as Element of Segm(n) by A1,Th10;
   reconsider e as Element of INT.Group(n) by A2;
     for h being 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) by A2;
    reconsider A as Nat;
    A4:A < n by A1,Th10;
    A5: h * e = (A + 0) mod n by A3
             .= h by A4,Th4;
       e * h = (0 + A) mod n by A3
             .= h by A4,Th4;
  hence thesis by A5;
 end;
hence thesis by GROUP_1:10;
end;

definition
 let h be Element of INT.Group;
 func @'h -> Integer equals :
 Def7: h;
  coherence by Def4,INT_1:12;
end;

definition
 let h be Integer;
 func @'h -> Element of INT.Group equals
    h;
 coherence by Def4,INT_1:12;
end;

theorem Th37:
 for h being Element of INT.Group holds h" = -@'h
  proof
   A1: now let h,g be Element of INT.Group, A,B be Integer;
   assume h = A & g = B;
   hence h * g = addint.(A,B) by Def4,VECTSP_1:def 10
              .= A + B by Th14;
   end;
  let h be Element of INT.Group;
   A2:h=@'h by Def7;
   reconsider g=-@'h as Element of INT.Group by Def4,INT_1:12;
     h *g =@'h + -@'h by A1,A2 .=1.INT.Group by Th35,XCMPLX_0:def 6;
   hence thesis by GROUP_1:20;
   end;

 reserve G1 for Subgroup of INT.Group,
         h for Element of INT.Group;
Lm4:now let h,g be Element of INT.Group, A,B be Integer;
     assume h = A & g = B;
     hence h * g = addint.(A,B) by Def4,VECTSP_1:def 10
           .= A + B by Th14;
end;

theorem Th38:
 for h st h=1 holds for k holds h|^k = k
  proof
  let h;
  assume A1:h=1;
  defpred P[Nat] means h|^$1=$1;
  h|^0=0 by Th35,GROUP_1:43; then
A2: P[0];
 A3: for k st P[k] holds P[k+1]
  proof
    let k; assume h|^k = k;
    then h|^k * h = k + 1 by A1,Lm4;
    hence thesis by GROUP_1:49;
  end;
   for k holds P[k] from Ind(A2,A3);
   hence thesis;
  end;

theorem Th39:
 for h,j1 st h=1 holds j1 = h |^ j1
  proof
   let h,j1;
   assume A1:h=1;
   consider k such that A2:j1 = k or j1 = -k by INT_1:8;
      now per cases by A2;
    suppose j1=k;
        hence thesis by A1,Th38;
    suppose A3: j1=-k;
         reconsider k'=k as Integer;
         reconsider k' as Element of INT.Group by Def4,INT_1:12
;
           h|^j1 = (h|^k)" by A3,GROUP_1:71
         .= (k')" by A1,Th38 .= -@'k' by Th37 .= j1 by A3,Def7;
         hence thesis;
      end;
    hence thesis;
  end;

       :::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
       ::             Definition of cyclic group                  ::
       :::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

Lm5:
ex a being Element of INT.Group
  st the HGrStr of INT.Group = gr {a}
proof
 reconsider h = 1 as Element of INT by INT_1:12;
 reconsider h as Element of INT.Group by Def4;
 take h;
   {h} c= the carrier of (Omega).INT.Group &
 (for G1 being strict Subgroup of INT.Group
  st {h} c= the carrier of G1 holds
 (Omega).INT.Group is Subgroup of G1 )
  proof
   A1: {h} c= the carrier of INT.Group;
      for G1 st {h} c= the carrier of G1 holds (Omega).
INT.Group is Subgroup of G1
    proof
      let G1;
      assume A2:{h} c= the carrier of G1;
        the carrier of (Omega).INT.Group c= the carrier of G1
      proof
        let x;
        assume that A3: x in the carrier of (Omega).INT.Group and
        A4: not x in the carrier of G1;
          x in (Omega).INT.Group by A3,RLVECT_1:def 1;
        then x in INT.Group by GROUP_2:def 8;
        then x in INT by Def4,RLVECT_1:def 1;
        then reconsider x'=x as Integer by INT_1:12;
          h in {h} by TARSKI:def 1;
        then reconsider h''=h as Element of G1 by A2;
        A5: (h'')|^x' in the carrier of G1;
          (h'')|^x'=h|^x' by GROUP_4:4;
        hence contradiction by A4,A5,Th39;
      end;
hence thesis by GROUP_2:66;
end;
hence thesis by A1,GROUP_2:def 8;
end;
then (Omega).INT.Group = gr {h} by GROUP_4:def 5;
hence thesis by GROUP_2:def 8;
end;

definition let IT be Group;
 attr IT is cyclic means
:Def9:  ex a being Element of IT st the HGrStr of IT=gr {a};
end;

definition
 cluster strict cyclic Group;
  existence
   proof INT.Group is cyclic by Def9,Lm5;
    hence thesis;
   end;
end;

theorem Th40:
 (1).G is cyclic
 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;
    {PG} c= the carrier of (Omega).(1).G &
  ( for G1 being strict Subgroup of (1).G st {PG} c= the carrier of G1 holds
  (Omega).(1).G is Subgroup of G1 )
   proof
A1:    {PG} = the carrier of (1).G by GROUP_2:def 7;
       ( for G1 being 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 A2:{PG} c= the carrier of G1;
           the carrier of (Omega).(1).G =the carrier of (1).G by GROUP_2:def 8;
         then the carrier of (Omega).
(1).G c=the carrier of G1 by A2,GROUP_2:def 7;
         hence thesis by GROUP_2:66;
       end;
     hence thesis by A1,GROUP_2:def 8;
   end;
  then (Omega).(1).G = gr {PG} by GROUP_4:def 5;
  hence thesis by GROUP_2:def 8;
 end;

theorem Th41:
 G is cyclic Group iff ex a being Element of G st
  for b being Element of G ex j1 st b=a|^j1
 proof
   thus G is cyclic Group implies ex a being Element of G st
    for b being Element of G ex j1 st b=a|^j1
     proof
      assume G is cyclic Group;
      then consider a being Element of G such that
       A1: the HGrStr of G = gr {a} by Def9;
      take a;
        for b being Element of G ex j1 st b=a|^j1
       proof
        let b be Element of G;
          b in gr {a} by A1,RLVECT_1:def 1;
        hence thesis by Th25;
       end;
     hence thesis;
    end;
  thus (ex a being Element of G st
    for b being Element of G
    ex j1 st b = a|^j1) implies G is cyclic Group
     proof
      given a being Element of G such that
      A2:for b being Element of G
      ex j1 st b = a|^j1;
        for b being 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 Th25;
       end;
      then the HGrStr of G = gr {a} by GROUP_2:71;
      hence thesis by Def9;
    end;
end;

theorem Th42:
 G is finite implies (G is cyclic Group iff
  ex a being Element of G st
   for b being Element of G ex n st b=a|^n)
 proof
  assume A1: G is finite;
  thus G is cyclic Group implies
  ex a being Element of G st
  for b being Element of G ex n st b=a|^n
     proof
       assume G is cyclic Group;
       then consider a being Element of G such that
       A2: for b being Element of G ex j2 st b=a|^j2
        by Th41;
       take a;
          let b be Element of G;
          consider j2 such that A3: b = a|^j2 by A2;
          consider n such that A4:j2=n or j2=-n by INT_1:8;
          per cases by A4;
            suppose j2=n; hence thesis by A3;
            suppose A5:j2=-n;
                  ord G >=1 by A1,GROUP_1:90;
                then ord G > 0 by AXIOMS:22;
                then n mod ord G <=ord G by NAT_1:46;
     then reconsider q'=ord G -( n mod ord G) as Nat by INT_1:18;
                take q';
                  b=(a|^n)" by A3,A5,GROUP_1:71
                .= a|^q' by A1,Th30;
  hence thesis;
  end;
      given a being Element of G such that
      A6:  for b being Element of G ex n st b=a|^n;
        for b being Element of G ex j2 st b=a|^j2
        proof
         let b be Element of G;
         consider n such that A7:b=a|^n by A6;
         reconsider n as Integer;
         take n;
         thus thesis by A7;
        end;
   hence thesis by Th41;
 end;

theorem Th43:
 for G being strict Group holds
  G is finite implies
   ( G is cyclic Group iff
      ex a being Element of G st ord a =ord G )
 proof let G be strict Group;
  assume A1: G is finite;
    thus G is cyclic Group implies
     ex a being Element of G st ord a =ord G
      proof
       assume G is cyclic Group;
       then consider a being Element of G such that
       A2: G = gr {a} by Def9;
       take a;
       thus thesis by A1,A2,Th27;
      end;
       given a being Element of G such that A3:ord a =ord G;
          ex a being Element of G st G = gr {a}
        proof
         consider a being Element of G such that
         A4: ord a = ord G by A3;
         take a;
           ord gr {a} = ord G by A1,A4,Th27;
         hence thesis by A1,GROUP_2:85;
        end;
      hence thesis by Def9;
 end;

theorem
   for H being strict Subgroup of G holds
  G is finite & G is cyclic Group implies
   H is cyclic Group
 proof let H be strict Subgroup of G;
  assume that A1: G is finite and A2:G is cyclic Group;
  consider a such that
  A3: for b being Element of G ex n st b = a|^n by A1,A2,Th42;
  A4: H is finite by A1,GROUP_2:48;
  then A5: ord H >= 1 by GROUP_1:90;
  per cases by A5,REAL_1:def 5;
     suppose ord H =1;
          then H = (1).G by A4,GROUP_2:82;
          hence thesis by Th40;
     suppose ord H > 1;
          then consider h being Element of H such that
          A6:h <>1.H by Th31;
          defpred P[Nat] means
            $1 > 0 & a|^$1 is Element of H;
          h is Element of G by GROUP_2:51;
          then consider n such that A7: h = a|^n by A3;
          n <> 0
           proof
            assume n = 0;
            then h = 1.G by A7,GROUP_1:59 .= 1.H by GROUP_2:53;
            hence contradiction by A6;
           end;
            then n > 0 by NAT_1:19;
           then A8:  ex n st P[n] by A7;
       ex h1 being Element of H st
       for b being Element of H ex s st b = h1|^s
      proof
       ex k st P[k] & for n st P[n] holds k <= n from Min(A8); then
       consider n such that
       A9: (n>0 & a|^n is Element of H) and
       A10: for k st
       (k>0 & a|^k is Element of H) holds n <= k;
       consider h1 being Element of H such that
       A11: h1 = a|^n by A9;
       take h1;
          for b being Element of H ex s st b = h1|^s
       proof
         let b be Element of H;
           b is Element of G by GROUP_2:51;
         then consider p such that A12: b = a|^p by A3;
         consider s,r such that A13: p = (n*s) + r and
         A14:r < n by A9,NAT_1:42;
         A15:  r =0
          proof
           assume r<>0;
           then A16: r >0 by NAT_1:19;
A17:      a|^p = a|^(n*s) * (a|^r) by A13,GROUP_1:48;
              h1|^s=a|^n|^s by A11,GROUP_4:3;
     then (h1|^s)"=(a|^n|^s)" by GROUP_2:57 .= (a|^(n * s ))" by GROUP_1:50;
          then reconsider g= (a|^(n*s))" as Element of H;
          reconsider b=a|^p as Element of H by A12;
             (a|^(n*s))" * (a|^p)
          = ((a|^(n*s))" *(a|^(n*s)))*(a|^r) by A17,VECTSP_1:def 16
          .= 1.G *(a|^r) by GROUP_1:def 5 .= a|^ r by GROUP_1:def 4;
          then g*b = a|^r by GROUP_2:52;
          hence contradiction by A10,A14,A16;
        end;
     take s;
       a|^p = a|^n|^s by A13,A15,GROUP_1:50 .= h1|^s by A11,GROUP_4:3;
     hence thesis by A12;
   end;
 hence thesis;
end;
hence thesis by A4,Th42;
end;

theorem
   for G being strict Group holds
  G is finite & ord (G) = p & p is prime implies
   G is cyclic Group
 proof let G be strict Group;
  assume that A1: G is finite and A2: ord (G) = p and
              A3: p is prime;
    ex a being Element of G st ord a = p
  proof
   assume A4: for a being Element of G holds ord a <> p;
   A5: now let a be Element of G;
      ord a divides p by A1,A2,Th28;
   then ord a = 1 or ord a = p by A3,INT_2:def 5;
   hence ord a = 1 by A4;
end;
A6:the carrier of G c= the carrier of (1).G
 proof
     for x being set holds x in the carrier of G implies
      x in the carrier of (1).G
      proof
       let x be set;
       assume x in the carrier of G;
       then reconsider x'=x as Element of G;
         ord x' = 1 by A5;
       then x' = 1.G by GROUP_1:85;
       then x' in {1.G} by TARSKI:def 1;
      hence thesis by GROUP_2:def 7;
     end;
 hence thesis by TARSKI:def 3;
end;
   the carrier of (1).G c= the carrier of G by GROUP_2:def 5;
 then the carrier of G = the carrier of (1).G by A6,XBOOLE_0:def 10;
 then G = (1).G by GROUP_2:70;
 then ord G = 1 by GROUP_2:81;
 hence contradiction by A2,A3,INT_2:def 5;
end;
hence thesis by A1,A2,Th43;
end;

theorem Th46:
 for n st n>0 ex g being Element of INT.Group(n) st
  for b being Element of INT.Group(n) ex j1 st b = g|^j1
  proof
   let n;
   assume A1:n>0;
   then A2: INT.Group(n) = HGrStr(#Segm(n),addint(n)#) by Def6;

A3: now let h,g be Element of INT.Group(n),
            A,B be Element of Segm(n);
      assume h = A & g = B;
      hence h * g = (addint(n)).(A,B) by A2,VECTSP_1:def 10
                 .= (A + B) mod n by A1,Def5;
    end;
         0 +1 < n+1 by A1,REAL_1:53;
       then A4:n >=1 by NAT_1:38;
        now per cases by A4,REAL_1:def 5;
      suppose n=1;
   then the carrier of INT.Group(n) = {1.INT.Group(n)} by A2,Th13,Th36
      .= the carrier of (1).INT.Group(n) by GROUP_2:def 7;
      then INT.Group(n) = (1).INT.Group(n) by GROUP_2:70;
      then INT.Group(n) is cyclic Group by Th40;
      hence thesis by Th41;
suppose n>1;
     then reconsider g'= 1 as Element of Segm(n) by A1,Th10;
     reconsider g=g' as Element of INT.Group(n) by A2;
       for b being Element of INT.Group(n) ex j1 st b = g|^j1
      proof
       let b be Element of INT.Group(n);
       reconsider b'=b as Nat by A1,A2,Lm1;
       defpred P[Nat] means g|^$1 = $1 mod n;
       g|^0 = 1.INT.Group(n) by GROUP_1:43 .= 0 by A1,Th36
             .= 0 mod n by Th6; then
       A5:P[0];
       A6: for k st P[k] holds P[k+1]
       proof
        let k;
        k mod n < n by A1,NAT_1:46;
        then reconsider e=(k mod n) as Element of Segm(n) by A1,Th10;
        assume A7: g|^k = k mod n;
          g|^(k+1) =g|^k*(g|^1) by GROUP_1:48 .=g|^k*g by GROUP_1:44
               .= (e +g') mod n by A3,A7 .=(k+1) mod n by Th2;
         hence thesis;
         end;
  A8:  for k holds P[k] from Ind(A5,A6);
  A9:  b'<n by A1,A2,Th10;
A10:   g|^b'=b' mod n by A8 .= b by A9,Th4;
        reconsider b' as Integer;
        take b';
        thus thesis by A10;
    end;
    hence thesis;
  end;
  hence thesis;
end;

definition
 cluster cyclic -> commutative Group;
 coherence
proof let G;
 assume A1:G is cyclic;
   for a,b being Element of G holds a * b = b * a
 proof
  let a,b be Element of G;
    ex e being Element of G st
   (ex j2 st a=e|^j2 & ex j3 st b=e|^j3)
  proof
   consider e being Element of G such that
   A2:for d being Element of G ex j3 st d=e|^j3 by A1,Th41;
   take e;
   A3:ex j2 st a=e|^j2 by A2;
     ex j3 st b=e|^j3 by A2;
   hence thesis by A3;
  end;
  then consider e being Element of G,j2,j3 such that
  A4:( a = e|^j2 & b = e|^j3);
    a * b = e |^(j3 + j2) by A4,GROUP_1:63 .= b * a by A4,GROUP_1:63;
  hence thesis;
 end;
 hence thesis by VECTSP_1:def 17;
end;
end;

canceled;

theorem Th48:
 INT.Group is cyclic
proof
 reconsider h = 1 as Element of INT by INT_1:12;
 reconsider h as Element of INT.Group by Def4;
 take h;
   {h} c= the carrier of (Omega).INT.Group &
 ( for G1 being strict Subgroup of INT.Group st {h} c= the carrier of G1 holds
    (Omega).INT.Group is Subgroup of G1 )
 proof
  A1: {h} c= the carrier of (Omega).INT.Group
  proof
     {h} c= the carrier of INT.Group;
   hence thesis by GROUP_2:def 8;
  end;
    for G1 st {h} c= the carrier of G1 holds (Omega).INT.Group is Subgroup of
G1
  proof
   let G1;
   assume A2:{h} c= the carrier of G1;
     the carrier of (Omega).INT.Group c= the carrier of G1
   proof
      for x holds x in the carrier of (Omega).INT.Group implies x in
 the carrier of G1
    proof
     let x;
     assume that A3: x in the carrier of (Omega).INT.Group and
                 A4: not x in the carrier of G1;
       x in (Omega).INT.Group by A3,RLVECT_1:def 1;
     then x in INT.Group by GROUP_2:def 8;
     then x in INT by Def4,RLVECT_1:def 1;
     then reconsider x'=x as Integer by INT_1:12;
       h in {h} by TARSKI:def 1;
     then reconsider h''=h as Element of G1 by A2;
     A5: (h'')|^x' in the carrier of G1;
       (h'')|^x'=h|^x' by GROUP_4:4;
     hence contradiction by A4,A5,Th39;
    end;
    hence the carrier of (Omega).
INT.Group c= the carrier of G1 by TARSKI:def 3;
    thus thesis;
   end;
   hence thesis by GROUP_2:66;
  end;
  hence thesis by A1;
 end;
 then (Omega).INT.Group = gr {h} by GROUP_4:def 5;
 hence thesis by GROUP_2:def 8;
end;

theorem Th49:
 for n st n > 0 holds INT.Group(n) is cyclic Group
proof
 let n;
 assume n > 0;
 then ex g being Element of INT.Group(n) st
 for b being Element of INT.Group(n) ex j1 st b = g|^j1 by Th46;
 hence thesis by Th41;
end;

theorem
   INT.Group is commutative Group
proof
   INT.Group is cyclic Group by Th48;
 hence thesis;
end;

theorem
   for n st n>0 holds INT.Group(n) is commutative Group by Th49;

Back to top