:: GROUP_3 semantic presentation

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 mult 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 Th5: :: 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

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) by GROUP_2:116;

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

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) by GROUP_2:118;

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines Subgroups GROUP_3:def 1 :

registration

let G be Group;
cluster Subgroups G -> non empty ;
coherence

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 ;

end;

:: deftheorem defines |^ GROUP_3:def 2 :

theorem Th20: :: GROUP_3:20

for G being Group
for a, b being Element of G holds
( a |^ b = ((b " ) * a) * b & a |^ b = (b " ) * (a * b) ) by GROUP_1:def 4;

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 Th26: :: GROUP_3:26

for G being Group
for a being Element of G holds
( a |^ (a " ) = a & (a " ) |^ a = a " )

proof end;

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:
let a, b be Element of G;
thus (a |^ 0) |^ b = (1. G) |^ b by GROUP_1:43
.= 1. G by Th22
.= (a |^ b) |^ 0 by GROUP_1:43 ; :: thesis:

end;

Lm3: now

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

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

proof end;

end;

:: deftheorem defines |^ GROUP_3:def 3 :

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 ;
func g |^ A -> Subset of G equals :: GROUP_3:def 5
{g} |^ A;
correctness ;

end;

:: deftheorem defines |^ GROUP_3:def 4 :

:: deftheorem defines |^ GROUP_3:def 5 :

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 Th53: :: 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 Th54: :: 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 Th53;

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

proof end;

correctness by GROUP_2:68;

end;

:: deftheorem Def6 defines |^ GROUP_3:def 6 :

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 Ord H = Ord (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;

theorem Th79: :: GROUP_3:79

for G being Group
for a being Element of G
for H being Subgroup of G st H is finite holds
ord H = ord (H |^ a)

proof end;

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 :

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 by Th89;
symmetry 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 ;

end;

:: deftheorem defines con_class GROUP_3:def 8 :

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 :

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 by Th105;
symmetry 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

proof end;

end;

:: deftheorem defines con_class GROUP_3:def 10 :

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

proof end;

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 HGrStr(# the carrier of H1,the mult of H1 #) = H2 |^ g;

end;

:: deftheorem Def11 defines are_conjugated GROUP_3:def 11 :

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 by Th122;
symmetry 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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def12 defines con_class GROUP_3:def 12 :

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

proof end;

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 = HGrStr(# the carrier of IT,the mult of IT #);

end;

:: deftheorem Def13 defines normal GROUP_3:def 13 :

registration

let G be Group;
cluster strict normal Subgroup of G;
existence

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

proof end;

uniqueness by GROUP_2:68;

end;

:: deftheorem Def14 defines Normalizator GROUP_3:def 14 :

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 ;

end;

:: deftheorem defines Normalizator GROUP_3:def 15 :

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;