:: Classes of Conjugation. Normal Subgroups
:: by Wojciech A. Trybulec
::
:: Received August 10, 1990
:: Copyright (c) 1990-2019 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies GROUP_1, SUBSET_1, GROUP_2, NAT_1, INT_1, RELAT_1, BINOP_1,
ALGSTR_0, FUNCT_1, STRUCT_0, TARSKI, ZFMISC_1, XBOOLE_0, FINSET_1,
CARD_1, NEWTON, ARYTM_3, XXREAL_0, COMPLEX1, RLSUB_1, CQC_SIM1, SETFAM_1,
PRE_TOPC, GROUP_3;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NAT_1, BINOP_1,
RELAT_1, FUNCT_1, FUNCT_2, FINSET_1, CARD_1, STRUCT_0, ALGSTR_0, GROUP_1,
GROUP_2, DOMAIN_1, XXREAL_0, INT_1, INT_2;
constructors SETFAM_1, WELLORD2, BINOP_1, XXREAL_0, NAT_1, INT_2, REALSET1,
REAL_1, GROUP_2, RELSET_1, BINOP_2, NUMBERS;
registrations XBOOLE_0, SUBSET_1, FUNCT_1, RELSET_1, FINSET_1, XREAL_0, INT_1,
STRUCT_0, GROUP_1, GROUP_2, ORDINAL1;
requirements NUMERALS, SUBSET, BOOLE;
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 multF 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 * H * A = a * (H * A);
theorem :: GROUP_3:11
A * H * a = A * (H * a);
theorem :: GROUP_3:12
H * a * A = H * (a * A);
theorem :: GROUP_3:13
H1 * a * H2 = H1 * (a * H2);
definition
let G;
func Subgroups G -> set means
:: GROUP_3:def 1
for x being object holds x in it iff x is strict Subgroup of G;
end;
registration
let G;
cluster Subgroups G -> non empty;
end;
theorem :: GROUP_3:14
for G being strict Group holds G in Subgroups G;
theorem :: GROUP_3:15
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:16
a |^ g = b |^ g implies a = b;
theorem :: GROUP_3:17
(1_G) |^ a = 1_G;
theorem :: GROUP_3:18
a |^ b = 1_G implies a = 1_G;
theorem :: GROUP_3:19
a |^ 1_G = a;
theorem :: GROUP_3:20
a |^ a = a;
theorem :: GROUP_3:21
a |^ a" = a & a" |^ a = a";
theorem :: GROUP_3:22
a |^ b = a iff a * b = b * a;
theorem :: GROUP_3:23
(a * b) |^ g = a |^ g * (b |^ g);
theorem :: GROUP_3:24
a |^ g |^ h = a |^ (g * h);
theorem :: GROUP_3:25
a |^ b |^ b" = a & a |^ b" |^ b = a;
theorem :: GROUP_3:26
a" |^ b = (a |^ b)";
theorem :: GROUP_3:27
(a |^ n) |^ b = (a |^ b) |^ n;
theorem :: GROUP_3:28
(a |^ i) |^ b = (a |^ b) |^ i;
theorem :: GROUP_3:29
G is commutative Group implies a |^ b = a;
theorem :: GROUP_3:30
(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;
theorem :: GROUP_3:31
x in A |^ B iff ex g,h st x = g |^ h & g in A & h in B;
theorem :: GROUP_3:32
A |^ B <> {} iff A <> {} & B <> {};
theorem :: GROUP_3:33
A |^ B c= B" * A * B;
theorem :: GROUP_3:34
(A * B) |^ C c= A |^ C * (B |^ C);
theorem :: GROUP_3:35
A |^ B |^ C = A |^ (B * C);
theorem :: GROUP_3:36
A" |^ B = (A |^ B)";
theorem :: GROUP_3:37
{a} |^ {b} = {a |^ b};
theorem :: GROUP_3:38
{a} |^ {b,c} = {a |^ b,a |^ c};
theorem :: GROUP_3:39
{a,b} |^ {c} = {a |^ c,b |^ c};
theorem :: GROUP_3:40
{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;
theorem :: GROUP_3:41
x in A |^ g iff ex h st x = h |^ g & h in A;
theorem :: GROUP_3:42
x in g |^ A iff ex h st x = g |^ h & h in A;
theorem :: GROUP_3:43
g |^ A c= A" * g * A;
theorem :: GROUP_3:44
A |^ B |^ g = A |^ (B * g);
theorem :: GROUP_3:45
A |^ g |^ B = A |^ (g * B);
theorem :: GROUP_3:46
g |^ A |^ B = g |^ (A * B);
theorem :: GROUP_3:47
A |^ a |^ b = A |^ (a * b);
theorem :: GROUP_3:48
a |^ A |^ b = a |^ (A * b);
theorem :: GROUP_3:49
a |^ b |^ A = a |^ (b * A);
theorem :: GROUP_3:50
A |^ g = g" * A * g;
theorem :: GROUP_3:51
(A * B) |^ a c= (A |^ a) * (B |^ a);
theorem :: GROUP_3:52
A |^ 1_G = A;
theorem :: GROUP_3:53
A <> {} implies (1_G) |^ A = {1_G};
theorem :: GROUP_3:54
A |^ a |^ a" = A & A |^ a" |^ a = A;
theorem :: GROUP_3:55
G is commutative Group iff for A,B st B <> {} holds A |^ B = A;
theorem :: GROUP_3:56
G is commutative Group iff for A,g holds A |^ g = A;
theorem :: GROUP_3:57
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;
theorem :: GROUP_3:58
x in H |^ a iff ex g st x = g |^ a & g in H;
theorem :: GROUP_3:59
the carrier of H |^ a = a" * H * a;
theorem :: GROUP_3:60
H |^ a |^ b = H |^ (a * b);
theorem :: GROUP_3:61
for H being strict Subgroup of G holds H |^ 1_G = H;
theorem :: GROUP_3:62
for H being strict Subgroup of G holds H |^ a |^ a" = H & H |^ a " |^ a = H;
theorem :: GROUP_3:63
(H1 /\ H2) |^ a = (H1 |^ a) /\ (H2 |^ a);
theorem :: GROUP_3:64
card H = card(H |^ a);
theorem :: GROUP_3:65
H is finite iff H |^ a is finite;
registration
let G,a;
let H be finite Subgroup of G;
cluster H |^ a -> finite;
end;
theorem :: GROUP_3:66
for H being finite Subgroup of G holds card H = card(H |^ a);
theorem :: GROUP_3:67
(1).G |^ a = (1).G;
theorem :: GROUP_3:68
for H being strict Subgroup of G holds H |^ a = (1).G implies H = (1). G;
theorem :: GROUP_3:69
for G being Group, a being Element of G holds (Omega).G |^ a = (Omega).G;
theorem :: GROUP_3:70
for H being strict Subgroup of G holds H |^ a = G implies H = G;
theorem :: GROUP_3:71
Index H = Index(H |^ a);
theorem :: GROUP_3:72
Left_Cosets H is finite implies index H = index(H |^ a);
theorem :: GROUP_3:73
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;
end;
notation
let G,a,b;
antonym a,b are_not_conjugated for a,b are_conjugated;
end;
theorem :: GROUP_3:74
a,b are_conjugated iff ex g st b = a |^ g;
theorem :: GROUP_3:75
a,a are_conjugated;
theorem :: GROUP_3:76
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:77
a,b are_conjugated & b,c are_conjugated implies a,c are_conjugated;
theorem :: GROUP_3:78
a,1_G are_conjugated or 1_G,a are_conjugated implies a = 1_G;
theorem :: GROUP_3:79
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;
theorem :: GROUP_3:80
x in con_class a iff ex b st b = x & a,b are_conjugated;
theorem :: GROUP_3:81
a in con_class b iff a,b are_conjugated;
theorem :: GROUP_3:82
a |^ g in con_class a;
theorem :: GROUP_3:83
a in con_class a;
theorem :: GROUP_3:84
a in con_class b implies b in con_class a;
theorem :: GROUP_3:85
con_class a = con_class b iff con_class a meets con_class b;
theorem :: GROUP_3:86
con_class a = {1_G} iff a = 1_G;
theorem :: GROUP_3:87
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;
end;
notation
let G,A,B;
antonym A,B are_not_conjugated for A,B are_conjugated;
end;
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},{b} are_conjugated iff a,b are_conjugated;
theorem :: GROUP_3:93
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;
theorem :: GROUP_3:94
x in con_class A iff ex B st x = B & A,B are_conjugated;
theorem :: GROUP_3:95
A in con_class B iff A,B are_conjugated;
theorem :: GROUP_3:96
A |^ g in con_class A;
theorem :: GROUP_3:97
A in con_class A;
theorem :: GROUP_3:98
A in con_class B implies B in con_class A;
theorem :: GROUP_3:99
con_class A = con_class B iff con_class A meets con_class B;
theorem :: GROUP_3:100
con_class{a} = {{b} : b in con_class a};
theorem :: GROUP_3:101
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 multMagma of H1 = H2 |^ g;
end;
notation
let G,H1,H2;
antonym H1,H2 are_not_conjugated for H1,H2 are_conjugated;
end;
theorem :: GROUP_3:102
for H1,H2 being strict Subgroup of G holds H1,H2 are_conjugated
iff ex g st H2 = H1 |^ g;
theorem :: GROUP_3:103
for H1 being strict Subgroup of G holds H1,H1 are_conjugated;
theorem :: GROUP_3:104
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:105
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
for x being object holds x in it iff
ex H1 being strict Subgroup of G st x = H1 & H,H1 are_conjugated;
end;
theorem :: GROUP_3:106
x in con_class H implies x is strict Subgroup of G;
theorem :: GROUP_3:107
for H1,H2 being strict Subgroup of G holds H1 in con_class H2
iff H1,H2 are_conjugated;
theorem :: GROUP_3:108
for H being strict Subgroup of G holds H |^ g in con_class H;
theorem :: GROUP_3:109
for H being strict Subgroup of G holds H in con_class H;
theorem :: GROUP_3:110
for H1,H2 being strict Subgroup of G holds H1 in con_class H2 implies
H2 in con_class H1;
theorem :: GROUP_3:111
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:112
G is finite implies con_class H is finite;
theorem :: GROUP_3:113
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 multMagma of IT;
end;
registration
let G;
cluster strict normal for Subgroup of G;
end;
reserve N2 for normal Subgroup of G;
theorem :: GROUP_3:114
(1).G is normal & (Omega).G is normal;
theorem :: GROUP_3:115
for N1,N2 being strict normal Subgroup of G holds N1 /\ N2 is normal;
theorem :: GROUP_3:116
for H being strict Subgroup of G holds G is commutative Group implies
H is normal;
theorem :: GROUP_3:117
H is normal Subgroup of G iff for a holds a * H = H * a;
theorem :: GROUP_3:118
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:119
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:120
for H being Subgroup of G holds H is normal Subgroup of G iff for A
holds A * H = H * A;
theorem :: GROUP_3:121
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:122
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:123
for H being strict Subgroup of G holds H is normal Subgroup of G iff
con_class H = {H};
theorem :: GROUP_3:124
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:125
for N1,N2 being strict normal Subgroup of G holds carr N1 *
carr N2 = carr N2 * carr N1;
theorem :: GROUP_3:126
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:127
for N being normal Subgroup of G holds Left_Cosets N = Right_Cosets N;
theorem :: GROUP_3:128
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 Normalizer A -> strict Subgroup of G means
:: GROUP_3:def 14
the carrier of it = {h : A |^ h = A};
end;
theorem :: GROUP_3:129
x in Normalizer A iff ex h st x = h & A |^ h = A;
theorem :: GROUP_3:130
card con_class A = Index Normalizer A;
theorem :: GROUP_3:131
con_class A is finite or Left_Cosets Normalizer A is finite implies
ex C being finite set st C = con_class A & card C = index Normalizer A;
theorem :: GROUP_3:132
card con_class a = Index Normalizer{a};
theorem :: GROUP_3:133
con_class a is finite or Left_Cosets Normalizer{a} is finite implies
ex C being finite set st C = con_class a & card C = index Normalizer{a};
definition
let G;
let H;
func Normalizer H -> strict Subgroup of G equals
:: GROUP_3:def 15
Normalizer carr H;
end;
theorem :: GROUP_3:134
for H being strict Subgroup of G holds x in Normalizer H iff
ex h st x = h & H |^ h = H;
theorem :: GROUP_3:135
for H being strict Subgroup of G holds card con_class H = Index
Normalizer H;
theorem :: GROUP_3:136
for H being strict Subgroup of G holds con_class H is finite or
Left_Cosets Normalizer H is finite implies ex C being finite set st C =
con_class H & card C = index Normalizer H;
theorem :: GROUP_3:137
for G being strict Group, H being strict Subgroup of G holds H
is normal Subgroup of G iff Normalizer H = G;
theorem :: GROUP_3:138
for G being strict Group holds Normalizer (1).G = G;
theorem :: GROUP_3:139
for G being strict Group holds Normalizer (Omega).G = G;