Journal of Formalized Mathematics
Volume 2, 1990
University of Bialystok
Copyright (c) 1990 Association of Mizar Users

Classes of Conjugation. Normal Subgroups

by
Wojciech A. Trybulec

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};