:: Some Properties of $p$-Groups and Commutative $p$-Groups
::  by Xiquan Liang and Dailu Li
::
:: Received April 29, 2010
:: Copyright (c) 2010 Association of Mizar Users

environ

 vocabularies ARYTM_3, RELAT_1, FUNCT_1, SUBSET_1, BINOP_1, GROUP_1, NAT_1,
      CARD_1, GROUP_2, FUNCT_2, FINSET_1, GRAPH_1, NEWTON, XBOOLE_0, NAT_3,
      GROUP_10, ALGSTR_0, NUMBERS, INT_2, ORDINAL1, XXREAL_0, GROUP_6,
      PRE_TOPC, STRUCT_0, GROUP_5, QC_LANG1, CQC_SIM1, WELLORD1, MOEBIUS1,
      GROUPP_1;
 notations TARSKI, XBOOLE_0, SUBSET_1, CARD_1, NUMBERS, XCMPLX_0, XXREAL_0,
      INT_2, NAT_1, NAT_D, FINSET_1, RELAT_1, FUNCT_1, RELSET_1, FUNCT_2,
      FINSEQ_1, RVSUM_1, STRUCT_0, ALGSTR_0, GROUP_1, GROUP_2, GROUP_3,
      EQREL_1, FUNCOP_1, NEWTON, DOMAIN_1, GR_CY_1, ORDINAL1, GROUP_4,
      CARD_FIN, PARTFUN1, NAT_3, TOPGRP_1, GROUP_10, REAL_1, BINOP_2, BINOP_1,
      MOEBIUS1, GROUP_5, GROUP_6, GRSOLV_1, RLVECT_1, INT_1, FINSEQOP,
      SETWISEO;
 constructors SETFAM_1, WELLORD2, XXREAL_0, NAT_D, EQREL_1, BINARITH, WSIERP_1,
      REALSET2, UPROOTS, GR_CY_1, GROUP_4, CARD_FIN, NAT_3, TOPGRP_1, SEQ_1,
      GROUP_2, DYNKIN, RELSET_1, GROUP_10, BINOP_1, SETWISEO, REAL_1, NAT_1,
      BINOP_2, GRSOLV_1, GRNILP_1, GROUP_5, FINSOP_1, SETWOP_2, RVSUM_1,
      FINSEQOP, INT_1, RLVECT_1, NEWTON, MOEBIUS1, GROUP_6, INT_2, ORDINAL1,
      GROUP_3, REALSET1, FUNCOP_1, ZFMISC_1, ALGSTR_0;
 registrations XBOOLE_0, SUBSET_1, FUNCT_1, ORDINAL1, RELSET_1, FINSET_1,
      XXREAL_0, XREAL_0, NAT_1, INT_1, CARD_1, FINSEQ_1, NEWTON, STRUCT_0,
      GROUP_2, GROUP_1, GROUP_3, GROUP_4, GR_CY_1, FUNCT_2, NAT_3, REALSET1,
      VALUED_0, DYNKIN, GROUP_10, NUMBERS, ALGSTR_0, GRSOLV_1, GRNILP_1,
      RELAT_1, BINOP_2, MEMBERED, FINSEQ_2, REAL_1, MOEBIUS1, GROUP_6;
 requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM;
 definitions GROUP_1, GROUP_2, TARSKI, REALSET1, RELAT_1, WELLORD2, STRUCT_0,
      FUNCT_2, GROUP_10, INT_1, BINOP_1, FINSEQOP, RLVECT_1, SETWISEO, GR_CY_1,
      NEWTON, GRSOLV_1, GRNILP_1, GROUP_5, ALGSTR_0, MOEBIUS1, XXREAL_0,
      GROUP_4, INT_2, GROUP_6, ZFMISC_1, ORDINAL1;
 theorems GROUP_2, GROUP_3, GROUP_6, NAT_1, GROUP_1, ORDINAL1, STRUCT_0, NAT_D,
      GR_CY_1, NEWTON, PEPIN, GROUP_8, NAT_3, GROUP_10, INT_2, GROUP_5,
      MOEBIUS1, NAT_5, GROUP_11, GROUP_4, TARSKI;
 schemes NAT_1;

begin :: $p$-Groups

reserve G for Group,
  a,b for Element of G,
  m, n for Nat,
  p for prime (natural number);

theorem Th1:
  (for r being natural number holds n <> p |^ r) implies
  ex s being Element of NAT st s is prime & s divides n & s <> p
proof
  assume
A1: for r being natural number holds n <> p |^ r;
  per cases;
  suppose
A2:  n = 0;
    per cases;
    suppose
A3:   p = 2;
      take s = 3;
      thus s is prime by PEPIN:44;
      thus s divides n by A2,INT_2:16;
      thus s <> p by A3;
    end;
    suppose
A4:   p <> 2;
      take s = 2;
      thus s is prime by INT_2:44;
      thus s divides n by A2,INT_2:16;
      thus s <> p by A4;
    end;
  end;
  suppose
A5: n <> 0;
A6: p > 1 by INT_2:def 5;
  reconsider r1 = p |-count n as Element of NAT;
A7: p |^ r1 divides n by A5,A6,NAT_3:def 7;
A8: not p |^ (r1+1) divides n by A5,A6,NAT_3:def 7;
  consider s1 be natural number such that
A9: n = p |^ r1 * s1 by A7,NAT_D:def 3;
  s1 >= 2
  proof
    assume not s1 >= 2;
    then s1 < 1 + 1;
    then s1 <= 1 by NAT_1:13;
    then s1 = 0 or s1 = 1 by NAT_1:26;
    hence contradiction by A5,A1,A9;
  end;
  then consider s be Element of NAT such that
A10: s is prime and
A11: s divides s1 by INT_2:48;
A12: s1 divides n by A9,NAT_D:def 3;
  take s;
  s <> p
  proof
    assume s = p;
    then consider s2 be natural number such that
A13: s1 = p * s2 by A11,NAT_D:def 3;
    n = p |^ r1 * p * s2 by A9,A13
     .= p |^ (r1+1) * s2 by NEWTON:11;
    hence contradiction by A8,NAT_D:def 3;
  end;
  hence thesis by A10,A11,A12,NAT_D:4;
end;
end;

theorem Th2:
  for n,m being natural number holds n divides p |^ m implies
  ex r be natural number st n = p |^ r & r <= m
proof
  let n,m be natural number;
  assume
A1: n divides p |^ m;
  n > 0
  proof
    assume n <= 0;
    then n = 0;
    hence contradiction by A1,INT_2:3;
  end;
  then n in NatDivisors (p|^ m) by A1,MOEBIUS1:39;
  then n in {p|^ k where k is Element of NAT : k <= m} by NAT_5:19;
  then consider r be Element of NAT such that
A2: n = p|^ r & r <= m;
  take r;
  thus thesis by A2;
end;

theorem Th3:
  a |^ n = 1_G implies a" |^ n = 1_G
proof
  assume a |^ n = 1_G;
  then a" |^ n = (1_G)" by GROUP_1:72
          .= 1_G by GROUP_1:16;
  hence thesis;
end;

theorem Th4:
  a" |^ n = 1_G implies a |^ n = 1_G
proof
  a"" = a;
  hence thesis by Th3;
end;

theorem Th5:
  ord (a") = ord a
proof
  a |^ ord a = 1_G by GROUP_1:82;
  then a" |^ ord a = 1_G by Th3; then
A1: ord (a") divides ord a by GROUP_1:86;
  a" |^ ord (a") = 1_G by GROUP_1:82;
  then a |^ ord (a") = 1_G by Th4;
  then ord a divides ord (a") by GROUP_1:86;
  hence thesis by A1,NAT_D:5;
end;

theorem Th6:
  ord (a |^ b) = ord a
proof
  (a |^ b) |^ ord a = (a |^ ord a) |^ b by GROUP_3:33
                     .= (1_G) |^ b by GROUP_1:82
                     .= 1_G by GROUP_3:22; then
A1: ord (a |^ b) divides ord a by GROUP_1:86;
  (a |^ ord (a |^ b)) |^ b = (a |^ b) |^ ord (a |^ b) by GROUP_3:33
                          .= 1_G by GROUP_1:82;
  then ord a divides ord (a |^ b) by GROUP_3:23,GROUP_1:86;
  hence thesis by A1,NAT_D:5;
end;

theorem Th7:
  for G being Group, N being Subgroup of G
  for a,b being Element of G holds
  N is normal & b in N implies
  for n ex g being Element of G st g in N & (a * b)|^ n = a |^ n * g
proof
  let G be Group;
  let N be Subgroup of G;
  let a,b be Element of G;
  assume
A1: N is normal & b in N;
   defpred P[Nat] means for n ex g being Element of G
   st g in N & (a * b)|^ $1 = a |^ $1 * g;
A2: (a * b)|^ 0 = 1_G by GROUP_1:43;
    a |^ 0 * 1_G = 1_G * 1_G by GROUP_1:43
                .= 1_G by GROUP_1:def 5;
    then
A3: P[0] by A2,GROUP_2:55;
A4: now let n;
    assume P[n];
    then consider g1 be Element of G such that
A5: g1 in N & (a * b)|^ n = a |^ n * g1;
A6: (a * b)|^ (n + 1) = a |^ n * g1 * (a * b) by A5,GROUP_1:66
                     .= a |^ n * (g1 * (a * b)) by GROUP_1:def 4
                     .= a |^ n * ((g1 * a) * b) by GROUP_1:def 4;
    a * N = N * a by A1,GROUP_3:140;
    then g1 * a in a * N by A5, GROUP_2:126;
    then consider g2 be Element of G such that
A7: g1 * a = a * g2 & g2 in N by GROUP_2:125;
 (g1 * a) * b = a * (g2 * b) by A7,GROUP_1:def 4;
then  a |^ n * ((g1 * a) * b) = a |^ n * a * (g2 * b) by GROUP_1:def 4
                            .= a |^ (n + 1) * (g2 * b) by GROUP_1:66;
    hence P[n+1] by A1,A6,A7,GROUP_2:59;
  end;
  for n holds P[n] from NAT_1:sch 2(A3,A4);
  hence thesis;
end;

theorem Th8:
  for G being Group, N being normal Subgroup of G,
      a being Element of G, S being Element of G./.N holds
      S = a * N implies
  for n holds S |^ n = (a |^ n) * N
proof
  let G be Group;
  let N be normal Subgroup of G;
  let a be Element of G;
  let S be Element of G./.N;
  assume
A1: S = a * N;
  defpred P[Nat] means for n holds S |^ $1 = (a |^ $1) * N;
A2: S |^ 0 = 1_ (G./.N) by GROUP_1:43;
  (a |^ 0) * N = 1_G * N by GROUP_1:43
              .= carr N by GROUP_2:132;
  then
A3: P[0] by A2,GROUP_6:29;
A4: now
    let n;
    assume
A5: P[n];
 S |^ (n + 1) = S |^ n * S by GROUP_1:66
                .= @ (S |^ n) * @ S by GROUP_6:def 4
                .= ((a |^ n) * N) * (a * N) by A1,A5
                .= ((a |^ n) * a) * N  by GROUP_11:1
                .= (a |^ (n + 1)) * N by GROUP_1:66;
    hence P[n+1];
    end;
  for n holds P[n] from NAT_1:sch 2(A3,A4);
  hence thesis;
end;

theorem Th9:
  for G being Group, H being Subgroup of G, a,b being Element of G
  holds a * H = b * H implies ex h being Element of G st a = b * h & h in H
proof
  let G be Group;
  let H be Subgroup of G;
  let a,b be Element of G;
  a in a * H by GROUP_2:130;
  hence thesis by GROUP_2:125;
end;

theorem Th10:
  for G being finite Group, N being normal Subgroup of G holds
  N is Subgroup of center G & G./.N is cyclic
  implies G is commutative
proof
  let G be finite Group;
  let N be normal Subgroup of G;
  assume that
A1: N is  Subgroup of center G and
A2: G./.N is cyclic;
  reconsider I = G./.N as finite Group;
  consider S be Element of I such that
A3: for T being Element of I ex n being Nat st T = S |^ n
   by A2,GR_CY_1:42;
  consider a1 be Element of G such that
A4: S = a1 * N & S = N * a1 by GROUP_6:26;
  for a,b being Element of G holds a * b = b * a
  proof
    let a,b be Element of G;
A5: a * N is Element of I & b * N is Element of I by GROUP_6:27;
    then consider r1 be Nat such that
A6: a * N = S |^ r1 by A3;
    a * N = (a1 |^ r1) * N by A4,Th8,A6;
    then consider c1 be Element of G such that
A7: a = (a1 |^ r1) * c1 & c1 in N by Th9;
A8: c1 in center G by A1,A7,GROUP_2:49;
    consider r2 be Nat such that
A9: b * N = S |^ r2 by A3,A5;
    b * N = (a1 |^ r2) * N by A4,Th8,A9;
    then consider c2 be Element of G such that
A10: b = (a1 |^ r2) * c2 & c2 in N by Th9;
A11: c2 in center G by A1,A10,GROUP_2:49;
    a * b = (a1 |^ r1) * (c1 * ((a1 |^ r2) * c2)) by A7,A10,GROUP_1:def 4
         .= (a1 |^ r1) * (((a1 |^ r2) * c2) * c1) by A8,GROUP_5:89
         .= (a1 |^ r1) * ((a1 |^ r2) * (c2 * c1)) by GROUP_1:def 4
         .= ((a1 |^ r1) * (a1 |^ r2)) * (c2 * c1) by GROUP_1:def 4
         .= (a1 |^ (r1 + r2)) * (c2 * c1) by GROUP_1:63
         .= ((a1 |^ r2) * (a1 |^ r1)) * (c2 * c1) by GROUP_1:63
         .= (a1 |^ r2) * ((a1 |^ r1) * (c2 * c1)) by GROUP_1:def 4
         .= (a1 |^ r2) * ((a1 |^ r1) * c2 * c1) by GROUP_1:def 4
         .= (a1 |^ r2) * (c2 * (a1 |^ r1) * c1) by A11,GROUP_5:89
         .= (a1 |^ r2) * (c2 * ((a1 |^ r1) * c1)) by GROUP_1:def 4
         .= b * a by GROUP_1:def 4,A7,A10;
    hence thesis;
  end;
  hence thesis by GROUP_1:def 16;
end;

theorem
  for G being finite Group, N being normal Subgroup of G holds
  N = center G & G./.N is cyclic implies G is commutative
proof
  let G be finite Group;
  let N be normal Subgroup of G;
  assume
A1: N = center G & G./.N is cyclic;
  then N is Subgroup of center G by GROUP_2:63;
  hence thesis by A1,Th10;
end;

theorem
  for G being finite Group, H being Subgroup of G holds
  card H <> card G implies ex a being Element of G st not a in H
proof
  let G be finite Group;
  let H be Subgroup of G;
  assume
A1: card H <> card G;
  assume not ex a being Element of G st not a in H;
  then the multMagma of H = the multMagma of G by GROUP_2:71;
  hence contradiction by A1;
end;

definition
  let p be natural number;
  let G be Group;
  let a be Element of G;
  attr a is p-element means   :Def1:
  ex r being natural number st ord a = p |^ r;
end;

theorem Th13:
  1_G is m-element
proof
A1: ord 1_G = 1 by GROUP_1:84;
  m |^ 0 = 1 by NEWTON:9;
  hence thesis by A1,Def1;
end;

registration
  let G,m;
  cluster m-element Element of G;
  existence
  proof
    take 1_G;
    thus thesis by Th13;
  end;
end;

registration
  let p,G;
  let a be p-element Element of G;
  cluster a" -> p-element;
coherence
proof
  consider n be natural number such that
A1:ord a = p |^ n by Def1;
   ord (a") = p |^ n by A1,Th5;
  hence thesis by Def1;
end;
end;

theorem
  a |^ b is p-element implies a is p-element
proof
  assume a |^ b is p-element;
  then consider r be natural number such that
A1: ord (a |^ b) = p |^ r by Def1;
  ord a = p |^ r by A1,Th6;
  hence thesis by Def1;
end;

registration
  let p,G,b;
  let a be p-element Element of G;
  cluster a |^ b -> p-element;
  coherence
  proof
    consider n be natural number such that
A1: ord a = p |^ n by Def1;
    ord (a |^ b) = p |^ n by A1,Th6;
    hence thesis by Def1;
  end;
end;

registration
  let p;
  let G be commutative Group, a,b be p-element Element of G;
  cluster a * b -> p-element;
  coherence
proof
   consider n be natural number such that
A1: ord a = p |^ n by Def1;
   consider m be natural number such that
A2: ord b = p |^ m by Def1;
A3: a |^ (p |^(n + m)) = a |^ (p |^ n * p |^ m) by NEWTON:13
                     .= a |^ (p |^ n) |^ (p |^ m) by GROUP_1:67
                     .= (1_G) |^ (p |^ m) by A1,GROUP_1:82
                     .= 1_G by GROUP_1:61;
 b |^ (p |^(n + m)) = b |^ (p |^ m * p |^ n) by NEWTON:13
                     .= b |^ (p |^ m) |^ (p |^ n) by GROUP_1:67
                     .= (1_G) |^ (p |^ n) by A2,GROUP_1:82
                     .= 1_G by GROUP_1:61;
  then (a * b) |^ (p |^(n + m)) = 1_G * 1_G by A3,GROUP_1:96
     .= 1_G by GROUP_1:def 5;
  then consider r be natural number such that
A4: ord (a * b) = p |^ r & r <= (n + m) by GROUP_1:86,Th2;
  take r;
  thus thesis by A4;
end;
end;

registration
  let p;
  let G be finite p-group Group;
  cluster -> p-element Element of G;
  coherence
proof
  let a be Element of G;
  consider m be natural number such that
A1: card G = p |^ m by GROUP_10:def 17;
  ex r be natural number st
  ord a = p |^ r & r <= m by A1,GR_CY_1:28,Th2;
  hence thesis by Def1;
end;
end;

theorem Th15:
  for G being finite Group,H being Subgroup of G
  for a being Element of G st H is p-group & a in H
  holds a is p-element
proof
  let G be finite Group;
  let H be Subgroup of G;
  let a be Element of G;
  assume that
A1: H is p-group and
A2: a in H;
 a is Element of H by A2,STRUCT_0:def 5;
  then consider b be Element of H such that
A3: b= a;
  consider r be natural number such that
A4: ord b = p |^ r by A1,Def1;
  ord a = p |^ r by A3,GROUP_8:5,A4;
  hence thesis by Def1;
end;

registration
  let p;
  let G be finite p-group Group;
  cluster -> p-group Subgroup of G;
coherence
  proof
    let H be Subgroup of G;
    consider m be natural number such that
A1: card G = p |^ m by GROUP_10:def 17;
    ex r be natural number st card H = p |^ r & r <= m by A1,GROUP_2:178,Th2;
    hence thesis by GROUP_10:def 17;
  end;
end;

theorem Th16:
  (1).G is p-group
proof
  take 0;
  thus card (1).G = 1 by GROUP_2:81
  .= p |^ 0 by NEWTON:9;
end;

registration
  let p;
  let G be Group;
  cluster p-group Subgroup of G;
  existence
  proof
    take (1).G;
    thus thesis by Th16;
  end;
end;

registration
  let p;
  let G be finite Group, G1 be p-group Subgroup of G, G2 be Subgroup of G;
  cluster G1 /\ G2 -> p-group;
coherence
proof
  reconsider H1 = G1 /\ G2 as Subgroup of G1 by GROUP_2:106;
  H1 is p-group;
  hence thesis;
end;
  cluster G2 /\ G1 -> p-group;
coherence;
end;

theorem Th17:
  for G being finite Group st for a being Element of G holds a is p-element
  holds G is p-group
proof
  let G be finite Group;
  assume
A1: for a being Element of G holds a is p-element;
  assume not G is p-group;
  then for r being natural number holds card G <> p |^ r by GROUP_10:def 17;
  then consider s be Element of NAT such that
A2: s is prime & s divides card G and
A3: s <> p by Th1;
  consider b be Element of G such that
A4: ord b = s by A2,GROUP_10:13;
  b is p-element by A1;
  then ex r1 be natural number st ord b = p |^ r1 by Def1;
  hence contradiction by A2,A4,NAT_3:6,A3;
end;

registration
  let p;
  let G be finite p-group Group, N being normal Subgroup of G;
  cluster G./.N -> p-group;
  coherence
proof
  consider r be natural number such that
A1: card G = p |^ r by GROUP_10:def 17;
A2: card G = card N * index N by GROUP_2:177;
A3: card(G./.N) = index N by GROUP_6:33;
  reconsider n = card(G./.N) as natural number;
  n divides p |^ r by A1,A2,NAT_D:def 3,A3;
  then ex r1 be natural number st
  n = p |^ r1 & r1 <= r by Th2;
  hence thesis by GROUP_10:def 17;
end;
end;

theorem
  for G being finite Group, N being normal Subgroup of G
  st N is p-group & G./.N is p-group holds
  G is p-group
proof
  let G be finite Group;
  let N be normal Subgroup of G;
  assume that
A1: N is p-group and
A2: G./.N is p-group;
  consider r1 be natural number such that
A3: card N = p |^ r1 by A1,GROUP_10:def 17;
  consider r2 be natural number such that
A4: card (G./.N) = p |^ r2 by A2,GROUP_10:def 17;
 card(G./.N) = index N by GROUP_6:33;
  then card G = p |^ r1 * p |^ r2 by A3,A4,GROUP_2:177
        .= p |^ (r1 + r2) by NEWTON:13;
  hence thesis by GROUP_10:def 17;
end;

theorem Th19:
  for G being finite commutative Group,H,H1,H2 being Subgroup of G st
  H1 is p-group & H2 is p-group &
  the carrier of H = H1 * H2 holds H is p-group
proof
  let G be finite commutative Group;
  let H,H1,H2 be Subgroup of G;
  assume that
A1: H1 is p-group & H2 is p-group and
A2: the carrier of H = H1 * H2;
for a being Element of H holds a is p-element
  proof
    let a be Element of H;
    a in H1 * H2 by A2;
    then consider b1,b2 be Element of G such that
A3: a = b1 * b2 & b1 in H1 & b2 in H2 by GROUP_11:6;
    b1 is p-element & b2 is p-element by A1,A3,Th15;
    then consider r be natural number such that
A4: ord (b1 * b2) = p |^ r by Def1;
    ord a = p |^ r by A3,GROUP_8:5,A4;
    hence thesis by Def1;
  end;
  hence thesis by Th17;
end;

theorem Th20:
  for G being finite Group, H,N being Subgroup of G holds
  N is normal Subgroup of G &
  H is p-group & N is p-group
  implies ex P being strict Subgroup of G st the carrier of P = H * N &
  P is p-group
proof
  let G be finite Group;
  let H,N be Subgroup of G;
  assume that
A1: N is normal Subgroup of G and
A2: H is p-group & N is p-group;
  H * N = N * H by A1,GROUP_5:8;
  then consider P be strict Subgroup of G such that
A3: the carrier of P = H * N by GROUP_2:93;
A4: for a being Element of P holds a is p-element
  proof
    let a be Element of P;
    a in H * N by A3;
    then consider b,c be Element of G such that
A5: a = b * c & b in H & c in N by GROUP_11:6;
    b is p-element by A5,A2,Th15;
    then consider n be natural number such that
A6: ord b = p |^ n by Def1;
A7: b |^(p |^ n) = 1_G by A6,GROUP_1:82;
    consider d be Element of G such that
A8: d in N & (b * c) |^(p |^ n) = b |^(p |^ n) * d by A1,A5,Th7;
    d is p-element by A2,A8,Th15;
    then consider m be natural number such that
A9: ord d = p |^ m by Def1;
A10: d |^(p |^ m) = 1_G by A9,GROUP_1:82;
A11:a |^(p |^ (n + m)) = (b * c) |^(p |^ (n + m)) by A5,GROUP_8:4
                      .= (b * c) |^(p |^ n * (p |^ m)) by NEWTON:13
                      .= (b * c) |^(p |^ n) |^ (p |^ m) by GROUP_1:67
                      .= 1_G by A7,A8,GROUP_1:def 5,A10;
    reconsider a1 = a as Element of G by GROUP_2:51;
    a1 |^(p |^ (n + m)) = 1_G by A11,GROUP_8:4;
    then consider r be natural number such that
A12: ord a1 = p |^ r & r <= n + m by GROUP_1:86,Th2;
 ord a = p |^ r by A12,GROUP_8:5;
    hence thesis by Def1;
  end;
  take P;
  thus thesis by A3,A4,Th17;
end;

theorem Th21:
  for G being finite Group,N1,N2 being normal Subgroup of G
  holds N1 is p-group &
  N2 is p-group implies ex N being strict normal Subgroup of G
  st the carrier of N = N1 * N2 & N is p-group
proof
  let G be finite Group;
  let N1,N2 be normal Subgroup of G;
  assume N1 is p-group & N2 is p-group; then
  consider N be strict Subgroup of G such that
A1: the carrier of N = N1 * N2 & N is p-group by Th20;
  for x,y be Element of G st y in N holds x * y * x" in N
  proof
    let x,y be Element of G;
    assume y in N;
    then y in the carrier of N by STRUCT_0:def 5;
    then consider a,b be Element of G such that
A2: y = a * b & a in N1 & b in N2 by A1,GROUP_11:6;
A3: x * y * x" =((x * a) * b) * x" by A2,GROUP_1:def 4
              .=(x * a) * (b * x") by GROUP_1:def 4
              .=(x * a) * 1_G * (b * x") by GROUP_1:def 5
              .=(x * a) * (x" * x) * (b * x") by GROUP_1:def 6
              .=(x * a) * x" * x * (b * x") by GROUP_1:def 4
              .=((x * a) * x") * (x * (b * x")) by GROUP_1:def 4
              .=(x * a * x") * (x * b * x") by GROUP_1:def 4;
    x * a * x" in N1 & x * b * x" in N2 by A2,GROUP_11:4;
    then x * y * x" in N1 * N2 by A3,GROUP_11:6;
    hence thesis by A1,STRUCT_0:def 5;
  end;
  then N is normal Subgroup of G by GROUP_11:5;
  hence thesis by A1;
end;

registration
  let p;
  let G be p-group finite Group, H be finite Group, g be Homomorphism of G,H;
  cluster Image g -> p-group;
  coherence
proof
  for h being Element of Image g holds h is p-element
  proof
    let h be Element of Image g;
    h in Image g by STRUCT_0:def 5;
    then consider a be Element of G such that
A1: h = g.a by GROUP_6:54;
    consider n be natural number such that
A2: ord a = p |^ n by Def1;
A3: g.(a |^(p |^ n)) = (g.a) |^(p |^ n) by GROUP_6:46
                    .= h |^(p |^ n) by A1,GROUP_8:4;
A4: g.(a |^(p |^ n)) = g.(1_G) by A2,GROUP_1:82
                    .= 1_H by GROUP_6:40;
    reconsider h1 = h as Element of H by GROUP_2:51;
  h1 |^(p |^ n) = 1_H by A3,A4,GROUP_8:4;
    then consider r be natural number such that
A5: ord h1 = p |^ r & r <= n by GROUP_1:86,Th2;
    ord h = p |^ r by A5,GROUP_8:5;
    hence thesis by Def1;
  end;
  hence thesis by Th17;
end;
end;

theorem Th22:
  for G,H being strict Group holds G,H are_isomorphic &
  G is p-group implies H is p-group
proof
  let G,H being strict Group;
  assume that
A1: G,H are_isomorphic and
A2: G is p-group;
  consider r be natural number such that
A3: card G = p |^ r by A2,GROUP_10:def 17;
  card H = p |^ r by A1,A3,GROUP_6:84;
  hence thesis by GROUP_10:def 17;
end;

definition
  let p be prime (natural number);
  let G be Group such that
A1: G is p-group;
  func expon (G,p) -> Nat means
  :Def2:
  card G = p |^ it;
  existence by A1,GROUP_10:def 17;
  uniqueness
  proof
    let a,b be Nat such that
A2: card G = p |^ a and
A3: card G = p |^ b;
   p > 1 by INT_2:def 5;
   hence thesis by A2,A3,PEPIN:31;
  end;
end;

definition
  let p be prime (natural number);
  let G be Group;
  redefine func expon (G,p) -> Element of NAT;
  coherence by ORDINAL1:def 13;
end;

theorem
  for G being finite Group, H being Subgroup of G st
  G is p-group holds expon (H,p) <= expon (G,p)
proof
  let G be finite Group;
  let H be Subgroup of G;
  assume
A1: G is p-group;
  then card G = p |^ expon (G,p) by Def2;
  then ex r be natural number st
  card H = p |^ r & r <= expon (G,p) by GROUP_2:178,Th2;
  hence thesis by A1,Def2;
end;

theorem Th24:
  for G being strict finite Group st G is p-group & expon (G,p) = 0 holds
  G = (1).G
proof
  let G be strict finite Group;
  assume G is p-group & expon (G,p) = 0; then
A1: card G = p |^ 0 by Def2
          .= 1 by NEWTON:9;
  card (1).G = 1 by GROUP_2:81;
  hence thesis by A1,GROUP_2:85;
end;

theorem Th25:
  for G being strict finite Group holds G is p-group &
  expon (G,p) = 1 implies G is cyclic
proof
  let G be strict finite Group;
  assume G is p-group & expon (G,p) = 1;
  then card G = p |^ 1 by Def2
             .= p by NEWTON:10;
  hence thesis by GR_CY_1:45;
end;

theorem
  for G being finite Group,p being prime (natural number)
  for a being Element of G holds G is p-group & expon (G,p) = 2 &
  ord a = p |^2 implies G is commutative
proof
  let G be finite Group;
  let p be prime (natural number);
  let a be Element of G;
  assume that
A1: G is p-group & expon (G,p) = 2 and
A2: ord a = p |^2;
  card G = p |^2 by A1,Def2;
  then G is cyclic by A2,GR_CY_1:43;
  hence thesis;
end;

begin :: Commutative $p$-Groups

definition
  let p be natural number;
  let G be Group;
  attr G is p-commutative-group-like means
  :Def3:
  for a,b be Element of G holds (a * b) |^ p = a |^ p * (b |^ p);
end;

definition
  let p be natural number;
  let G be Group;
  attr G is p-commutative-group means
  :Def4:
  G is p-group p-commutative-group-like;
end;

registration
  let p be natural number;
  cluster p-commutative-group -> p-group p-commutative-group-like Group;
  coherence by Def4;
  cluster p-group p-commutative-group-like -> p-commutative-group Group;
  coherence by Def4;
end;

theorem Th27:
  (1).G is p-commutative-group-like
  proof
    let a,b be Element of (1).G;
A1: the carrier of (1).G = {1_G} by GROUP_2:def 7;
    hence (a * b) |^ p = 1_G by TARSKI:def 1
    .= a |^ p * (b |^ p) by A1,TARSKI:def 1;
  end;

registration
  let p;
  cluster p-commutative-group finite cyclic commutative Group;
  existence
  proof
    take (1).the Group;
    (1).the Group is p-commutative-group-like p-group by Th16,Th27;
    hence thesis;
  end;
end;

registration
  let p;
  let G be p-commutative-group-like finite Group;
  cluster -> p-commutative-group-like Subgroup of G;
coherence
proof
  let H be Subgroup of G;
  let a,b be Element of H;
  reconsider a2 = a, b2 = b as Element of G by GROUP_2:51;
A1: a * b = a2 * b2 by GROUP_8:2;
A2:a |^ p = a2 |^ p & b |^ p = b2 |^ p by GROUP_8:4;
  thus (a * b) |^ p = (a2 * b2) |^ p by A1,GROUP_8:4
  .= a2 |^ p * (b2 |^ p) by Def3
  .= a |^ p * (b |^ p) by A2,GROUP_8:2;
end;
end;

registration
  let p;
  cluster p-group finite commutative -> p-commutative-group Group;
  coherence
proof
  let G be Group such that
A1: G is p-group finite commutative;
  for a,b being Element of G holds (a * b) |^ p = a |^ p * (b |^ p)
  by A1,GROUP_1:96;
  then G is p-commutative-group-like by Def3;
  hence thesis by A1;
end;
end;

theorem
  for G being strict finite Group st card G = p holds
  G is p-commutative-group
proof
  let G be strict finite Group;
  assume
A1: card G = p;
  p = p |^1 by NEWTON:10; then
A2: G is p-group by A1,GROUP_10:def 17;
  G is cyclic Group by A1,GR_CY_1:45;
  hence thesis by A2;
end;

registration
  let p,G;
  cluster p-commutative-group finite Subgroup of G;
  existence
  proof
    take (1).G;
    (1).G is p-commutative-group-like p-group by Th16,Th27;
    hence thesis;
  end;
end;

registration
  let p;
  let G be finite Group, H1 be p-commutative-group-like Subgroup of G,
  H2 be Subgroup of G;
  cluster H1 /\ H2 -> p-commutative-group-like;
coherence
proof
  reconsider H = H1 /\ H2 as Subgroup of H1 by GROUP_2:106;
  H is p-commutative-group-like;
  hence thesis;
end;
  cluster H2 /\ H1 -> p-commutative-group-like;
coherence;
end;

registration
  let p;
  let G be finite p-commutative-group-like Group,
      N be normal Subgroup of G;
  cluster G./.N -> p-commutative-group-like;
coherence
proof
    let S,T be Element of G./.N;
    consider a be Element of G such that
A1: S = a * N & S = N * a by GROUP_6:26;
    consider b be Element of G such that
A2: T = b * N & T = N * b by GROUP_6:26;
A3: S * T = @ S * @ T by GROUP_6:24
         .=(a * b) * N by A1,A2,GROUP_11:1;
    set c = a * b;
A4: (S * T) |^ p = (c |^ p) * N by A3,Th8
                .= (a |^ p * (b |^ p))* N by Def3
                .= ((a |^ p) * N) * ((b |^ p) * N) by GROUP_11:1;
A5: S |^ p = (a |^ p) * N by A1,Th8;
    T |^ p = (b |^ p) * N by A2,Th8;
    hence thesis by A4,A5,GROUP_6:def 4;
end;
end;

theorem
  for G being finite Group,a,b being Element of G st
  G is p-commutative-group-like
  holds for n holds (a * b) |^ (p |^n) = a |^ (p |^n) * (b |^ (p |^n))
proof
  let G be finite Group;
  let a,b be Element of G;
  assume
A1: G is p-commutative-group-like;
  defpred P[Nat] means for n holds
  (a * b) |^ (p |^ $1) = a |^ (p |^$1) * (b |^ (p |^$1));
A2: (a * b) |^ (p |^0) = (a * b) |^ 1 by NEWTON:9
                      .= a * b by GROUP_1:44;
  a |^ (p |^0) * (b |^ (p |^0)) = a |^ 1 * (b |^ (p |^0)) by NEWTON:9
                               .= a * (b |^ (p |^0)) by GROUP_1:44
                               .= a * (b |^1) by NEWTON:9
                               .= a * b by GROUP_1:44;
  then
A3: P[0] by A2;
A4: now
    let n;
    assume
A5: P[n];
    set a1 = a |^ (p |^n), b1 = b |^ (p |^n);
 (a * b) |^ (p |^ (n + 1)) = (a * b) |^ (p |^ n * p) by NEWTON:11
                .= ((a * b) |^ (p |^ n)) |^ p by GROUP_1:67
                .= (a |^ (p |^n) * (b |^ (p |^n))) |^ p by A5
                .= a1 |^ p * (b1 |^ p) by A1,Def3
                .= a |^ ((p |^n) * p) * (b |^ (p |^n) |^ p) by GROUP_1:67
                .= a |^ ((p |^n) * p) * (b |^ ((p |^n) * p)) by GROUP_1:67
                .= a |^ (p |^(n +1)) * (b |^ ((p |^n) * p)) by NEWTON:11
                .= a |^ (p |^(n +1)) * (b |^ (p |^(n +1))) by NEWTON:11;
    hence P[n+1];
    end;
  for n holds P[n] from NAT_1:sch 2(A3,A4);
  hence thesis;
end;

theorem
  for G being finite commutative Group,H,H1,H2 being Subgroup of G st
  H1 is p-commutative-group & H2 is p-commutative-group &
  the carrier of H = H1 * H2 holds H is p-commutative-group
proof
  let G be finite commutative Group;
  let H,H1,H2 be Subgroup of G;
  assume that
A1: H1 is p-commutative-group &
  H2 is p-commutative-group and
A2: the carrier of H = H1 * H2;
  H is p-group by A1,A2,Th19;
  hence thesis;
end;

theorem
  for G being finite Group, H being Subgroup of G,
    N being strict normal Subgroup of G holds
    N is Subgroup of center G &
    H is p-commutative-group &
    N is p-commutative-group implies
  ex P being strict Subgroup of G st the carrier of P = H * N &
  P is p-commutative-group
proof
  let G be finite Group;
  let H be Subgroup of G;
  let N be strict normal Subgroup of G;
  assume that
A1: N is Subgroup of center G and
A2: H is p-commutative-group & N is p-commutative-group;
  consider P be strict Subgroup of G such that
A3: the carrier of P = H * N & P is p-group by A2,Th20;
  set P1 = P;
  for a,b being Element of P holds (a * b) |^ p = a |^ p * (b |^ p)
  proof
    let a,b be Element of P;
A4: a in H * N & b in H * N by A3;
    then consider a1,a2 be Element of G such that
A5: a = a1 * a2 & a1 in H & a2 in N by GROUP_11:6;
A6: a2 in center G by A1,A5,GROUP_2:49;
    consider b1,b2 be Element of G such that
A7: b = b1 * b2 & b1 in H & b2 in N by A4,GROUP_11:6;
A8: b2 in center G by A1,A7,GROUP_2:49;
    then a2 * b2 in center G & b2 * a2 in center G by A6,GROUP_2:59;
    then
A9: (a1 * b1) * (b2 * a2) = (b2 * a2) * (a1 * b1) by GROUP_5:89;
    reconsider c1 = a1,d1 = b1 as Element of H by A5,A7,STRUCT_0:def 5;
A10: a1 |^ p = c1 |^ p & b1 |^ p = d1 |^ p by GROUP_4:4;
    a1 * b1 = c1 * d1 by GROUP_2:52; then
A11: (a1 * b1) |^ p = (c1 * d1) |^ p by GROUP_8:4
                   .= c1 |^ p * (d1 |^ p) by A2,Def3
                   .= a1 |^ p * (b1 |^ p) by A10,GROUP_2:52;
    reconsider c2 = a2,d2 = b2 as Element of N by A5,A7,STRUCT_0:def 5;
A12: a2 |^ p = c2 |^ p & b2 |^ p = d2 |^ p by GROUP_4:4;
    b2 * a2 = d2 * c2 by GROUP_2:52; then
A13: (b2 * a2) |^ p = (d2 * c2) |^ p by GROUP_8:4
                   .= d2 |^ p * (c2 |^ p) by  A2,Def3
                   .= b2 |^ p * (a2 |^ p) by A12,GROUP_2:52;
A14: a2 |^ p in center G by A6,GROUP_4:6;
A15: a1 * a2 = a2 * a1 by A6,GROUP_5:89;
A16: b1 * b2 = b2 * b1 by A8,GROUP_5:89;
    a * b = (a1 * a2) * (b1 * b2) by A5,A7,GROUP_2:52; then
A17: (a * b) |^ p = (a1 * a2 * (b1 * b2))|^ p by GROUP_8:4
             .= (a1 * (a2 * (b1 * b2)))|^ p by GROUP_1:def 4
             .= (a1 * ((b1 * b2) * a2))|^ p by A6,GROUP_5:89
             .= (a1 * (b1 * (b2 * a2)))|^ p by GROUP_1:def 4
             .= ((a1 * b1) * (b2 * a2))|^ p by GROUP_1:def 4
             .= (a1 * b1)|^ p * ((b2 * a2)|^ p) by A9,GROUP_1:73
             .= a1 |^ p * (b1 |^ p) * (a2 |^ p * (b2 |^ p)) by A11,A13,A14,
              GROUP_5:89
             .= a1 |^ p * (b1 |^ p * (a2 |^ p * (b2 |^ p))) by GROUP_1:def 4
             .= a1 |^ p * ((b1 |^ p * (a2 |^ p)) * (b2 |^ p)) by GROUP_1:def 4
             .= a1 |^ p * ((a2 |^ p * (b1 |^ p)) * (b2 |^ p)) by A14,GROUP_5:89
             .= (a1 |^ p * (a2 |^ p * (b1 |^ p))) * (b2 |^ p) by GROUP_1:def 4
             .= (a1 |^ p * (a2 |^ p) * (b1 |^ p)) * (b2 |^ p) by GROUP_1:def 4
             .= (a1 |^ p * (a2 |^ p)) * (b1 |^ p * (b2 |^ p)) by GROUP_1:def 4
             .= (a1 * a2)|^ p * (b1 |^ p * (b2 |^ p)) by A15,GROUP_1:73
             .= (a1 * a2)|^ p * ((b1 * b2) |^ p) by A16,GROUP_1:73;
A18:   a |^ p = (a1 * a2)|^ p by A5,GROUP_4:4;
       b |^ p = (b1 * b2)|^ p by A7,GROUP_4:4;
    hence thesis by A17,A18,GROUP_2:52;
  end;
  then P1 is p-commutative-group-like by Def3;
  hence thesis by A3;
end;

theorem
  for G being finite Group,N1,N2 being normal Subgroup of G holds
  N2 is Subgroup of center G & N1 is p-commutative-group &
  N2 is p-commutative-group implies
  ex N being strict normal Subgroup of G
  st the carrier of N = N1 * N2 & N is p-commutative-group
proof
  let G be finite Group;
  let N1,N2 be normal Subgroup of G;
  assume that
A1: N2 is Subgroup of center G and
A2: N1 is p-commutative-group & N2 is p-commutative-group;
  consider N be strict normal Subgroup of G such that
A3: the carrier of N = N1 * N2 & N is p-group by A2,Th21;
 for a,b being Element of N holds (a * b) |^ p = a |^ p * (b |^ p)
  proof
    let a,b be Element of N;
A4: a in N1 * N2 & b in N1 * N2 by A3;
    then consider a1,a2 be Element of G such that
A5: a = a1 * a2 & a1 in N1 & a2 in N2 by GROUP_11:6;
A6: a2 in center G by A1,A5,GROUP_2:49;
    consider b1,b2 be Element of G such that
A7: b = b1 * b2 & b1 in N1 & b2 in N2 by A4,GROUP_11:6;
A8: b2 in center G by A1,A7,GROUP_2:49;
    then a2 * b2 in center G & b2 * a2 in center G by A6,GROUP_2:59;
    then
A9: (a1 * b1) * (b2 * a2) = (b2 * a2) * (a1 * b1) by GROUP_5:89;
    reconsider c1 = a1,d1 = b1 as Element of N1 by A5,A7,STRUCT_0:def 5;
A10: a1 |^ p = c1 |^ p & b1 |^ p = d1 |^ p by GROUP_4:4;
    a1 * b1 = c1 * d1 by GROUP_2:52; then
A11: (a1 * b1) |^ p = (c1 * d1) |^ p by GROUP_8:4
                   .= c1 |^ p * (d1 |^ p) by A2,Def3
                   .= a1 |^ p * (b1 |^ p) by A10,GROUP_2:52;
    reconsider c2 = a2,d2 = b2 as Element of N2 by A5,A7,STRUCT_0:def 5;
A12: a2 |^ p = c2 |^ p & b2 |^ p = d2 |^ p by GROUP_4:4;
    b2 * a2 = d2 * c2 by GROUP_2:52; then
A13: (b2 * a2) |^ p = (d2 * c2) |^ p by GROUP_8:4
                   .= d2 |^ p * (c2 |^ p) by A2,Def3
                   .= b2 |^ p * (a2 |^ p) by A12,GROUP_2:52;
A14: a2 |^ p in center G by A6,GROUP_4:6;
A15: a1 * a2 = a2 * a1 by A6,GROUP_5:89;
A16: b1 * b2 = b2 * b1 by A8,GROUP_5:89;
    a * b = (a1 * a2) * (b1 * b2) by A5,A7,GROUP_2:52; then
A17: (a * b) |^ p = (a1 * a2 * (b1 * b2))|^ p by GROUP_8:4
             .= (a1 * (a2 * (b1 * b2)))|^ p by GROUP_1:def 4
             .= (a1 * ((b1 * b2) * a2))|^ p by A6,GROUP_5:89
             .= (a1 * (b1 * (b2 * a2)))|^ p by GROUP_1:def 4
             .= ((a1 * b1) * (b2 * a2))|^ p by GROUP_1:def 4
             .= (a1 * b1)|^ p * ((b2 * a2)|^ p) by A9,GROUP_1:73
             .= a1 |^ p * (b1 |^ p) * (a2 |^ p * (b2 |^ p)) by A11,A13,A14,
              GROUP_5:89
             .= a1 |^ p * (b1 |^ p * (a2 |^ p * (b2 |^ p))) by GROUP_1:def 4
             .= a1 |^ p * ((b1 |^ p * (a2 |^ p)) * (b2 |^ p)) by GROUP_1:def 4
             .= a1 |^ p * ((a2 |^ p * (b1 |^ p)) * (b2 |^ p)) by A14,GROUP_5:89
             .= (a1 |^ p * (a2 |^ p * (b1 |^ p))) * (b2 |^ p) by GROUP_1:def 4
             .= (a1 |^ p * (a2 |^ p) * (b1 |^ p)) * (b2 |^ p) by GROUP_1:def 4
             .= (a1 |^ p * (a2 |^ p)) * (b1 |^ p * (b2 |^ p)) by GROUP_1:def 4
             .= (a1 * a2)|^ p * (b1 |^ p * (b2 |^ p)) by A15,GROUP_1:73
             .= (a1 * a2)|^ p * ((b1 * b2) |^ p) by A16,GROUP_1:73;
A18:   a |^ p = (a1 * a2)|^ p by A5,GROUP_4:4;
       b |^ p = (b1 * b2)|^ p by A7,GROUP_4:4;
    hence thesis by A17,A18,GROUP_2:52;
  end;
  then N is p-commutative-group-like by Def3;
  hence thesis by A3;
end;

theorem Th33:
  for G,H being Group holds G,H are_isomorphic &
  G is p-commutative-group-like implies H is p-commutative-group-like
proof
  let G,H be Group;
  assume that
A1: G,H are_isomorphic and
A2: G is p-commutative-group-like;
    let h1,h2 be Element of H;
    consider h being Homomorphism of G,H such that
A3: h is bijective by A1,GROUP_6:def 15;
    consider a be Element of G such that
A4: h.a = h1 by A3,GROUP_6:68;
    consider b be Element of G such that
A5: h.b = h2 by A3,GROUP_6:68;
    h1 * h2 = h.(a * b) by A4,A5,GROUP_6:def 7;
    then (h1 * h2) |^ p = h.((a * b) |^ p) by GROUP_6:46
                       .= h.(a |^ p * (b |^ p)) by A2,Def3
                       .= h.(a |^ p) * h.(b |^ p) by GROUP_6:def 7
                       .= (h.a) |^ p * h.(b |^ p) by GROUP_6:46
                       .= h1 |^ p * (h2 |^ p) by A4,A5,GROUP_6:46;
    hence thesis;
end;

theorem
  for G,H being strict Group holds G,H are_isomorphic &
  G is p-commutative-group implies H is p-commutative-group
proof
  let G,H be strict Group;
  assume that
A1: G,H are_isomorphic and
A2: G is p-commutative-group;
A3: H is p-group by A1,A2,Th22;
    H is p-commutative-group-like by A1,A2,Th33;
    hence thesis by A3;
end;

registration
  let p;
  let G be p-commutative-group-like finite Group, H be finite Group;
  let g be Homomorphism of G,H;
  cluster Image g -> p-commutative-group-like;
coherence
proof
  let g1,g2 be Element of Image g;
  reconsider h1 = g1,h2 = g2 as Element of H by GROUP_2:51;
  g1 in Image g by STRUCT_0:def 5;
  then consider a be Element of G such that
A1: g1 = g.a by GROUP_6:54;
    g2 in Image g by STRUCT_0:def 5;
    then consider b be Element of G such that
A2: g2 = g.b by GROUP_6:54;
    g1 * g2 = h1 * h2 by GROUP_2:52
    .= g.(a * b) by A1,A2,GROUP_6:def 7; then
A3: (g1 * g2) |^ p = (g.(a * b)) |^ p by GROUP_8:4
    .= g.((a * b)|^ p) by GROUP_6:46
    .= g.(a |^ p * (b |^ p)) by Def3
    .= g.(a |^ p) * g.(b |^ p) by GROUP_6:def 7
    .= g.(a) |^ p * g.(b |^ p) by GROUP_6:46
    .= h1 |^ p * (h2 |^ p) by A1,A2,GROUP_6:46;
    h1 |^ p = g1 |^ p & h2 |^ p = g2 |^ p by GROUP_8:4;
    hence thesis by GROUP_2:52,A3;
  end;
end;

theorem
  for G being strict finite Group st G is p-group &
  expon (G,p) = 0 holds G is p-commutative-group
proof
  let G be strict finite Group;
  assume
A1:G is p-group & expon (G,p) = 0;
  then G = (1).G by Th24;
  hence thesis by A1;
end;

theorem
  for G being strict finite Group st G is p-group &
  expon (G,p) = 1 holds G is p-commutative-group
proof
  let G be strict finite Group;
  assume
A1: G is p-group & expon (G,p) = 1;
  then G is cyclic by Th25;
  hence thesis by A1;
end;