:: GROUP_3 semantic presentation

theorem Th1: :: GROUP_3:1

for b₁ being Group
for b₂, b₃ being Element of b₁ holds
( (b₂ * b₃) * (b₃ " ) = b₂ & (b₂ * (b₃ " )) * b₃ = b₂ & ((b₃ " ) * b₃) * b₂ = b₂ & (b₃ * (b₃ " )) * b₂ = b₂ & b₂ * (b₃ * (b₃ " )) = b₂ & b₂ * ((b₃ " ) * b₃) = b₂ & (b₃ " ) * (b₃ * b₂) = b₂ & b₃ * ((b₃ " ) * b₂) = b₂ )

proof end;

Lemma2: for b₁ being commutative Group
for b₂, b₃ being Element of b₁ holds b₂ * b₃ = b₃ * b₂
;

theorem Th2: :: GROUP_3:2

for b₁ being Group holds
( b₁ is commutative Group iff the mult of b₁ is commutative )

proof end;

theorem Th3: :: GROUP_3:3

for b₁ being Group holds (1). b₁ is commutative

proof end;

theorem Th4: :: GROUP_3:4

for b₁ being Group
for b₂, b₃, b₄, b₅ being Subset of b₁ st b₂ c= b₃ & b₄ c= b₅ holds
b₂ * b₄ c= b₃ * b₅

proof end;

theorem Th5: :: GROUP_3:5

for b₁ being Group
for b₂ being Element of b₁
for b₃, b₄ being Subset of b₁ st b₃ c= b₄ holds
( b₂ * b₃ c= b₂ * b₄ & b₃ * b₂ c= b₄ * b₂ ) by Th4;

theorem Th6: :: GROUP_3:6

for b₁ being Group
for b₂ being Element of b₁
for b₃, b₄ being Subgroup of b₁ st b₃ is Subgroup of b₄ holds
( b₂ * b₃ c= b₂ * b₄ & b₃ * b₂ c= b₄ * b₂ )

proof end;

theorem Th7: :: GROUP_3:7

for b₁ being Group
for b₂ being Element of b₁
for b₃ being Subgroup of b₁ holds b₂ * b₃ = {b₂} * b₃ ;

theorem Th8: :: GROUP_3:8

for b₁ being Group
for b₂ being Element of b₁
for b₃ being Subgroup of b₁ holds b₃ * b₂ = b₃ * {b₂} ;

theorem Th9: :: GROUP_3:9

for b₁ being Group
for b₂ being Element of b₁
for b₃ being Subset of b₁
for b₄ being Subgroup of b₁ holds (b₂ * b₃) * b₄ = b₂ * (b₃ * b₄) by GROUP_2:116;

theorem Th10: :: GROUP_3:10

for b₁ being Group
for b₂ being Element of b₁
for b₃ being Subset of b₁
for b₄ being Subgroup of b₁ holds (b₃ * b₂) * b₄ = b₃ * (b₂ * b₄)

proof end;

theorem Th11: :: GROUP_3:11

for b₁ being Group
for b₂ being Element of b₁
for b₃ being Subset of b₁
for b₄ being Subgroup of b₁ holds (b₂ * b₄) * b₃ = b₂ * (b₄ * b₃)

proof end;

theorem Th12: :: GROUP_3:12

for b₁ being Group
for b₂ being Element of b₁
for b₃ being Subset of b₁
for b₄ being Subgroup of b₁ holds (b₃ * b₄) * b₂ = b₃ * (b₄ * b₂)

proof end;

theorem Th13: :: GROUP_3:13

for b₁ being Group
for b₂ being Element of b₁
for b₃ being Subset of b₁
for b₄ being Subgroup of b₁ holds (b₄ * b₂) * b₃ = b₄ * (b₂ * b₃)

proof end;

theorem Th14: :: GROUP_3:14

for b₁ being Group
for b₂ being Element of b₁
for b₃ being Subset of b₁
for b₄ being Subgroup of b₁ holds (b₄ * b₃) * b₂ = b₄ * (b₃ * b₂) by GROUP_2:118;

theorem Th15: :: GROUP_3:15

for b₁ being Group
for b₂ being Element of b₁
for b₃, b₄ being Subgroup of b₁ holds (b₃ * b₂) * b₄ = b₃ * (b₂ * b₄) by Th10;

definition

let c₁ be Group;
func Subgroups c₁ -> set means :Def1: :: GROUP_3:def 1
for b₁ being set holds
( b₁ in a₂ iff b₁ is strict Subgroup of a₁ );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines Subgroups GROUP_3:def 1 :

registration

let c₁ be Group;
cluster Subgroups a₁ -> non empty ;
coherence

proof end;

end;

theorem Th16: :: GROUP_3:16

canceled;

theorem Th17: :: GROUP_3:17

canceled;

theorem Th18: :: GROUP_3:18

for b₁ being strict Group holds b₁ in Subgroups b₁

proof end;

theorem Th19: :: GROUP_3:19

for b₁ being Group st b₁ is finite holds
Subgroups b₁ is finite

proof end;

definition

let c₁ be Group;
let c₂, c₃ be Element of c₁;
func c₂ |^ c₃ -> Element of a₁ equals :: GROUP_3:def 2
((a₃ " ) * a₂) * a₃;
correctness ;

end;

:: deftheorem Def2 defines |^ GROUP_3:def 2 :

theorem Th20: :: GROUP_3:20

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

theorem Th21: :: GROUP_3:21

for b₁ being Group
for b₂, b₃, b₄ being Element of b₁ st b₂ |^ b₃ = b₄ |^ b₃ holds
b₂ = b₄

proof end;

theorem Th22: :: GROUP_3:22

for b₁ being Group
for b₂ being Element of b₁ holds (1. b₁) |^ b₂ = 1. b₁

proof end;

theorem Th23: :: GROUP_3:23

for b₁ being Group
for b₂, b₃ being Element of b₁ st b₂ |^ b₃ = 1. b₁ holds
b₂ = 1. b₁

proof end;

theorem Th24: :: GROUP_3:24

for b₁ being Group
for b₂ being Element of b₁ holds b₂ |^ (1. b₁) = b₂

proof end;

theorem Th25: :: GROUP_3:25

for b₁ being Group
for b₂ being Element of b₁ holds b₂ |^ b₂ = b₂

proof end;

theorem Th26: :: GROUP_3:26

for b₁ being Group
for b₂ being Element of b₁ holds
( b₂ |^ (b₂ " ) = b₂ & (b₂ " ) |^ b₂ = b₂ " )

proof end;

theorem Th27: :: GROUP_3:27

for b₁ being Group
for b₂, b₃ being Element of b₁ holds
( b₂ |^ b₃ = b₂ iff b₂ * b₃ = b₃ * b₂ )

proof end;

theorem Th28: :: GROUP_3:28

for b₁ being Group
for b₂, b₃, b₄ being Element of b₁ holds (b₂ * b₃) |^ b₄ = (b₂ |^ b₄) * (b₃ |^ b₄)

proof end;

theorem Th29: :: GROUP_3:29

for b₁ being Group
for b₂, b₃, b₄ being Element of b₁ holds (b₂ |^ b₃) |^ b₄ = b₂ |^ (b₃ * b₄)

proof end;

theorem Th30: :: GROUP_3:30

for b₁ being Group
for b₂, b₃ being Element of b₁ holds
( (b₂ |^ b₃) |^ (b₃ " ) = b₂ & (b₂ |^ (b₃ " )) |^ b₃ = b₂ )

proof end;

theorem Th31: :: GROUP_3:31

canceled;

theorem Th32: :: GROUP_3:32

for b₁ being Group
for b₂, b₃ being Element of b₁ holds (b₂ " ) |^ b₃ = (b₂ |^ b₃) "

proof end;

E21: now

let c₁ be Group;
let c₂, c₃ be Element of c₁;
thus (c₂ |^ 0) |^ c₃ = (1. c₁) |^ c₃ by GROUP_1:43
.= 1. c₁ by Th22
.= (c₂ |^ c₃) |^ 0 by GROUP_1:43 ;

end;

E22: now

let c₁ be Nat;
assume E23: for b₁ being Group
for b₂, b₃ being Element of b₁ holds (b₂ |^ c₁) |^ b₃ = (b₂ |^ b₃) |^ c₁ ;
let c₂ be Group;
let c₃, c₄ be Element of c₂;
thus (c₃ |^ (c₁ + 1)) |^ c₄ = ((c₃ |^ c₁) * c₃) |^ c₄ by GROUP_1:49
.= ((c₃ |^ c₁) |^ c₄) * (c₃ |^ c₄) by Th28
.= ((c₃ |^ c₄) |^ c₁) * (c₃ |^ c₄) by E23
.= (c₃ |^ c₄) |^ (c₁ + 1) by GROUP_1:49 ;

end;

Lemma23: for b₁ being Nat
for b₂ being Group
for b₃, b₄ being Element of b₂ holds (b₃ |^ b₁) |^ b₄ = (b₃ |^ b₄) |^ b₁

proof end;

theorem Th33: :: GROUP_3:33

for b₁ being Group
for b₂, b₃ being Element of b₁
for b₄ being Nat holds (b₂ |^ b₄) |^ b₃ = (b₂ |^ b₃) |^ b₄ by Lemma23;

theorem Th34: :: GROUP_3:34

for b₁ being Group
for b₂, b₃ being Element of b₁
for b₄ being Integer holds (b₂ |^ b₄) |^ b₃ = (b₂ |^ b₃) |^ b₄

proof end;

theorem Th35: :: GROUP_3:35

for b₁ being Group
for b₂, b₃ being Element of b₁ st b₁ is commutative Group holds
b₂ |^ b₃ = b₂

proof end;

theorem Th36: :: GROUP_3:36

for b₁ being Group st ( for b₂, b₃ being Element of b₁ holds b₂ |^ b₃ = b₂ ) holds
b₁ is commutative

proof end;

definition

let c₁ be Group;
let c₂, c₃ be Subset of c₁;
func c₂ |^ c₃ -> Subset of a₁ equals :: GROUP_3:def 3
{ (b₁ |^ b₂) where B is Element of a₁, B is Element of a₁ : ( b₁ in a₂ & b₂ in a₃ ) } ;
coherence

proof end;

end;

:: deftheorem Def3 defines |^ GROUP_3:def 3 :

theorem Th37: :: GROUP_3:37

canceled;

theorem Th38: :: GROUP_3:38

for b₁ being set
for b₂ being Group
for b₃, b₄ being Subset of b₂ holds
( b₁ in b₃ |^ b₄ iff ex b₅, b₆ being Element of b₂ st
( b₁ = b₅ |^ b₆ & b₅ in b₃ & b₆ in b₄ ) ) ;

theorem Th39: :: GROUP_3:39

for b₁ being Group
for b₂, b₃ being Subset of b₁ holds
( b₂ |^ b₃ <> {} iff ( b₂ <> {} & b₃ <> {} ) )

proof end;

theorem Th40: :: GROUP_3:40

for b₁ being Group
for b₂, b₃ being Subset of b₁ holds b₂ |^ b₃ c= ((b₃ " ) * b₂) * b₃

proof end;

theorem Th41: :: GROUP_3:41

for b₁ being Group
for b₂, b₃, b₄ being Subset of b₁ holds (b₂ * b₃) |^ b₄ c= (b₂ |^ b₄) * (b₃ |^ b₄)

proof end;

theorem Th42: :: GROUP_3:42

for b₁ being Group
for b₂, b₃, b₄ being Subset of b₁ holds (b₂ |^ b₃) |^ b₄ = b₂ |^ (b₃ * b₄)

proof end;

theorem Th43: :: GROUP_3:43

for b₁ being Group
for b₂, b₃ being Subset of b₁ holds (b₂ " ) |^ b₃ = (b₂ |^ b₃) "

proof end;

theorem Th44: :: GROUP_3:44

for b₁ being Group
for b₂, b₃ being Element of b₁ holds {b₂} |^ {b₃} = {(b₂ |^ b₃)}

proof end;

theorem Th45: :: GROUP_3:45

for b₁ being Group
for b₂, b₃, b₄ being Element of b₁ holds {b₂} |^ {b₃,b₄} = {(b₂ |^ b₃),(b₂ |^ b₄)}

proof end;

theorem Th46: :: GROUP_3:46

for b₁ being Group
for b₂, b₃, b₄ being Element of b₁ holds {b₂,b₃} |^ {b₄} = {(b₂ |^ b₄),(b₃ |^ b₄)}

proof end;

theorem Th47: :: GROUP_3:47

for b₁ being Group
for b₂, b₃, b₄, b₅ being Element of b₁ holds {b₂,b₃} |^ {b₄,b₅} = {(b₂ |^ b₄),(b₂ |^ b₅),(b₃ |^ b₄),(b₃ |^ b₅)}

proof end;

definition

let c₁ be Group;
let c₂ be Subset of c₁;
let c₃ be Element of c₁;
func c₂ |^ c₃ -> Subset of a₁ equals :: GROUP_3:def 4
a₂ |^ {a₃};
correctness ;
func c₃ |^ c₂ -> Subset of a₁ equals :: GROUP_3:def 5
{a₃} |^ a₂;
correctness ;

end;

:: deftheorem Def4 defines |^ GROUP_3:def 4 :

:: deftheorem Def5 defines |^ GROUP_3:def 5 :

theorem Th48: :: GROUP_3:48

canceled;

theorem Th49: :: GROUP_3:49

canceled;

theorem Th50: :: GROUP_3:50

for b₁ being set
for b₂ being Group
for b₃ being Element of b₂
for b₄ being Subset of b₂ holds
( b₁ in b₄ |^ b₃ iff ex b₅ being Element of b₂ st
( b₁ = b₅ |^ b₃ & b₅ in b₄ ) )

proof end;

theorem Th51: :: GROUP_3:51

for b₁ being set
for b₂ being Group
for b₃ being Element of b₂
for b₄ being Subset of b₂ holds
( b₁ in b₃ |^ b₄ iff ex b₅ being Element of b₂ st
( b₁ = b₃ |^ b₅ & b₅ in b₄ ) )

proof end;

theorem Th52: :: GROUP_3:52

for b₁ being Group
for b₂ being Element of b₁
for b₃ being Subset of b₁ holds b₂ |^ b₃ c= ((b₃ " ) * b₂) * b₃

proof end;

theorem Th53: :: GROUP_3:53

for b₁ being Group
for b₂ being Element of b₁
for b₃, b₄ being Subset of b₁ holds (b₃ |^ b₄) |^ b₂ = b₃ |^ (b₄ * b₂) by Th42;

theorem Th54: :: GROUP_3:54

for b₁ being Group
for b₂ being Element of b₁
for b₃, b₄ being Subset of b₁ holds (b₃ |^ b₂) |^ b₄ = b₃ |^ (b₂ * b₄) by Th42;

theorem Th55: :: GROUP_3:55

for b₁ being Group
for b₂ being Element of b₁
for b₃, b₄ being Subset of b₁ holds (b₂ |^ b₃) |^ b₄ = b₂ |^ (b₃ * b₄) by Th42;

theorem Th56: :: GROUP_3:56

for b₁ being Group
for b₂, b₃ being Element of b₁
for b₄ being Subset of b₁ holds (b₄ |^ b₂) |^ b₃ = b₄ |^ (b₂ * b₃)

proof end;

theorem Th57: :: GROUP_3:57

for b₁ being Group
for b₂, b₃ being Element of b₁
for b₄ being Subset of b₁ holds (b₂ |^ b₄) |^ b₃ = b₂ |^ (b₄ * b₃) by Th53;

theorem Th58: :: GROUP_3:58

for b₁ being Group
for b₂, b₃ being Element of b₁
for b₄ being Subset of b₁ holds (b₂ |^ b₃) |^ b₄ = b₂ |^ (b₃ * b₄)

proof end;

theorem Th59: :: GROUP_3:59

for b₁ being Group
for b₂ being Element of b₁
for b₃ being Subset of b₁ holds b₃ |^ b₂ = ((b₂ " ) * b₃) * b₂

proof end;

theorem Th60: :: GROUP_3:60

for b₁ being Group
for b₂ being Element of b₁
for b₃, b₄ being Subset of b₁ holds (b₃ * b₄) |^ b₂ c= (b₃ |^ b₂) * (b₄ |^ b₂) by Th41;

theorem Th61: :: GROUP_3:61

for b₁ being Group
for b₂ being Subset of b₁ holds b₂ |^ (1. b₁) = b₂

proof end;

theorem Th62: :: GROUP_3:62

for b₁ being Group
for b₂ being Subset of b₁ st b₂ <> {} holds
(1. b₁) |^ b₂ = {(1. b₁)}

proof end;

theorem Th63: :: GROUP_3:63

for b₁ being Group
for b₂ being Element of b₁
for b₃ being Subset of b₁ holds
( (b₃ |^ b₂) |^ (b₂ " ) = b₃ & (b₃ |^ (b₂ " )) |^ b₂ = b₃ )

proof end;

theorem Th64: :: GROUP_3:64

canceled;

theorem Th65: :: GROUP_3:65

for b₁ being Group holds
( b₁ is commutative Group iff for b₂, b₃ being Subset of b₁ st b₃ <> {} holds
b₂ |^ b₃ = b₂ )

proof end;

theorem Th66: :: GROUP_3:66

for b₁ being Group holds
( b₁ is commutative Group iff for b₂ being Subset of b₁
for b₃ being Element of b₁ holds b₂ |^ b₃ = b₂ )

proof end;

theorem Th67: :: GROUP_3:67

for b₁ being Group holds
( b₁ is commutative Group iff for b₂ being Subset of b₁
for b₃ being Element of b₁ st b₂ <> {} holds
b₃ |^ b₂ = {b₃} )

proof end;

definition

let c₁ be Group;
let c₂ be Subgroup of c₁;
let c₃ be Element of c₁;
func c₂ |^ c₃ -> strict Subgroup of a₁ means :Def6: :: GROUP_3:def 6
the carrier of a₄ = (carr a₂) |^ a₃;
existence

proof end;

correctness by GROUP_2:68;

end;

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

theorem Th68: :: GROUP_3:68

canceled;

theorem Th69: :: GROUP_3:69

canceled;

theorem Th70: :: GROUP_3:70

for b₁ being set
for b₂ being Group
for b₃ being Element of b₂
for b₄ being Subgroup of b₂ holds
( b₁ in b₄ |^ b₃ iff ex b₅ being Element of b₂ st
( b₁ = b₅ |^ b₃ & b₅ in b₄ ) )

proof end;

theorem Th71: :: GROUP_3:71

for b₁ being Group
for b₂ being Element of b₁
for b₃ being Subgroup of b₁ holds the carrier of (b₃ |^ b₂) = ((b₂ " ) * b₃) * b₂

proof end;

theorem Th72: :: GROUP_3:72

for b₁ being Group
for b₂, b₃ being Element of b₁
for b₄ being Subgroup of b₁ holds (b₄ |^ b₂) |^ b₃ = b₄ |^ (b₂ * b₃)

proof end;

theorem Th73: :: GROUP_3:73

for b₁ being Group
for b₂ being strict Subgroup of b₁ holds b₂ |^ (1. b₁) = b₂

proof end;

theorem Th74: :: GROUP_3:74

for b₁ being Group
for b₂ being Element of b₁
for b₃ being strict Subgroup of b₁ holds
( (b₃ |^ b₂) |^ (b₂ " ) = b₃ & (b₃ |^ (b₂ " )) |^ b₂ = b₃ )

proof end;

theorem Th75: :: GROUP_3:75

canceled;

theorem Th76: :: GROUP_3:76

for b₁ being Group
for b₂ being Element of b₁
for b₃, b₄ being Subgroup of b₁ holds (b₃ /\ b₄) |^ b₂ = (b₃ |^ b₂) /\ (b₄ |^ b₂)

proof end;

theorem Th77: :: GROUP_3:77

for b₁ being Group
for b₂ being Element of b₁
for b₃ being Subgroup of b₁ holds Ord b₃ = Ord (b₃ |^ b₂)

proof end;

theorem Th78: :: GROUP_3:78

for b₁ being Group
for b₂ being Element of b₁
for b₃ being Subgroup of b₁ holds
( b₃ is finite iff b₃ |^ b₂ is finite )

proof end;

theorem Th79: :: GROUP_3:79

for b₁ being Group
for b₂ being Element of b₁
for b₃ being Subgroup of b₁ st b₃ is finite holds
ord b₃ = ord (b₃ |^ b₂)

proof end;

theorem Th80: :: GROUP_3:80

for b₁ being Group
for b₂ being Element of b₁ holds ((1). b₁) |^ b₂ = (1). b₁

proof end;

theorem Th81: :: GROUP_3:81

for b₁ being Group
for b₂ being Element of b₁
for b₃ being strict Subgroup of b₁ st b₃ |^ b₂ = (1). b₁ holds
b₃ = (1). b₁

proof end;

theorem Th82: :: GROUP_3:82

for b₁ being Group
for b₂ being Element of b₁ holds ((Omega). b₁) |^ b₂ = (Omega). b₁

proof end;

theorem Th83: :: GROUP_3:83

for b₁ being Group
for b₂ being Element of b₁
for b₃ being strict Subgroup of b₁ st b₃ |^ b₂ = b₁ holds
b₃ = b₁

proof end;

theorem Th84: :: GROUP_3:84

for b₁ being Group
for b₂ being Element of b₁
for b₃ being Subgroup of b₁ holds Index b₃ = Index (b₃ |^ b₂)

proof end;

theorem Th85: :: GROUP_3:85

for b₁ being Group
for b₂ being Element of b₁
for b₃ being Subgroup of b₁ st Left_Cosets b₃ is finite holds
index b₃ = index (b₃ |^ b₂)

proof end;

theorem Th86: :: GROUP_3:86

for b₁ being Group st b₁ is commutative Group holds
for b₂ being strict Subgroup of b₁
for b₃ being Element of b₁ holds b₂ |^ b₃ = b₂

proof end;

definition

let c₁ be Group;
let c₂, c₃ be Element of c₁;
pred c₂,c₃ are_conjugated means :Def7: :: GROUP_3:def 7
ex b₁ being Element of a₁ st a₂ = a₃ |^ b₁;

end;

:: deftheorem Def7 defines are_conjugated GROUP_3:def 7 :

notation

let c₁ be Group;
let c₂, c₃ be Element of c₁;
antonym c₂,c₃ are_not_conjugated for c₂,c₃ are_conjugated ;

end;

theorem Th87: :: GROUP_3:87

canceled;

theorem Th88: :: GROUP_3:88

for b₁ being Group
for b₂, b₃ being Element of b₁ holds
( b₂,b₃ are_conjugated iff ex b₄ being Element of b₁ st b₃ = b₂ |^ b₄ )

proof end;

theorem Th89: :: GROUP_3:89

for b₁ being Group
for b₂ being Element of b₁ holds b₂,b₂ are_conjugated

proof end;

theorem Th90: :: GROUP_3:90

for b₁ being Group
for b₂, b₃ being Element of b₁ st b₂,b₃ are_conjugated holds
b₃,b₂ are_conjugated

proof end;

definition

let c₁ be Group;
let c₂, c₃ be Element of c₁;
redefine pred are_conjugated as c₂,c₃ are_conjugated ;
reflexivity by Th89;
symmetry by Th90;

end;

theorem Th91: :: GROUP_3:91

for b₁ being Group
for b₂, b₃, b₄ being Element of b₁ st b₂,b₃ are_conjugated & b₃,b₄ are_conjugated holds
b₂,b₄ are_conjugated

proof end;

theorem Th92: :: GROUP_3:92

for b₁ being Group
for b₂ being Element of b₁ st ( b₂, 1. b₁ are_conjugated or 1. b₁,b₂ are_conjugated ) holds
b₂ = 1. b₁

proof end;

theorem Th93: :: GROUP_3:93

for b₁ being Group
for b₂ being Element of b₁ holds b₂ |^ (carr ((Omega). b₁)) = { b₃ where B is Element of b₁ : b₂,b₃ are_conjugated }

proof end;

definition

let c₁ be Group;
let c₂ be Element of c₁;
func con_class c₂ -> Subset of a₁ equals :: GROUP_3:def 8
a₂ |^ (carr ((Omega). a₁));
correctness ;

end;

:: deftheorem Def8 defines con_class GROUP_3:def 8 :

theorem Th94: :: GROUP_3:94

canceled;

theorem Th95: :: GROUP_3:95

for b₁ being set
for b₂ being Group
for b₃ being Element of b₂ holds
( b₁ in con_class b₃ iff ex b₄ being Element of b₂ st
( b₄ = b₁ & b₃,b₄ are_conjugated ) )

proof end;

theorem Th96: :: GROUP_3:96

for b₁ being Group
for b₂, b₃ being Element of b₁ holds
( b₂ in con_class b₃ iff b₂,b₃ are_conjugated )

proof end;

theorem Th97: :: GROUP_3:97

for b₁ being Group
for b₂, b₃ being Element of b₁ holds b₂ |^ b₃ in con_class b₂

proof end;

theorem Th98: :: GROUP_3:98

for b₁ being Group
for b₂ being Element of b₁ holds b₂ in con_class b₂ by Th96;

theorem Th99: :: GROUP_3:99

for b₁ being Group
for b₂, b₃ being Element of b₁ st b₂ in con_class b₃ holds
b₃ in con_class b₂

proof end;

theorem Th100: :: GROUP_3:100

for b₁ being Group
for b₂, b₃ being Element of b₁ holds
( con_class b₂ = con_class b₃ iff con_class b₂ meets con_class b₃ )

proof end;

theorem Th101: :: GROUP_3:101

for b₁ being Group
for b₂ being Element of b₁ holds
( con_class b₂ = {(1. b₁)} iff b₂ = 1. b₁ )

proof end;

theorem Th102: :: GROUP_3:102

for b₁ being Group
for b₂ being Element of b₁
for b₃ being Subset of b₁ holds (con_class b₂) * b₃ = b₃ * (con_class b₂)

proof end;

definition

let c₁ be Group;
let c₂, c₃ be Subset of c₁;
pred c₂,c₃ are_conjugated means :Def9: :: GROUP_3:def 9
ex b₁ being Element of a₁ st a₂ = a₃ |^ b₁;

end;

:: deftheorem Def9 defines are_conjugated GROUP_3:def 9 :

notation

let c₁ be Group;
let c₂, c₃ be Subset of c₁;
antonym c₂,c₃ are_not_conjugated for c₂,c₃ are_conjugated ;

end;

theorem Th103: :: GROUP_3:103

canceled;

theorem Th104: :: GROUP_3:104

for b₁ being Group
for b₂, b₃ being Subset of b₁ holds
( b₂,b₃ are_conjugated iff ex b₄ being Element of b₁ st b₃ = b₂ |^ b₄ )

proof end;

theorem Th105: :: GROUP_3:105

for b₁ being Group
for b₂ being Subset of b₁ holds b₂,b₂ are_conjugated

proof end;

theorem Th106: :: GROUP_3:106

for b₁ being Group
for b₂, b₃ being Subset of b₁ st b₂,b₃ are_conjugated holds
b₃,b₂ are_conjugated

proof end;

definition

let c₁ be Group;
let c₂, c₃ be Subset of c₁;
redefine pred are_conjugated as c₂,c₃ are_conjugated ;
reflexivity by Th105;
symmetry by Th106;

end;

theorem Th107: :: GROUP_3:107

for b₁ being Group
for b₂, b₃, b₄ being Subset of b₁ st b₂,b₃ are_conjugated & b₃,b₄ are_conjugated holds
b₂,b₄ are_conjugated

proof end;

theorem Th108: :: GROUP_3:108

for b₁ being Group
for b₂, b₃ being Element of b₁ holds
( {b₂},{b₃} are_conjugated iff b₂,b₃ are_conjugated )

proof end;

theorem Th109: :: GROUP_3:109

for b₁ being Group
for b₂ being Subset of b₁
for b₃ being Subgroup of b₁ st b₂, carr b₃ are_conjugated holds
ex b₄ being strict Subgroup of b₁ st the carrier of b₄ = b₂

proof end;

definition

let c₁ be Group;
let c₂ be Subset of c₁;
func con_class c₂ -> Subset-Family of a₁ equals :: GROUP_3:def 10
{ b₁ where B is Subset of a₁ : a₂,b₁ are_conjugated } ;
coherence

proof end;

end;

:: deftheorem Def10 defines con_class GROUP_3:def 10 :

theorem Th110: :: GROUP_3:110

canceled;

theorem Th111: :: GROUP_3:111

for b₁ being set
for b₂ being Group
for b₃ being Subset of b₂ holds
( b₁ in con_class b₃ iff ex b₄ being Subset of b₂ st
( b₁ = b₄ & b₃,b₄ are_conjugated ) ) ;

theorem Th112: :: GROUP_3:112

canceled;

theorem Th113: :: GROUP_3:113

for b₁ being Group
for b₂, b₃ being Subset of b₁ holds
( b₂ in con_class b₃ iff b₂,b₃ are_conjugated )

proof end;

theorem Th114: :: GROUP_3:114

for b₁ being Group
for b₂ being Element of b₁
for b₃ being Subset of b₁ holds b₃ |^ b₂ in con_class b₃

proof end;

theorem Th115: :: GROUP_3:115

for b₁ being Group
for b₂ being Subset of b₁ holds b₂ in con_class b₂ ;

theorem Th116: :: GROUP_3:116

for b₁ being Group
for b₂, b₃ being Subset of b₁ st b₂ in con_class b₃ holds
b₃ in con_class b₂

proof end;

theorem Th117: :: GROUP_3:117

for b₁ being Group
for b₂, b₃ being Subset of b₁ holds
( con_class b₂ = con_class b₃ iff con_class b₂ meets con_class b₃ )

proof end;

theorem Th118: :: GROUP_3:118

for b₁ being Group
for b₂ being Element of b₁ holds con_class {b₂} = { {b₃} where B is Element of b₁ : b₃ in con_class b₂ }

proof end;

theorem Th119: :: GROUP_3:119

for b₁ being Group
for b₂ being Subset of b₁ st b₁ is finite holds
con_class b₂ is finite

proof end;

definition

let c₁ be Group;
let c₂, c₃ be Subgroup of c₁;
pred c₂,c₃ are_conjugated means :Def11: :: GROUP_3:def 11
ex b₁ being Element of a₁ st HGrStr(# the carrier of a₂,the mult of a₂ #) = a₃ |^ b₁;

end;

:: deftheorem Def11 defines are_conjugated GROUP_3:def 11 :

notation

let c₁ be Group;
let c₂, c₃ be Subgroup of c₁;
antonym c₂,c₃ are_not_conjugated for c₂,c₃ are_conjugated ;

end;

theorem Th120: :: GROUP_3:120

canceled;

theorem Th121: :: GROUP_3:121

for b₁ being Group
for b₂, b₃ being strict Subgroup of b₁ holds
( b₂,b₃ are_conjugated iff ex b₄ being Element of b₁ st b₃ = b₂ |^ b₄ )

proof end;

theorem Th122: :: GROUP_3:122

for b₁ being Group
for b₂ being strict Subgroup of b₁ holds b₂,b₂ are_conjugated

proof end;

theorem Th123: :: GROUP_3:123

for b₁ being Group
for b₂, b₃ being strict Subgroup of b₁ st b₂,b₃ are_conjugated holds
b₃,b₂ are_conjugated

proof end;

definition

let c₁ be Group;
let c₂, c₃ be strict Subgroup of c₁;
redefine pred are_conjugated as c₂,c₃ are_conjugated ;
reflexivity by Th122;
symmetry by Th123;

end;

theorem Th124: :: GROUP_3:124

for b₁ being Group
for b₂ being Subgroup of b₁
for b₃, b₄ being strict Subgroup of b₁ st b₃,b₄ are_conjugated & b₄,b₂ are_conjugated holds
b₃,b₂ are_conjugated

proof end;

definition

let c₁ be Group;
let c₂ be Subgroup of c₁;
func con_class c₂ -> Subset of (Subgroups a₁) means :Def12: :: GROUP_3:def 12
for b₁ being set holds
( b₁ in a₃ iff ex b₂ being strict Subgroup of a₁ st
( b₁ = b₂ & a₂,b₂ are_conjugated ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def12 defines con_class GROUP_3:def 12 :

theorem Th125: :: GROUP_3:125

canceled;

theorem Th126: :: GROUP_3:126

canceled;

theorem Th127: :: GROUP_3:127

for b₁ being set
for b₂ being Group
for b₃ being Subgroup of b₂ st b₁ in con_class b₃ holds
b₁ is strict Subgroup of b₂

proof end;

theorem Th128: :: GROUP_3:128

for b₁ being Group
for b₂, b₃ being strict Subgroup of b₁ holds
( b₂ in con_class b₃ iff b₂,b₃ are_conjugated )

proof end;

theorem Th129: :: GROUP_3:129

for b₁ being Group
for b₂ being Element of b₁
for b₃ being strict Subgroup of b₁ holds b₃ |^ b₂ in con_class b₃

proof end;

theorem Th130: :: GROUP_3:130

for b₁ being Group
for b₂ being strict Subgroup of b₁ holds b₂ in con_class b₂

proof end;

theorem Th131: :: GROUP_3:131

for b₁ being Group
for b₂, b₃ being strict Subgroup of b₁ st b₂ in con_class b₃ holds
b₃ in con_class b₂

proof end;

theorem Th132: :: GROUP_3:132

for b₁ being Group
for b₂, b₃ being strict Subgroup of b₁ holds
( con_class b₂ = con_class b₃ iff con_class b₂ meets con_class b₃ )

proof end;

theorem Th133: :: GROUP_3:133

for b₁ being Group
for b₂ being Subgroup of b₁ st b₁ is finite holds
con_class b₂ is finite

proof end;

theorem Th134: :: GROUP_3:134

for b₁ being Group
for b₂ being Subgroup of b₁
for b₃ being strict Subgroup of b₁ holds
( b₃,b₂ are_conjugated iff carr b₃, carr b₂ are_conjugated )

proof end;

definition

let c₁ be Group;
let c₂ be Subgroup of c₁;
attr a₂ is normal means :Def13: :: GROUP_3:def 13
for b₁ being Element of a₁ holds a₂ |^ b₁ = HGrStr(# the carrier of a₂,the mult of a₂ #);

end;

:: deftheorem Def13 defines normal GROUP_3:def 13 :

registration

let c₁ be Group;
cluster strict normal Subgroup of a₁;
existence

proof end;

end;

theorem Th135: :: GROUP_3:135

canceled;

theorem Th136: :: GROUP_3:136

canceled;

theorem Th137: :: GROUP_3:137

for b₁ being Group holds
( (1). b₁ is normal & (Omega). b₁ is normal )

proof end;

theorem Th138: :: GROUP_3:138

for b₁ being Group
for b₂, b₃ being strict normal Subgroup of b₁ holds b₂ /\ b₃ is normal

proof end;

theorem Th139: :: GROUP_3:139

for b₁ being Group
for b₂ being strict Subgroup of b₁ st b₁ is commutative Group holds
b₂ is normal

proof end;

theorem Th140: :: GROUP_3:140

for b₁ being Group
for b₂ being Subgroup of b₁ holds
( b₂ is normal Subgroup of b₁ iff for b₃ being Element of b₁ holds b₃ * b₂ = b₂ * b₃ )

proof end;

theorem Th141: :: GROUP_3:141

for b₁ being Group
for b₂ being Subgroup of b₁ holds
( b₂ is normal Subgroup of b₁ iff for b₃ being Element of b₁ holds b₃ * b₂ c= b₂ * b₃ )

proof end;

theorem Th142: :: GROUP_3:142

for b₁ being Group
for b₂ being Subgroup of b₁ holds
( b₂ is normal Subgroup of b₁ iff for b₃ being Element of b₁ holds b₂ * b₃ c= b₃ * b₂ )

proof end;

theorem Th143: :: GROUP_3:143

for b₁ being Group
for b₂ being Subgroup of b₁ holds
( b₂ is normal Subgroup of b₁ iff for b₃ being Subset of b₁ holds b₃ * b₂ = b₂ * b₃ )

proof end;

theorem Th144: :: GROUP_3:144

for b₁ being Group
for b₂ being strict Subgroup of b₁ holds
( b₂ is normal Subgroup of b₁ iff for b₃ being Element of b₁ holds b₂ is Subgroup of b₂ |^ b₃ )

proof end;

theorem Th145: :: GROUP_3:145

for b₁ being Group
for b₂ being strict Subgroup of b₁ holds
( b₂ is normal Subgroup of b₁ iff for b₃ being Element of b₁ holds b₂ |^ b₃ is Subgroup of b₂ )

proof end;

theorem Th146: :: GROUP_3:146

for b₁ being Group
for b₂ being strict Subgroup of b₁ holds
( b₂ is normal Subgroup of b₁ iff con_class b₂ = {b₂} )

proof end;

theorem Th147: :: GROUP_3:147

for b₁ being Group
for b₂ being strict Subgroup of b₁ holds
( b₂ is normal Subgroup of b₁ iff for b₃ being Element of b₁ st b₃ in b₂ holds
con_class b₃ c= carr b₂ )

proof end;

Lemma90: for b₁ being Group
for b₂ being normal Subgroup of b₁
for b₃ being strict normal Subgroup of b₁ holds (carr b₃) * (carr b₂) c= (carr b₂) * (carr b₃)

proof end;

theorem Th148: :: GROUP_3:148

for b₁ being Group
for b₂, b₃ being strict normal Subgroup of b₁ holds (carr b₂) * (carr b₃) = (carr b₃) * (carr b₂)

proof end;

theorem Th149: :: GROUP_3:149

for b₁ being Group
for b₂, b₃ being strict normal Subgroup of b₁ ex b₄ being strict normal Subgroup of b₁ st the carrier of b₄ = (carr b₂) * (carr b₃)

proof end;

theorem Th150: :: GROUP_3:150

for b₁ being Group
for b₂ being normal Subgroup of b₁ holds Left_Cosets b₂ = Right_Cosets b₂

proof end;

theorem Th151: :: GROUP_3:151

for b₁ being Group
for b₂ being Subgroup of b₁ st Left_Cosets b₂ is finite & index b₂ = 2 holds
b₂ is normal Subgroup of b₁

proof end;

definition

let c₁ be Group;
let c₂ be Subset of c₁;
func Normalizator c₂ -> strict Subgroup of a₁ means :Def14: :: GROUP_3:def 14
the carrier of a₃ = { b₁ where B is Element of a₁ : a₂ |^ b₁ = a₂ } ;
existence

proof end;

uniqueness by GROUP_2:68;

end;

:: deftheorem Def14 defines Normalizator GROUP_3:def 14 :

theorem Th152: :: GROUP_3:152

canceled;

theorem Th153: :: GROUP_3:153

canceled;

theorem Th154: :: GROUP_3:154

for b₁ being set
for b₂ being Group
for b₃ being Subset of b₂ holds
( b₁ in Normalizator b₃ iff ex b₄ being Element of b₂ st
( b₁ = b₄ & b₃ |^ b₄ = b₃ ) )

proof end;

theorem Th155: :: GROUP_3:155

for b₁ being Group
for b₂ being Subset of b₁ holds Card (con_class b₂) = Index (Normalizator b₂)

proof end;

theorem Th156: :: GROUP_3:156

for b₁ being Group
for b₂ being Subset of b₁ st ( con_class b₂ is finite or Left_Cosets (Normalizator b₂) is finite ) holds
ex b₃ being finite set st
( b₃ = con_class b₂ & card b₃ = index (Normalizator b₂) )

proof end;

theorem Th157: :: GROUP_3:157

for b₁ being Group
for b₂ being Element of b₁ holds Card (con_class b₂) = Index (Normalizator {b₂})

proof end;

theorem Th158: :: GROUP_3:158

for b₁ being Group
for b₂ being Element of b₁ st ( con_class b₂ is finite or Left_Cosets (Normalizator {b₂}) is finite ) holds
ex b₃ being finite set st
( b₃ = con_class b₂ & card b₃ = index (Normalizator {b₂}) )

proof end;

definition

let c₁ be Group;
let c₂ be Subgroup of c₁;
func Normalizator c₂ -> strict Subgroup of a₁ equals :: GROUP_3:def 15
Normalizator (carr a₂);
correctness ;

end;

:: deftheorem Def15 defines Normalizator GROUP_3:def 15 :

theorem Th159: :: GROUP_3:159

canceled;

theorem Th160: :: GROUP_3:160

for b₁ being set
for b₂ being Group
for b₃ being strict Subgroup of b₂ holds
( b₁ in Normalizator b₃ iff ex b₄ being Element of b₂ st
( b₁ = b₄ & b₃ |^ b₄ = b₃ ) )

proof end;

theorem Th161: :: GROUP_3:161

for b₁ being Group
for b₂ being strict Subgroup of b₁ holds Card (con_class b₂) = Index (Normalizator b₂)

proof end;

theorem Th162: :: GROUP_3:162

for b₁ being Group
for b₂ being strict Subgroup of b₁ st ( con_class b₂ is finite or Left_Cosets (Normalizator b₂) is finite ) holds
ex b₃ being finite set st
( b₃ = con_class b₂ & card b₃ = index (Normalizator b₂) )

proof end;

theorem Th163: :: GROUP_3:163

for b₁ being strict Group
for b₂ being strict Subgroup of b₁ holds
( b₂ is normal Subgroup of b₁ iff Normalizator b₂ = b₁ )

proof end;

theorem Th164: :: GROUP_3:164

for b₁ being strict Group holds Normalizator ((1). b₁) = b₁

proof end;

theorem Th165: :: GROUP_3:165

for b₁ being strict Group holds Normalizator ((Omega). b₁) = b₁

proof end;