:: GROUP_2 semantic presentation

Lemma1: for b₁ being set
for b₂ being non empty 1-sorted
for b₃ being Subset of b₂ st b₁ in b₃ holds
b₁ is Element of b₂
;

theorem Th1: :: GROUP_2:1

canceled;

theorem Th2: :: GROUP_2:2

canceled;

theorem Th3: :: GROUP_2:3

for b₁ being non empty 1-sorted
for b₂ being Subset of b₁ st b₁ is finite holds
b₂ is finite

proof end;

definition

let c₁ be Group;
let c₂ be Subset of c₁;
func c₂ " -> Subset of a₁ equals :: GROUP_2:def 1
{ (b₁ " ) where B is Element of a₁ : b₁ in a₂ } ;
coherence

proof end;

end;

:: deftheorem Def1 defines " GROUP_2:def 1 :

theorem Th4: :: GROUP_2:4

canceled;

theorem Th5: :: GROUP_2:5

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

theorem Th6: :: GROUP_2:6

for b₁ being Group
for b₂ being Element of b₁ holds {b₂} " = {(b₂ " )}

proof end;

theorem Th7: :: GROUP_2:7

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

proof end;

theorem Th8: :: GROUP_2:8

for b₁ being Group holds ({} the carrier of b₁) " = {}

proof end;

theorem Th9: :: GROUP_2:9

for b₁ being Group holds ([#] the carrier of b₁) " = the carrier of b₁

proof end;

theorem Th10: :: GROUP_2:10

for b₁ being Group
for b₂ being Subset of b₁ holds
( b₂ <> {} iff b₂ " <> {} )

proof end;

definition

let c₁ be non empty HGrStr ;
let c₂, c₃ be Subset of c₁;
func c₂ * c₃ -> Subset of a₁ equals :: GROUP_2:def 2
{ (b₁ * b₂) where B is Element of a₁, B is Element of a₁ : ( b₁ in a₂ & b₂ in a₃ ) } ;
coherence

proof end;

end;

:: deftheorem Def2 defines * GROUP_2:def 2 :

theorem Th11: :: GROUP_2:11

canceled;

theorem Th12: :: GROUP_2:12

for b₁ being set
for b₂ being non empty HGrStr
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 Th13: :: GROUP_2:13

for b₁ being non empty HGrStr
for b₂, b₃ being Subset of b₁ holds
( ( b₂ <> {} & b₃ <> {} ) iff b₂ * b₃ <> {} )

proof end;

theorem Th14: :: GROUP_2:14

for b₁ being non empty HGrStr
for b₂, b₃, b₄ being Subset of b₁ st b₁ is associative holds
(b₂ * b₃) * b₄ = b₂ * (b₃ * b₄)

proof end;

theorem Th15: :: GROUP_2:15

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

proof end;

theorem Th16: :: GROUP_2:16

for b₁ being non empty HGrStr
for b₂, b₃, b₄ being Subset of b₁ holds b₂ * (b₃ \/ b₄) = (b₂ * b₃) \/ (b₂ * b₄)

proof end;

theorem Th17: :: GROUP_2:17

for b₁ being non empty HGrStr
for b₂, b₃, b₄ being Subset of b₁ holds (b₂ \/ b₃) * b₄ = (b₂ * b₄) \/ (b₃ * b₄)

proof end;

theorem Th18: :: GROUP_2:18

for b₁ being non empty HGrStr
for b₂, b₃, b₄ being Subset of b₁ holds b₂ * (b₃ /\ b₄) c= (b₂ * b₃) /\ (b₂ * b₄)

proof end;

theorem Th19: :: GROUP_2:19

for b₁ being non empty HGrStr
for b₂, b₃, b₄ being Subset of b₁ holds (b₂ /\ b₃) * b₄ c= (b₂ * b₄) /\ (b₃ * b₄)

proof end;

theorem Th20: :: GROUP_2:20

for b₁ being non empty HGrStr
for b₂ being Subset of b₁ holds
( ({} the carrier of b₁) * b₂ = {} & b₂ * ({} the carrier of b₁) = {} )

proof end;

theorem Th21: :: GROUP_2:21

for b₁ being Group
for b₂ being Subset of b₁ st b₂ <> {} holds
( ([#] the carrier of b₁) * b₂ = the carrier of b₁ & b₂ * ([#] the carrier of b₁) = the carrier of b₁ )

proof end;

theorem Th22: :: GROUP_2:22

for b₁ being non empty HGrStr
for b₂, b₃ being Element of b₁ holds {b₂} * {b₃} = {(b₂ * b₃)}

proof end;

theorem Th23: :: GROUP_2:23

for b₁ being non empty HGrStr
for b₂, b₃, b₄ being Element of b₁ holds {b₂} * {b₃,b₄} = {(b₂ * b₃),(b₂ * b₄)}

proof end;

theorem Th24: :: GROUP_2:24

for b₁ being non empty HGrStr
for b₂, b₃, b₄ being Element of b₁ holds {b₂,b₃} * {b₄} = {(b₂ * b₄),(b₃ * b₄)}

proof end;

theorem Th25: :: GROUP_2:25

for b₁ being non empty HGrStr
for b₂, b₃, b₄, b₅ being Element of b₁ holds {b₂,b₃} * {b₄,b₅} = {(b₂ * b₄),(b₂ * b₅),(b₃ * b₄),(b₃ * b₅)}

proof end;

theorem Th26: :: GROUP_2:26

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

proof end;

theorem Th27: :: GROUP_2:27

for b₁ being Group
for b₂ being Subset of b₁ st ( for b₃ being Element of b₁ st b₃ in b₂ holds
b₃ " in b₂ ) holds
b₂ " = b₂

proof end;

theorem Th28: :: GROUP_2:28

for b₁ being non empty HGrStr
for b₂, b₃ being Subset of b₁ st ( for b₄, b₅ being Element of b₁ st b₄ in b₂ & b₅ in b₃ holds
b₄ * b₅ = b₅ * b₄ ) holds
b₂ * b₃ = b₃ * b₂

proof end;

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

theorem Th29: :: GROUP_2:29

for b₁ being non empty HGrStr
for b₂, b₃ being Subset of b₁ st b₁ is commutative Group holds
b₂ * b₃ = b₃ * b₂

proof end;

theorem Th30: :: GROUP_2:30

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

proof end;

definition

let c₁ be non empty HGrStr ;
let c₂ be Element of c₁;
let c₃ be Subset of c₁;
func c₂ * c₃ -> Subset of a₁ equals :: GROUP_2:def 3
{a₂} * a₃;
correctness ;
func c₃ * c₂ -> Subset of a₁ equals :: GROUP_2:def 4
a₃ * {a₂};
correctness ;

end;

:: deftheorem Def3 defines * GROUP_2:def 3 :

:: deftheorem Def4 defines * GROUP_2:def 4 :

theorem Th31: :: GROUP_2:31

canceled;

theorem Th32: :: GROUP_2:32

canceled;

theorem Th33: :: GROUP_2:33

for b₁ being set
for b₂ being non empty HGrStr
for b₃ being Subset of b₂
for b₄ being Element of b₂ holds
( b₁ in b₄ * b₃ iff ex b₅ being Element of b₂ st
( b₁ = b₄ * b₅ & b₅ in b₃ ) )

proof end;

theorem Th34: :: GROUP_2:34

for b₁ being set
for b₂ being non empty HGrStr
for b₃ being Subset of b₂
for b₄ being Element of b₂ holds
( b₁ in b₃ * b₄ iff ex b₅ being Element of b₂ st
( b₁ = b₅ * b₄ & b₅ in b₃ ) )

proof end;

theorem Th35: :: GROUP_2:35

for b₁ being non empty HGrStr
for b₂, b₃ being Subset of b₁
for b₄ being Element of b₁ st b₁ is associative holds
(b₄ * b₂) * b₃ = b₄ * (b₂ * b₃) by Th14;

theorem Th36: :: GROUP_2:36

for b₁ being non empty HGrStr
for b₂, b₃ being Subset of b₁
for b₄ being Element of b₁ st b₁ is associative holds
(b₂ * b₄) * b₃ = b₂ * (b₄ * b₃) by Th14;

theorem Th37: :: GROUP_2:37

for b₁ being non empty HGrStr
for b₂, b₃ being Subset of b₁
for b₄ being Element of b₁ st b₁ is associative holds
(b₂ * b₃) * b₄ = b₂ * (b₃ * b₄) by Th14;

theorem Th38: :: GROUP_2:38

for b₁ being non empty HGrStr
for b₂ being Subset of b₁
for b₃, b₄ being Element of b₁ st b₁ is associative holds
(b₃ * b₄) * b₂ = b₃ * (b₄ * b₂)

proof end;

theorem Th39: :: GROUP_2:39

for b₁ being non empty HGrStr
for b₂ being Subset of b₁
for b₃, b₄ being Element of b₁ st b₁ is associative holds
(b₃ * b₂) * b₄ = b₃ * (b₂ * b₄) by Th14;

theorem Th40: :: GROUP_2:40

for b₁ being non empty HGrStr
for b₂ being Subset of b₁
for b₃, b₄ being Element of b₁ st b₁ is associative holds
(b₂ * b₃) * b₄ = b₂ * (b₃ * b₄)

proof end;

theorem Th41: :: GROUP_2:41

for b₁ being non empty HGrStr
for b₂ being Element of b₁ holds
( ({} the carrier of b₁) * b₂ = {} & b₂ * ({} the carrier of b₁) = {} ) by Th20;

theorem Th42: :: GROUP_2:42

for b₁ being Group
for b₂ being Element of b₁ holds
( ([#] the carrier of b₁) * b₂ = the carrier of b₁ & b₂ * ([#] the carrier of b₁) = the carrier of b₁ ) by Th21;

theorem Th43: :: GROUP_2:43

for b₁ being non empty Group-like HGrStr
for b₂ being Subset of b₁ holds
( (1. b₁) * b₂ = b₂ & b₂ * (1. b₁) = b₂ )

proof end;

theorem Th44: :: GROUP_2:44

for b₁ being non empty Group-like HGrStr
for b₂ being Element of b₁
for b₃ being Subset of b₁ st b₁ is commutative Group holds
b₂ * b₃ = b₃ * b₂ by Th29;

definition

let c₁ be non empty Group-like HGrStr ;
mode Subgroup of c₁ -> non empty Group-like HGrStr means :Def5: :: GROUP_2:def 5
( the carrier of a₂ c= the carrier of a₁ & the mult of a₂ = the mult of a₁ || the carrier of a₂ );
existence

proof end;

end;

:: deftheorem Def5 defines Subgroup GROUP_2:def 5 :

theorem Th45: :: GROUP_2:45

canceled;

theorem Th46: :: GROUP_2:46

canceled;

theorem Th47: :: GROUP_2:47

canceled;

theorem Th48: :: GROUP_2:48

for b₁ being non empty Group-like HGrStr
for b₂ being Subgroup of b₁ st b₁ is finite holds
b₂ is finite

proof end;

theorem Th49: :: GROUP_2:49

for b₁ being set
for b₂ being non empty Group-like HGrStr
for b₃ being Subgroup of b₂ st b₁ in b₃ holds
b₁ in b₂

proof end;

theorem Th50: :: GROUP_2:50

for b₁ being non empty Group-like HGrStr
for b₂ being Subgroup of b₁
for b₃ being Element of b₂ holds b₃ in b₁

proof end;

theorem Th51: :: GROUP_2:51

for b₁ being non empty Group-like HGrStr
for b₂ being Subgroup of b₁
for b₃ being Element of b₂ holds b₃ is Element of b₁

proof end;

theorem Th52: :: GROUP_2:52

for b₁ being non empty Group-like HGrStr
for b₂, b₃ being Element of b₁
for b₄ being Subgroup of b₁
for b₅, b₆ being Element of b₄ st b₅ = b₂ & b₆ = b₃ holds
b₅ * b₆ = b₂ * b₃

proof end;

registration

let c₁ be Group;
cluster -> associative Subgroup of a₁;
coherence

proof end;

end;

theorem Th53: :: GROUP_2:53

for b₁ being Group
for b₂ being Subgroup of b₁ holds 1. b₂ = 1. b₁

proof end;

theorem Th54: :: GROUP_2:54

for b₁ being Group
for b₂, b₃ being Subgroup of b₁ holds 1. b₂ = 1. b₃

proof end;

theorem Th55: :: GROUP_2:55

for b₁ being Group
for b₂ being Subgroup of b₁ holds 1. b₁ in b₂

proof end;

theorem Th56: :: GROUP_2:56

for b₁ being Group
for b₂, b₃ being Subgroup of b₁ holds 1. b₂ in b₃

proof end;

theorem Th57: :: GROUP_2:57

for b₁ being Group
for b₂ being Element of b₁
for b₃ being Subgroup of b₁
for b₄ being Element of b₃ st b₄ = b₂ holds
b₄ " = b₂ "

proof end;

theorem Th58: :: GROUP_2:58

for b₁ being Group
for b₂ being Subgroup of b₁ holds inverse_op b₂ = (inverse_op b₁) | the carrier of b₂

proof end;

theorem Th59: :: GROUP_2:59

for b₁ being Group
for b₂, b₃ being Element of b₁
for b₄ being Subgroup of b₁ st b₂ in b₄ & b₃ in b₄ holds
b₂ * b₃ in b₄

proof end;

theorem Th60: :: GROUP_2:60

for b₁ being Group
for b₂ being Element of b₁
for b₃ being Subgroup of b₁ st b₂ in b₃ holds
b₂ " in b₃

proof end;

registration

let c₁ be Group;
cluster non empty strict Group-like associative Subgroup of a₁;
existence

proof end;

end;

theorem Th61: :: GROUP_2:61

for b₁ being Group
for b₂ being Subset of b₁ st b₂ <> {} & ( for b₃, b₄ being Element of b₁ st b₃ in b₂ & b₄ in b₂ holds
b₃ * b₄ in b₂ ) & ( for b₃ being Element of b₁ st b₃ in b₂ holds
b₃ " in b₂ ) holds
ex b₃ being strict Subgroup of b₁ st the carrier of b₃ = b₂

proof end;

theorem Th62: :: GROUP_2:62

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

proof end;

registration

let c₁ be commutative Group;
cluster -> associative commutative Subgroup of a₁;
coherence by Th62;

end;

theorem Th63: :: GROUP_2:63

for b₁ being Group holds b₁ is Subgroup of b₁

proof end;

theorem Th64: :: GROUP_2:64

for b₁, b₂ being Group st b₁ is Subgroup of b₂ & b₂ is Subgroup of b₁ holds
HGrStr(# the carrier of b₁,the mult of b₁ #) = HGrStr(# the carrier of b₂,the mult of b₂ #)

proof end;

theorem Th65: :: GROUP_2:65

for b₁, b₂, b₃ being Group st b₁ is Subgroup of b₂ & b₂ is Subgroup of b₃ holds
b₁ is Subgroup of b₃

proof end;

theorem Th66: :: GROUP_2:66

for b₁ being Group
for b₂, b₃ being Subgroup of b₁ st the carrier of b₂ c= the carrier of b₃ holds
b₂ is Subgroup of b₃

proof end;

theorem Th67: :: GROUP_2:67

for b₁ being Group
for b₂, b₃ being Subgroup of b₁ st ( for b₄ being Element of b₁ st b₄ in b₂ holds
b₄ in b₃ ) holds
b₂ is Subgroup of b₃

proof end;

theorem Th68: :: GROUP_2:68

for b₁ being Group
for b₂, b₃ being Subgroup of b₁ st the carrier of b₂ = the carrier of b₃ holds
HGrStr(# the carrier of b₂,the mult of b₂ #) = HGrStr(# the carrier of b₃,the mult of b₃ #)

proof end;

theorem Th69: :: GROUP_2:69

for b₁ being Group
for b₂, b₃ being Subgroup of b₁ st ( for b₄ being Element of b₁ holds
( b₄ in b₂ iff b₄ in b₃ ) ) holds
HGrStr(# the carrier of b₂,the mult of b₂ #) = HGrStr(# the carrier of b₃,the mult of b₃ #)

proof end;

definition

let c₁ be Group;
let c₂, c₃ be strict Subgroup of c₁;
redefine pred = as c₂ = c₃ means :: GROUP_2:def 6
for b₁ being Element of a₁ holds
( b₁ in a₂ iff b₁ in a₃ );
compatibility by Th69;

end;

:: deftheorem Def6 defines = GROUP_2:def 6 :

theorem Th70: :: GROUP_2:70

for b₁ being strict Group
for b₂ being strict Subgroup of b₁ st the carrier of b₂ = the carrier of b₁ holds
b₂ = b₁

proof end;

theorem Th71: :: GROUP_2:71

for b₁ being Group
for b₂ being Subgroup of b₁ st ( for b₃ being Element of b₁ holds b₃ in b₂ ) holds
HGrStr(# the carrier of b₂,the mult of b₂ #) = HGrStr(# the carrier of b₁,the mult of b₁ #)

proof end;

definition

let c₁ be Group;
func (1). c₁ -> strict Subgroup of a₁ means :Def7: :: GROUP_2:def 7
the carrier of a₂ = {(1. a₁)};
existence

proof end;

uniqueness by Th68;

end;

:: deftheorem Def7 defines (1). GROUP_2:def 7 :

definition

let c₁ be Group;
func (Omega). c₁ -> strict Subgroup of a₁ equals :: GROUP_2:def 8
HGrStr(# the carrier of a₁,the mult of a₁ #);
coherence

proof end;

end;

:: deftheorem Def8 defines (Omega). GROUP_2:def 8 :

theorem Th72: :: GROUP_2:72

canceled;

theorem Th73: :: GROUP_2:73

canceled;

theorem Th74: :: GROUP_2:74

canceled;

theorem Th75: :: GROUP_2:75

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

proof end;

theorem Th76: :: GROUP_2:76

for b₁ being Group
for b₂, b₃ being Subgroup of b₁ holds (1). b₂ = (1). b₃

proof end;

theorem Th77: :: GROUP_2:77

for b₁ being Group
for b₂ being Subgroup of b₁ holds (1). b₁ is Subgroup of b₂

proof end;

theorem Th78: :: GROUP_2:78

for b₁ being strict Group
for b₂ being Subgroup of b₁ holds b₂ is Subgroup of (Omega). b₁ ;

theorem Th79: :: GROUP_2:79

for b₁ being strict Group holds b₁ is Subgroup of (Omega). b₁ ;

theorem Th80: :: GROUP_2:80

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

proof end;

theorem Th81: :: GROUP_2:81

for b₁ being Group holds ord ((1). b₁) = 1

proof end;

theorem Th82: :: GROUP_2:82

for b₁ being Group
for b₂ being strict Subgroup of b₁ st b₂ is finite & ord b₂ = 1 holds
b₂ = (1). b₁

proof end;

theorem Th83: :: GROUP_2:83

for b₁ being Group
for b₂ being Subgroup of b₁ holds Ord b₂ <=` Ord b₁

proof end;

theorem Th84: :: GROUP_2:84

for b₁ being Group
for b₂ being Subgroup of b₁ st b₁ is finite holds
ord b₂ <= ord b₁

proof end;

theorem Th85: :: GROUP_2:85

for b₁ being strict Group
for b₂ being strict Subgroup of b₁ st b₁ is finite & ord b₁ = ord b₂ holds
b₂ = b₁

proof end;

definition

let c₁ be Group;
let c₂ be Subgroup of c₁;
func carr c₂ -> Subset of a₁ equals :: GROUP_2:def 9
the carrier of a₂;
coherence by Def5;

end;

:: deftheorem Def9 defines carr GROUP_2:def 9 :

theorem Th86: :: GROUP_2:86

canceled;

theorem Th87: :: GROUP_2:87

for b₁ being Group
for b₂ being Subgroup of b₁ holds carr b₂ <> {} ;

theorem Th88: :: GROUP_2:88

for b₁ being set
for b₂ being Group
for b₃ being Subgroup of b₂ holds
( b₁ in carr b₃ iff b₁ in b₃ ) by RLVECT_1:def 1;

theorem Th89: :: GROUP_2:89

for b₁ being Group
for b₂, b₃ being Element of b₁
for b₄ being Subgroup of b₁ st b₂ in carr b₄ & b₃ in carr b₄ holds
b₂ * b₃ in carr b₄

proof end;

theorem Th90: :: GROUP_2:90

for b₁ being Group
for b₂ being Element of b₁
for b₃ being Subgroup of b₁ st b₂ in carr b₃ holds
b₂ " in carr b₃

proof end;

theorem Th91: :: GROUP_2:91

for b₁ being Group
for b₂ being Subgroup of b₁ holds (carr b₂) * (carr b₂) = carr b₂

proof end;

theorem Th92: :: GROUP_2:92

for b₁ being Group
for b₂ being Subgroup of b₁ holds (carr b₂) " = carr b₂

proof end;

theorem Th93: :: GROUP_2:93

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

proof end;

theorem Th94: :: GROUP_2:94

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

proof end;

definition

let c₁ be Group;
let c₂, c₃ be Subgroup of c₁;
func c₂ /\ c₃ -> strict Subgroup of a₁ means :Def10: :: GROUP_2:def 10
the carrier of a₄ = (carr a₂) /\ (carr a₃);
existence

proof end;

uniqueness by Th68;

end;

:: deftheorem Def10 defines /\ GROUP_2:def 10 :

theorem Th95: :: GROUP_2:95

canceled;

theorem Th96: :: GROUP_2:96

canceled;

theorem Th97: :: GROUP_2:97

for b₁ being Group
for b₂, b₃ being Subgroup of b₁ holds
( ( for b₄ being Subgroup of b₁ st b₄ = b₂ /\ b₃ holds
the carrier of b₄ = the carrier of b₂ /\ the carrier of b₃ ) & ( for b₄ being strict Subgroup of b₁ st the carrier of b₄ = the carrier of b₂ /\ the carrier of b₃ holds
b₄ = b₂ /\ b₃ ) )

proof end;

theorem Th98: :: GROUP_2:98

for b₁ being Group
for b₂, b₃ being Subgroup of b₁ holds carr (b₂ /\ b₃) = (carr b₂) /\ (carr b₃) by Def10;

theorem Th99: :: GROUP_2:99

for b₁ being set
for b₂ being Group
for b₃, b₄ being Subgroup of b₂ holds
( b₁ in b₃ /\ b₄ iff ( b₁ in b₃ & b₁ in b₄ ) )

proof end;

theorem Th100: :: GROUP_2:100

for b₁ being Group
for b₂ being strict Subgroup of b₁ holds b₂ /\ b₂ = b₂

proof end;

theorem Th101: :: GROUP_2:101

for b₁ being Group
for b₂, b₃ being Subgroup of b₁ holds b₂ /\ b₃ = b₃ /\ b₂

proof end;

definition

let c₁ be Group;
let c₂, c₃ be Subgroup of c₁;
redefine func /\ as c₂ /\ c₃ -> strict Subgroup of a₁;
commutativity by Th101;

end;

theorem Th102: :: GROUP_2:102

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

proof end;

Lemma59: for b₁ being Group
for b₂ being Subgroup of b₁
for b₃ being strict Subgroup of b₁ holds
( b₃ is Subgroup of b₂ iff b₃ /\ b₂ = b₃ )

proof end;

theorem Th103: :: GROUP_2:103

for b₁ being Group
for b₂ being Subgroup of b₁ holds
( ((1). b₁) /\ b₂ = (1). b₁ & b₂ /\ ((1). b₁) = (1). b₁ )

proof end;

theorem Th104: :: GROUP_2:104

for b₁ being strict Group
for b₂ being strict Subgroup of b₁ holds
( b₂ /\ ((Omega). b₁) = b₂ & ((Omega). b₁) /\ b₂ = b₂ ) by Lemma59;

theorem Th105: :: GROUP_2:105

for b₁ being strict Group holds ((Omega). b₁) /\ ((Omega). b₁) = b₁ by Th104;

Lemma61: for b₁ being Group
for b₂, b₃ being Subgroup of b₁ holds b₂ /\ b₃ is Subgroup of b₂

proof end;

theorem Th106: :: GROUP_2:106

for b₁ being Group
for b₂, b₃ being Subgroup of b₁ holds
( b₂ /\ b₃ is Subgroup of b₂ & b₂ /\ b₃ is Subgroup of b₃ ) by Lemma61;

theorem Th107: :: GROUP_2:107

for b₁ being Group
for b₂ being Subgroup of b₁
for b₃ being strict Subgroup of b₁ holds
( b₃ is Subgroup of b₂ iff b₃ /\ b₂ = b₃ ) by Lemma59;

theorem Th108: :: GROUP_2:108

for b₁ being Group
for b₂, b₃, b₄ being Subgroup of b₁ st b₂ is Subgroup of b₃ holds
b₂ /\ b₄ is Subgroup of b₃

proof end;

theorem Th109: :: GROUP_2:109

for b₁ being Group
for b₂, b₃, b₄ being Subgroup of b₁ st b₂ is Subgroup of b₃ & b₂ is Subgroup of b₄ holds
b₂ is Subgroup of b₃ /\ b₄

proof end;

theorem Th110: :: GROUP_2:110

for b₁ being Group
for b₂, b₃, b₄ being Subgroup of b₁ st b₂ is Subgroup of b₃ holds
b₂ /\ b₄ is Subgroup of b₃ /\ b₄

proof end;

theorem Th111: :: GROUP_2:111

for b₁ being Group
for b₂, b₃ being Subgroup of b₁ st ( b₂ is finite or b₃ is finite ) holds
b₂ /\ b₃ is finite

proof end;

definition

let c₁ be Group;
let c₂ be Subgroup of c₁;
let c₃ be Subset of c₁;
func c₃ * c₂ -> Subset of a₁ equals :: GROUP_2:def 11
a₃ * (carr a₂);
correctness ;
func c₂ * c₃ -> Subset of a₁ equals :: GROUP_2:def 12
(carr a₂) * a₃;
correctness ;

end;

:: deftheorem Def11 defines * GROUP_2:def 11 :

:: deftheorem Def12 defines * GROUP_2:def 12 :

theorem Th112: :: GROUP_2:112

canceled;

theorem Th113: :: GROUP_2:113

canceled;

theorem Th114: :: GROUP_2:114

for b₁ being set
for b₂ being Group
for b₃ being Subset of b₂
for b₄ being Subgroup 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₄ ) )

proof end;

theorem Th115: :: GROUP_2:115

for b₁ being set
for b₂ being Group
for b₃ being Subset of b₂
for b₄ being Subgroup 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₃ ) )

proof end;

theorem Th116: :: GROUP_2:116

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

theorem Th117: :: GROUP_2:117

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

theorem Th118: :: GROUP_2:118

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

theorem Th119: :: GROUP_2:119

for b₁ being Group
for b₂ being Subset of b₁
for b₃, b₄ being Subgroup of b₁ holds (b₂ * b₃) * b₄ = b₂ * (b₃ * (carr b₄)) by Th14;

theorem Th120: :: GROUP_2:120

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

theorem Th121: :: GROUP_2:121

for b₁ being Group
for b₂ being Subset of b₁
for b₃, b₄ being Subgroup of b₁ holds (b₃ * (carr b₄)) * b₂ = b₃ * (b₄ * b₂) by Th118;

theorem Th122: :: GROUP_2:122

for b₁ being Group
for b₂ being Subset of b₁
for b₃ being Subgroup of b₁ st b₁ is commutative Group holds
b₂ * b₃ = b₃ * b₂ by Th29;

definition

let c₁ be Group;
let c₂ be Subgroup of c₁;
let c₃ be Element of c₁;
func c₃ * c₂ -> Subset of a₁ equals :: GROUP_2:def 13
a₃ * (carr a₂);
correctness ;
func c₂ * c₃ -> Subset of a₁ equals :: GROUP_2:def 14
(carr a₂) * a₃;
correctness ;

end;

:: deftheorem Def13 defines * GROUP_2:def 13 :

:: deftheorem Def14 defines * GROUP_2:def 14 :

theorem Th123: :: GROUP_2:123

canceled;

theorem Th124: :: GROUP_2:124

canceled;

theorem Th125: :: GROUP_2:125

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 Th126: :: GROUP_2:126

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 Th127: :: GROUP_2:127

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

theorem Th128: :: GROUP_2:128

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

theorem Th129: :: GROUP_2:129

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

theorem Th130: :: GROUP_2:130

for b₁ being Group
for b₂ being Element of b₁
for b₃ being Subgroup of b₁ holds
( b₂ in b₂ * b₃ & b₂ in b₃ * b₂ )

proof end;

theorem Th131: :: GROUP_2:131

canceled;

theorem Th132: :: GROUP_2:132

for b₁ being Group
for b₂ being Subgroup of b₁ holds
( (1. b₁) * b₂ = carr b₂ & b₂ * (1. b₁) = carr b₂ ) by Th43;

theorem Th133: :: GROUP_2:133

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

proof end;

theorem Th134: :: GROUP_2:134

for b₁ being Group
for b₂ being Element of b₁ holds
( b₂ * ((Omega). b₁) = the carrier of b₁ & ((Omega). b₁) * b₂ = the carrier of b₁ )

proof end;

theorem Th135: :: GROUP_2:135

for b₁ being Group
for b₂ being Element of b₁
for b₃ being Subgroup of b₁ st b₁ is commutative Group holds
b₂ * b₃ = b₃ * b₂ by Th44;

theorem Th136: :: GROUP_2:136

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

proof end;

theorem Th137: :: GROUP_2:137

for b₁ being Group
for b₂, b₃ being Element of b₁
for b₄ being Subgroup of b₁ holds
( b₂ * b₄ = b₃ * b₄ iff (b₃ " ) * b₂ in b₄ )

proof end;

theorem Th138: :: GROUP_2:138

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

proof end;

theorem Th139: :: GROUP_2:139

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

proof end;

theorem Th140: :: GROUP_2:140

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

proof end;

theorem Th141: :: GROUP_2:141

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

proof end;

theorem Th142: :: GROUP_2:142

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

proof end;

theorem Th143: :: GROUP_2:143

for b₁ being Group
for b₂, b₃ being Element of b₁
for b₄ being Subgroup of b₁ holds
( b₄ * b₂ = b₄ * b₃ iff b₃ * (b₂ " ) in b₄ )

proof end;

theorem Th144: :: GROUP_2:144

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

proof end;

theorem Th145: :: GROUP_2:145

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

proof end;

theorem Th146: :: GROUP_2:146

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

proof end;

theorem Th147: :: GROUP_2:147

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

proof end;

theorem Th148: :: GROUP_2:148

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 Th149: :: GROUP_2:149

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 Th150: :: GROUP_2:150

for b₁ being Group
for b₂ being Element of b₁
for b₃ being Subgroup of b₁ ex b₄ being strict Subgroup of b₁ st the carrier of b₄ = (b₂ * b₃) * (b₂ " )

proof end;

theorem Th151: :: GROUP_2:151

for b₁ being Group
for b₂, b₃ being Element of b₁
for b₄ being Subgroup of b₁ holds b₂ * b₄,b₃ * b₄ are_equipotent

proof end;

theorem Th152: :: GROUP_2:152

for b₁ being Group
for b₂, b₃ being Element of b₁
for b₄ being Subgroup of b₁ holds b₂ * b₄,b₄ * b₃ are_equipotent

proof end;

theorem Th153: :: GROUP_2:153

for b₁ being Group
for b₂, b₃ being Element of b₁
for b₄ being Subgroup of b₁ holds b₄ * b₂,b₄ * b₃ are_equipotent

proof end;

theorem Th154: :: GROUP_2:154

for b₁ being Group
for b₂ being Element of b₁
for b₃ being Subgroup of b₁ holds
( carr b₃,b₂ * b₃ are_equipotent & carr b₃,b₃ * b₂ are_equipotent )

proof end;

theorem Th155: :: GROUP_2:155

for b₁ being Group
for b₂ being Element of b₁
for b₃ being Subgroup of b₁ holds
( Ord b₃ = Card (b₂ * b₃) & Ord b₃ = Card (b₃ * b₂) )

proof end;

theorem Th156: :: GROUP_2:156

for b₁ being Group
for b₂ being Element of b₁
for b₃ being Subgroup of b₁ st b₃ is finite holds
ex b₄, b₅ being finite set st
( b₄ = b₂ * b₃ & b₅ = b₃ * b₂ & ord b₃ = card b₄ & ord b₃ = card b₅ )

proof end;

definition

let c₁ be Group;
let c₂ be Subgroup of c₁;
func Left_Cosets c₂ -> Subset-Family of a₁ means :Def15: :: GROUP_2:def 15
for b₁ being Subset of a₁ holds
( b₁ in a₃ iff ex b₂ being Element of a₁ st b₁ = b₂ * a₂ );
existence

proof end;

uniqueness

proof end;

func Right_Cosets c₂ -> Subset-Family of a₁ means :Def16: :: GROUP_2:def 16
for b₁ being Subset of a₁ holds
( b₁ in a₃ iff ex b₂ being Element of a₁ st b₁ = a₂ * b₂ );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def15 defines Left_Cosets GROUP_2:def 15 :

:: deftheorem Def16 defines Right_Cosets GROUP_2:def 16 :

theorem Th157: :: GROUP_2:157

canceled;

theorem Th158: :: GROUP_2:158

canceled;

theorem Th159: :: GROUP_2:159

canceled;

theorem Th160: :: GROUP_2:160

canceled;

theorem Th161: :: GROUP_2:161

canceled;

theorem Th162: :: GROUP_2:162

canceled;

theorem Th163: :: GROUP_2:163

canceled;

theorem Th164: :: GROUP_2:164

for b₁ being Group
for b₂ being Subgroup of b₁ st b₁ is finite holds
( Right_Cosets b₂ is finite & Left_Cosets b₂ is finite )

proof end;

theorem Th165: :: GROUP_2:165

for b₁ being Group
for b₂ being Subgroup of b₁ holds
( carr b₂ in Left_Cosets b₂ & carr b₂ in Right_Cosets b₂ )

proof end;

theorem Th166: :: GROUP_2:166

for b₁ being Group
for b₂ being Subgroup of b₁ holds Left_Cosets b₂, Right_Cosets b₂ are_equipotent

proof end;

theorem Th167: :: GROUP_2:167

for b₁ being Group
for b₂ being Subgroup of b₁ holds
( union (Left_Cosets b₂) = the carrier of b₁ & union (Right_Cosets b₂) = the carrier of b₁ )

proof end;

theorem Th168: :: GROUP_2:168

for b₁ being Group holds Left_Cosets ((1). b₁) = { {b₂} where B is Element of b₁ : verum }

proof end;

theorem Th169: :: GROUP_2:169

for b₁ being Group holds Right_Cosets ((1). b₁) = { {b₂} where B is Element of b₁ : verum }

proof end;

theorem Th170: :: GROUP_2:170

for b₁ being Group
for b₂ being strict Subgroup of b₁ st Left_Cosets b₂ = { {b₃} where B is Element of b₁ : verum } holds
b₂ = (1). b₁

proof end;

theorem Th171: :: GROUP_2:171

for b₁ being Group
for b₂ being strict Subgroup of b₁ st Right_Cosets b₂ = { {b₃} where B is Element of b₁ : verum } holds
b₂ = (1). b₁

proof end;

theorem Th172: :: GROUP_2:172

for b₁ being Group holds
( Left_Cosets ((Omega). b₁) = {the carrier of b₁} & Right_Cosets ((Omega). b₁) = {the carrier of b₁} )

proof end;

theorem Th173: :: GROUP_2:173

for b₁ being strict Group
for b₂ being strict Subgroup of b₁ st Left_Cosets b₂ = {the carrier of b₁} holds
b₂ = b₁

proof end;

theorem Th174: :: GROUP_2:174

for b₁ being strict Group
for b₂ being strict Subgroup of b₁ st Right_Cosets b₂ = {the carrier of b₁} holds
b₂ = b₁

proof end;

definition

let c₁ be Group;
let c₂ be Subgroup of c₁;
func Index c₂ -> Cardinal equals :: GROUP_2:def 17
Card (Left_Cosets a₂);
correctness ;

end;

:: deftheorem Def17 defines Index GROUP_2:def 17 :

theorem Th175: :: GROUP_2:175

for b₁ being Group
for b₂ being Subgroup of b₁ holds
( Index b₂ = Card (Left_Cosets b₂) & Index b₂ = Card (Right_Cosets b₂) )

proof end;

definition

let c₁ be Group;
let c₂ be Subgroup of c₁;
assume E93: Left_Cosets c₂ is finite ;
func index c₂ -> Nat means :Def18: :: GROUP_2:def 18
ex b₁ being finite set st
( b₁ = Left_Cosets a₂ & a₃ = card b₁ );
existence

proof end;

uniqueness ;

end;

:: deftheorem Def18 defines index GROUP_2:def 18 :

theorem Th176: :: GROUP_2:176

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

proof end;

definition

let c₁ be non empty set ;
let c₂ be Element of c₁;
redefine func { as {c₂} -> Element of Fin a₁;
coherence

proof end;

end;

Lemma94: for b₁ being Nat
for b₂ being finite set st ( for b₃ being set st b₃ in b₂ holds
ex b₄ being finite set st
( b₄ = b₃ & card b₄ = b₁ & ( for b₅ being set st b₅ in b₂ & b₃ <> b₅ holds
( b₃,b₅ are_equipotent & b₃ misses b₅ ) ) ) ) holds
ex b₃ being finite set st
( b₃ = union b₂ & card b₃ = b₁ * (card b₂) )

proof end;

theorem Th177: :: GROUP_2:177

for b₁ being Group
for b₂ being Subgroup of b₁ st b₁ is finite holds
ord b₁ = (ord b₂) * (index b₂)

proof end;

theorem Th178: :: GROUP_2:178

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

proof end;

theorem Th179: :: GROUP_2:179

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

proof end;

theorem Th180: :: GROUP_2:180

for b₁ being Group holds index ((Omega). b₁) = 1

proof end;

theorem Th181: :: GROUP_2:181

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

proof end;

theorem Th182: :: GROUP_2:182

for b₁ being Group holds Index ((1). b₁) = Ord b₁

proof end;

theorem Th183: :: GROUP_2:183

for b₁ being Group st b₁ is finite holds
index ((1). b₁) = ord b₁

proof end;

theorem Th184: :: GROUP_2:184

for b₁ being Group
for b₂ being strict Subgroup of b₁ st b₁ is finite & index b₂ = ord b₁ holds
b₂ = (1). b₁

proof end;

theorem Th185: :: GROUP_2:185

for b₁ being Group
for b₂ being strict Subgroup of b₁ st Left_Cosets b₂ is finite & Index b₂ = Ord b₁ holds
( b₁ is finite & b₂ = (1). b₁ )

proof end;

theorem Th186: :: GROUP_2:186

for b₁ being Nat
for b₂ being finite set st ( for b₃ being set st b₃ in b₂ holds
ex b₄ being finite set st
( b₄ = b₃ & card b₄ = b₁ & ( for b₅ being set st b₅ in b₂ & b₃ <> b₅ holds
( b₃,b₅ are_equipotent & b₃ misses b₅ ) ) ) ) holds
ex b₃ being finite set st
( b₃ = union b₂ & card b₃ = b₁ * (card b₂) ) by Lemma94;