:: Subgroup and Cosets of Subgroups. Lagrange theorem
:: by Wojciech A. Trybulec
::
:: 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 b1, b2 being Subset of G st b1 = { (g ") where g is Element of G : g in b2 } holds
b2 = { (g ") where g is Element of G : g in b1 }
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 b1 being non empty Group-like multMagma st
( the carrier of b1 c= the carrier of G & the multF of b1 = the multF of G || the carrier of b1 )
proof end;
end;

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

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 ;

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 ;

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 b1 being Subgroup of G holds b1 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 = () | 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;
existence
ex b1 being Subgroup of G st b1 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 b1 being Subgroup of G holds b1 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 b1 being strict Subgroup of G st the carrier of b1 = {(1_ G)}
proof end;
uniqueness
for b1, b2 being strict Subgroup of G st the carrier of b1 = {(1_ G)} & the carrier of b2 = {(1_ G)} holds
b1 = b2
by Th59;
end;

:: deftheorem Def7 defines (1). GROUP_2:def 7 :
for G being Group
for b2 being strict Subgroup of G holds
( b2 = (1). G iff the carrier of b2 = {(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 b1 being strict Subgroup of G
for b2 being Group st b1 = multMagma(# the carrier of b2, the multF of b2 #) holds
b1 = multMagma(# the carrier of b1, the multF of b1 #)
;
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;
coherence
(1). G is finite
by Th68;
existence
ex b1 being Subgroup of G st
( b1 is strict & b1 is finite )
proof end;
end;

registration
existence
ex b1 being Group st
( b1 is strict & b1 is finite )
proof end;
end;

registration
let G be finite Group;
cluster -> finite for Subgroup of G;
coherence
for b1 being Subgroup of G holds b1 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 ;

theorem :: GROUP_2:72
for G being finite Group
for H being Subgroup of G holds card H <= card G by ;

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 b1 being strict Subgroup of G st the carrier of b1 = (carr H1) /\ (carr H2)
proof end;
uniqueness
for b1, b2 being strict Subgroup of G st the carrier of b1 = (carr H1) /\ (carr H2) & the carrier of b2 = (carr H1) /\ (carr H2) holds
b1 = b2
by Th59;
end;

:: deftheorem Def10 defines /\ GROUP_2:def 10 :
for G being Group
for H1, H2 being Subgroup of G
for b4 being strict Subgroup of G holds
( b4 = H1 /\ H2 iff the carrier of b4 = (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 /\ () = H & () /\ H = H ) by Lm3;

theorem :: GROUP_2:87
for G being strict Group holds () /\ () = 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 * () = the carrier of 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 ;

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 b1 being Subset-Family of G st
for A being Subset of G holds
( A in b1 iff ex a being Element of G st A = a * H )
proof end;
uniqueness
for b1, b2 being Subset-Family of G st ( for A being Subset of G holds
( A in b1 iff ex a being Element of G st A = a * H ) ) & ( for A being Subset of G holds
( A in b2 iff ex a being Element of G st A = a * H ) ) holds
b1 = b2
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 b1 being Subset-Family of G st
for A being Subset of G holds
( A in b1 iff ex a being Element of G st A = H * a )
proof end;
uniqueness
for b1, b2 being Subset-Family of G st ( for A being Subset of G holds
( A in b1 iff ex a being Element of G st A = H * a ) ) & ( for A being Subset of G holds
( A in b2 iff ex a being Element of G st A = H * a ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def15 defines Left_Cosets GROUP_2:def 15 :
for G being Group
for H being Subgroup of G
for b3 being Subset-Family of G holds
( b3 = Left_Cosets H iff for A being Subset of G holds
( A in b3 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 b3 being Subset-Family of G holds
( b3 = Right_Cosets H iff for A being Subset of G holds
( A in b3 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 () = the carrier of G & union () = 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 () = { the carrier of G} & Right_Cosets () = { 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 ();
correctness
coherence
card () is Cardinal
;
;
end;

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

theorem :: GROUP_2:145
for G being Group
for H being Subgroup of G holds
( Index H = card () & Index H = card () ) by ;

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 b1 being Element of NAT ex B being finite set st
( B = Left_Cosets H & b1 = card B )
proof end;
uniqueness
for b1, b2 being Element of NAT st ex B being finite set st
( B = Left_Cosets H & b1 = card B ) & ex B being finite set st
( B = Left_Cosets H & b2 = card B ) holds
b1 = b2
;
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 b3 being Element of NAT holds
( b3 = index H iff ex B being finite set st
( B = Left_Cosets H & b3 = 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) * ()
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 = () * ()
proof end;

theorem :: GROUP_2:150
for G being Group holds index () = 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;