The abstract of the Mizar article:

Commutator and Center of a Group

by

Wojciech A. Trybulec

Received May 15, 1991

MML identifier: GROUP_5

[ Mizar article, MML identifier index ]

environ

 vocabulary INT_1, REALSET1, GROUP_2, GROUP_3, FINSEQ_1, GROUP_1, RELAT_1,
      LATTICES, BINOP_1, FUNCT_1, BOOLE, QC_LANG1, RCOMP_1, ARYTM_1, GROUP_4,
      RLSUB_1, VECTSP_1, SUBSET_1, FINSET_1, CARD_1, TARSKI, GROUP_5, CARD_3,
      FINSEQ_4;
 notation TARSKI, XBOOLE_0, SUBSET_1, NAT_1, STRUCT_0, XCMPLX_0, FUNCT_1,
      CARD_1, FINSEQ_1, FINSET_1, FINSEQ_4, INT_1, RLVECT_1, VECTSP_1, GROUP_1,
      GROUP_2, GROUP_3, GROUP_4, DOMAIN_1;
 constructors REAL_1, GROUP_4, DOMAIN_1, NAT_1, FINSEQ_4, MEMBERED, XBOOLE_0;
 clusters CARD_1, INT_1, GROUP_1, GROUP_2, GROUP_3, RELSET_1, STRUCT_0,
      MEMBERED, ZFMISC_1, XBOOLE_0;
 requirements NUMERALS, BOOLE, SUBSET;


begin :: Preliminaries.

scheme SubsetFD3{C,D,E() -> non empty set,
    F(set,set,set) -> Element of D(), P[set,set,set]}:
 {F(c,d,e) where c is Element of C(),d is Element of D(),
                 e is Element of E() : P[c,d,e]} is Subset of D();

 reserve x,y for set,
         k,n for Nat,
         i for Integer,
         G for Group,
         a,b,c,d,e for Element of G,
         A,B,C,D for Subset of G,
         H,H1,H2,H3,H4 for Subgroup of G,
         N1,N2 for normal Subgroup of G,
         F,F1,F2 for FinSequence of the carrier of G,
         I,I1,I2 for FinSequence of INT;

theorem :: GROUP_5:1
 x in (1).G iff x = 1.G;

theorem :: GROUP_5:2
   a in H & b in H implies a |^ b in H;

theorem :: GROUP_5:3
 for N being strict normal Subgroup of G
 holds a in N implies a |^ b in N;

theorem :: GROUP_5:4
 x in H1 * H2 iff ex a,b st x = a * b & a in H1 & b in H2;

theorem :: GROUP_5:5
 H1 * H2 = H2 * H1 implies
  (x in H1 "\/" H2 iff ex a,b st x = a * b & a in H1 & b in H2);

theorem :: GROUP_5:6
   G is commutative Group implies
  (x in H1 "\/" H2 iff ex a,b st x = a * b & a in H1 & b in H2);

theorem :: GROUP_5:7
 for N1,N2 being strict normal Subgroup of G
 holds x in N1 "\/" N2 iff ex a,b st x = a * b & a in N1 & b in N2;

theorem :: GROUP_5:8
   for N being normal Subgroup of G holds
 H * N = N * H;

definition let G,F,a;
 func F |^ a -> FinSequence of the carrier of G means
:: GROUP_5:def 1
   len it = len F &
        for k st k in dom F holds it.k = (F/.k) |^ a;
end;

canceled 3;

theorem :: GROUP_5:12
 (F1 |^ a) ^ (F2 |^ a) = (F1 ^ F2) |^ a;

theorem :: GROUP_5:13
 (<*> the carrier of G) |^ a = {};

theorem :: GROUP_5:14
 <* a *> |^ b = <* a |^ b *>;

theorem :: GROUP_5:15
 <* a,b *> |^ c = <* a |^ c,b |^ c *>;

theorem :: GROUP_5:16
   <* a,b,c *> |^ d = <* a |^ d,b |^ d,c |^ d *>;

theorem :: GROUP_5:17
 Product(F |^ a) = Product(F) |^ a;

theorem :: GROUP_5:18
 (F |^ a) |^ I = (F |^ I) |^ a;

begin :: Commutators.

definition let G,a,b;
 func [.a,b.] -> Element of G equals
:: GROUP_5:def 2
    a" * b" * a * b;
end;

theorem :: GROUP_5:19
 [.a,b.] = a" * b" * a * b & [.a,b.] = a" * (b" * a) * b &
 [.a,b.] = a" * (b" * a * b) & [.a,b.] = a" * (b" * (a * b)) &
 [.a,b.] = (a" * b") * (a * b);

theorem :: GROUP_5:20
 [.a,b.] = (b * a)" * (a * b);

theorem :: GROUP_5:21
 [.a,b.] = (b" |^ a) * b & [.a,b.] = a" * (a |^ b);

theorem :: GROUP_5:22
 [.1.G,a.] = 1.G & [.a,1.G.] = 1.G;

theorem :: GROUP_5:23
 [.a,a.] = 1.G;

theorem :: GROUP_5:24
   [.a,a".] = 1.G & [.a",a.] = 1.G;

theorem :: GROUP_5:25
 [.a,b.]" = [.b,a.];

theorem :: GROUP_5:26
 [.a,b.] |^ c = [.a |^ c,b |^ c.];

theorem :: GROUP_5:27
   [.a,b.] = (a" |^ 2) * ((a * b") |^ 2)* (b |^ 2);

theorem :: GROUP_5:28
 [.a * b,c.] = [.a,c.] |^ b * [.b,c.];

theorem :: GROUP_5:29
   [.a,b * c.] = [.a,c.] * ([.a,b.] |^ c);

theorem :: GROUP_5:30
 [.a",b.] = [.b,a.] |^ a";

theorem :: GROUP_5:31
 [.a,b".] = [.b,a.] |^ b";

theorem :: GROUP_5:32
   [.a",b".] = [.a,b.] |^ (a * b)" & [.a",b".] = [.a,b.] |^ (b * a)";

theorem :: GROUP_5:33
   [.a,b |^ a".] = [.b,a".];

theorem :: GROUP_5:34
   [.a |^ b",b.] = [.b",a.];

theorem :: GROUP_5:35
   [.a |^ n,b.] = a |^ (- n) * ((a |^ b) |^ n);

theorem :: GROUP_5:36
   [.a,b |^ n.] = (b |^ a) |^ (- n) * (b |^ n);

theorem :: GROUP_5:37
   [.a |^ i,b.] = a |^ (- i) * ((a |^ b) |^ i);

theorem :: GROUP_5:38
   [.a,b |^ i.] = (b |^ a) |^ (- i) * (b |^ i);

theorem :: GROUP_5:39
 [.a,b.] = 1.G iff a * b = b * a;

theorem :: GROUP_5:40
   G is commutative Group iff for a,b holds [.a,b.] = 1.G;

theorem :: GROUP_5:41
 a in H & b in H implies [.a,b.] in H;

definition let G,a,b,c;
 func [.a,b,c.] -> Element of G equals
:: GROUP_5:def 3
    [.[.a,b.],c.];
end;

canceled;

theorem :: GROUP_5:43
   [.a,b,1.G.] = 1.G & [.a,1.G,b.] = 1.G & [.1.G,a,b.] = 1.G;

theorem :: GROUP_5:44
   [.a,a,b.] = 1.G;

theorem :: GROUP_5:45
   [.a,b,a.] = [.a |^ b,a.];

theorem :: GROUP_5:46
   [.b,a,a.] = ([.b,a".] * [.b,a.]) |^ a;

theorem :: GROUP_5:47
   [.a,b,b |^ a.] = [.b,[.b,a.].];

theorem :: GROUP_5:48
   [.a * b,c.] = [.a,c.] * [.a,c,b.] * [.b,c.];

theorem :: GROUP_5:49
   [.a,b * c.] = [.a,c.] * [.a,b.] * [.a,b,c.];

::
::  P. Hall Identity.
::

theorem :: GROUP_5:50
   ([.a,b",c.] |^ b) * ([.b,c",a.] |^ c) * ([.c,a",b.] |^ a) = 1.G;

definition let G,A,B;
 func commutators(A,B) -> Subset of G equals
:: GROUP_5:def 4
    {[.a,b.] : a in A & b in B};
end;

canceled;

theorem :: GROUP_5:52
 x in commutators(A,B) iff ex a,b st x = [.a,b.] & a in A & b in B;

theorem :: GROUP_5:53
   commutators({} the carrier of G,A) = {} & commutators(A,{}
 the carrier of G) = {};

theorem :: GROUP_5:54
   commutators({a},{b}) = {[.a,b.]};

theorem :: GROUP_5:55
 A c= B & C c= D implies commutators(A,C) c= commutators(B,D);

theorem :: GROUP_5:56
 G is commutative Group iff
  for A,B st A <> {} & B <> {} holds commutators(A,B) = {1.G};

definition let G,H1,H2;
 func commutators(H1,H2) -> Subset of G equals
:: GROUP_5:def 5
    commutators(carr H1,carr H2);
end;

canceled;

theorem :: GROUP_5:58
 x in commutators(H1,H2) iff ex a,b st x = [.a,b.] & a in H1 & b in H2;

theorem :: GROUP_5:59
 1.G in commutators(H1,H2);

theorem :: GROUP_5:60
   commutators((1).G,H) = {1.G} & commutators(H,(1).G) = {1.G};

theorem :: GROUP_5:61
 for N being strict normal Subgroup of G
 holds commutators(H,N) c= carr N & commutators(N,H) c= carr N;

theorem :: GROUP_5:62
 H1 is Subgroup of H2 & H3 is Subgroup of H4 implies
  commutators(H1,H3) c= commutators(H2,H4);

theorem :: GROUP_5:63
 G is commutative Group iff for H1,H2 holds commutators(H1,H2) = {1.G};

definition let G;
 func commutators G -> Subset of G equals
:: GROUP_5:def 6
    commutators((Omega).G,(Omega).G);
end;

canceled;

theorem :: GROUP_5:65
 x in commutators G iff ex a,b st x = [.a,b.];

theorem :: GROUP_5:66
   G is commutative Group iff commutators G = {1.G};

definition let G,A,B;
 func [.A,B.] -> strict Subgroup of G equals
:: GROUP_5:def 7
    gr commutators(A,B);
end;

canceled;

theorem :: GROUP_5:68
 a in A & b in B implies [.a,b.] in [.A,B.];

theorem :: GROUP_5:69
 x in [.A,B.] iff
  ex F,I st len F = len I & rng F c= commutators(A,B) & x = Product(F |^ I);

theorem :: GROUP_5:70
   A c= C & B c= D implies [.A,B.] is Subgroup of [.C,D.];

definition let G,H1,H2;
 func [.H1,H2.] -> strict Subgroup of G equals
:: GROUP_5:def 8
    [.carr H1,carr H2.];
end;

canceled;

theorem :: GROUP_5:72
 [.H1,H2.] = gr commutators(H1,H2);

theorem :: GROUP_5:73
 x in [.H1,H2.] iff
  ex F,I st len F = len I & rng F c= commutators(H1,H2) & x = Product(F |^ I);

theorem :: GROUP_5:74
 a in H1 & b in H2 implies [.a,b.] in [.H1,H2.];

theorem :: GROUP_5:75
   H1 is Subgroup of H2 & H3 is Subgroup of H4 implies
  [.H1,H3.] is Subgroup of [.H2,H4.];

theorem :: GROUP_5:76
   for N being strict normal Subgroup of G holds
 [.N,H.] is Subgroup of N & [.H,N.] is Subgroup of N;

theorem :: GROUP_5:77
 for N1,N2 being strict normal Subgroup of G
 holds [.N1,N2.] is normal Subgroup of G;

theorem :: GROUP_5:78
 [.N1,N2.] = [.N2,N1.];

theorem :: GROUP_5:79
 for N1,N2,N3 being strict normal Subgroup of G
 holds [.N1 "\/" N2,N3.] = [.N1,N3.] "\/" [.N2,N3.];

theorem :: GROUP_5:80
   for N1,N2,N3 being strict normal Subgroup of G holds
 [.N1,N2 "\/" N3.] = [.N1,N2.] "\/" [.N1,N3.];

definition let G be Group;
 func G` -> strict normal Subgroup of G equals
:: GROUP_5:def 9
    [.(Omega).G,(Omega).G.];
end;

canceled;

theorem :: GROUP_5:82
 for G being Group holds
 G` = gr commutators G;

theorem :: GROUP_5:83
 for G being Group holds
 x in G` iff
  ex F being FinSequence of the carrier of G,I
    st len F = len I & rng F c= commutators G & x = Product(F |^ I);

theorem :: GROUP_5:84
 for G being strict Group, a,b be Element of G
    holds [.a,b.] in G`;

theorem :: GROUP_5:85
   for G being strict Group holds G is commutative Group iff G` = (1).G;

theorem :: GROUP_5:86
   for G being Group, H being strict Subgroup of G holds
 Left_Cosets H is finite & index H = 2 implies G` is Subgroup of H;

begin :: Center of a Group.

definition let G;
 func center G -> strict Subgroup of G means
:: GROUP_5:def 10
   the carrier of it = {a : for b holds a * b = b * a};
end;

canceled 2;

theorem :: GROUP_5:89
 a in center G iff for b holds a * b = b * a;

theorem :: GROUP_5:90
   center G is normal Subgroup of G;

theorem :: GROUP_5:91
   for H being Subgroup of G holds
 H is Subgroup of center G implies H is normal Subgroup of G;

theorem :: GROUP_5:92
   center G is commutative;

theorem :: GROUP_5:93
   a in center G iff con_class a = {a};

theorem :: GROUP_5:94
   for G being strict Group holds
 G is commutative Group iff center G = G;

begin :: Auxiliary theorems.

reserve E for non empty set,
        p, q for FinSequence of E;

theorem :: GROUP_5:95
   k in dom p implies (p ^ q)/.k = p/.k;

theorem :: GROUP_5:96
   k in dom q implies (p ^ q)/.(len p + k) = q/.k;