The abstract of the Mizar article:

Classes of Conjugation. Normal Subgroups

by

Wojciech A. Trybulec

Received August 10, 1990

MML identifier: GROUP_3

[ Mizar article, MML identifier index ]

environ

 vocabulary REALSET1, GROUP_2, INT_1, RELAT_1, GROUP_1, BINOP_1, VECTSP_1,
      FUNCT_1, FINSET_1, CARD_1, ABSVALUE, BOOLE, TARSKI, RLSUB_1, SETFAM_1,
      ARYTM_1, GROUP_3;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, XCMPLX_0, XREAL_0, NAT_1,
      BINOP_1, RELAT_1, FUNCT_1, FUNCT_2, STRUCT_0, RLVECT_1, FINSET_1,
      VECTSP_1, GROUP_2, DOMAIN_1, CARD_1, INT_1, GROUP_1;
 constructors WELLORD2, REAL_1, BINOP_1, GROUP_2, DOMAIN_1, NAT_1, MEMBERED,
      XBOOLE_0;
 clusters SUBSET_1, FUNCT_1, FINSET_1, GROUP_2, GROUP_1, STRUCT_0, RELSET_1,
      INT_1, MEMBERED, ZFMISC_1, XBOOLE_0;
 requirements NUMERALS, SUBSET, BOOLE, ARITHM;


begin

reserve x,y,y1,y2 for set;
reserve G for Group;
reserve a,b,c,d,g,h for Element of G;
reserve A,B,C,D for Subset of G;
reserve H,H1,H2,H3 for Subgroup of G;
reserve n for Nat;
reserve i for Integer;

theorem :: GROUP_3:1
 a * b * b" = a & a * b" * b = a & b" * b * a = a & b * b" * a = a &
 a * (b * b") = a & a * (b" * b) = a & b" * (b * a) = a & b * (b" * a) = a;

theorem :: GROUP_3:2
   G is commutative Group iff the mult of G is commutative;

theorem :: GROUP_3:3
   (1).G is commutative;

theorem :: GROUP_3:4
 A c= B & C c= D implies A * C c= B * D;

theorem :: GROUP_3:5
 A c= B implies a * A c= a * B & A * a c= B * a;

theorem :: GROUP_3:6
 H1 is Subgroup of H2 implies a * H1 c= a * H2 & H1 * a c= H2 * a;

theorem :: GROUP_3:7
 a * H = {a} * H;

theorem :: GROUP_3:8
 H * a = H * {a};

theorem :: GROUP_3:9
   a * A * H = a * (A * H);

theorem :: GROUP_3:10
 A * a * H = A * (a * H);

theorem :: GROUP_3:11
   a * H * A = a * (H * A);

theorem :: GROUP_3:12
   A * H * a = A * (H * a);

theorem :: GROUP_3:13
   H * a * A = H * (a * A);

theorem :: GROUP_3:14
   H * A * a = H * (A * a);

theorem :: GROUP_3:15
   H1 * a * H2 = H1 * (a * H2);

definition let G;
 func Subgroups G -> set means
:: GROUP_3:def 1
   x in it iff x is strict Subgroup of G;
end;

definition let G;
 cluster Subgroups G -> non empty;
end;

canceled 2;

theorem :: GROUP_3:18
   for G being strict Group holds G in Subgroups G;

theorem :: GROUP_3:19
 G is finite implies Subgroups G is finite;

definition let G,a,b;
 func a |^ b -> Element of G equals
:: GROUP_3:def 2
    b" * a * b;
end;

theorem :: GROUP_3:20
 a |^ b = b" * a * b & a |^ b = b" * (a * b);

theorem :: GROUP_3:21
 a |^ g = b |^ g implies a = b;

theorem :: GROUP_3:22
 (1.G) |^ a = 1.G;

theorem :: GROUP_3:23
 a |^ b = 1.G implies a = 1.G;

theorem :: GROUP_3:24
 a |^ 1.G = a;

theorem :: GROUP_3:25
 a |^ a = a;

theorem :: GROUP_3:26
 a |^ a" = a & a" |^ a = a";

theorem :: GROUP_3:27
 a |^ b = a iff a * b = b * a;

theorem :: GROUP_3:28
 (a * b) |^ g = a |^ g * (b |^ g);

theorem :: GROUP_3:29
 a |^ g |^ h = a |^ (g * h);

theorem :: GROUP_3:30
 a |^ b |^ b" = a & a |^ b" |^ b = a;

canceled;

theorem :: GROUP_3:32
 a" |^ b = (a |^ b)";

theorem :: GROUP_3:33
   (a |^ n) |^ b = (a |^ b) |^ n;

theorem :: GROUP_3:34
   (a |^ i) |^ b = (a |^ b) |^ i;

theorem :: GROUP_3:35
 G is commutative Group implies a |^ b = a;

theorem :: GROUP_3:36
 (for a,b holds a |^ b = a) implies G is commutative;

definition let G,A,B;
 func A |^ B -> Subset of G equals
:: GROUP_3:def 3
    {g |^ h : g in A & h in B};
end;

canceled;

theorem :: GROUP_3:38
 x in A |^ B iff ex g,h st x = g |^ h & g in A & h in B;

theorem :: GROUP_3:39
 A |^ B <> {} iff A <> {} & B <> {};

theorem :: GROUP_3:40
 A |^ B c= B" * A * B;

theorem :: GROUP_3:41
 (A * B) |^ C c= A |^ C * (B |^ C);

theorem :: GROUP_3:42
 A |^ B |^ C = A |^ (B * C);

theorem :: GROUP_3:43
   A" |^ B = (A |^ B)";

theorem :: GROUP_3:44
 {a} |^ {b} = {a |^ b};

theorem :: GROUP_3:45
   {a} |^ {b,c} = {a |^ b,a |^ c};

theorem :: GROUP_3:46
   {a,b} |^ {c} = {a |^ c,b |^ c};

theorem :: GROUP_3:47
   {a,b} |^ {c,d} = {a |^ c,a |^ d,b |^ c,b |^ d};

definition let G,A,g;
 func A |^ g -> Subset of G equals
:: GROUP_3:def 4
    A |^ {g};
 func g |^ A -> Subset of G equals
:: GROUP_3:def 5
    {g} |^ A;
end;

canceled 2;

theorem :: GROUP_3:50
 x in A |^ g iff ex h st x = h |^ g & h in A;

theorem :: GROUP_3:51
 x in g |^ A iff ex h st x = g |^ h & h in A;

theorem :: GROUP_3:52
   g |^ A c= A" * g * A;

theorem :: GROUP_3:53
 A |^ B |^ g = A |^ (B * g);

theorem :: GROUP_3:54
 A |^ g |^ B = A |^ (g * B);

theorem :: GROUP_3:55
   g |^ A |^ B = g |^ (A * B);

theorem :: GROUP_3:56
 A |^ a |^ b = A |^ (a * b);

theorem :: GROUP_3:57
   a |^ A |^ b = a |^ (A * b);

theorem :: GROUP_3:58
   a |^ b |^ A = a |^ (b * A);

theorem :: GROUP_3:59
 A |^ g = g" * A * g;

theorem :: GROUP_3:60
   (A * B) |^ a c= (A |^ a) * (B |^ a);

theorem :: GROUP_3:61
 A |^ 1.G = A;

theorem :: GROUP_3:62
   A <> {} implies (1.G) |^ A = {1.G};

theorem :: GROUP_3:63
 A |^ a |^ a" = A & A |^ a" |^ a = A;

canceled;

theorem :: GROUP_3:65
 G is commutative Group iff for A,B st B <> {} holds A |^ B = A;

theorem :: GROUP_3:66
   G is commutative Group iff for A,g holds A |^ g = A;

theorem :: GROUP_3:67
   G is commutative Group iff for A,g st A <> {} holds g |^ A = {g};

definition let G,H,a;
 func H |^ a -> strict Subgroup of G means
:: GROUP_3:def 6
   the carrier of it = carr(H) |^ a;
end;

canceled 2;

theorem :: GROUP_3:70
 x in H |^ a iff ex g st x = g |^ a & g in H;

theorem :: GROUP_3:71
 the carrier of H |^ a = a" * H * a;

theorem :: GROUP_3:72
 H |^ a |^ b = H |^ (a * b);

theorem :: GROUP_3:73
 for H being strict Subgroup of G holds H |^ 1.G = H;

theorem :: GROUP_3:74
 for H being strict Subgroup of G holds
 H |^ a |^ a" = H & H |^ a" |^ a = H;

canceled;

theorem :: GROUP_3:76
 (H1 /\ H2) |^ a = (H1 |^ a) /\ (H2 |^ a);

theorem :: GROUP_3:77
 Ord H = Ord(H |^ a);

theorem :: GROUP_3:78
 H is finite iff H |^ a is finite;

theorem :: GROUP_3:79
 H is finite implies ord H = ord(H |^ a);

theorem :: GROUP_3:80
 (1).G |^ a = (1).G;

theorem :: GROUP_3:81
   for H being strict Subgroup of G holds H |^ a = (1).G implies H = (1).G;

theorem :: GROUP_3:82
 for G being Group, a being Element of G
  holds (Omega).G |^ a = (Omega).G;

theorem :: GROUP_3:83
   for H being strict Subgroup of G holds
 H |^ a = G implies H = G;

theorem :: GROUP_3:84
 Index H = Index(H |^ a);

theorem :: GROUP_3:85
   Left_Cosets H is finite implies index H = index(H |^ a);

theorem :: GROUP_3:86
 G is commutative Group implies
  for H being strict Subgroup of G for a holds H |^ a = H;

definition let G,a,b;
 pred a,b are_conjugated means
:: GROUP_3:def 7
   ex g st a = b |^ g;
 antonym a,b are_not_conjugated;
end;

canceled;

theorem :: GROUP_3:88
 a,b are_conjugated iff ex g st b = a |^ g;

theorem :: GROUP_3:89
 a,a are_conjugated;

theorem :: GROUP_3:90
 a,b are_conjugated implies b,a are_conjugated;

definition let G,a,b;
 redefine pred a,b are_conjugated;
 reflexivity;
 symmetry;
end;

theorem :: GROUP_3:91
 a,b are_conjugated & b,c are_conjugated implies a,c are_conjugated;

theorem :: GROUP_3:92
 a,1.G are_conjugated or 1.G,a are_conjugated implies a = 1.G;

theorem :: GROUP_3:93
 a |^ carr (Omega).G = {b : a,b are_conjugated};

definition let G,a;
 func con_class a -> Subset of G equals
:: GROUP_3:def 8
    a |^ carr (Omega).G;
end;

canceled;

theorem :: GROUP_3:95
 x in con_class a iff ex b st b = x & a,b are_conjugated;

theorem :: GROUP_3:96
 a in con_class b iff a,b are_conjugated;

theorem :: GROUP_3:97
 a |^ g in con_class a;

theorem :: GROUP_3:98
  a in con_class a;

theorem :: GROUP_3:99
   a in con_class b implies b in con_class a;

theorem :: GROUP_3:100
   con_class a = con_class b iff con_class a meets con_class b;

theorem :: GROUP_3:101
   con_class a = {1.G} iff a = 1.G;

theorem :: GROUP_3:102
   con_class a * A = A * con_class a;

definition let G,A,B;
 pred A,B are_conjugated means
:: GROUP_3:def 9
   ex g st A = B |^ g;
 antonym A,B are_not_conjugated;
end;

canceled;

theorem :: GROUP_3:104
 A,B are_conjugated iff ex g st B = A |^ g;

theorem :: GROUP_3:105
 A,A are_conjugated;

theorem :: GROUP_3:106
 A,B are_conjugated implies B,A are_conjugated;

definition let G,A,B;
 redefine pred A,B are_conjugated;
 reflexivity;
 symmetry;
end;

theorem :: GROUP_3:107
 A,B are_conjugated & B,C are_conjugated implies A,C are_conjugated;

theorem :: GROUP_3:108
 {a},{b} are_conjugated iff a,b are_conjugated;

theorem :: GROUP_3:109
 A,carr H1 are_conjugated implies
  ex H2 being strict Subgroup of G st the carrier of H2 = A;

definition let G,A;
 func con_class A -> Subset-Family of G equals
:: GROUP_3:def 10
    {B : A,B are_conjugated};
end;

canceled;

theorem :: GROUP_3:111
 x in con_class A iff ex B st x = B & A,B are_conjugated;

canceled;

theorem :: GROUP_3:113
 A in con_class B iff A,B are_conjugated;

theorem :: GROUP_3:114
   A |^ g in con_class A;

theorem :: GROUP_3:115
  A in con_class A;

theorem :: GROUP_3:116
   A in con_class B implies B in con_class A;

theorem :: GROUP_3:117
   con_class A = con_class B iff con_class A meets con_class B;

theorem :: GROUP_3:118
 con_class{a} = {{b} : b in con_class a};

theorem :: GROUP_3:119
   G is finite implies con_class A is finite;

definition let G,H1,H2;
 pred H1,H2 are_conjugated means
:: GROUP_3:def 11
   ex g st the HGrStr of H1 = H2 |^ g;
 antonym H1,H2 are_not_conjugated;
end;

canceled;

theorem :: GROUP_3:121
 for H1,H2 being strict Subgroup of G holds
 H1,H2 are_conjugated iff ex g st H2 = H1 |^ g;

theorem :: GROUP_3:122
 for H1 being strict Subgroup of G holds H1,H1 are_conjugated;

theorem :: GROUP_3:123
 for H1,H2 being strict Subgroup of G holds
 H1,H2 are_conjugated implies H2,H1 are_conjugated;

definition let G; let H1,H2 be strict Subgroup of G;
 redefine pred H1,H2 are_conjugated;
 reflexivity;
 symmetry;
end;

theorem :: GROUP_3:124
 for H1,H2 being strict Subgroup of G holds
 H1,H2 are_conjugated & H2,H3 are_conjugated implies H1,H3 are_conjugated;

reserve L for Subset of Subgroups G;

definition let G,H;
 func con_class H -> Subset of Subgroups G means
:: GROUP_3:def 12
   x in it iff
   ex H1 being strict Subgroup of G st x = H1 & H,H1 are_conjugated;
end;

canceled 2;

theorem :: GROUP_3:127
 x in con_class H implies x is strict Subgroup of G;

theorem :: GROUP_3:128
 for H1,H2 being strict Subgroup of G holds
 H1 in con_class H2 iff H1,H2 are_conjugated;

theorem :: GROUP_3:129
 for H being strict Subgroup of G holds H |^ g in con_class H;

theorem :: GROUP_3:130
 for H being strict Subgroup of G holds H in con_class H;

theorem :: GROUP_3:131
   for H1,H2 being strict Subgroup of G holds
 H1 in con_class H2 implies H2 in con_class H1;

theorem :: GROUP_3:132
   for H1,H2 being strict Subgroup of G holds
 con_class H1 = con_class H2 iff con_class H1 meets con_class H2;

theorem :: GROUP_3:133
   G is finite implies con_class H is finite;

theorem :: GROUP_3:134
 for H1 being strict Subgroup of G holds
 H1,H2 are_conjugated iff carr H1,carr H2 are_conjugated;

definition let G;
 let IT be Subgroup of G;
 attr IT is normal means
:: GROUP_3:def 13
   for a holds IT |^ a = the HGrStr of IT;
end;

definition let G;
 cluster strict normal Subgroup of G;
end;

reserve N2 for normal Subgroup of G;

canceled 2;

theorem :: GROUP_3:137
 (1).G is normal & (Omega).G is normal;

theorem :: GROUP_3:138
   for N1,N2 being strict normal Subgroup of G
 holds N1 /\ N2 is normal;

theorem :: GROUP_3:139
   for H being strict Subgroup of G holds
 G is commutative Group implies H is normal;

theorem :: GROUP_3:140
 H is normal Subgroup of G iff for a holds a * H = H * a;

theorem :: GROUP_3:141
 for H being Subgroup of G holds
 H is normal Subgroup of G iff for a holds a * H c= H * a;

theorem :: GROUP_3:142
 for H being Subgroup of G holds
 H is normal Subgroup of G iff for a holds H * a c= a * H;

theorem :: GROUP_3:143
   for H being Subgroup of G holds
 H is normal Subgroup of G iff for A holds A * H = H * A;

theorem :: GROUP_3:144
   for H being strict Subgroup of G holds
 H is normal Subgroup of G iff for a holds H is Subgroup of H |^ a;

theorem :: GROUP_3:145
   for H being strict Subgroup of G holds
 H is normal Subgroup of G iff for a holds H |^ a is Subgroup of H;

theorem :: GROUP_3:146
   for H being strict Subgroup of G holds
 H is normal Subgroup of G iff con_class H = {H};

theorem :: GROUP_3:147
   for H being strict Subgroup of G holds
 H is normal Subgroup of G iff for a st a in H holds con_class a c= carr H;

theorem :: GROUP_3:148
 for N1,N2 being strict normal Subgroup of G
 holds carr N1 * carr N2 = carr N2 * carr N1;

theorem :: GROUP_3:149
   for N1,N2 being strict normal Subgroup of G
 ex N being strict normal Subgroup of G
 st the carrier of N = carr N1 * carr N2;

theorem :: GROUP_3:150
   for N being normal Subgroup of G holds
 Left_Cosets N = Right_Cosets N;

theorem :: GROUP_3:151
   for H being Subgroup of G holds
 Left_Cosets H is finite & index H = 2 implies H is normal Subgroup of G;

definition let G; let A;
 func Normalizator A -> strict Subgroup of G means
:: GROUP_3:def 14
   the carrier of it = {h : A |^ h = A};
end;

canceled 2;

theorem :: GROUP_3:154
 x in Normalizator A iff ex h st x = h & A |^ h = A;

theorem :: GROUP_3:155
 Card con_class A = Index Normalizator A;

theorem :: GROUP_3:156
   con_class A is finite or Left_Cosets Normalizator A is finite implies
  ex C being finite set st C = con_class A & card C = index Normalizator A;

theorem :: GROUP_3:157
 Card con_class a = Index Normalizator{a};

theorem :: GROUP_3:158
   con_class a is finite or Left_Cosets Normalizator{a} is finite implies
  ex C being finite set st C = con_class a & card C = index Normalizator{a};

definition let G; let H;
 func Normalizator H -> strict Subgroup of G equals
:: GROUP_3:def 15
    Normalizator carr H;
end;

canceled;

theorem :: GROUP_3:160
 for H being strict Subgroup of G
 holds x in Normalizator H iff ex h st x = h & H |^ h = H;

theorem :: GROUP_3:161
 for H being strict Subgroup of G holds
 Card con_class H = Index Normalizator H;

theorem :: GROUP_3:162
   for H being strict Subgroup of G holds
 con_class H is finite or Left_Cosets Normalizator H is finite implies
 ex C being finite set st C = con_class H & card C = index Normalizator H;

theorem :: GROUP_3:163
 for G being strict Group, H being strict Subgroup of G
 holds H is normal Subgroup of G iff Normalizator H = G;

theorem :: GROUP_3:164
   for G being strict Group holds Normalizator (1).G = G;

theorem :: GROUP_3:165
   for G being strict Group holds Normalizator (Omega).G = G;

::
::  Auxiliary theorems.
::

theorem :: GROUP_3:166
   for X being finite set st card X = 2 ex x,y st x <> y & X = {x,y};