group_8.miz



    begin

    reserve G for strict Group,

a,b,x,y,z for Element of G,

H,K for strict Subgroup of G,

p for Element of NAT ,

A for Subset of G;

    theorem :: GROUP_8:1

    for G be strict finite Group holds p is prime & ( card G) = p implies ex a be Element of G st ( ord a) = p

    proof

      let G be strict finite Group;

      assume that

       A1: p is prime and

       A2: ( card G) = p;

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

      hence thesis by A2, GR_CY_1: 19;

    end;

    theorem :: GROUP_8:2

    for G be Group, H be Subgroup of G, a1,a2 be Element of H holds for b1,b2 be Element of G st a1 = b1 & a2 = b2 holds (a1 * a2) = (b1 * b2)

    proof

      let G be Group, H be Subgroup of G;

      let a1,a2 be Element of H;

      

       A1: the carrier of H c= the carrier of G by GROUP_2:def 5;

      let b1,b2 be Element of G such that

       A2: a1 = b1 and

       A3: a2 = b2;

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

      then

       A4: the multF of G is ManySortedSet of [:the carrier of G, the carrier of G:] by PARTFUN1:def 2;

      the multF of H = (the multF of G || the carrier of H) by GROUP_2:def 5;

      hence thesis by A1, A2, A3, A4, ALTCAT_1: 5;

    end;

    theorem :: GROUP_8:3

    for G be Group, H be Subgroup of G, a be Element of H holds for b be Element of G st a = b holds for n be Element of NAT holds (a |^ n) = (b |^ n) by GROUP_4: 1;

    theorem :: GROUP_8:4

    for G be Group, H be Subgroup of G, a be Element of H holds for b be Element of G st a = b holds for i be Integer holds (a |^ i) = (b |^ i) by GROUP_4: 2;

    theorem :: GROUP_8:5

    for G be Group, H be Subgroup of G, a be Element of H holds for b be Element of G st a = b & G is finite holds ( ord a) = ( ord b)

    proof

      let G be Group, H be Subgroup of G;

      let a be Element of H;

      let b be Element of G such that

       A1: a = b and

       A2: G is finite;

      

       A3: not a is being_of_order_0 by A2, GR_CY_1: 6;

      

       A4: not b is being_of_order_0 by A2, GR_CY_1: 6;

      

       A5: (a |^ ( ord a)) = ( 1_ H) by A3, GROUP_1:def 11;

      

       A6: (b |^ ( ord b)) = ( 1_ G) by A4, GROUP_1:def 11;

      (a |^ ( ord a)) = (b |^ ( ord a)) by A1, GROUP_4: 1;

      then

       A7: ( ord b) divides ( ord a) by A5, A6, GROUP_1: 44, GROUP_2: 44;

      (a |^ ( ord b)) = ( 1_ G) by A1, A6, GROUP_4: 1;

      then (a |^ ( ord b)) = ( 1_ H) by GROUP_2: 44;

      then ( ord a) divides ( ord b) by GROUP_1: 44;

      hence thesis by A7, NAT_D: 5;

    end;

    theorem :: GROUP_8:6

    for G be Group, H be Subgroup of G, h be Element of G st h in H holds (H * h) c= the carrier of H

    proof

      let G be Group, H be Subgroup of G;

      let h be Element of G such that

       A1: h in H;

      let a be object;

      assume a in (H * h);

      then

      consider g be Element of G such that

       A2: a = (g * h) and

       A3: g in H by GROUP_2: 104;

      (g * h) in H by A1, A3, GROUP_2: 50;

      hence thesis by A2;

    end;

    theorem :: GROUP_8:7

    

     Th7: for G be Group holds for a be Element of G st a <> ( 1_ G) holds ( gr {a}) <> ( (1). G)

    proof

      let G be Group;

      let a be Element of G such that

       A1: a <> ( 1_ G);

      assume

       A2: ( gr {a}) = ( (1). G);

      

       A3: the carrier of ( (1). G) = {( 1_ G)} by GROUP_2:def 7;

      

       A4: {a} c= the carrier of ( gr {a}) by GROUP_4:def 4;

      for xx be set holds xx = a implies xx = ( 1_ G)

      proof

        let xx be set;

        assume xx = a;

        then xx in {a} by TARSKI:def 1;

        hence thesis by A2, A3, A4, TARSKI:def 1;

      end;

      hence thesis by A1;

    end;

    theorem :: GROUP_8:8

    for G be Group, m be Integer holds (( 1_ G) |^ m) = ( 1_ G) by GROUP_1: 31;

    theorem :: GROUP_8:9

    

     Th9: for m be Integer holds (a |^ (m * ( ord a))) = ( 1_ G)

    proof

      let m be Integer;

      per cases ;

        suppose a is being_of_order_0;

        then ( ord a) = 0 by GROUP_1:def 11;

        hence thesis by GROUP_1: 25;

      end;

        suppose not a is being_of_order_0;

        then

         A1: (a |^ ( ord a)) = ( 1_ G) by GROUP_1:def 11;

        (( 1_ G) |^ m) = ( 1_ G) by GROUP_1: 31;

        hence thesis by A1, GROUP_1: 35;

      end;

    end;

    theorem :: GROUP_8:10

    

     Th10: for a st not a is being_of_order_0 holds for m be Integer holds (a |^ m) = (a |^ (m mod ( ord a)))

    proof

      let a such that

       A1: not a is being_of_order_0;

      let m be Integer;

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

      then (m mod ( ord a)) = (m - ((m div ( ord a)) * ( ord a))) by INT_1:def 10;

      

      then (a |^ (m mod ( ord a))) = (a |^ (m + ( - ((1 * (m div ( ord a))) * ( ord a)))))

      .= ((a |^ m) * (a |^ (( - (m div ( ord a))) * ( ord a)))) by GROUP_1: 33

      .= ((a |^ m) * ( 1_ G)) by Th9

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

      hence thesis;

    end;

    theorem :: GROUP_8:11

    

     Th11: not b is being_of_order_0 implies ( gr {b}) is finite

    proof

      assume

       A1: not b is being_of_order_0;

      then

       A2: ( ord b) <> 0 by GROUP_1:def 11;

      deffunc B( Nat) = (b |^ $1);

      consider f be FinSequence such that

       A3: ( len f) = ( ord b) & for i be Nat st i in ( dom f) holds (f . i) = B(i) from FINSEQ_1:sch 2;

      

       A4: ( dom f) = ( Seg ( ord b)) by A3, FINSEQ_1:def 3;

      the carrier of ( gr {b}) c= ( rng f)

      proof

        let x be object;

        assume x in the carrier of ( gr {b});

        then

         A5: x in ( gr {b});

        then x in G by GROUP_2: 40;

        then

        reconsider a = x as Element of G;

        consider m be Integer such that

         A6: a = (b |^ m) by A5, GR_CY_1: 5;

        set k = (m mod ( ord b));

        reconsider k as Element of NAT by INT_1: 3, NEWTON: 64;

        

         A7: a = (b |^ k) by A1, A6, Th10;

        per cases ;

          suppose

           A8: k = 0 ;

          ( ord b) >= ( 0 + 1) by A2, NAT_1: 13;

          then

           A9: ( ord b) in ( Seg ( ord b)) by FINSEQ_1: 1;

          a = ( 1_ G) by A7, A8, GROUP_1: 25

          .= (b |^ ( ord b)) by A1, GROUP_1:def 11

          .= (f . ( ord b)) by A3, A4, A9;

          hence thesis by A4, A9, FUNCT_1:def 3;

        end;

          suppose

           A10: k <> 0 ;

          

           A11: k < ( ord b) by A2, NEWTON: 65;

          k >= ( 0 + 1) by A10, NAT_1: 13;

          then

           A12: k in ( Seg ( ord b)) by A11, FINSEQ_1: 1;

          then a = (f . k) by A3, A4, A7;

          hence thesis by A4, A12, FUNCT_1:def 3;

        end;

      end;

      hence the carrier of ( gr {b}) is finite;

    end;

    theorem :: GROUP_8:12

    

     Th12: b is being_of_order_0 implies (b " ) is being_of_order_0

    proof

      assume

       A1: b is being_of_order_0;

      for n be Nat st ((b " ) |^ n) = ( 1_ G) holds n = 0

      proof

        let n be Nat;

        assume ((b " ) |^ n) = ( 1_ G);

        then ((b |^ n) " ) = ( 1_ G) by GROUP_1: 37;

        then ((b |^ n) " ) = (( 1_ G) " ) by GROUP_1: 8;

        then (b |^ n) = ( 1_ G) by GROUP_1: 9;

        hence thesis by A1, GROUP_1:def 10;

      end;

      hence thesis by GROUP_1:def 10;

    end;

    theorem :: GROUP_8:13

    

     Th13: b is being_of_order_0 iff for n be Integer st (b |^ n) = ( 1_ G) holds n = 0

    proof

      thus b is being_of_order_0 implies for n be Integer st (b |^ n) = ( 1_ G) holds n = 0

      proof

        assume

         A1: b is being_of_order_0;

        

         A2: for m be Nat holds (b |^ ( - m)) = ( 1_ G) implies m = 0

        proof

          let m be Nat;

          assume

           A3: (b |^ ( - m)) = ( 1_ G);

          (b |^ ( - m)) = ((b |^ m) " ) by GROUP_1: 36;

          then

           A4: ((b " ) |^ m) = ( 1_ G) by A3, GROUP_1: 37;

          (b " ) is being_of_order_0 by A1, Th12;

          hence thesis by A4, GROUP_1:def 10;

        end;

        for n be Integer holds (b |^ n) = ( 1_ G) implies n = 0

        proof

          let n be Integer;

          assume

           A5: (b |^ n) = ( 1_ G);

          consider k be Nat such that

           A6: n = k or n = ( - k) by INT_1: 2;

          per cases by A6;

            suppose n = k;

            hence thesis by A1, A5, GROUP_1:def 10;

          end;

            suppose

             A7: n = ( - k);

            then k = 0 by A2, A5;

            hence thesis by A7;

          end;

        end;

        hence thesis;

      end;

      assume for n be Integer holds (b |^ n) = ( 1_ G) implies n = 0 ;

      then for n be Nat holds (b |^ n) = ( 1_ G) implies n = 0 ;

      hence thesis by GROUP_1:def 10;

    end;

    theorem :: GROUP_8:14

    for G st ex a st a <> ( 1_ G) holds (for H holds H = G or H = ( (1). G)) iff G is cyclic & G is finite & ex p be Element of NAT st ( card G) = p & p is prime

    proof

      let G such that

       A1: ex a st a <> ( 1_ G);

      thus (for H holds H = G or H = ( (1). G)) implies G is cyclic & G is finite & ex p be Element of NAT st ( card G) = p & p is prime

      proof

        assume

         A2: for H holds H = G or H = ( (1). G);

        consider b such that

         A3: b <> ( 1_ G) by A1;

        

         A4: ( gr {b}) = G by A2, A3, Th7;

        

         A5: not b is being_of_order_0

        proof

          assume

           A6: b is being_of_order_0;

          then

           A7: (b |^ 2) <> ( 1_ G) by GROUP_1:def 10;

           not b in ( gr {(b |^ 2)})

          proof

            assume b in ( gr {(b |^ 2)});

            then

            consider j1 be Integer such that

             A8: b = ((b |^ 2) |^ j1) by GR_CY_1: 5;

            b = (b |^ (2 * j1)) by A8, GROUP_1: 35;

            then ((b " ) * (b |^ (2 * j1))) = ( 1_ G) by GROUP_1:def 5;

            then ((b |^ ( - 1)) * (b |^ (2 * j1))) = ( 1_ G) by GROUP_1: 32;

            then (b |^ (( - 1) + (2 * j1))) = ( 1_ G) by GROUP_1: 33;

            then (( - 1) + (2 * j1)) = 0 by A6, Th13;

            hence thesis by INT_1: 9;

          end;

          then ( gr {(b |^ 2)}) <> G;

          hence contradiction by A2, A7, Th7;

        end;

        then

        consider n be Element of NAT such that

         A9: n = ( ord b) and not b is being_of_order_0;

        

         A10: G is finite by A4, A5, Th11;

        then

         A11: ( card G) = n by A4, A9, GR_CY_1: 7;

        n is prime

        proof

          assume

           A12: not n is prime;

          ex u,v be Element of NAT st u > 1 & v > 1 & n = (u * v)

          proof

            

             A13: not (n > 1 & for m be Nat holds m divides n implies m = 1 or m = n) by A12, INT_2:def 4;

            n >= 1 by A10, A11, GROUP_1: 45;

            then n > 1 by A3, A9, GROUP_1: 43, XXREAL_0: 1;

            then

            consider m be Nat such that

             A14: m <> 1 and

             A15: m <> n and

             A16: m divides n by A13;

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

            consider o be Nat such that

             A17: n = (m * o) by A16, NAT_D:def 3;

            reconsider o as Element of NAT by ORDINAL1:def 12;

            take u = m;

            take v = o;

            u <> 0

            proof

              assume u = 0 ;

              then n = ( 0 * (n div 0 )) by A16, NAT_D: 3;

              hence contradiction by A10, A11;

            end;

            then

             A18: ( 0 + 1) <= u by INT_1: 7;

             0 < v by A10, A11, A17;

            then

             A19: ( 0 + 1) <= v by INT_1: 7;

            v <> 1 by A15, A17;

            hence thesis by A14, A17, A18, A19, XXREAL_0: 1;

          end;

          then

          consider u,v be Element of NAT such that

           A20: u > 1 and

           A21: v > 1 and

           A22: n = (u * v);

          ( ord (b |^ v)) = u by A4, A10, A11, A22, GR_CY_2: 8;

          then

           A23: ( card ( gr {(b |^ v)})) = u by A10, GR_CY_1: 7;

          

           A24: u <> n by A20, A21, A22, XCMPLX_1: 7;

          ( gr {(b |^ v)}) <> ( (1). G) by A20, A23, GROUP_2: 69;

          hence thesis by A2, A11, A23, A24;

        end;

        hence thesis by A4, A5, A11, Th11, GR_CY_2: 4;

      end;

      assume that G is cyclic and

       A25: G is finite and

       A26: ex p be Element of NAT st ( card G) = p & p is prime;

      let H;

      reconsider G as finite Group by A25;

      reconsider H as Subgroup of G;

      ( card G) = (( card H) * ( index H)) by GROUP_2: 147;

      then

       A27: ( card H) divides ( card G) by NAT_D:def 3;

      per cases by A26, A27, INT_2:def 4;

        suppose ( card H) = ( card G);

        hence thesis by GROUP_2: 73;

      end;

        suppose ( card H) = 1;

        hence thesis by GROUP_2: 70;

      end;

    end;

    theorem :: GROUP_8:15

    

     Th15: for G be Group, x,y,z be Element of G holds for A be Subset of G holds z in ((x * A) * y) iff ex a be Element of G st z = ((x * a) * y) & a in A

    proof

      let G be Group;

      let x,y,z be Element of G;

      let A be Subset of G;

      thus z in ((x * A) * y) implies ex a be Element of G st z = ((x * a) * y) & a in A

      proof

        assume z in ((x * A) * y);

        then

        consider b be Element of G such that

         A1: z = (b * y) and

         A2: b in (x * A) by GROUP_2: 28;

        consider u be Element of G such that

         A3: b = (x * u) and

         A4: u in A by A2, GROUP_2: 27;

        take u;

        thus thesis by A1, A3, A4;

      end;

      given a be Element of G such that

       A5: z = ((x * a) * y) and

       A6: a in A;

      ex h be Element of G st z = (h * y) & h in (x * A) by A5, A6, GROUP_2: 27;

      hence thesis by GROUP_2: 28;

    end;

    theorem :: GROUP_8:16

    for G be Group, A be non empty Subset of G holds for x be Element of G holds ( card A) = ( card (((x " ) * A) * x))

    proof

      let G be Group, A be non empty Subset of G;

      let x be Element of G;

      set B = (((x " ) * A) * x);

      A is non empty & B is non empty

      proof

        set a = the Element of A;

        (((x " ) * a) * x) in B by Th15;

        hence thesis;

      end;

      then

      reconsider B as non empty Subset of G;

      deffunc F( Element of G) = (((x " ) * $1) * x);

      consider f be Function of A, the carrier of G such that

       A1: for a be Element of A holds (f . a) = F(a) from FUNCT_2:sch 4;

      

       A2: ( dom f) = A by FUNCT_2:def 1;

      

       A3: ( rng f) c= B

      proof

        let s be object;

        assume s in ( rng f);

        then

        consider a be object such that

         A4: a in A and

         A5: s = (f . a) by A2, FUNCT_1:def 3;

        reconsider a as Element of A by A4;

        s = F(a) by A1, A5;

        hence thesis by Th15;

      end;

      

       A6: B c= ( rng f)

      proof

        let s be object;

        assume s in B;

        then

        consider a be Element of G such that

         A7: s = (((x " ) * a) * x) and

         A8: a in A by Th15;

        ex x be Element of G st x in ( dom f) & s = (f . x)

        proof

          take a;

          thus thesis by A1, A7, A8, FUNCT_2:def 1;

        end;

        hence thesis by FUNCT_1:def 3;

      end;

      reconsider f as Function of A, B by A2, A3, FUNCT_2: 2;

      deffunc FF( Element of G) = ((x * $1) * (x " ));

      consider g be Function of B, the carrier of G such that

       A9: for b be Element of B holds (g . b) = FF(b) from FUNCT_2:sch 4;

      

       A10: ( dom g) = B by FUNCT_2:def 1;

      ( rng g) c= A

      proof

        let s be object;

        assume s in ( rng g);

        then

        consider a be object such that

         A11: a in B and

         A12: s = (g . a) by A10, FUNCT_1:def 3;

        reconsider a as Element of B by A11;

        

         A13: s = FF(a) by A9, A12;

        consider c be Element of G such that

         A14: a = (((x " ) * c) * x) and

         A15: c in A by Th15;

        s = (((x * ((x " ) * c)) * x) * (x " )) by A13, A14, GROUP_1:def 3

        .= ((((x * (x " )) * c) * x) * (x " )) by GROUP_1:def 3

        .= (((x * (x " )) * c) * (x * (x " ))) by GROUP_1:def 3

        .= ((( 1_ G) * c) * (x * (x " ))) by GROUP_1:def 5

        .= ((( 1_ G) * c) * ( 1_ G)) by GROUP_1:def 5

        .= (( 1_ G) * c) by GROUP_1:def 4

        .= c by GROUP_1:def 4;

        hence thesis by A15;

      end;

      then

      reconsider g as Function of B, A by A10, FUNCT_2: 2;

      

       A16: for a,b be Element of A st (f . a) = (f . b) holds a = b

      proof

        let a,b be Element of A such that

         A17: (f . a) = (f . b);

        

         A18: (((x " ) * a) * x) in B by Th15;

        

         A19: (((x " ) * b) * x) in B by Th15;

        

         A20: (g . (f . a)) = (g . (((x " ) * a) * x)) by A1

        .= ((x * (((x " ) * a) * x)) * (x " )) by A9, A18

        .= (((x * ((x " ) * a)) * x) * (x " )) by GROUP_1:def 3

        .= ((((x * (x " )) * a) * x) * (x " )) by GROUP_1:def 3

        .= (((x * (x " )) * a) * (x * (x " ))) by GROUP_1:def 3

        .= ((( 1_ G) * a) * (x * (x " ))) by GROUP_1:def 5

        .= (a * (x * (x " ))) by GROUP_1:def 4

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

        .= a by GROUP_1:def 4;

        (g . (f . b)) = (g . (((x " ) * b) * x)) by A1

        .= ((x * (((x " ) * b) * x)) * (x " )) by A9, A19

        .= (((x * ((x " ) * b)) * x) * (x " )) by GROUP_1:def 3

        .= ((((x * (x " )) * b) * x) * (x " )) by GROUP_1:def 3

        .= (((x * (x " )) * b) * (x * (x " ))) by GROUP_1:def 3

        .= ((( 1_ G) * b) * (x * (x " ))) by GROUP_1:def 5

        .= (b * (x * (x " ))) by GROUP_1:def 4

        .= (b * ( 1_ G)) by GROUP_1:def 5

        .= b by GROUP_1:def 4;

        hence thesis by A17, A20;

      end;

      (A,B) are_equipotent

      proof

        take f;

        thus thesis by A3, A6, A16, FUNCT_2:def 1, GROUP_6: 1, XBOOLE_0:def 10;

      end;

      hence thesis by CARD_1: 5;

    end;

    definition

      let G, H, K;

      :: GROUP_8:def1

      func Double_Cosets (H,K) -> Subset-Family of G means A in it iff ex a st A = ((H * a) * K);

      existence

      proof

        defpred P[ set] means ex a st $1 = ((H * a) * K);

        ex F be Subset-Family of G st for A be Subset of G holds A in F iff P[A] from SUBSET_1:sch 3;

        hence thesis;

      end;

      uniqueness

      proof

        let F1,F2 be Subset-Family of G;

        defpred P[ set] means ex a st $1 = ((H * a) * K);

        assume

         A1: for A holds A in F1 iff P[A];

        assume

         A2: for A holds A in F2 iff P[A];

        thus thesis from SUBSET_1:sch 4( A1, A2);

      end;

    end

    theorem :: GROUP_8:17

    

     Th17: z in ((H * x) * K) iff ex g,h be Element of G st z = ((g * x) * h) & g in H & h in K

    proof

      thus z in ((H * x) * K) implies ex g,h be Element of G st z = ((g * x) * h) & g in H & h in K

      proof

        assume z in ((H * x) * K);

        then

        consider g1,g2 be Element of G such that

         A1: z = (g1 * g2) and

         A2: g1 in (H * x) and

         A3: g2 in K by GROUP_2: 94;

        ex h1 be Element of G st (g1 = (h1 * x)) & (h1 in H) by A2, GROUP_2: 104;

        hence thesis by A1, A3;

      end;

      given g,h be Element of G such that

       A4: z = ((g * x) * h) and

       A5: g in H and

       A6: h in K;

      ex g1,g2 be Element of G st z = (g1 * g2) & g1 in (H * x) & g2 in K by A5, A4, A6, GROUP_2: 104;

      hence thesis by GROUP_2: 94;

    end;

    theorem :: GROUP_8:18

    for H, K holds ((H * x) * K) = ((H * y) * K) or not ex z st z in ((H * x) * K) & z in ((H * y) * K)

    proof

      let H, K;

      per cases ;

        suppose not ex z st z in ((H * x) * K) & z in ((H * y) * K);

        hence thesis;

      end;

        suppose ex z st z in ((H * x) * K) & z in ((H * y) * K);

        then

        consider z such that

         A1: z in ((H * x) * K) and

         A2: z in ((H * y) * K);

        consider h1,k1 be Element of G such that

         A3: z = ((h1 * x) * k1) and

         A4: h1 in H and

         A5: k1 in K by A1, Th17;

        consider h2,k2 be Element of G such that

         A6: z = ((h2 * y) * k2) and

         A7: h2 in H and

         A8: k2 in K by A2, Th17;

        for a be object st a in ((H * x) * K) holds a in ((H * y) * K)

        proof

          let a be object;

          assume a in ((H * x) * K);

          then

          consider h,k be Element of G such that

           A9: a = ((h * x) * k) and

           A10: h in H and

           A11: k in K by Th17;

          ex c,d be Element of G st a = ((c * y) * d) & c in H & d in K

          proof

            h = (h * ( 1_ G)) by GROUP_1:def 4;

            then

             A12: ((h * x) * k) = ((((h * ( 1_ G)) * x) * ( 1_ G)) * k) by GROUP_1:def 4;

            ( 1_ G) = ((h1 " ) * h1) by GROUP_1:def 5;

            

            then

             A13: ((h * x) * k) = ((((h * ((h1 " ) * h1)) * x) * (k1 * (k1 " ))) * k) by A12, GROUP_1:def 5

            .= (((((h * ((h1 " ) * h1)) * x) * k1) * (k1 " )) * k) by GROUP_1:def 3

            .= ((((((h * (h1 " )) * h1) * x) * k1) * (k1 " )) * k) by GROUP_1:def 3

            .= (((((h * (h1 " )) * (h1 * x)) * k1) * (k1 " )) * k) by GROUP_1:def 3

            .= ((((h * (h1 " )) * ((h2 * y) * k2)) * (k1 " )) * k) by A3, A6, GROUP_1:def 3

            .= (((((h * (h1 " )) * (h2 * y)) * k2) * (k1 " )) * k) by GROUP_1:def 3

            .= ((((((h * (h1 " )) * h2) * y) * k2) * (k1 " )) * k) by GROUP_1:def 3

            .= (((((h * (h1 " )) * h2) * y) * (k2 * (k1 " ))) * k) by GROUP_1:def 3

            .= ((((h * (h1 " )) * h2) * y) * ((k2 * (k1 " )) * k)) by GROUP_1:def 3;

            take ((h * (h1 " )) * h2);

            take ((k2 * (k1 " )) * k);

            (h1 " ) in H by A4, GROUP_2: 51;

            then

             A14: (h * (h1 " )) in H by A10, GROUP_2: 50;

            (k1 " ) in K by A5, GROUP_2: 51;

            then (k2 * (k1 " )) in K by A8, GROUP_2: 50;

            hence thesis by A7, A9, A11, A13, A14, GROUP_2: 50;

          end;

          hence thesis by Th17;

        end;

        then

         A15: ((H * x) * K) c= ((H * y) * K);

        for a be object st a in ((H * y) * K) holds a in ((H * x) * K)

        proof

          let a be object;

          assume a in ((H * y) * K);

          then

          consider h,k be Element of G such that

           A16: a = ((h * y) * k) and

           A17: h in H and

           A18: k in K by Th17;

          ex c,d be Element of G st a = ((c * x) * d) & c in H & d in K

          proof

            h = (h * ( 1_ G)) by GROUP_1:def 4;

            then

             A19: ((h * y) * k) = ((((h * ( 1_ G)) * y) * ( 1_ G)) * k) by GROUP_1:def 4;

            ( 1_ G) = ((h2 " ) * h2) by GROUP_1:def 5;

            

            then

             A20: ((h * y) * k) = ((((h * ((h2 " ) * h2)) * y) * (k2 * (k2 " ))) * k) by A19, GROUP_1:def 5

            .= (((((h * ((h2 " ) * h2)) * y) * k2) * (k2 " )) * k) by GROUP_1:def 3

            .= ((((((h * (h2 " )) * h2) * y) * k2) * (k2 " )) * k) by GROUP_1:def 3

            .= (((((h * (h2 " )) * (h2 * y)) * k2) * (k2 " )) * k) by GROUP_1:def 3

            .= ((((h * (h2 " )) * ((h1 * x) * k1)) * (k2 " )) * k) by A3, A6, GROUP_1:def 3

            .= (((((h * (h2 " )) * (h1 * x)) * k1) * (k2 " )) * k) by GROUP_1:def 3

            .= ((((((h * (h2 " )) * h1) * x) * k1) * (k2 " )) * k) by GROUP_1:def 3

            .= (((((h * (h2 " )) * h1) * x) * (k1 * (k2 " ))) * k) by GROUP_1:def 3

            .= ((((h * (h2 " )) * h1) * x) * ((k1 * (k2 " )) * k)) by GROUP_1:def 3;

            take ((h * (h2 " )) * h1);

            take ((k1 * (k2 " )) * k);

            (h2 " ) in H by A7, GROUP_2: 51;

            then

             A21: (h * (h2 " )) in H by A17, GROUP_2: 50;

            (k2 " ) in K by A8, GROUP_2: 51;

            then (k1 * (k2 " )) in K by A5, GROUP_2: 50;

            hence thesis by A4, A16, A18, A20, A21, GROUP_2: 50;

          end;

          hence thesis by Th17;

        end;

        then ((H * y) * K) c= ((H * x) * K);

        hence thesis by A15, XBOOLE_0:def 10;

      end;

    end;

    reserve G for Group;

    reserve H,B,A for Subgroup of G,

D for Subgroup of A;

    registration

      let G, A;

      cluster ( Left_Cosets A) -> non empty;

      coherence by GROUP_2: 135;

    end

    notation

      let G be Group;

      let H be Subgroup of G;

      synonym index (G,H) for index H;

    end

    theorem :: GROUP_8:19

    

     Th19: D = (A /\ B) & G is finite implies ( index (G,B)) >= ( index (A,D))

    proof

      assume that

       A1: D = (A /\ B) and

       A2: G is finite;

      reconsider LCB = ( Left_Cosets B) as finite non empty set by A2;

      reconsider LCD = ( Left_Cosets D) as finite non empty set by A2;

       A3:

      now

        let x,y be Element of G;

        let x9,y9 be Element of A such that

         A4: x9 = x and

         A5: y9 = y;

        

         A6: (y9 " ) = (y " ) by A5, GROUP_2: 48;

        

         A7: ((y9 " ) * x9) in A;

        (x * B) = (y * B) iff ((y " ) * x) in B by GROUP_2: 114;

        then (x * B) = (y * B) iff ((y9 " ) * x9) in B by A4, A6, GROUP_2: 43;

        then (x * B) = (y * B) iff ((y9 " ) * x9) in D by A1, A7, GROUP_2: 82;

        hence (x * B) = (y * B) iff (x9 * D) = (y9 * D) by GROUP_2: 114;

      end;

      defpred P[ set, set] means ex a be Element of G, a9 be Element of A st a = a9 & $2 = (a * B) & $1 = (a9 * D);

      

       A8: for x be Element of LCD holds ex y be Element of LCB st P[x, y]

      proof

        let x be Element of LCD;

        x in LCD;

        then

        consider a9 be Element of A such that

         A9: x = (a9 * D) by GROUP_2:def 15;

        reconsider a = a9 as Element of G by GROUP_2: 42;

        reconsider y = (a * B) as Element of LCB by GROUP_2:def 15;

        take y, a, a9;

        thus thesis by A9;

      end;

      consider F be Function of LCD, LCB such that

       A10: for a be Element of LCD holds P[a, (F . a)] from FUNCT_2:sch 3( A8);

      

       A11: ( dom F) = LCD by FUNCT_2:def 1;

      

       A12: ( rng F) c= LCB by RELAT_1:def 19;

      

       A13: ( index D) = ( card LCD) by GROUP_2:def 18;

      

       A14: ( index B) = ( card LCB) by GROUP_2:def 18;

      F is one-to-one

      proof

        let x1,x2 be object;

        assume that

         A15: x1 in ( dom F) and

         A16: x2 in ( dom F);

        reconsider z1 = x1, z2 = x2 as Element of LCD by A15, A16, FUNCT_2:def 1;

        

         A17: ex a be Element of G, a9 be Element of A st (a = a9) & ((F . z1) = (a * B)) & (z1 = (a9 * D)) by A10;

        ex b be Element of G, b9 be Element of A st (b = b9) & ((F . z2) = (b * B)) & (z2 = (b9 * D)) by A10;

        hence thesis by A3, A17;

      end;

      then ( Segm ( index D)) c= ( Segm ( index B)) by A11, A12, A13, A14, CARD_1: 10;

      hence thesis by NAT_1: 39;

    end;

    theorem :: GROUP_8:20

    

     Th20: for G be finite Group, H be Subgroup of G holds ( index (G,H)) > 0

    proof

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

      ( card G) = (( card H) * ( index H)) by GROUP_2: 147;

      hence thesis;

    end;

    theorem :: GROUP_8:21

    for G be Group st G is finite holds for C be Subgroup of G holds for A,B be Subgroup of C holds for D be Subgroup of A st D = (A /\ B) holds for E be Subgroup of B st E = (A /\ B) holds for F be Subgroup of C st F = (A /\ B) holds (( index (C,A)),( index (C,B))) are_coprime implies ( index (C,B)) = ( index (A,D)) & ( index (C,A)) = ( index (B,E))

    proof

      let G such that

       A1: G is finite;

      let C be Subgroup of G;

      let A,B be Subgroup of C;

      let D be Subgroup of A such that

       A2: D = (A /\ B);

      let E be Subgroup of B such that

       A3: E = (A /\ B);

      let F be Subgroup of C such that

       A4: F = (A /\ B);

      assume that

       A5: (( index A),( index B)) are_coprime ;

      ( index F) = (( index E) * ( index B)) by A1, A3, A4, GROUP_2: 149;

      then

       A6: (( index E) * ( index B)) = (( index D) * ( index A)) by A1, A2, A4, GROUP_2: 149;

      then ( index B) qua Integer divides (( index A) qua Integer * ( index D) qua Integer) by INT_1:def 3;

      then

       A7: ( index B) qua Integer divides ( index D) qua Integer by A5, INT_2: 25;

      ex n be Element of NAT st ( index D) = (( index B) * n)

      proof

        consider i be Integer such that

         A8: ( index D) = (( index B) qua Integer * i) by A7, INT_1:def 3;

         0 <= i by A1, A8, Th20;

        then

        reconsider i as Element of NAT by INT_1: 3;

        take i;

        thus thesis by A8;

      end;

      then

       A9: ( index B) divides ( index D) by NAT_D:def 3;

      

       A10: ( index (C,B)) >= ( index (A,D)) by A1, A2, Th19;

      

       A11: ( index B) = ( index D)

      proof

        assume

         A12: ( index B) <> ( index D);

        ( index D) > 0 by A1, Th20;

        then ( index B) <= ( index D) by A9, NAT_D: 7;

        hence contradiction by A10, A12, XXREAL_0: 1;

      end;

      ( index A) qua Integer divides (( index B) qua Integer * ( index E) qua Integer) by A6, INT_1:def 3;

      then

       A13: ( index A) qua Integer divides ( index E) by A5, INT_2: 25;

      ex n be Element of NAT st ( index E) = (( index A) * n)

      proof

        consider i be Integer such that

         A14: ( index E) = (( index A) qua Integer * i) by A13, INT_1:def 3;

         0 <= i by A1, A14, Th20;

        then

        reconsider i as Element of NAT by INT_1: 3;

        take i;

        thus thesis by A14;

      end;

      then

       A15: ( index A) divides ( index E) by NAT_D:def 3;

      

       A16: ( index A) >= ( index E) by A1, A3, Th19;

      ( index A) = ( index E)

      proof

        assume

         A17: ( index A) <> ( index E);

        ( index E) > 0 by A1, Th20;

        then ( index A) <= ( index E) by A15, NAT_D: 7;

        hence contradiction by A16, A17, XXREAL_0: 1;

      end;

      hence thesis by A11;

    end;

    theorem :: GROUP_8:22

    

     Th22: for a be Element of G st a in H holds for j be Integer holds (a |^ j) in H

    proof

      let a be Element of G;

      assume

       A1: a in H;

      let j be Integer;

      consider k be Nat such that

       A2: j = k or j = ( - k) by INT_1: 2;

      per cases by A2;

        suppose

         A3: j = k;

        defpred P[ Nat] means (a |^ $1) in H;

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

        then

         A4: P[ 0 ] by GROUP_2: 46;

        

         A5: for n be Nat st P[n] holds P[(n + 1)]

        proof

          let n be Nat;

          assume P[n];

          then ((a |^ n) * a) in H by A1, GROUP_2: 50;

          hence thesis by GROUP_1: 34;

        end;

        for n be Nat holds P[n] from NAT_1:sch 2( A4, A5);

        hence thesis by A3;

      end;

        suppose

         A6: j = ( - k);

        defpred PP[ Nat] means (a |^ ( - $1)) in H;

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

        then

         A7: PP[ 0 ] by GROUP_2: 46;

        

         A8: for n be Nat st PP[n] holds PP[(n + 1)]

        proof

          let n be Nat such that

           A9: PP[n];

          (a " ) in H by A1, GROUP_2: 51;

          then ((a |^ ( - n)) * (a " )) in H by A9, GROUP_2: 50;

          then ((a |^ ( - n)) * (a |^ ( - 1))) in H by GROUP_1: 32;

          then (a |^ (( - n) + ( - 1))) in H by GROUP_1: 33;

          hence thesis;

        end;

        for n be Nat holds PP[n] from NAT_1:sch 2( A7, A8);

        hence thesis by A6;

      end;

    end;

    theorem :: GROUP_8:23

    

     Th23: for G be strict Group st G <> ( (1). G) holds ex b be Element of G st b <> ( 1_ G)

    proof

      let G be strict Group such that

       A1: G <> ( (1). G);

      assume

       A2: not ex b be Element of G st b <> ( 1_ G);

      for x,y be Element of G holds x = y

      proof

        let x,y be Element of G;

        x = ( 1_ G) by A2;

        hence thesis by A2;

      end;

      then G is trivial;

      hence contradiction by A1, GROUP_6: 12;

    end;

    theorem :: GROUP_8:24

    

     Th24: for G be strict Group holds for a be Element of G st G = ( gr {a}) holds for H be strict Subgroup of G st H <> ( (1). G) holds ex k be Nat st 0 < k & (a |^ k) in H

    proof

      let G be strict Group;

      let a be Element of G such that

       A1: G = ( gr {a});

      let H be strict Subgroup of G;

      assume H <> ( (1). G);

      then

       A2: H <> ( (1). H) by GROUP_2: 63;

      consider c be Element of H such that

       A3: c <> ( 1_ H) by A2, Th23;

      

       A4: c in H;

      then c in G by GROUP_2: 40;

      then

      reconsider c as Element of G;

      

       A5: c in ( gr {a}) by A1;

      ex j be Integer st c = (a |^ j) & j <> 0

      proof

        assume

         A6: not ex j be Integer st c = (a |^ j) & j <> 0 ;

        consider i be Integer such that

         A7: c = (a |^ i) by A5, GR_CY_1: 5;

        

         A8: (a |^ i) <> ( 1_ G) by A3, A7, GROUP_2: 44;

        i = 0 by A6, A7;

        hence contradiction by A8, GROUP_1: 25;

      end;

      then

      consider j be Integer such that

       A9: c = (a |^ j) and

       A10: j <> 0 ;

      consider n be Nat such that

       A11: j = n or j = ( - n) by INT_1: 2;

      per cases by A11;

        suppose j = n;

        hence thesis by A4, A9, A10;

      end;

        suppose

         A12: j = ( - n);

        then

         A13: 0 < n by A10;

        ((a |^ n) " ) in H by A4, A9, A12, GROUP_1: 36;

        then (((a |^ n) " ) " ) in H by GROUP_2: 51;

        hence thesis by A13;

      end;

    end;

    theorem :: GROUP_8:25

    for G be strict cyclic Group holds for H be strict Subgroup of G holds H is cyclic Group

    proof

      let G be strict cyclic Group;

      let H be strict Subgroup of G;

      per cases ;

        suppose H = ( (1). G);

        hence thesis;

      end;

        suppose

         A1: H <> ( (1). G);

        consider b be Element of G such that

         A2: the multMagma of G = ( gr {b}) by GR_CY_1:def 7;

        ex m be Nat st 0 < m & (b |^ m) in H & for j be Nat st 0 < j & (b |^ j) in H holds m <= j

        proof

          defpred P[ Nat] means 0 < $1 & (b |^ $1) in H;

          ex k be Nat st P[k] by A1, A2, Th24;

          then

           A3: ex k be Nat st P[k];

          ex m be Nat st P[m] & for j be Nat st P[j] holds m <= j from NAT_1:sch 5( A3);

          hence thesis;

        end;

        then

        consider m be Nat such that

         A4: 0 < m and

         A5: (b |^ m) in H and

         A6: for j be Nat st 0 < j & (b |^ j) in H holds m <= j;

        set c = (b |^ m);

        reconsider c as Element of H by A5;

        for a be Element of H holds ex i be Integer st a = (c |^ i)

        proof

          let a be Element of H;

          ex t be Integer st (b |^ t) in H & (b |^ t) = a

          proof

            

             A7: a in G by GROUP_2: 41;

            

             A8: a in ( gr {b}) by A2, GROUP_2: 41;

            a is Element of G by A7;

            then

            consider j1 be Integer such that

             A9: a = (b |^ j1) by A8, GR_CY_1: 5;

            (b |^ j1) in H by A9;

            hence thesis by A9;

          end;

          then

          consider t be Integer such that

           A10: (b |^ t) in H and

           A11: (b |^ t) = a;

          ex r,s be Integer st 0 <= s & s < m & t = ((m * r) + s)

          proof

            take (t div m);

            take (t mod m);

            thus thesis by A4, NEWTON: 64, NEWTON: 65, NEWTON: 66;

          end;

          then

          consider r,s be Integer such that

           A12: 0 <= s and

           A13: s < m and

           A14: t = ((m * r) + s);

          reconsider s as Element of NAT by A12, INT_1: 3;

          

           A15: (b |^ t) = ((b |^ (m * r)) * (b |^ s)) by A14, GROUP_1: 33

          .= (((b |^ m) |^ r) * (b |^ s)) by GROUP_1: 35;

          

           A16: ((b |^ m) |^ r) in H by A5, Th22;

          (b |^ s) in H

          proof

            set u = (b |^ t);

            set v = ((b |^ m) |^ r);

            

             A17: ((v " ) * u) = (((v " ) * v) * (b |^ s)) by A15, GROUP_1:def 3

            .= (( 1_ G) * (b |^ s)) by GROUP_1:def 5

            .= (b |^ s) by GROUP_1:def 4;

            (v " ) in H by A16, GROUP_2: 51;

            hence thesis by A10, A17, GROUP_2: 50;

          end;

          then s = 0 by A6, A13;

          then (b |^ s) = ( 1_ G) by GROUP_1: 25;

          then

           A18: (b |^ t) = ((b |^ m) |^ r) by A15, GROUP_1:def 4;

          ((b |^ m) |^ r) = (c |^ r) by GROUP_4: 2;

          hence thesis by A11, A18;

        end;

        then H = ( gr {c}) by GR_CY_2: 5;

        hence thesis by GR_CY_2: 4;

      end;

    end;