:: Subgroup and Cosets of Subgroups. Lagrange theorem
:: by Wojciech A. Trybulec
::
:: Received July 23, 1990
:: Copyright (c) 1990-2012 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
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;
funcA "  ->  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
proofend;
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  }
proofend;
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 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:3
for G being Group
for g being Element of G holds {g} " = {(g ")}
proofend;

theorem :: GROUP_2:4
for G being Group
for g, h being Element of G holds {g,h} " = {(g "),(h ")}
proofend;

theorem :: GROUP_2:5
for G being Group holds ({} the carrier of G) " = {}
proofend;

theorem :: GROUP_2:6
for G being Group holds ([#] the carrier of G) " = the carrier of G
proofend;

theorem Th7: :: GROUP_2:7
for G being Group
for A being Subset of G holds
( A <> {} iff A " <> {} )
proofend;

registration
let G be Group;
let A be empty Subset of G;
clusterA "  ->  empty ;
coherence
 A " is empty by Th7;
end;

registration
let G be Group;
let A be non empty Subset of G;
clusterA "  ->  non empty ;
coherence
 not A " is empty by Th7;
end;

definition
let G be non empty multMagma ;
let A, B be Subset of G;
funcA * B ->  Subset of G equals :: GROUP_2:def 2
 {  (g * h) where g, h is Element of G : ( g in A &amp; h in B )  }  ;
coherence
  {  (g * h) where g, h is Element of G : ( g in A &amp; h in B )  }  is Subset of G
proofend;
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 &amp; h in B )  }  ;

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

theorem Th8: :: GROUP_2:8
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 &amp; g in A &amp; h in B ) ) ;

theorem Th9: :: GROUP_2:9
for G being non empty multMagma
for A, B being Subset of G holds
( ( A <> {} &amp; B <> {} ) iff A * B <> {} )
proofend;

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

theorem :: GROUP_2:11
for G being Group
for A, B being Subset of G holds (A * B) " = (B ") * (A ")
proofend;

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

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

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

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

theorem Th16: :: GROUP_2:16
for G being non empty multMagma
for A being Subset of G holds
( ({} the carrier of G) * A = {} &amp; A * ({} the carrier of G) = {} )
proofend;

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 &amp; A * ([#] the carrier of G) = the carrier of G )
proofend;

theorem Th18: :: GROUP_2:18
for G being non empty multMagma
for g, h being Element of G holds {g} * {h} = {(g * h)}
proofend;

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

theorem :: GROUP_2:20
for G being non empty multMagma
for g1, g2, g being Element of G holds {g1,g2} * {g} = {(g1 * g),(g2 * g)}
proofend;

theorem :: GROUP_2:21
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)}
proofend;

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 &amp; g2 in A holds
g1 * g2 in A ) &amp; ( for g being Element of G st g in A holds
g " in A ) holds
A * A = A
proofend;

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

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 &amp; b in B holds
a * b = b * a ) holds
A * B = B * A
proofend;

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

theorem :: GROUP_2:26
for G being commutative Group
for A, B being Subset of G holds (A * B) " = (A ") * (B ")
proofend;

definition
let G be non empty multMagma ;
let g be Element of G;
let A be Subset of G;
funcg * A ->  Subset of G equals :: GROUP_2:def 3
{g} * A;
correctness
coherence
{g} * A is Subset of G;
;
funcA * 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 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 &amp; h in A ) )
proofend;

theorem Th28: :: GROUP_2:28
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 &amp; h in A ) )
proofend;

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

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

theorem :: GROUP_2:35
for G being non empty multMagma
for a being Element of G holds
( ({} the carrier of G) * a = {} &amp; 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 &amp; 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 &amp; A * (1_ G) = A )
proofend;

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 &amp; 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 &amp; the multF of b1 = the multF of G || the carrier of b1 )
proofend;
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 &amp; 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
proofend;

theorem Th40: :: GROUP_2:40
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
proofend;

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

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

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 &amp; h2 = g2 holds
h1 * h2 = g1 * g2
proofend;

registration
let G be Group;
cluster  ->  associative for Subgroup of G;
coherence
 for b1 being Subgroup of G holds b1 is associative
proofend;
end;

theorem Th44: :: GROUP_2:44
for G being Group
for H being Subgroup of G holds 1_ H = 1_ G
proofend;

theorem :: GROUP_2:45
for G being Group
for H1, H2 being Subgroup of G holds 1_ H1 = 1_ H2
proofend;

theorem Th46: :: GROUP_2:46
for G being Group
for H being Subgroup of G holds 1_ G in H
proofend;

theorem :: GROUP_2:47
for G being Group
for H1, H2 being Subgroup of G holds 1_ H1 in H2
proofend;

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 "
proofend;

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

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 &amp; g2 in H holds
g1 * g2 in H
proofend;

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

registration
let G be Group;
cluster non empty strict unital Group-like associative for Subgroup of G;
existence
 ex b1 being Subgroup of G st b1 is strict
proofend;
end;

theorem Th52: :: GROUP_2:52
for G being Group
for A being Subset of G st A <> {} &amp; ( for g1, g2 being Element of G st g1 in A &amp; g2 in A holds
g1 * g2 in A ) &amp; ( 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
proofend;

theorem Th53: :: GROUP_2:53
for G being Group
for H being Subgroup of G st G is commutative Group holds
H is commutative
proofend;

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

theorem Th55: :: GROUP_2:55
for G1, G2 being Group st G1 is Subgroup of G2 &amp; G2 is Subgroup of G1 holds
multMagma(# the carrier of G1, the multF of G1 #) = multMagma(# the carrier of G2, the multF of G2 #)
proofend;

theorem Th56: :: GROUP_2:56
for G1, G2, G3 being Group st G1 is Subgroup of G2 &amp; G2 is Subgroup of G3 holds
G1 is Subgroup of G3
proofend;

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

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

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

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

definition
let G be Group;
let H1, H2 be strict Subgroup of G;
:: original:=
redefine predH1 = 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 #)
proofend;

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

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)}
proofend;
uniqueness
 for b1, b2 being strict Subgroup of G st the carrier of b1 = {(1_ G)} &amp; 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
proofend;
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
proofend;

theorem :: GROUP_2:64
for G being Group
for H1, H2 being Subgroup of G holds (1). H1 = (1). H2
proofend;

theorem Th65: :: GROUP_2:65
for G being Group
for H being Subgroup of G holds (1). G is Subgroup of H
proofend;

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

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 b1 being Subgroup of G st
( b1 is strict &amp; b1 is finite )
proofend;
end;

registration
cluster non empty finite strict unital Group-like associative for multMagma ;
existence
 ex b1 being Group st
( b1 is strict &amp; b1 is finite )
proofend;
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
proofend;

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

theorem :: GROUP_2:71
for G being Group
for H being Subgroup of G holds card H c= card G
proofend;

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

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

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 &amp; g2 in carr H holds
g1 * g2 in carr H
proofend;

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

theorem :: GROUP_2:76
for G being Group
for H being Subgroup of G holds (carr H) * (carr H) = carr H
proofend;

theorem :: GROUP_2:77
for G being Group
for H being Subgroup of G holds (carr H) " = carr H
proofend;

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) ) &amp; ( ex H being Subgroup of G st the carrier of H = (carr H1) * (carr H2) implies (carr H1) * (carr H2) = (carr H2) * (carr H1) ) )
proofend;

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

definition
let G be Group;
let H1, H2 be Subgroup of G;
funcH1 /\ 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)
proofend;
uniqueness
 for b1, b2 being strict Subgroup of G st the carrier of b1 = (carr H1) /\ (carr H2) &amp; 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 ) &amp; ( for H being strict Subgroup of G st the carrier of H = the carrier of H1 /\ the carrier of H2 holds
H = H1 /\ H2 ) )
proofend;

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 set
for G being Group
for H1, H2 being Subgroup of G holds
( x in H1 /\ H2 iff ( x in H1 &amp; x in H2 ) )
proofend;

theorem :: GROUP_2:83
for G being Group
for H being strict Subgroup of G holds H /\ H = H
proofend;

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

theorem :: GROUP_2:84
for G being Group
for H1, H2, H3 being Subgroup of G holds (H1 /\ H2) /\ H3 = H1 /\ (H2 /\ H3)
proofend;

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

theorem :: GROUP_2:85
for G being Group
for H being Subgroup of G holds
( ((1). G) /\ H = (1). G &amp; H /\ ((1). G) = (1). G )
proofend;

theorem :: GROUP_2:86
for G being strict Group
for H being strict Subgroup of G holds
( H /\ ((Omega). G) = H &amp; ((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
proofend;

theorem :: GROUP_2:88
for G being Group
for H1, H2 being Subgroup of G holds
( H1 /\ H2 is Subgroup of H1 &amp; 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
proofend;

theorem :: GROUP_2:91
for G being Group
for H1, H2, H3 being Subgroup of G st H1 is Subgroup of H2 &amp; H1 is Subgroup of H3 holds
H1 is Subgroup of H2 /\ H3
proofend;

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

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

definition
let G be Group;
let H be Subgroup of G;
let A be Subset of G;
funcA * H ->  Subset of G equals :: GROUP_2:def 11
A * (carr H);
correctness
coherence
A * (carr H) is Subset of G;
;
funcH * 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 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 &amp; g1 in A &amp; g2 in H ) )
proofend;

theorem :: GROUP_2:95
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 &amp; g1 in H &amp; g2 in A ) )
proofend;

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;
funca * H ->  Subset of G equals :: GROUP_2:def 13
a * (carr H);
correctness
coherence
a * (carr H) is Subset of G;
;
funcH * 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 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 &amp; g in H ) )
proofend;

theorem Th104: :: GROUP_2:104
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 &amp; g in H ) )
proofend;

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 &amp; a in H * a )
proofend;

theorem :: GROUP_2:109
for G being Group
for H being Subgroup of G holds
( (1_ G) * H = carr H &amp; 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} &amp; a * ((1). G) = {a} )
proofend;

theorem Th111: :: GROUP_2:111
for G being Group
for a being Element of G holds
( a * ((Omega). G) = the carrier of G &amp; ((Omega). G) * a = the carrier of G )
proofend;

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

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

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

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

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) &amp; carr H c= ((a ") * H) * (a * H) )
proofend;

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

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

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

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

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

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 ")) &amp; carr H c= (H * (a ")) * (H * a) )
proofend;

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

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

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

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

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

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

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

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 &amp; carr H,H * a are_equipotent )
proofend;

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

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 &amp; C = H * a &amp; card H = card B &amp; card H = card C )
proofend;

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 )
proofend;
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 ) ) &amp; ( for A being Subset of G holds
( A in b2 iff ex a being Element of G st A = a * H ) ) holds
b1 = b2
proofend;
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 )
proofend;
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 ) ) &amp; ( for A being Subset of G holds
( A in b2 iff ex a being Element of G st A = H * a ) ) holds
b1 = b2
proofend;
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 &amp; 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 &amp; carr H in Right_Cosets H )
proofend;

theorem Th136: :: GROUP_2:136
for G being Group
for H being Subgroup of G holds Left_Cosets H, Right_Cosets H are_equipotent
proofend;

theorem Th137: :: GROUP_2:137
for G being Group
for H being Subgroup of G holds
( union (Left_Cosets H) = the carrier of G &amp; union (Right_Cosets H) = the carrier of G )
proofend;

theorem Th138: :: GROUP_2:138
for G being Group holds Left_Cosets ((1). G) =  {  {a} where a is Element of G : verum  }
proofend;

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

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

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

theorem Th142: :: GROUP_2:142
for G being Group holds
( Left_Cosets ((Omega). G) = { the carrier of G} &amp; Right_Cosets ((Omega). G) = { the carrier of G} )
proofend;

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

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

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) &amp; Index H = card (Right_Cosets H) )
proofend;

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 &amp; it = card B );
existence
 ex b1 being Element of NAT ex B being finite set st
( B = Left_Cosets H &amp; b1 = card B )
proofend;
uniqueness
 for b1, b2 being Element of NAT st ex B being finite set st
( B = Left_Cosets H &amp; b1 = card B ) &amp; ex B being finite set st
( B = Left_Cosets H &amp; 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 &amp; 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 &amp; index H = card B ) &amp; ex C being finite set st
( C = Right_Cosets H &amp; index H = card C ) )
proofend;

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 &amp; card B = k &amp; ( for Z being set st Z in X &amp; Y <> Z holds
( Y,Z are_equipotent &amp; Y misses Z ) ) ) ) holds
ex C being finite set st
( C = union X &amp; card C = k * (card X) )
proofend;

:: [WP: ] 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)
proofend;

theorem :: GROUP_2:148
for G being finite Group
for H being Subgroup of G holds card H divides card G
proofend;

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

theorem :: GROUP_2:150
for G being Group holds index ((Omega). G) = 1
proofend;

theorem :: GROUP_2:151
for G being strict Group
for H being strict Subgroup of G st Left_Cosets H is finite &amp; index H = 1 holds
H = G
proofend;

theorem :: GROUP_2:152
for G being Group holds Index ((1). G) = card G
proofend;

theorem :: GROUP_2:153
for G being finite Group holds index ((1). G) = card G
proofend;

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

theorem :: GROUP_2:155
for G being Group
for H being strict Subgroup of G st Left_Cosets H is finite &amp; Index H = card G holds
( G is finite &amp; H = (1). G )
proofend;

::
:: 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 &amp; card B = k &amp; ( for Z being set st Z in X &amp; Y <> Z holds
( Y,Z are_equipotent &amp; Y misses Z ) ) ) ) holds
ex C being finite set st
( C = union X &amp; card C = k * (card X) ) by Lm5;