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


begin

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 :: GROUP_2:3
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 :: 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 Th10: :: GROUP_2:10
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 Th10;
end;

registration
let G be Group;
let A be non empty Subset of G;
cluster A " -> non empty ;
coherence
not A " is empty by Th10;
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 :: GROUP_2:11
canceled;

theorem Th12: :: GROUP_2:12
for x being set
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 Th13: :: GROUP_2:13
for G being non empty multMagma
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 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: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 multMagma
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 multMagma
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 multMagma
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 multMagma
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 multMagma
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 multMagma
for g, h being Element of G holds {g} * {h} = {(g * h)}
proof end;

theorem :: GROUP_2:23
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:24
for G being non empty multMagma
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 multMagma
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 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 Th29: :: GROUP_2:29
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: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 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 :: GROUP_2:31
canceled;

theorem :: GROUP_2:32
canceled;

theorem Th33: :: GROUP_2:33
for x being set
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 Th34: :: GROUP_2:34
for x being set
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:35
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 Th14;

theorem :: GROUP_2:36
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 Th14;

theorem :: GROUP_2:37
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 Th14;

theorem Th38: :: GROUP_2:38
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:39
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 Th14;

theorem Th40: :: GROUP_2:40
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:41
for G being non empty multMagma
for a being Element of G holds
( ({} the carrier of G) * a = {} & a * ({} the carrier of G) = {} ) by Th20;

theorem :: 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 multMagma
for A being Subset of G holds
( (1_ G) * A = A & A * (1_ G) = A )
proof end;

theorem :: GROUP_2:44
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 Th29;

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 :: 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 multMagma
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 multMagma
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 multMagma
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 multMagma
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 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 Subgroup of G;
coherence
for b1 being Subgroup of G holds b1 is associative
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 unital Group-like associative Subgroup of G;
existence
ex b1 being Subgroup of G st b1 is strict
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 -> commutative Subgroup of G;
coherence
for b1 being Subgroup of G holds b1 is commutative 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
multMagma(# the carrier of G1, the multF of G1 #) = multMagma(# the carrier of G2, the multF 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
multMagma(# the carrier of H1, the multF of H1 #) = multMagma(# the carrier of H2, the multF 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
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 Th69;
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 Th70: :: GROUP_2:70
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 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
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 Th68;
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, b2 being strict Subgroup of G 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 :: 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;

registration
let G be Group;
cluster (1). G -> finite strict ;
coherence
(1). G is finite by Th80;
cluster non empty finite strict unital Group-like associative Subgroup of G;
existence
ex b1 being Subgroup of G st
( b1 is strict & b1 is finite )
proof end;
end;

registration
cluster non empty finite strict unital Group-like associative multMagma ;
existence
ex b1 being Group st
( b1 is strict & b1 is finite )
proof end;
end;

registration
let G be finite Group;
cluster -> finite Subgroup of G;
coherence
for b1 being Subgroup of G holds b1 is finite by Th48;
end;

theorem Th81: :: GROUP_2:81
for G being Group holds card ((1). G) = 1
proof end;

theorem Th82: :: GROUP_2:82
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:83
for G being Group
for H being Subgroup of G holds card H c= card G
proof end;

theorem :: GROUP_2:84
for G being finite Group
for H being Subgroup of G holds card H <= card G
proof end;

theorem :: GROUP_2:85
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 :: GROUP_2:86
canceled;

theorem :: GROUP_2:87
canceled;

theorem :: GROUP_2:88
canceled;

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
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 Th68;
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 :: 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 :: 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;

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:101
canceled;

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, 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: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 :: 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 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: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, 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: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
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: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 :: 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 :: 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 Th14;

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

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
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 :: 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 :: 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 :: 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 Th14;

theorem :: 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 :: 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 Th29;

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
( card H = card (a * H) & card H = card (H * a) )
proof end;

theorem Th156: :: GROUP_2:156
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: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 :: 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 ) ;

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

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 finite Group
for H being Subgroup of G holds card G = (card H) * (index H)
proof end;

theorem :: GROUP_2:178
for G being finite Group
for H being Subgroup of G holds card H divides card G
proof end;

theorem :: GROUP_2:179
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: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) = card G
proof end;

theorem :: GROUP_2:183
for G being finite Group holds index ((1). G) = card G
proof end;

theorem Th184: :: GROUP_2:184
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:185
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;

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;