:: Classes of Conjugation. Normal Subgroups
:: by Wojciech A. Trybulec
::
:: Received August 10, 1990
:: Copyright (c) 1990-2011 Association of Mizar Users


begin

theorem Th1: :: GROUP_3:1
for G being Group
for a, b being Element of G holds
( (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 )
proof end;

Lm1: for A being commutative Group
for a, b being Element of A holds a * b = b * a
;

theorem :: GROUP_3:2
for G being Group holds
( G is commutative Group iff the multF of G is commutative )
proof end;

theorem :: GROUP_3:3
for G being Group holds (1). G is commutative
proof end;

theorem Th4: :: GROUP_3:4
for G being Group
for A, B, C, D being Subset of G st A c= B & C c= D holds
A * C c= B * D
proof end;

theorem :: GROUP_3:5
for G being Group
for a being Element of G
for A, B being Subset of G st A c= B holds
( a * A c= a * B & A * a c= B * a ) by Th4;

theorem Th6: :: GROUP_3:6
for G being Group
for a being Element of G
for H1, H2 being Subgroup of G st H1 is Subgroup of H2 holds
( a * H1 c= a * H2 & H1 * a c= H2 * a )
proof end;

theorem :: GROUP_3:7
for G being Group
for a being Element of G
for H being Subgroup of G holds a * H = {a} * H ;

theorem :: GROUP_3:8
for G being Group
for a being Element of G
for H being Subgroup of G holds H * a = H * {a} ;

theorem :: GROUP_3:9
canceled;

theorem Th10: :: GROUP_3:10
for G being Group
for a being Element of G
for A being Subset of G
for H being Subgroup of G holds (A * a) * H = A * (a * H)
proof end;

theorem :: GROUP_3:11
for G being Group
for a being Element of G
for A being Subset of G
for H being Subgroup of G holds (a * H) * A = a * (H * A)
proof end;

theorem :: GROUP_3:12
for G being Group
for a being Element of G
for A being Subset of G
for H being Subgroup of G holds (A * H) * a = A * (H * a)
proof end;

theorem :: GROUP_3:13
for G being Group
for a being Element of G
for A being Subset of G
for H being Subgroup of G holds (H * a) * A = H * (a * A)
proof end;

theorem :: GROUP_3:14
canceled;

theorem :: GROUP_3:15
for G being Group
for a being Element of G
for H1, H2 being Subgroup of G holds (H1 * a) * H2 = H1 * (a * H2) by Th10;

definition
let G be Group;
func Subgroups G -> set means :Def1: :: GROUP_3:def 1
 for x being set holds
( x in it iff x is strict Subgroup of G );
existence
ex b1 being set st
for x being set holds
( x in b1 iff x is strict Subgroup of G )
proof end;
uniqueness
for b1, b2 being set st ( for x being set holds
( x in b1 iff x is strict Subgroup of G ) ) & ( for x being set holds
( x in b2 iff x is strict Subgroup of G ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines Subgroups GROUP_3:def 1 :
for G being Group
for b2 being set holds
( b2 = Subgroups G iff for x being set holds
( x in b2 iff x is strict Subgroup of G ) );

registration
let G be Group;
cluster Subgroups G -> non empty ;
coherence
not Subgroups G is empty
proof end;
end;

theorem :: GROUP_3:16
canceled;

theorem :: GROUP_3:17
canceled;

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

theorem Th19: :: GROUP_3:19
for G being Group st G is finite holds
Subgroups G is finite
proof end;

definition
let G be Group;
let a, b be Element of G;
func a |^ b -> Element of G equals :: GROUP_3:def 2
((b ") * a) * b;
correctness
coherence
((b ") * a) * b is Element of G;
;
end;

:: deftheorem defines |^ GROUP_3:def 2 :
for G being Group
for a, b being Element of G holds a |^ b = ((b ") * a) * b;

theorem :: GROUP_3:20
canceled;

theorem Th21: :: GROUP_3:21
for G being Group
for a, g, b being Element of G st a |^ g = b |^ g holds
a = b
proof end;

theorem Th22: :: GROUP_3:22
for G being Group
for a being Element of G holds (1_ G) |^ a = 1_ G
proof end;

theorem Th23: :: GROUP_3:23
for G being Group
for a, b being Element of G st a |^ b = 1_ G holds
a = 1_ G
proof end;

theorem Th24: :: GROUP_3:24
for G being Group
for a being Element of G holds a |^ (1_ G) = a
proof end;

theorem Th25: :: GROUP_3:25
for G being Group
for a being Element of G holds a |^ a = a
proof end;

theorem :: GROUP_3:26
for G being Group
for a being Element of G holds
( a |^ (a ") = a & (a ") |^ a = a " ) by Th1;

theorem Th27: :: GROUP_3:27
for G being Group
for a, b being Element of G holds
( a |^ b = a iff a * b = b * a )
proof end;

theorem Th28: :: GROUP_3:28
for G being Group
for a, b, g being Element of G holds (a * b) |^ g = (a |^ g) * (b |^ g)
proof end;

theorem Th29: :: GROUP_3:29
for G being Group
for a, g, h being Element of G holds (a |^ g) |^ h = a |^ (g * h)
proof end;

theorem Th30: :: GROUP_3:30
for G being Group
for a, b being Element of G holds
( (a |^ b) |^ (b ") = a & (a |^ (b ")) |^ b = a )
proof end;

theorem :: GROUP_3:31
canceled;

theorem Th32: :: GROUP_3:32
for G being Group
for a, b being Element of G holds (a ") |^ b = (a |^ b) "
proof end;

Lm2: now
let G be Group; :: thesis: for a, b being Element of G holds (a |^ 0) |^ b = (a |^ b) |^ 0
let a, b be Element of G; :: thesis: (a |^ 0) |^ b = (a |^ b) |^ 0
thus (a |^ 0) |^ b = (1_ G) |^ b by GROUP_1:43
.= 1_ G by Th22
.= (a |^ b) |^ 0 by GROUP_1:43 ; :: thesis: verum
end;

Lm3: now
let n be Nat; :: thesis: ( ( for G being Group
for a, b being Element of G holds (a |^ n) |^ b = (a |^ b) |^ n ) implies for G being Group
for a, b being Element of G holds (a |^ (n + 1)) |^ b = (a |^ b) |^ (n + 1) )
assume A1: for G being Group
for a, b being Element of G holds (a |^ n) |^ b = (a |^ b) |^ n ; :: thesis: for G being Group
for a, b being Element of G holds (a |^ (n + 1)) |^ b = (a |^ b) |^ (n + 1)
let G be Group; :: thesis: for a, b being Element of G holds (a |^ (n + 1)) |^ b = (a |^ b) |^ (n + 1)
let a, b be Element of G; :: thesis: (a |^ (n + 1)) |^ b = (a |^ b) |^ (n + 1)
thus (a |^ (n + 1)) |^ b = ((a |^ n) * a) |^ b by GROUP_1:66
.= ((a |^ n) |^ b) * (a |^ b) by Th28
.= ((a |^ b) |^ n) * (a |^ b) by A1
.= (a |^ b) |^ (n + 1) by GROUP_1:66 ; :: thesis: verum
end;

Lm4: for n being Nat
for G being Group
for a, b being Element of G holds (a |^ n) |^ b = (a |^ b) |^ n
proof end;

theorem :: GROUP_3:33
for G being Group
for a, b being Element of G
for n being Nat holds (a |^ n) |^ b = (a |^ b) |^ n by Lm4;

theorem :: GROUP_3:34
for G being Group
for a, b being Element of G
for i being Integer holds (a |^ i) |^ b = (a |^ b) |^ i
proof end;

theorem Th35: :: GROUP_3:35
for G being Group
for a, b being Element of G st G is commutative Group holds
a |^ b = a
proof end;

theorem Th36: :: GROUP_3:36
for G being Group st ( for a, b being Element of G holds a |^ b = a ) holds
G is commutative
proof end;

definition
let G be Group;
let A, B be Subset of G;
func A |^ B -> Subset of G equals :: GROUP_3:def 3
 { (g |^ h) where g, h is Element of G : ( g in A & h in B ) } ;
coherence
{ (g |^ h) where g, h is Element of G : ( g in A & h in B ) } is Subset of G
proof end;
end;

:: deftheorem defines |^ GROUP_3:def 3 :
for G being Group
for A, B being Subset of G holds A |^ B = { (g |^ h) where g, h is Element of G : ( g in A & h in B ) } ;

theorem :: GROUP_3:37
canceled;

theorem Th38: :: GROUP_3:38
for x being set
for G being Group
for A, B being Subset of G holds
( x in A |^ B iff ex g, h being Element of G st
( x = g |^ h & g in A & h in B ) ) ;

theorem Th39: :: GROUP_3:39
for G being Group
for A, B being Subset of G holds
( A |^ B <> {} iff ( A <> {} & B <> {} ) )
proof end;

theorem Th40: :: GROUP_3:40
for G being Group
for A, B being Subset of G holds A |^ B c= ((B ") * A) * B
proof end;

theorem Th41: :: GROUP_3:41
for G being Group
for A, B, C being Subset of G holds (A * B) |^ C c= (A |^ C) * (B |^ C)
proof end;

theorem Th42: :: GROUP_3:42
for G being Group
for A, B, C being Subset of G holds (A |^ B) |^ C = A |^ (B * C)
proof end;

theorem :: GROUP_3:43
for G being Group
for A, B being Subset of G holds (A ") |^ B = (A |^ B) "
proof end;

theorem Th44: :: GROUP_3:44
for G being Group
for a, b being Element of G holds {a} |^ {b} = {(a |^ b)}
proof end;

theorem :: GROUP_3:45
for G being Group
for a, b, c being Element of G holds {a} |^ {b,c} = {(a |^ b),(a |^ c)}
proof end;

theorem :: GROUP_3:46
for G being Group
for a, b, c being Element of G holds {a,b} |^ {c} = {(a |^ c),(b |^ c)}
proof end;

theorem :: GROUP_3:47
for G being Group
for a, b, c, d being Element of G holds {a,b} |^ {c,d} = {(a |^ c),(a |^ d),(b |^ c),(b |^ d)}
proof end;

definition
let G be Group;
let A be Subset of G;
let g be Element of G;
func A |^ g -> Subset of G equals :: GROUP_3:def 4
A |^ {g};
correctness
coherence
A |^ {g} is Subset of G;
;
func g |^ A -> Subset of G equals :: GROUP_3:def 5
{g} |^ A;
correctness
coherence
{g} |^ A is Subset of G;
;
end;

:: deftheorem defines |^ GROUP_3:def 4 :
for G being Group
for A being Subset of G
for g being Element of G holds A |^ g = A |^ {g};

:: deftheorem defines |^ GROUP_3:def 5 :
for G being Group
for A being Subset of G
for g being Element of G holds g |^ A = {g} |^ A;

theorem :: GROUP_3:48
canceled;

theorem :: GROUP_3:49
canceled;

theorem Th50: :: GROUP_3:50
for x being set
for G being Group
for g being Element of G
for A being Subset of G holds
( x in A |^ g iff ex h being Element of G st
( x = h |^ g & h in A ) )
proof end;

theorem Th51: :: GROUP_3:51
for x being set
for G being Group
for g being Element of G
for A being Subset of G holds
( x in g |^ A iff ex h being Element of G st
( x = g |^ h & h in A ) )
proof end;

theorem :: GROUP_3:52
for G being Group
for g being Element of G
for A being Subset of G holds g |^ A c= ((A ") * g) * A
proof end;

theorem :: GROUP_3:53
for G being Group
for g being Element of G
for A, B being Subset of G holds (A |^ B) |^ g = A |^ (B * g) by Th42;

theorem :: GROUP_3:54
for G being Group
for g being Element of G
for A, B being Subset of G holds (A |^ g) |^ B = A |^ (g * B) by Th42;

theorem :: GROUP_3:55
for G being Group
for g being Element of G
for A, B being Subset of G holds (g |^ A) |^ B = g |^ (A * B) by Th42;

theorem Th56: :: GROUP_3:56
for G being Group
for a, b being Element of G
for A being Subset of G holds (A |^ a) |^ b = A |^ (a * b)
proof end;

theorem :: GROUP_3:57
for G being Group
for a, b being Element of G
for A being Subset of G holds (a |^ A) |^ b = a |^ (A * b) by Th42;

theorem :: GROUP_3:58
for G being Group
for a, b being Element of G
for A being Subset of G holds (a |^ b) |^ A = a |^ (b * A)
proof end;

theorem Th59: :: GROUP_3:59
for G being Group
for g being Element of G
for A being Subset of G holds A |^ g = ((g ") * A) * g
proof end;

theorem :: GROUP_3:60
for G being Group
for a being Element of G
for A, B being Subset of G holds (A * B) |^ a c= (A |^ a) * (B |^ a) by Th41;

theorem Th61: :: GROUP_3:61
for G being Group
for A being Subset of G holds A |^ (1_ G) = A
proof end;

theorem :: GROUP_3:62
for G being Group
for A being Subset of G st A <> {} holds
(1_ G) |^ A = {(1_ G)}
proof end;

theorem Th63: :: GROUP_3:63
for G being Group
for a being Element of G
for A being Subset of G holds
( (A |^ a) |^ (a ") = A & (A |^ (a ")) |^ a = A )
proof end;

theorem :: GROUP_3:64
canceled;

theorem Th65: :: GROUP_3:65
for G being Group holds
( G is commutative Group iff for A, B being Subset of G st B <> {} holds
A |^ B = A )
proof end;

theorem :: GROUP_3:66
for G being Group holds
( G is commutative Group iff for A being Subset of G
for g being Element of G holds A |^ g = A )
proof end;

theorem :: GROUP_3:67
for G being Group holds
( G is commutative Group iff for A being Subset of G
for g being Element of G st A <> {} holds
g |^ A = {g} )
proof end;

definition
let G be Group;
let H be Subgroup of G;
let a be Element of G;
func H |^ a -> strict Subgroup of G means :Def6: :: GROUP_3:def 6
 the carrier of it = (carr H) |^ a;
existence
ex b1 being strict Subgroup of G st the carrier of b1 = (carr H) |^ a
proof end;
correctness
uniqueness
for b1, b2 being strict Subgroup of G st the carrier of b1 = (carr H) |^ a & the carrier of b2 = (carr H) |^ a holds
b1 = b2;
by GROUP_2:68;
end;

:: deftheorem Def6 defines |^ GROUP_3:def 6 :
for G being Group
for H being Subgroup of G
for a being Element of G
for b4 being strict Subgroup of G holds
( b4 = H |^ a iff the carrier of b4 = (carr H) |^ a );

theorem :: GROUP_3:68
canceled;

theorem :: GROUP_3:69
canceled;

theorem Th70: :: GROUP_3:70
for x being set
for G being Group
for a being Element of G
for H being Subgroup of G holds
( x in H |^ a iff ex g being Element of G st
( x = g |^ a & g in H ) )
proof end;

theorem Th71: :: GROUP_3:71
for G being Group
for a being Element of G
for H being Subgroup of G holds the carrier of (H |^ a) = ((a ") * H) * a
proof end;

theorem Th72: :: GROUP_3:72
for G being Group
for a, b being Element of G
for H being Subgroup of G holds (H |^ a) |^ b = H |^ (a * b)
proof end;

theorem Th73: :: GROUP_3:73
for G being Group
for H being strict Subgroup of G holds H |^ (1_ G) = H
proof end;

theorem Th74: :: GROUP_3:74
for G being Group
for a being Element of G
for H being strict Subgroup of G holds
( (H |^ a) |^ (a ") = H & (H |^ (a ")) |^ a = H )
proof end;

theorem :: GROUP_3:75
canceled;

theorem Th76: :: GROUP_3:76
for G being Group
for a being Element of G
for H1, H2 being Subgroup of G holds (H1 /\ H2) |^ a = (H1 |^ a) /\ (H2 |^ a)
proof end;

theorem Th77: :: GROUP_3:77
for G being Group
for a being Element of G
for H being Subgroup of G holds card H = card (H |^ a)
proof end;

theorem Th78: :: GROUP_3:78
for G being Group
for a being Element of G
for H being Subgroup of G holds
( H is finite iff H |^ a is finite )
proof end;

registration
let G be Group;
let a be Element of G;
let H be finite Subgroup of G;
cluster H |^ a -> finite strict ;
coherence
H |^ a is finite by Th78;
end;

theorem :: GROUP_3:79
for G being Group
for a being Element of G
for H being finite Subgroup of G holds card H = card (H |^ a) by Th77;

theorem Th80: :: GROUP_3:80
for G being Group
for a being Element of G holds ((1). G) |^ a = (1). G
proof end;

theorem :: GROUP_3:81
for G being Group
for a being Element of G
for H being strict Subgroup of G st H |^ a = (1). G holds
H = (1). G
proof end;

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

theorem :: GROUP_3:83
for G being Group
for a being Element of G
for H being strict Subgroup of G st H |^ a = G holds
H = G
proof end;

theorem Th84: :: GROUP_3:84
for G being Group
for a being Element of G
for H being Subgroup of G holds Index H = Index (H |^ a)
proof end;

theorem :: GROUP_3:85
for G being Group
for a being Element of G
for H being Subgroup of G st Left_Cosets H is finite holds
index H = index (H |^ a)
proof end;

theorem Th86: :: GROUP_3:86
for G being Group st G is commutative Group holds
for H being strict Subgroup of G
for a being Element of G holds H |^ a = H
proof end;

definition
let G be Group;
let a, b be Element of G;
pred a,b are_conjugated means :Def7: :: GROUP_3:def 7
 ex g being Element of G st a = b |^ g;
end;

:: deftheorem Def7 defines are_conjugated GROUP_3:def 7 :
for G being Group
for a, b being Element of G holds
( a,b are_conjugated iff ex g being Element of G st a = b |^ g );

notation
let G be Group;
let a, b be Element of G;
antonym a,b are_not_conjugated for a,b are_conjugated ;
end;

theorem :: GROUP_3:87
canceled;

theorem Th88: :: GROUP_3:88
for G being Group
for a, b being Element of G holds
( a,b are_conjugated iff ex g being Element of G st b = a |^ g )
proof end;

theorem Th89: :: GROUP_3:89
for G being Group
for a being Element of G holds a,a are_conjugated
proof end;

theorem Th90: :: GROUP_3:90
for G being Group
for a, b being Element of G st a,b are_conjugated holds
b,a are_conjugated
proof end;

definition
let G be Group;
let a, b be Element of G;
:: original: are_conjugated
redefine pred a,b are_conjugated ;
reflexivity
for a being Element of G holds a,a are_conjugated by Th89;
symmetry
for a, b being Element of G st a,b are_conjugated holds
b,a are_conjugated by Th90;
end;

theorem Th91: :: GROUP_3:91
for G being Group
for a, b, c being Element of G st a,b are_conjugated & b,c are_conjugated holds
a,c are_conjugated
proof end;

theorem Th92: :: GROUP_3:92
for G being Group
for a being Element of G st ( a, 1_ G are_conjugated or 1_ G,a are_conjugated ) holds
a = 1_ G
proof end;

theorem Th93: :: GROUP_3:93
for G being Group
for a being Element of G holds a |^ (carr ((Omega). G)) = { b where b is Element of G : a,b are_conjugated }
proof end;

definition
let G be Group;
let a be Element of G;
func con_class a -> Subset of G equals :: GROUP_3:def 8
a |^ (carr ((Omega). G));
correctness
coherence
a |^ (carr ((Omega). G)) is Subset of G;
;
end;

:: deftheorem defines con_class GROUP_3:def 8 :
for G being Group
for a being Element of G holds con_class a = a |^ (carr ((Omega). G));

theorem :: GROUP_3:94
canceled;

theorem Th95: :: GROUP_3:95
for x being set
for G being Group
for a being Element of G holds
( x in con_class a iff ex b being Element of G st
( b = x & a,b are_conjugated ) )
proof end;

theorem Th96: :: GROUP_3:96
for G being Group
for a, b being Element of G holds
( a in con_class b iff a,b are_conjugated )
proof end;

theorem Th97: :: GROUP_3:97
for G being Group
for a, g being Element of G holds a |^ g in con_class a
proof end;

theorem :: GROUP_3:98
for G being Group
for a being Element of G holds a in con_class a by Th96;

theorem :: GROUP_3:99
for G being Group
for a, b being Element of G st a in con_class b holds
b in con_class a
proof end;

theorem :: GROUP_3:100
for G being Group
for a, b being Element of G holds
( con_class a = con_class b iff con_class a meets con_class b )
proof end;

theorem :: GROUP_3:101
for G being Group
for a being Element of G holds
( con_class a = {(1_ G)} iff a = 1_ G )
proof end;

theorem :: GROUP_3:102
for G being Group
for a being Element of G
for A being Subset of G holds (con_class a) * A = A * (con_class a)
proof end;

definition
let G be Group;
let A, B be Subset of G;
pred A,B are_conjugated means :Def9: :: GROUP_3:def 9
 ex g being Element of G st A = B |^ g;
end;

:: deftheorem Def9 defines are_conjugated GROUP_3:def 9 :
for G being Group
for A, B being Subset of G holds
( A,B are_conjugated iff ex g being Element of G st A = B |^ g );

notation
let G be Group;
let A, B be Subset of G;
antonym A,B are_not_conjugated for A,B are_conjugated ;
end;

theorem :: GROUP_3:103
canceled;

theorem Th104: :: GROUP_3:104
for G being Group
for A, B being Subset of G holds
( A,B are_conjugated iff ex g being Element of G st B = A |^ g )
proof end;

theorem Th105: :: GROUP_3:105
for G being Group
for A being Subset of G holds A,A are_conjugated
proof end;

theorem Th106: :: GROUP_3:106
for G being Group
for A, B being Subset of G st A,B are_conjugated holds
B,A are_conjugated
proof end;

definition
let G be Group;
let A, B be Subset of G;
:: original: are_conjugated
redefine pred A,B are_conjugated ;
reflexivity
for A being Subset of G holds A,A are_conjugated by Th105;
symmetry
for A, B being Subset of G st A,B are_conjugated holds
B,A are_conjugated by Th106;
end;

theorem Th107: :: GROUP_3:107
for G being Group
for A, B, C being Subset of G st A,B are_conjugated & B,C are_conjugated holds
A,C are_conjugated
proof end;

theorem Th108: :: GROUP_3:108
for G being Group
for a, b being Element of G holds
( {a},{b} are_conjugated iff a,b are_conjugated )
proof end;

theorem Th109: :: GROUP_3:109
for G being Group
for A being Subset of G
for H1 being Subgroup of G st A, carr H1 are_conjugated holds
ex H2 being strict Subgroup of G st the carrier of H2 = A
proof end;

definition
let G be Group;
let A be Subset of G;
func con_class A -> Subset-Family of G equals :: GROUP_3:def 10
 { B where B is Subset of G : A,B are_conjugated } ;
coherence
{ B where B is Subset of G : A,B are_conjugated } is Subset-Family of G
proof end;
end;

:: deftheorem defines con_class GROUP_3:def 10 :
for G being Group
for A being Subset of G holds con_class A = { B where B is Subset of G : A,B are_conjugated } ;

theorem :: GROUP_3:110
canceled;

theorem :: GROUP_3:111
for x being set
for G being Group
for A being Subset of G holds
( x in con_class A iff ex B being Subset of G st
( x = B & A,B are_conjugated ) ) ;

theorem :: GROUP_3:112
canceled;

theorem Th113: :: GROUP_3:113
for G being Group
for A, B being Subset of G holds
( A in con_class B iff A,B are_conjugated )
proof end;

theorem :: GROUP_3:114
for G being Group
for g being Element of G
for A being Subset of G holds A |^ g in con_class A
proof end;

theorem :: GROUP_3:115
for G being Group
for A being Subset of G holds A in con_class A ;

theorem :: GROUP_3:116
for G being Group
for A, B being Subset of G st A in con_class B holds
B in con_class A
proof end;

theorem :: GROUP_3:117
for G being Group
for A, B being Subset of G holds
( con_class A = con_class B iff con_class A meets con_class B )
proof end;

theorem Th118: :: GROUP_3:118
for G being Group
for a being Element of G holds con_class {a} = { {b} where b is Element of G : b in con_class a }
proof end;

theorem :: GROUP_3:119
for G being Group
for A being Subset of G st G is finite holds
con_class A is finite ;

definition
let G be Group;
let H1, H2 be Subgroup of G;
pred H1,H2 are_conjugated means :Def11: :: GROUP_3:def 11
 ex g being Element of G st multMagma(# the carrier of H1, the multF of H1 #) = H2 |^ g;
end;

:: deftheorem Def11 defines are_conjugated GROUP_3:def 11 :
for G being Group
for H1, H2 being Subgroup of G holds
( H1,H2 are_conjugated iff ex g being Element of G st multMagma(# the carrier of H1, the multF of H1 #) = H2 |^ g );

notation
let G be Group;
let H1, H2 be Subgroup of G;
antonym H1,H2 are_not_conjugated for H1,H2 are_conjugated ;
end;

theorem :: GROUP_3:120
canceled;

theorem Th121: :: GROUP_3:121
for G being Group
for H1, H2 being strict Subgroup of G holds
( H1,H2 are_conjugated iff ex g being Element of G st H2 = H1 |^ g )
proof end;

theorem Th122: :: GROUP_3:122
for G being Group
for H1 being strict Subgroup of G holds H1,H1 are_conjugated
proof end;

theorem Th123: :: GROUP_3:123
for G being Group
for H1, H2 being strict Subgroup of G st H1,H2 are_conjugated holds
H2,H1 are_conjugated
proof end;

definition
let G be Group;
let H1, H2 be strict Subgroup of G;
:: original: are_conjugated
redefine pred H1,H2 are_conjugated ;
reflexivity
for H1 being strict Subgroup of G holds H1,H1 are_conjugated by Th122;
symmetry
for H1, H2 being strict Subgroup of G st H1,H2 are_conjugated holds
H2,H1 are_conjugated by Th123;
end;

theorem Th124: :: GROUP_3:124
for G being Group
for H3 being Subgroup of G
for H1, H2 being strict Subgroup of G st H1,H2 are_conjugated & H2,H3 are_conjugated holds
H1,H3 are_conjugated
proof end;

definition
let G be Group;
let H be Subgroup of G;
func con_class H -> Subset of (Subgroups G) means :Def12: :: GROUP_3:def 12
 for x being set holds
( x in it iff ex H1 being strict Subgroup of G st
( x = H1 & H,H1 are_conjugated ) );
existence
ex b1 being Subset of (Subgroups G) st
for x being set holds
( x in b1 iff ex H1 being strict Subgroup of G st
( x = H1 & H,H1 are_conjugated ) )
proof end;
uniqueness
for b1, b2 being Subset of (Subgroups G) st ( for x being set holds
( x in b1 iff ex H1 being strict Subgroup of G st
( x = H1 & H,H1 are_conjugated ) ) ) & ( for x being set holds
( x in b2 iff ex H1 being strict Subgroup of G st
( x = H1 & H,H1 are_conjugated ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def12 defines con_class GROUP_3:def 12 :
for G being Group
for H being Subgroup of G
for b3 being Subset of (Subgroups G) holds
( b3 = con_class H iff for x being set holds
( x in b3 iff ex H1 being strict Subgroup of G st
( x = H1 & H,H1 are_conjugated ) ) );

theorem :: GROUP_3:125
canceled;

theorem :: GROUP_3:126
canceled;

theorem Th127: :: GROUP_3:127
for x being set
for G being Group
for H being Subgroup of G st x in con_class H holds
x is strict Subgroup of G
proof end;

theorem Th128: :: GROUP_3:128
for G being Group
for H1, H2 being strict Subgroup of G holds
( H1 in con_class H2 iff H1,H2 are_conjugated )
proof end;

theorem Th129: :: GROUP_3:129
for G being Group
for g being Element of G
for H being strict Subgroup of G holds H |^ g in con_class H
proof end;

theorem Th130: :: GROUP_3:130
for G being Group
for H being strict Subgroup of G holds H in con_class H
proof end;

theorem :: GROUP_3:131
for G being Group
for H1, H2 being strict Subgroup of G st H1 in con_class H2 holds
H2 in con_class H1
proof end;

theorem :: GROUP_3:132
for G being Group
for H1, H2 being strict Subgroup of G holds
( con_class H1 = con_class H2 iff con_class H1 meets con_class H2 )
proof end;

theorem :: GROUP_3:133
for G being Group
for H being Subgroup of G st G is finite holds
con_class H is finite by Th19, FINSET_1:13;

theorem Th134: :: GROUP_3:134
for G being Group
for H2 being Subgroup of G
for H1 being strict Subgroup of G holds
( H1,H2 are_conjugated iff carr H1, carr H2 are_conjugated )
proof end;

definition
let G be Group;
let IT be Subgroup of G;
attr IT is normal means :Def13: :: GROUP_3:def 13
 for a being Element of G holds IT |^ a = multMagma(# the carrier of IT, the multF of IT #);
end;

:: deftheorem Def13 defines normal GROUP_3:def 13 :
for G being Group
for IT being Subgroup of G holds
( IT is normal iff for a being Element of G holds IT |^ a = multMagma(# the carrier of IT, the multF of IT #) );

registration
let G be Group;
cluster non empty strict unital Group-like associative normal Subgroup of G;
existence
ex b1 being Subgroup of G st
( b1 is strict & b1 is normal )
proof end;
end;

theorem :: GROUP_3:135
canceled;

theorem :: GROUP_3:136
canceled;

theorem Th137: :: GROUP_3:137
for G being Group holds
( (1). G is normal & (Omega). G is normal )
proof end;

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

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

theorem Th140: :: GROUP_3:140
for G being Group
for H being Subgroup of G holds
( H is normal Subgroup of G iff for a being Element of G holds a * H = H * a )
proof end;

theorem Th141: :: GROUP_3:141
for G being Group
for H being Subgroup of G holds
( H is normal Subgroup of G iff for a being Element of G holds a * H c= H * a )
proof end;

theorem Th142: :: GROUP_3:142
for G being Group
for H being Subgroup of G holds
( H is normal Subgroup of G iff for a being Element of G holds H * a c= a * H )
proof end;

theorem :: GROUP_3:143
for G being Group
for H being Subgroup of G holds
( H is normal Subgroup of G iff for A being Subset of G holds A * H = H * A )
proof end;

theorem :: GROUP_3:144
for G being Group
for H being strict Subgroup of G holds
( H is normal Subgroup of G iff for a being Element of G holds H is Subgroup of H |^ a )
proof end;

theorem :: GROUP_3:145
for G being Group
for H being strict Subgroup of G holds
( H is normal Subgroup of G iff for a being Element of G holds H |^ a is Subgroup of H )
proof end;

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

theorem :: GROUP_3:147
for G being Group
for H being strict Subgroup of G holds
( H is normal Subgroup of G iff for a being Element of G st a in H holds
con_class a c= carr H )
proof end;

Lm5: for G being Group
for N2 being normal Subgroup of G
for N1 being strict normal Subgroup of G holds (carr N1) * (carr N2) c= (carr N2) * (carr N1)
proof end;

theorem Th148: :: GROUP_3:148
for G being Group
for N1, N2 being strict normal Subgroup of G holds (carr N1) * (carr N2) = (carr N2) * (carr N1)
proof end;

theorem :: GROUP_3:149
for G being Group
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)
proof end;

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

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

definition
let G be Group;
let A be Subset of G;
func Normalizator A -> strict Subgroup of G means :Def14: :: GROUP_3:def 14
 the carrier of it = { h where h is Element of G : A |^ h = A } ;
existence
ex b1 being strict Subgroup of G st the carrier of b1 = { h where h is Element of G : A |^ h = A }
proof end;
uniqueness
for b1, b2 being strict Subgroup of G st the carrier of b1 = { h where h is Element of G : A |^ h = A } & the carrier of b2 = { h where h is Element of G : A |^ h = A } holds
b1 = b2 by GROUP_2:68;
end;

:: deftheorem Def14 defines Normalizator GROUP_3:def 14 :
for G being Group
for A being Subset of G
for b3 being strict Subgroup of G holds
( b3 = Normalizator A iff the carrier of b3 = { h where h is Element of G : A |^ h = A } );

theorem :: GROUP_3:152
canceled;

theorem :: GROUP_3:153
canceled;

theorem Th154: :: GROUP_3:154
for x being set
for G being Group
for A being Subset of G holds
( x in Normalizator A iff ex h being Element of G st
( x = h & A |^ h = A ) )
proof end;

theorem Th155: :: GROUP_3:155
for G being Group
for A being Subset of G holds card (con_class A) = Index (Normalizator A)
proof end;

theorem :: GROUP_3:156
for G being Group
for A being Subset of G st ( con_class A is finite or Left_Cosets (Normalizator A) is finite ) holds
ex C being finite set st
( C = con_class A & card C = index (Normalizator A) )
proof end;

theorem Th157: :: GROUP_3:157
for G being Group
for a being Element of G holds card (con_class a) = Index (Normalizator {a})
proof end;

theorem :: GROUP_3:158
for G being Group
for a being Element of G st ( con_class a is finite or Left_Cosets (Normalizator {a}) is finite ) holds
ex C being finite set st
( C = con_class a & card C = index (Normalizator {a}) )
proof end;

definition
let G be Group;
let H be Subgroup of G;
func Normalizator H -> strict Subgroup of G equals :: GROUP_3:def 15
 Normalizator (carr H);
correctness
coherence
Normalizator (carr H) is strict Subgroup of G;
;
end;

:: deftheorem defines Normalizator GROUP_3:def 15 :
for G being Group
for H being Subgroup of G holds Normalizator H = Normalizator (carr H);

theorem :: GROUP_3:159
canceled;

theorem Th160: :: GROUP_3:160
for x being set
for G being Group
for H being strict Subgroup of G holds
( x in Normalizator H iff ex h being Element of G st
( x = h & H |^ h = H ) )
proof end;

theorem Th161: :: GROUP_3:161
for G being Group
for H being strict Subgroup of G holds card (con_class H) = Index (Normalizator H)
proof end;

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

theorem Th163: :: GROUP_3:163
for G being strict Group
for H being strict Subgroup of G holds
( H is normal Subgroup of G iff Normalizator H = G )
proof end;

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

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