:: Subgroup and Cosets of Subgroups. Lagrange theorem
:: by Wojciech A. Trybulec
::
:: Received July 23, 1990
:: Copyright (c) 1990-2021 Association of Mizar Users

Lm1: for x being object
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

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

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
{ (g ") where g is Element of G : g in A } is Subset of G

proof end;

involutiveness
for b₁, b₂ being Subset of G st b₁ = { (g ") where g is Element of G : g in b₂ } holds
b₂ = { (g ") where g is Element of G : g in b₁ }

proof end;

end;

:: deftheorem defines " GROUP_2:def 1 :
for G being Group
for A being Subset of G holds A " = { (g ") where g is Element of G : g in A } ;

theorem Th2: :: GROUP_2:2

for x being object
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:3

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

proof end;

theorem :: GROUP_2:4

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

proof end;

theorem :: GROUP_2:5

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

proof end;

theorem :: GROUP_2:6

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

proof end;

theorem Th7: :: GROUP_2:7

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

proof end;

registration

let G be Group;
let A be empty Subset of G;

cluster A " -> empty ;

coherence
A " is empty by Th7;

end;

registration

let G be Group;
let A be non empty Subset of G;

cluster A " -> non empty ;

coherence
not A " is empty by Th7;

end;

definition

let G be non empty multMagma ;
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
{ (g * h) where g, h is Element of G : ( g in A & h in B ) } is Subset of G

proof end;

end;

:: deftheorem defines * GROUP_2:def 2 :
for G being non empty multMagma
for A, B being Subset of G holds A * B = { (g * h) where g, h is Element of G : ( g in A & h in B ) } ;

definition

let G be non empty commutative multMagma ;
let A, B be Subset of G;
:: original: *
redefine func A * B -> Subset of G;
commutativity
for A, B being Subset of G holds A * B = B * A

proof end;

end;

theorem Th8: :: GROUP_2:8

for x being object
for G being non empty multMagma
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 Th9: :: GROUP_2:9

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

proof end;

theorem Th10: :: GROUP_2:10

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

proof end;

theorem :: GROUP_2:11

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

proof end;

theorem :: GROUP_2:12

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

proof end;

theorem :: GROUP_2:13

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

proof end;

theorem :: GROUP_2:14

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

proof end;

theorem :: GROUP_2:15

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

proof end;

theorem Th16: :: GROUP_2:16

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

proof end;

theorem Th17: :: GROUP_2:17

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 Th18: :: GROUP_2:18

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

proof end;

theorem :: GROUP_2:19

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

proof end;

theorem :: GROUP_2:20

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

proof end;

theorem :: GROUP_2:21

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

proof end;

theorem Th22: :: GROUP_2:22

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 Th23: :: GROUP_2:23

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:24

for G being non empty multMagma
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 Th25: :: GROUP_2:25

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

proof end;

theorem :: GROUP_2:26

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 multMagma ;
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
coherence
{g} * A is Subset of G;
;

func A * g -> Subset of G equals :: GROUP_2:def 4
A * {g};

correctness
coherence
A * {g} is Subset of G;
;

end;

:: deftheorem defines * GROUP_2:def 3 :
for G being non empty multMagma
for g being Element of G
for A being Subset of G holds g * A = {g} * A;

:: deftheorem defines * GROUP_2:def 4 :
for G being non empty multMagma
for g being Element of G
for A being Subset of G holds A * g = A * {g};

theorem Th27: :: GROUP_2:27

for x being object
for G being non empty multMagma
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 Th28: :: GROUP_2:28

for x being object
for G being non empty multMagma
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:29

for G being non empty multMagma
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 Th10;

theorem :: GROUP_2:30

for G being non empty multMagma
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 Th10;

theorem :: GROUP_2:31

for G being non empty multMagma
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 Th10;

theorem Th32: :: GROUP_2:32

for G being non empty multMagma
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 :: GROUP_2:33

for G being non empty multMagma
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 Th10;

theorem Th34: :: GROUP_2:34

for G being non empty multMagma
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:35

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

theorem :: GROUP_2:36

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 Th17;

theorem Th37: :: GROUP_2:37

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

proof end;

theorem :: GROUP_2:38

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

definition

let G be non empty Group-like multMagma ;

mode Subgroup of G -> non empty Group-like multMagma means :Def5: :: GROUP_2:def 5
( the carrier of it c= the carrier of G & the multF of it = the multF of G || the carrier of it );

existence
ex b₁ being non empty Group-like multMagma st
( the carrier of b₁ c= the carrier of G & the multF of b₁ = the multF of G || the carrier of b₁ )

proof end;

end;

:: deftheorem Def5 defines Subgroup GROUP_2:def 5 :
for G, b₂ being non empty Group-like multMagma holds
( b₂ is Subgroup of G iff ( the carrier of b₂ c= the carrier of G & the multF of b₂ = the multF of G || the carrier of b₂ ) );

theorem Th39: :: GROUP_2:39

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

proof end;

theorem Th40: :: GROUP_2:40

for x being object
for G being non empty Group-like multMagma
for H being Subgroup of G st x in H holds
x in G

proof end;

theorem Th41: :: GROUP_2:41

for G being non empty Group-like multMagma
for H being Subgroup of G
for h being Element of H holds h in G by Th40, STRUCT_0:def 5;

theorem Th42: :: GROUP_2:42

for G being non empty Group-like multMagma
for H being Subgroup of G
for h being Element of H holds h is Element of G by Th41, STRUCT_0:def 5;

theorem Th43: :: GROUP_2:43

for G being non empty Group-like multMagma
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 for Subgroup of G;

coherence
for b₁ being Subgroup of G holds b₁ is associative

proof end;

end;

theorem Th44: :: GROUP_2:44

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

proof end;

theorem :: GROUP_2:45

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

proof end;

theorem Th46: :: GROUP_2:46

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

proof end;

theorem :: GROUP_2:47

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

proof end;

theorem Th48: :: GROUP_2:48

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:49

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

proof end;

theorem Th50: :: GROUP_2:50

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 Th51: :: GROUP_2:51

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 unital Group-like associative for Subgroup of G;

existence
ex b₁ being Subgroup of G st b₁ is strict

proof end;

end;

theorem Th52: :: GROUP_2:52

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 Th53: :: GROUP_2:53

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 -> commutative for Subgroup of G;

coherence
for b₁ being Subgroup of G holds b₁ is commutative by Th53;

end;

theorem Th54: :: GROUP_2:54

for G being Group holds G is Subgroup of G

proof end;

theorem Th55: :: GROUP_2:55

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

proof end;

theorem Th56: :: GROUP_2:56

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 Th57: :: GROUP_2:57

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 Th58: :: GROUP_2:58

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 Th59: :: GROUP_2:59

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

proof end;

theorem Th60: :: GROUP_2:60

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
multMagma(# the carrier of H1, the multF of H1 #) = multMagma(# the carrier of H2, the multF 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
( H1 = H2 iff for g being Element of G holds
( g in H1 iff g in H2 ) ) by Th60;

end;

:: deftheorem defines = GROUP_2:def 6 :
for G being Group
for H1, H2 being strict Subgroup of G holds
( H1 = H2 iff for g being Element of G holds
( g in H1 iff g in H2 ) );

theorem Th61: :: GROUP_2:61

for G being Group
for H being Subgroup of G st the carrier of G c= the carrier of H holds
multMagma(# the carrier of H, the multF of H #) = multMagma(# the carrier of G, the multF of G #)

proof end;

theorem Th62: :: GROUP_2:62

for G being Group
for H being Subgroup of G st ( for g being Element of G holds g in H ) holds
multMagma(# the carrier of H, the multF of H #) = multMagma(# the carrier of G, the multF 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
ex b₁ being strict Subgroup of G st the carrier of b₁ = {(1_ G)}

proof end;

uniqueness
for b₁, b₂ being strict Subgroup of G st the carrier of b₁ = {(1_ G)} & the carrier of b₂ = {(1_ G)} holds
b₁ = b₂ by Th59;

end;

:: deftheorem Def7 defines (1). GROUP_2:def 7 :
for G being Group
for b₂ being strict Subgroup of G holds
( b₂ = (1). G iff the carrier of b₂ = {(1_ G)} );

definition

let G be Group;

func (Omega). G -> strict Subgroup of G equals :: GROUP_2:def 8
multMagma(# the carrier of G, the multF of G #);

coherence
multMagma(# the carrier of G, the multF of G #) is strict Subgroup of G

proof end;

projectivity
for b₁ being strict Subgroup of G
for b₂ being Group st b₁ = multMagma(# the carrier of b₂, the multF of b₂ #) holds
b₁ = multMagma(# the carrier of b₁, the multF of b₁ #) ;

end;

:: deftheorem defines (Omega). GROUP_2:def 8 :
for G being Group holds (Omega). G = multMagma(# the carrier of G, the multF of G #);

theorem Th63: :: GROUP_2:63

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

proof end;

theorem :: GROUP_2:64

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

proof end;

theorem Th65: :: GROUP_2:65

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

proof end;

theorem :: GROUP_2:66

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

theorem :: GROUP_2:67

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

theorem Th68: :: GROUP_2:68

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

proof end;

registration

let G be Group;

cluster (1). G -> finite strict ;

coherence
(1). G is finite by Th68;

cluster non empty finite strict unital Group-like associative for Subgroup of G;

existence
ex b₁ being Subgroup of G st
( b₁ is strict & b₁ is finite )

proof end;

end;

registration

cluster non empty finite strict unital Group-like associative for multMagma ;

existence
ex b₁ being Group st
( b₁ is strict & b₁ is finite )

proof end;

end;

registration

let G be finite Group;

cluster -> finite for Subgroup of G;

coherence
for b₁ being Subgroup of G holds b₁ is finite by Th39;

end;

theorem Th69: :: GROUP_2:69

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

proof end;

theorem Th70: :: GROUP_2:70

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

proof end;

theorem :: GROUP_2:71

for G being Group
for H being Subgroup of G holds card H c= card G by Def5, CARD_1:11;

theorem :: GROUP_2:72

for G being finite Group
for H being Subgroup of G holds card H <= card G by Def5, NAT_1:43;

theorem :: GROUP_2:73

for G being finite Group
for H being Subgroup of G st card G = card H holds
multMagma(# the carrier of H, the multF of H #) = multMagma(# the carrier of G, the multF of 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
the carrier of H is Subset of G by Def5;

end;

:: deftheorem defines carr GROUP_2:def 9 :
for G being Group
for H being Subgroup of G holds carr H = the carrier of H;

theorem Th74: :: GROUP_2:74

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 Th75: :: GROUP_2:75

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:76

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

proof end;

theorem :: GROUP_2:77

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

proof end;

theorem Th78: :: GROUP_2:78

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:79

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
ex b₁ being strict Subgroup of G st the carrier of b₁ = (carr H1) /\ (carr H2)

proof end;

uniqueness
for b₁, b₂ being strict Subgroup of G st the carrier of b₁ = (carr H1) /\ (carr H2) & the carrier of b₂ = (carr H1) /\ (carr H2) holds
b₁ = b₂ by Th59;

end;

:: deftheorem Def10 defines /\ GROUP_2:def 10 :
for G being Group
for H1, H2 being Subgroup of G
for b₄ being strict Subgroup of G holds
( b₄ = H1 /\ H2 iff the carrier of b₄ = (carr H1) /\ (carr H2) );

theorem Th80: :: GROUP_2:80

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

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

theorem Th82: :: GROUP_2:82

for x being object
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:83

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

proof end;

definition

let G be Group;
let H1, H2 be Subgroup of G;
:: original: /\
redefine func H1 /\ H2 -> strict Subgroup of G;
commutativity
for H1, H2 being Subgroup of G holds H1 /\ H2 = H2 /\ H1

proof end;

end;

theorem :: GROUP_2:84

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, H1 being Subgroup of G holds
( H1 is Subgroup of H2 iff multMagma(# the carrier of (H1 /\ H2), the multF of (H1 /\ H2) #) = multMagma(# the carrier of H1, the multF of H1 #) )

proof end;

theorem :: GROUP_2:85

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

proof end;

theorem :: GROUP_2:86

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:87

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

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

proof end;

theorem :: GROUP_2:88

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:89

for G being Group
for H2, H1 being Subgroup of G holds
( H1 is Subgroup of H2 iff multMagma(# the carrier of (H1 /\ H2), the multF of (H1 /\ H2) #) = multMagma(# the carrier of H1, the multF of H1 #) ) by Lm3;

theorem :: GROUP_2:90

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:91

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:92

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:93

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
coherence
A * (carr H) is Subset of G;
;

func H * A -> Subset of G equals :: GROUP_2:def 12
(carr H) * A;

correctness
coherence
(carr H) * A is Subset of G;
;

end;

:: deftheorem defines * GROUP_2:def 11 :
for G being Group
for H being Subgroup of G
for A being Subset of G holds A * H = A * (carr H);

:: deftheorem defines * GROUP_2:def 12 :
for G being Group
for H being Subgroup of G
for A being Subset of G holds H * A = (carr H) * A;

theorem :: GROUP_2:94

for x being object
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:95

for x being object
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 :: GROUP_2:96

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 Th10;

theorem :: GROUP_2:97

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 Th10;

theorem :: GROUP_2:98

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 Th10;

theorem :: GROUP_2:99

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 Th10;

theorem :: GROUP_2:100

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 Th10;

theorem :: GROUP_2:101

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 Th10;

theorem :: GROUP_2:102

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 Th25;

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
coherence
a * (carr H) is Subset of G;
;

func H * a -> Subset of G equals :: GROUP_2:def 14
(carr H) * a;

correctness
coherence
(carr H) * a is Subset of G;
;

end;

:: deftheorem defines * GROUP_2:def 13 :
for G being Group
for H being Subgroup of G
for a being Element of G holds a * H = a * (carr H);

:: deftheorem defines * GROUP_2:def 14 :
for G being Group
for H being Subgroup of G
for a being Element of G holds H * a = (carr H) * a;

theorem Th103: :: GROUP_2:103

for x being object
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 Th104: :: GROUP_2:104

for x being object
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 :: GROUP_2:105

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 Th32;

theorem :: GROUP_2:106

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 Th10;

theorem :: GROUP_2:107

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 Th34;

theorem Th108: :: GROUP_2:108

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:109

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

theorem Th110: :: GROUP_2:110

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

proof end;

theorem Th111: :: GROUP_2:111

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:112

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 Th25;

theorem Th113: :: GROUP_2:113

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 Th114: :: GROUP_2:114

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 Th115: :: GROUP_2:115

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 Th116: :: GROUP_2:116

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:117

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:118

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 Th119: :: GROUP_2:119

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 Th120: :: GROUP_2:120

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:121

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 Th122: :: GROUP_2:122

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:123

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:124

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:125

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

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

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 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 * H are_equipotent

proof end;

theorem Th129: :: GROUP_2:129

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 Th130: :: GROUP_2:130

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 Th131: :: GROUP_2:131

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:132

for G being Group
for a being Element of G
for H being Subgroup of G holds
( card H = card (a * H) & card H = card (H * a) ) by Th131, CARD_1:5;

theorem Th133: :: GROUP_2:133

for G being Group
for a being Element of G
for H being finite Subgroup of G ex B, C being finite set st
( B = a * H & C = H * a & card H = card B & card 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
ex b₁ being Subset-Family of G st
for A being Subset of G holds
( A in b₁ iff ex a being Element of G st A = a * H )

proof end;

uniqueness
for b₁, b₂ being Subset-Family of G st ( for A being Subset of G holds
( A in b₁ iff ex a being Element of G st A = a * H ) ) & ( for A being Subset of G holds
( A in b₂ iff ex a being Element of G st A = a * H ) ) holds
b₁ = b₂

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
ex b₁ being Subset-Family of G st
for A being Subset of G holds
( A in b₁ iff ex a being Element of G st A = H * a )

proof end;

uniqueness
for b₁, b₂ being Subset-Family of G st ( for A being Subset of G holds
( A in b₁ iff ex a being Element of G st A = H * a ) ) & ( for A being Subset of G holds
( A in b₂ iff ex a being Element of G st A = H * a ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def15 defines Left_Cosets GROUP_2:def 15 :
for G being Group
for H being Subgroup of G
for b₃ being Subset-Family of G holds
( b₃ = Left_Cosets H iff for A being Subset of G holds
( A in b₃ iff ex a being Element of G st A = a * H ) );

:: deftheorem Def16 defines Right_Cosets GROUP_2:def 16 :
for G being Group
for H being Subgroup of G
for b₃ being Subset-Family of G holds
( b₃ = Right_Cosets H iff for A being Subset of G holds
( A in b₃ iff ex a being Element of G st A = H * a ) );

theorem :: GROUP_2:134

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 ) ;

theorem :: GROUP_2:135

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 Th136: :: GROUP_2:136

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

proof end;

theorem Th137: :: GROUP_2:137

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 Th138: :: GROUP_2:138

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

proof end;

theorem :: GROUP_2:139

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

proof end;

theorem :: GROUP_2:140

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:141

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 Th142: :: GROUP_2:142

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

proof end;

theorem Th143: :: GROUP_2:143

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:144

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
coherence
card (Left_Cosets H) is Cardinal;
;

end;

:: deftheorem defines Index GROUP_2:def 17 :
for G being Group
for H being Subgroup of G holds Index H = card (Left_Cosets H);

theorem :: GROUP_2:145

for G being Group
for H being Subgroup of G holds
( Index H = card (Left_Cosets H) & Index H = card (Right_Cosets H) ) by Th136, CARD_1:5;

definition

let G be Group;
let H be Subgroup of G;
assume A1: Left_Cosets H is finite ;

func index H -> Element of NAT means :Def18: :: GROUP_2:def 18
ex B being finite set st
( B = Left_Cosets H & it = card B );

existence
ex b₁ being Element of NAT ex B being finite set st
( B = Left_Cosets H & b₁ = card B )

proof end;

uniqueness
for b₁, b₂ being Element of NAT st ex B being finite set st
( B = Left_Cosets H & b₁ = card B ) & ex B being finite set st
( B = Left_Cosets H & b₂ = card B ) holds
b₁ = b₂ ;

end;

:: deftheorem Def18 defines index GROUP_2:def 18 :
for G being Group
for H being Subgroup of G st Left_Cosets H is finite holds
for b₃ being Element of NAT holds
( b₃ = index H iff ex B being finite set st
( B = Left_Cosets H & b₃ = card B ) );

theorem :: GROUP_2:146

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;

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;

:: Lagrange Theorem for Groups

theorem Th147: :: GROUP_2:147

for G being finite Group
for H being Subgroup of G holds card G = (card H) * (index H)

proof end;

theorem :: GROUP_2:148

for G being finite Group
for H being Subgroup of G holds card H divides card G

proof end;

theorem :: GROUP_2:149

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

proof end;

theorem :: GROUP_2:150

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

proof end;

theorem :: GROUP_2:151

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:152

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

proof end;

theorem :: GROUP_2:153

for G being finite Group holds index ((1). G) = card G

proof end;

theorem Th154: :: GROUP_2:154

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

proof end;

theorem :: GROUP_2:155

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

proof end;

::
:: Auxiliary theorems.
::

theorem :: GROUP_2:156

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;