:: GROUP_2 semantic presentation

Lm1: for x being set
for G being non empty 1-sorted
for A being Subset of G st x in A holds
x is Element of G
;

theorem :: GROUP_2:1

canceled;

theorem :: GROUP_2:2

canceled;

theorem Th3: :: GROUP_2:3

for G being non empty 1-sorted
for A being Subset of G st G is finite holds
A is finite

proof end;

definition

let G be Group;
let A be Subset of G;
func A " -> Subset of G equals :: GROUP_2:def 1
{ (g " ) where g is Element of G : g in A } ;
coherence

proof end;

end;

:: deftheorem defines " GROUP_2:def 1 :

theorem :: GROUP_2:4

canceled;

theorem Th5: :: GROUP_2:5

for x being set
for G being Group
for A being Subset of G holds
( x in A " iff ex g being Element of G st
( x = g " & g in A ) ) ;

theorem :: GROUP_2:6

for G being Group
for g being Element of G holds {g} " = {(g " )}

proof end;

theorem :: GROUP_2:7

for G being Group
for g, h being Element of G holds {g,h} " = {(g " ),(h " )}

proof end;

theorem :: GROUP_2:8

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

proof end;

theorem :: GROUP_2:9

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

proof end;

theorem :: GROUP_2:10

for G being Group
for A being Subset of G holds
( A <> {} iff A " <> {} )

proof end;

definition

let G be non empty HGrStr ;
let A, B be Subset of G;
func A * B -> Subset of G equals :: GROUP_2:def 2
{ (g * h) where g, h is Element of G : ( g in A & h in B ) } ;
coherence

proof end;

end;

:: deftheorem defines * GROUP_2:def 2 :

theorem :: GROUP_2:11

canceled;

theorem Th12: :: GROUP_2:12

for x being set
for G being non empty HGrStr
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 Th13: :: GROUP_2:13

for G being non empty HGrStr
for A, B being Subset of G holds
( ( A <> {} & B <> {} ) iff A * B <> {} )

proof end;

theorem Th14: :: GROUP_2:14

for G being non empty HGrStr
for A, B, C being Subset of G st G is associative holds
(A * B) * C = A * (B * C)

proof end;

theorem :: GROUP_2:15

for G being Group
for A, B being Subset of G holds (A * B) " = (B " ) * (A " )

proof end;

theorem :: GROUP_2:16

for G being non empty HGrStr
for A, B, C being Subset of G holds A * (B \/ C) = (A * B) \/ (A * C)

proof end;

theorem :: GROUP_2:17

for G being non empty HGrStr
for A, B, C being Subset of G holds (A \/ B) * C = (A * C) \/ (B * C)

proof end;

theorem :: GROUP_2:18

for G being non empty HGrStr
for A, B, C being Subset of G holds A * (B /\ C) c= (A * B) /\ (A * C)

proof end;

theorem :: GROUP_2:19

for G being non empty HGrStr
for A, B, C being Subset of G holds (A /\ B) * C c= (A * C) /\ (B * C)

proof end;

theorem Th20: :: GROUP_2:20

for G being non empty HGrStr
for A being Subset of G holds
( ({} the carrier of G) * A = {} & A * ({} the carrier of G) = {} )

proof end;

theorem Th21: :: GROUP_2:21

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

proof end;

theorem Th22: :: GROUP_2:22

for G being non empty HGrStr
for g, h being Element of G holds {g} * {h} = {(g * h)}

proof end;

theorem :: GROUP_2:23

for G being non empty HGrStr
for g, g1, g2 being Element of G holds {g} * {g1,g2} = {(g * g1),(g * g2)}

proof end;

theorem :: GROUP_2:24

for G being non empty HGrStr
for g1, g2, g being Element of G holds {g1,g2} * {g} = {(g1 * g),(g2 * g)}

proof end;

theorem :: GROUP_2:25

for G being non empty HGrStr
for g, h, g1, g2 being Element of G holds {g,h} * {g1,g2} = {(g * g1),(g * g2),(h * g1),(h * g2)}

proof end;

theorem Th26: :: GROUP_2:26

for G being Group
for A being Subset of G st ( for g1, g2 being Element of G st g1 in A & g2 in A holds
g1 * g2 in A ) & ( for g being Element of G st g in A holds
g " in A ) holds
A * A = A

proof end;

theorem Th27: :: GROUP_2:27

for G being Group
for A being Subset of G st ( for g being Element of G st g in A holds
g " in A ) holds
A " = A

proof end;

theorem :: GROUP_2:28

for G being non empty HGrStr
for A, B being Subset of G st ( for a, b being Element of G st a in A & b in B holds
a * b = b * a ) holds
A * B = B * A

proof end;

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

theorem Th29: :: GROUP_2:29

for G being non empty HGrStr
for A, B being Subset of G st G is commutative Group holds
A * B = B * A

proof end;

theorem :: GROUP_2:30

for G being commutative Group
for A, B being Subset of G holds (A * B) " = (A " ) * (B " )

proof end;

definition

let G be non empty HGrStr ;
let g be Element of G;
let A be Subset of G;
func g * A -> Subset of G equals :: GROUP_2:def 3
{g} * A;
correctness ;
func A * g -> Subset of G equals :: GROUP_2:def 4
A * {g};
correctness ;

end;

:: deftheorem defines * GROUP_2:def 3 :

:: deftheorem defines * GROUP_2:def 4 :

theorem :: GROUP_2:31

canceled;

theorem :: GROUP_2:32

canceled;

theorem Th33: :: GROUP_2:33

for x being set
for G being non empty HGrStr
for A being Subset of G
for g being Element of G holds
( x in g * A iff ex h being Element of G st
( x = g * h & h in A ) )

proof end;

theorem Th34: :: GROUP_2:34

for x being set
for G being non empty HGrStr
for A being Subset of G
for g being Element of G holds
( x in A * g iff ex h being Element of G st
( x = h * g & h in A ) )

proof end;

theorem :: GROUP_2:35

for G being non empty HGrStr
for A, B being Subset of G
for g being Element of G st G is associative holds
(g * A) * B = g * (A * B) by Th14;

theorem :: GROUP_2:36

for G being non empty HGrStr
for A, B being Subset of G
for g being Element of G st G is associative holds
(A * g) * B = A * (g * B) by Th14;

theorem :: GROUP_2:37

for G being non empty HGrStr
for A, B being Subset of G
for g being Element of G st G is associative holds
(A * B) * g = A * (B * g) by Th14;

theorem Th38: :: GROUP_2:38

for G being non empty HGrStr
for A being Subset of G
for g, h being Element of G st G is associative holds
(g * h) * A = g * (h * A)

proof end;

theorem Th39: :: GROUP_2:39

for G being non empty HGrStr
for A being Subset of G
for g, h being Element of G st G is associative holds
(g * A) * h = g * (A * h) by Th14;

theorem Th40: :: GROUP_2:40

for G being non empty HGrStr
for A being Subset of G
for g, h being Element of G st G is associative holds
(A * g) * h = A * (g * h)

proof end;

theorem :: GROUP_2:41

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

theorem Th42: :: GROUP_2:42

for G being Group
for a being Element of G holds
( ([#] the carrier of G) * a = the carrier of G & a * ([#] the carrier of G) = the carrier of G ) by Th21;

theorem Th43: :: GROUP_2:43

for G being non empty Group-like HGrStr
for A being Subset of G holds
( (1. G) * A = A & A * (1. G) = A )

proof end;

theorem Th44: :: GROUP_2:44

for G being non empty Group-like HGrStr
for g being Element of G
for A being Subset of G st G is commutative Group holds
g * A = A * g by Th29;

definition

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

proof end;

end;

:: deftheorem Def5 defines Subgroup GROUP_2:def 5 :

theorem :: GROUP_2:45

canceled;

theorem :: GROUP_2:46

canceled;

theorem :: GROUP_2:47

canceled;

theorem Th48: :: GROUP_2:48

for G being non empty Group-like HGrStr
for H being Subgroup of G st G is finite holds
H is finite

proof end;

theorem Th49: :: GROUP_2:49

for x being set
for G being non empty Group-like HGrStr
for H being Subgroup of G st x in H holds
x in G

proof end;

theorem Th50: :: GROUP_2:50

for G being non empty Group-like HGrStr
for H being Subgroup of G
for h being Element of H holds h in G

proof end;

theorem Th51: :: GROUP_2:51

for G being non empty Group-like HGrStr
for H being Subgroup of G
for h being Element of H holds h is Element of G

proof end;

theorem Th52: :: GROUP_2:52

for G being non empty Group-like HGrStr
for g1, g2 being Element of G
for H being Subgroup of G
for h1, h2 being Element of H st h1 = g1 & h2 = g2 holds
h1 * h2 = g1 * g2

proof end;

registration

let G be Group;
cluster -> associative Subgroup of G;
coherence

proof end;

end;

theorem Th53: :: GROUP_2:53

for G being Group
for H being Subgroup of G holds 1. H = 1. G

proof end;

theorem :: GROUP_2:54

for G being Group
for H1, H2 being Subgroup of G holds 1. H1 = 1. H2

proof end;

theorem Th55: :: GROUP_2:55

for G being Group
for H being Subgroup of G holds 1. G in H

proof end;

theorem :: GROUP_2:56

for G being Group
for H1, H2 being Subgroup of G holds 1. H1 in H2

proof end;

theorem Th57: :: GROUP_2:57

for G being Group
for g being Element of G
for H being Subgroup of G
for h being Element of H st h = g holds
h " = g "

proof end;

theorem :: GROUP_2:58

for G being Group
for H being Subgroup of G holds inverse_op H = (inverse_op G) | the carrier of H

proof end;

theorem Th59: :: GROUP_2:59

for G being Group
for g1, g2 being Element of G
for H being Subgroup of G st g1 in H & g2 in H holds
g1 * g2 in H

proof end;

theorem Th60: :: GROUP_2:60

for G being Group
for g being Element of G
for H being Subgroup of G st g in H holds
g " in H

proof end;

registration

let G be Group;
cluster non empty strict Group-like associative Subgroup of G;
existence

proof end;

end;

theorem Th61: :: GROUP_2:61

for G being Group
for A being Subset of G st A <> {} & ( for g1, g2 being Element of G st g1 in A & g2 in A holds
g1 * g2 in A ) & ( for g being Element of G st g in A holds
g " in A ) holds
ex H being strict Subgroup of G st the carrier of H = A

proof end;

theorem Th62: :: GROUP_2:62

for G being Group
for H being Subgroup of G st G is commutative Group holds
H is commutative

proof end;

registration

let G be commutative Group;
cluster -> associative commutative Subgroup of G;
coherence by Th62;

end;

theorem Th63: :: GROUP_2:63

for G being Group holds G is Subgroup of G

proof end;

theorem Th64: :: GROUP_2:64

for G1, G2 being Group st G1 is Subgroup of G2 & G2 is Subgroup of G1 holds
HGrStr(# the carrier of G1,the mult of G1 #) = HGrStr(# the carrier of G2,the mult of G2 #)

proof end;

theorem Th65: :: GROUP_2:65

for G1, G2, G3 being Group st G1 is Subgroup of G2 & G2 is Subgroup of G3 holds
G1 is Subgroup of G3

proof end;

theorem Th66: :: GROUP_2:66

for G being Group
for H1, H2 being Subgroup of G st the carrier of H1 c= the carrier of H2 holds
H1 is Subgroup of H2

proof end;

theorem Th67: :: GROUP_2:67

for G being Group
for H1, H2 being Subgroup of G st ( for g being Element of G st g in H1 holds
g in H2 ) holds
H1 is Subgroup of H2

proof end;

theorem Th68: :: GROUP_2:68

for G being Group
for H1, H2 being Subgroup of G st the carrier of H1 = the carrier of H2 holds
HGrStr(# the carrier of H1,the mult of H1 #) = HGrStr(# the carrier of H2,the mult of H2 #)

proof end;

theorem Th69: :: GROUP_2:69

for G being Group
for H1, H2 being Subgroup of G st ( for g being Element of G holds
( g in H1 iff g in H2 ) ) holds
HGrStr(# the carrier of H1,the mult of H1 #) = HGrStr(# the carrier of H2,the mult of H2 #)

proof end;

definition

let G be Group;
let H1, H2 be strict Subgroup of G;
:: original: =
redefine pred H1 = H2 means :: GROUP_2:def 6
for g being Element of G holds
( g in H1 iff g in H2 );
compatibility by Th69;

end;

:: deftheorem defines = GROUP_2:def 6 :

theorem Th70: :: GROUP_2:70

for G being strict Group
for H being strict Subgroup of G st the carrier of H = the carrier of G holds
H = G

proof end;

theorem Th71: :: GROUP_2:71

for G being Group
for H being Subgroup of G st ( for g being Element of G holds g in H ) holds
HGrStr(# the carrier of H,the mult of H #) = HGrStr(# the carrier of G,the mult of G #)

proof end;

definition

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

proof end;

uniqueness by Th68;

end;

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

definition

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

proof end;

end;

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

theorem :: GROUP_2:72

canceled;

theorem :: GROUP_2:73

canceled;

theorem :: GROUP_2:74

canceled;

theorem Th75: :: GROUP_2:75

for G being Group
for H being Subgroup of G holds (1). H = (1). G

proof end;

theorem :: GROUP_2:76

for G being Group
for H1, H2 being Subgroup of G holds (1). H1 = (1). H2

proof end;

theorem Th77: :: GROUP_2:77

for G being Group
for H being Subgroup of G holds (1). G is Subgroup of H

proof end;

theorem :: GROUP_2:78

for G being strict Group
for H being Subgroup of G holds H is Subgroup of (Omega). G ;

theorem :: GROUP_2:79

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

theorem Th80: :: GROUP_2:80

for G being Group holds (1). G is finite

proof end;

theorem Th81: :: GROUP_2:81

for G being Group holds ord ((1). G) = 1

proof end;

theorem Th82: :: GROUP_2:82

for G being Group
for H being strict Subgroup of G st H is finite & ord H = 1 holds
H = (1). G

proof end;

theorem :: GROUP_2:83

for G being Group
for H being Subgroup of G holds Ord H <=` Ord G

proof end;

theorem :: GROUP_2:84

for G being Group
for H being Subgroup of G st G is finite holds
ord H <= ord G

proof end;

theorem :: GROUP_2:85

for G being strict Group
for H being strict Subgroup of G st G is finite & ord G = ord H holds
H = G

proof end;

definition

let G be Group;
let H be Subgroup of G;
func carr H -> Subset of G equals :: GROUP_2:def 9
the carrier of H;
coherence by Def5;

end;

:: deftheorem defines carr GROUP_2:def 9 :

theorem :: GROUP_2:86

canceled;

theorem :: GROUP_2:87

for G being Group
for H being Subgroup of G holds carr H <> {} ;

theorem Th88: :: GROUP_2:88

for x being set
for G being Group
for H being Subgroup of G holds
( x in carr H iff x in H ) by RLVECT_1:def 1;

theorem Th89: :: GROUP_2:89

for G being Group
for g1, g2 being Element of G
for H being Subgroup of G st g1 in carr H & g2 in carr H holds
g1 * g2 in carr H

proof end;

theorem Th90: :: GROUP_2:90

for G being Group
for g being Element of G
for H being Subgroup of G st g in carr H holds
g " in carr H

proof end;

theorem :: GROUP_2:91

for G being Group
for H being Subgroup of G holds (carr H) * (carr H) = carr H

proof end;

theorem :: GROUP_2:92

for G being Group
for H being Subgroup of G holds (carr H) " = carr H

proof end;

theorem Th93: :: GROUP_2:93

for G being Group
for H1, H2 being Subgroup of G holds
( ( (carr H1) * (carr H2) = (carr H2) * (carr H1) implies ex H being strict Subgroup of G st the carrier of H = (carr H1) * (carr H2) ) & ( ex H being Subgroup of G st the carrier of H = (carr H1) * (carr H2) implies (carr H1) * (carr H2) = (carr H2) * (carr H1) ) )

proof end;

theorem :: GROUP_2:94

for G being Group
for H1, H2 being Subgroup of G st G is commutative Group holds
ex H being strict Subgroup of G st the carrier of H = (carr H1) * (carr H2)

proof end;

definition

let G be Group;
let H1, H2 be Subgroup of G;
func H1 /\ H2 -> strict Subgroup of G means :Def10: :: GROUP_2:def 10
the carrier of it = (carr H1) /\ (carr H2);
existence

proof end;

uniqueness by Th68;

end;

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

theorem :: GROUP_2:95

canceled;

theorem :: GROUP_2:96

canceled;

theorem Th97: :: GROUP_2:97

for G being Group
for H1, H2 being Subgroup of G holds
( ( for H being Subgroup of G st H = H1 /\ H2 holds
the carrier of H = the carrier of H1 /\ the carrier of H2 ) & ( for H being strict Subgroup of G st the carrier of H = the carrier of H1 /\ the carrier of H2 holds
H = H1 /\ H2 ) )

proof end;

theorem Th98: :: GROUP_2:98

for G being Group
for H1, H2 being Subgroup of G holds carr (H1 /\ H2) = (carr H1) /\ (carr H2) by Def10;

theorem Th99: :: GROUP_2:99

for x being set
for G being Group
for H1, H2 being Subgroup of G holds
( x in H1 /\ H2 iff ( x in H1 & x in H2 ) )

proof end;

theorem :: GROUP_2:100

for G being Group
for H being strict Subgroup of G holds H /\ H = H

proof end;

theorem Th101: :: GROUP_2:101

for G being Group
for H1, H2 being Subgroup of G holds H1 /\ H2 = H2 /\ H1

proof end;

definition

let G be Group;
let H1, H2 be Subgroup of G;
:: original: /\
redefine func H1 /\ H2 -> strict Subgroup of G;
commutativity by Th101;

end;

theorem :: GROUP_2:102

for G being Group
for H1, H2, H3 being Subgroup of G holds (H1 /\ H2) /\ H3 = H1 /\ (H2 /\ H3)

proof end;

Lm3: for G being Group
for H2 being Subgroup of G
for H1 being strict Subgroup of G holds
( H1 is Subgroup of H2 iff H1 /\ H2 = H1 )

proof end;

theorem :: GROUP_2:103

for G being Group
for H being Subgroup of G holds
( ((1). G) /\ H = (1). G & H /\ ((1). G) = (1). G )

proof end;

theorem Th104: :: GROUP_2:104

for G being strict Group
for H being strict Subgroup of G holds
( H /\ ((Omega). G) = H & ((Omega). G) /\ H = H ) by Lm3;

theorem :: GROUP_2:105

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

Lm4: for G being Group
for H1, H2 being Subgroup of G holds H1 /\ H2 is Subgroup of H1

proof end;

theorem :: GROUP_2:106

for G being Group
for H1, H2 being Subgroup of G holds
( H1 /\ H2 is Subgroup of H1 & H1 /\ H2 is Subgroup of H2 ) by Lm4;

theorem :: GROUP_2:107

for G being Group
for H2 being Subgroup of G
for H1 being strict Subgroup of G holds
( H1 is Subgroup of H2 iff H1 /\ H2 = H1 ) by Lm3;

theorem :: GROUP_2:108

for G being Group
for H1, H2, H3 being Subgroup of G st H1 is Subgroup of H2 holds
H1 /\ H3 is Subgroup of H2

proof end;

theorem :: GROUP_2:109

for G being Group
for H1, H2, H3 being Subgroup of G st H1 is Subgroup of H2 & H1 is Subgroup of H3 holds
H1 is Subgroup of H2 /\ H3

proof end;

theorem :: GROUP_2:110

for G being Group
for H1, H2, H3 being Subgroup of G st H1 is Subgroup of H2 holds
H1 /\ H3 is Subgroup of H2 /\ H3

proof end;

theorem :: GROUP_2:111

for G being Group
for H1, H2 being Subgroup of G st ( H1 is finite or H2 is finite ) holds
H1 /\ H2 is finite

proof end;

definition

let G be Group;
let H be Subgroup of G;
let A be Subset of G;
func A * H -> Subset of G equals :: GROUP_2:def 11
A * (carr H);
correctness ;
func H * A -> Subset of G equals :: GROUP_2:def 12
(carr H) * A;
correctness ;

end;

:: deftheorem defines * GROUP_2:def 11 :

:: deftheorem defines * GROUP_2:def 12 :

theorem :: GROUP_2:112

canceled;

theorem :: GROUP_2:113

canceled;

theorem :: GROUP_2:114

for x being set
for G being Group
for A being Subset of G
for H being Subgroup of G holds
( x in A * H iff ex g1, g2 being Element of G st
( x = g1 * g2 & g1 in A & g2 in H ) )

proof end;

theorem :: GROUP_2:115

for x being set
for G being Group
for A being Subset of G
for H being Subgroup of G holds
( x in H * A iff ex g1, g2 being Element of G st
( x = g1 * g2 & g1 in H & g2 in A ) )

proof end;

theorem Th116: :: GROUP_2:116

for G being Group
for A, B being Subset of G
for H being Subgroup of G holds (A * B) * H = A * (B * H) by Th14;

theorem :: GROUP_2:117

for G being Group
for A, B being Subset of G
for H being Subgroup of G holds (A * H) * B = A * (H * B) by Th14;

theorem Th118: :: GROUP_2:118

for G being Group
for A, B being Subset of G
for H being Subgroup of G holds (H * A) * B = H * (A * B) by Th14;

theorem :: GROUP_2:119

for G being Group
for A being Subset of G
for H1, H2 being Subgroup of G holds (A * H1) * H2 = A * (H1 * (carr H2)) by Th14;

theorem :: GROUP_2:120

for G being Group
for A being Subset of G
for H1, H2 being Subgroup of G holds (H1 * A) * H2 = H1 * (A * H2) by Th116;

theorem :: GROUP_2:121

for G being Group
for A being Subset of G
for H1, H2 being Subgroup of G holds (H1 * (carr H2)) * A = H1 * (H2 * A) by Th118;

theorem :: GROUP_2:122

for G being Group
for A being Subset of G
for H being Subgroup of G st G is commutative Group holds
A * H = H * A by Th29;

definition

let G be Group;
let H be Subgroup of G;
let a be Element of G;
func a * H -> Subset of G equals :: GROUP_2:def 13
a * (carr H);
correctness ;
func H * a -> Subset of G equals :: GROUP_2:def 14
(carr H) * a;
correctness ;

end;

:: deftheorem defines * GROUP_2:def 13 :

:: deftheorem defines * GROUP_2:def 14 :

theorem :: GROUP_2:123

canceled;

theorem :: GROUP_2:124

canceled;

theorem Th125: :: GROUP_2:125

for x being set
for G being Group
for a being Element of G
for H being Subgroup of G holds
( x in a * H iff ex g being Element of G st
( x = a * g & g in H ) )

proof end;

theorem Th126: :: GROUP_2:126

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

for G being Group
for a, b being Element of G
for H being Subgroup of G holds (a * b) * H = a * (b * H) by Th38;

theorem Th128: :: GROUP_2:128

for G being Group
for a, b being Element of G
for H being Subgroup of G holds (a * H) * b = a * (H * b) by Th39;

theorem Th129: :: GROUP_2:129

for G being Group
for a, b being Element of G
for H being Subgroup of G holds (H * a) * b = H * (a * b) by Th40;

theorem Th130: :: GROUP_2:130

for G being Group
for a being Element of G
for H being Subgroup of G holds
( a in a * H & a in H * a )

proof end;

theorem :: GROUP_2:131

canceled;

theorem Th132: :: GROUP_2:132

for G being Group
for H being Subgroup of G holds
( (1. G) * H = carr H & H * (1. G) = carr H ) by Th43;

theorem Th133: :: GROUP_2:133

for G being Group
for a being Element of G holds
( ((1). G) * a = {a} & a * ((1). G) = {a} )

proof end;

theorem Th134: :: GROUP_2:134

for G being Group
for a being Element of G holds
( a * ((Omega). G) = the carrier of G & ((Omega). G) * a = the carrier of G )

proof end;

theorem :: GROUP_2:135

for G being Group
for a being Element of G
for H being Subgroup of G st G is commutative Group holds
a * H = H * a by Th44;

theorem Th136: :: GROUP_2:136

for G being Group
for a being Element of G
for H being Subgroup of G holds
( a in H iff a * H = carr H )

proof end;

theorem Th137: :: GROUP_2:137

for G being Group
for a, b being Element of G
for H being Subgroup of G holds
( a * H = b * H iff (b " ) * a in H )

proof end;

theorem Th138: :: GROUP_2:138

for G being Group
for a, b being Element of G
for H being Subgroup of G holds
( a * H = b * H iff a * H meets b * H )

proof end;

theorem Th139: :: GROUP_2:139

for G being Group
for a, b being Element of G
for H being Subgroup of G holds (a * b) * H c= (a * H) * (b * H)

proof end;

theorem :: GROUP_2:140

for G being Group
for a being Element of G
for H being Subgroup of G holds
( carr H c= (a * H) * ((a " ) * H) & carr H c= ((a " ) * H) * (a * H) )

proof end;

theorem :: GROUP_2:141

for G being Group
for a being Element of G
for H being Subgroup of G holds (a |^ 2) * H c= (a * H) * (a * H)

proof end;

theorem Th142: :: GROUP_2:142

for G being Group
for a being Element of G
for H being Subgroup of G holds
( a in H iff H * a = carr H )

proof end;

theorem Th143: :: GROUP_2:143

for G being Group
for a, b being Element of G
for H being Subgroup of G holds
( H * a = H * b iff b * (a " ) in H )

proof end;

theorem :: GROUP_2:144

for G being Group
for a, b being Element of G
for H being Subgroup of G holds
( H * a = H * b iff H * a meets H * b )

proof end;

theorem Th145: :: GROUP_2:145

for G being Group
for a, b being Element of G
for H being Subgroup of G holds (H * a) * b c= (H * a) * (H * b)

proof end;

theorem :: GROUP_2:146

for G being Group
for a being Element of G
for H being Subgroup of G holds
( carr H c= (H * a) * (H * (a " )) & carr H c= (H * (a " )) * (H * a) )

proof end;

theorem :: GROUP_2:147

for G being Group
for a being Element of G
for H being Subgroup of G holds H * (a |^ 2) c= (H * a) * (H * a)

proof end;

theorem :: GROUP_2:148

for G being Group
for a being Element of G
for H1, H2 being Subgroup of G holds a * (H1 /\ H2) = (a * H1) /\ (a * H2)

proof end;

theorem :: GROUP_2:149

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

for G being Group
for a being Element of G
for H2 being Subgroup of G ex H1 being strict Subgroup of G st the carrier of H1 = (a * H2) * (a " )

proof end;

theorem Th151: :: GROUP_2:151

for G being Group
for a, b being Element of G
for H being Subgroup of G holds a * H,b * H are_equipotent

proof end;

theorem Th152: :: GROUP_2:152

for G being Group
for a, b being Element of G
for H being Subgroup of G holds a * H,H * b are_equipotent

proof end;

theorem Th153: :: GROUP_2:153

for G being Group
for a, b being Element of G
for H being Subgroup of G holds H * a,H * b are_equipotent

proof end;

theorem Th154: :: GROUP_2:154

for G being Group
for a being Element of G
for H being Subgroup of G holds
( carr H,a * H are_equipotent & carr H,H * a are_equipotent )

proof end;

theorem :: GROUP_2:155

for G being Group
for a being Element of G
for H being Subgroup of G holds
( Ord H = Card (a * H) & Ord H = Card (H * a) )

proof end;

theorem Th156: :: GROUP_2:156

for G being Group
for a being Element of G
for H being Subgroup of G st H is finite holds
ex B, C being finite set st
( B = a * H & C = H * a & ord H = card B & ord H = card C )

proof end;

definition

let G be Group;
let H be Subgroup of G;
func Left_Cosets H -> Subset-Family of G means :Def15: :: GROUP_2:def 15
for A being Subset of G holds
( A in it iff ex a being Element of G st A = a * H );
existence

proof end;

uniqueness

proof end;

func Right_Cosets H -> Subset-Family of G means :Def16: :: GROUP_2:def 16
for A being Subset of G holds
( A in it iff ex a being Element of G st A = H * a );
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 :: GROUP_2:157

canceled;

theorem :: GROUP_2:158

canceled;

theorem :: GROUP_2:159

canceled;

theorem :: GROUP_2:160

canceled;

theorem :: GROUP_2:161

canceled;

theorem :: GROUP_2:162

canceled;

theorem :: GROUP_2:163

canceled;

theorem Th164: :: GROUP_2:164

for G being Group
for H being Subgroup of G st G is finite holds
( Right_Cosets H is finite & Left_Cosets H is finite )

proof end;

theorem :: GROUP_2:165

for G being Group
for H being Subgroup of G holds
( carr H in Left_Cosets H & carr H in Right_Cosets H )

proof end;

theorem Th166: :: GROUP_2:166

for G being Group
for H being Subgroup of G holds Left_Cosets H, Right_Cosets H are_equipotent

proof end;

theorem Th167: :: GROUP_2:167

for G being Group
for H being Subgroup of G holds
( union (Left_Cosets H) = the carrier of G & union (Right_Cosets H) = the carrier of G )

proof end;

theorem Th168: :: GROUP_2:168

for G being Group holds Left_Cosets ((1). G) = { {a} where a is Element of G : verum }

proof end;

theorem :: GROUP_2:169

for G being Group holds Right_Cosets ((1). G) = { {a} where a is Element of G : verum }

proof end;

theorem :: GROUP_2:170

for G being Group
for H being strict Subgroup of G st Left_Cosets H = { {a} where a is Element of G : verum } holds
H = (1). G

proof end;

theorem :: GROUP_2:171

for G being Group
for H being strict Subgroup of G st Right_Cosets H = { {a} where a is Element of G : verum } holds
H = (1). G

proof end;

theorem Th172: :: GROUP_2:172

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

proof end;

theorem Th173: :: GROUP_2:173

for G being strict Group
for H being strict Subgroup of G st Left_Cosets H = {the carrier of G} holds
H = G

proof end;

theorem :: GROUP_2:174

for G being strict Group
for H being strict Subgroup of G st Right_Cosets H = {the carrier of G} holds
H = G

proof end;

definition

let G be Group;
let H be Subgroup of G;
func Index H -> Cardinal equals :: GROUP_2:def 17
Card (Left_Cosets H);
correctness ;

end;

:: deftheorem defines Index GROUP_2:def 17 :

theorem :: GROUP_2:175

for G being Group
for H being Subgroup of G holds
( Index H = Card (Left_Cosets H) & Index H = Card (Right_Cosets H) )

proof end;

definition

let G be Group;
let H be Subgroup of G;
assume A1: Left_Cosets H is finite ;
func index H -> Nat means :Def18: :: GROUP_2:def 18
ex B being finite set st
( B = Left_Cosets H & it = card B );
existence

proof end;

uniqueness ;

end;

:: deftheorem Def18 defines index GROUP_2:def 18 :

theorem :: GROUP_2:176

for G being Group
for H being Subgroup of G st Left_Cosets H is finite holds
( ex B being finite set st
( B = Left_Cosets H & index H = card B ) & ex C being finite set st
( C = Right_Cosets H & index H = card C ) )

proof end;

definition

let D be non empty set ;
let d be Element of D;
:: original: {
redefine func {d} -> Element of Fin D;
coherence

proof end;

end;

Lm5: for k being Nat
for X being finite set st ( for Y being set st Y in X holds
ex B being finite set st
( B = Y & card B = k & ( for Z being set st Z in X & Y <> Z holds
( Y,Z are_equipotent & Y misses Z ) ) ) ) holds
ex C being finite set st
( C = union X & card C = k * (card X) )

proof end;

theorem Th177: :: GROUP_2:177

for G being Group
for H being Subgroup of G st G is finite holds
ord G = (ord H) * (index H)

proof end;

theorem :: GROUP_2:178

for G being Group
for H being Subgroup of G st G is finite holds
ord H divides ord G

proof end;

theorem :: GROUP_2:179

for G being Group
for I, H being Subgroup of G
for J being Subgroup of H st G is finite & I = J holds
index I = (index J) * (index H)

proof end;

theorem :: GROUP_2:180

for G being Group holds index ((Omega). G) = 1

proof end;

theorem :: GROUP_2:181

for G being strict Group
for H being strict Subgroup of G st Left_Cosets H is finite & index H = 1 holds
H = G

proof end;

theorem :: GROUP_2:182

for G being Group holds Index ((1). G) = Ord G

proof end;

theorem :: GROUP_2:183

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

proof end;

theorem Th184: :: GROUP_2:184

for G being Group
for H being strict Subgroup of G st G is finite & index H = ord G holds
H = (1). G

proof end;

theorem :: GROUP_2:185

for G being Group
for H being strict Subgroup of G st Left_Cosets H is finite & Index H = Ord G holds
( G is finite & H = (1). G )

proof end;

theorem :: GROUP_2:186

for k being Nat
for X being finite set st ( for Y being set st Y in X holds
ex B being finite set st
( B = Y & card B = k & ( for Z being set st Z in X & Y <> Z holds
( Y,Z are_equipotent & Y misses Z ) ) ) ) holds
ex C being finite set st
( C = union X & card C = k * (card X) ) by Lm5;