:: Subgroup and Cosets of Subgroups. Lagrange theorem
:: by Wojciech A. Trybulec
::
:: Received July 23, 1990
:: Copyright (c) 1990-2021 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, XBOOLE_0, STRUCT_0, SUBSET_1, FINSET_1, NAT_1, GROUP_1,
RELAT_1, TARSKI, ALGSTR_0, BINOP_1, REALSET1, ZFMISC_1, FUNCT_1, RLSUB_1,
CARD_1, XXREAL_0, NEWTON, SETFAM_1, CQC_SIM1, FINSUB_1, SETWISEO,
ARYTM_3, GROUP_2;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, FINSUB_1, FINSET_1,
REALSET1, XCMPLX_0, XXREAL_0, CARD_1, ORDINAL1, NUMBERS, STRUCT_0,
ALGSTR_0, GROUP_1, WELLORD2, BINOP_1, SETWISEO, DOMAIN_1, RELAT_1,
FUNCT_1, RELSET_1, NAT_1, NAT_D, MCART_1;
constructors SETFAM_1, PARTFUN1, WELLORD2, BINOP_1, SETWISEO, XXREAL_0, NAT_1,
NAT_D, MEMBERED, REALSET1, GROUP_1, RELSET_1;
registrations SUBSET_1, RELSET_1, FINSET_1, FINSUB_1, MEMBERED, REALSET1,
STRUCT_0, GROUP_1, ALGSTR_0, CARD_1, ORDINAL1, XCMPLX_0;
requirements NUMERALS, BOOLE, SUBSET, ARITHM;
begin
reserve x for object;
reserve G for non empty 1-sorted;
reserve A for Subset of G;
theorem :: GROUP_2:1
G is finite implies A is finite;
reserve y,y1,y2,Y,Z for set;
reserve k for Nat;
reserve G for Group;
reserve a,g,h for Element of G;
reserve A for Subset of G;
definition
let G,A;
func A" -> Subset of G equals
:: GROUP_2:def 1
{g" : g in A};
involutiveness;
end;
theorem :: GROUP_2:2
x in A" iff ex g st x = g" & g in A;
theorem :: GROUP_2:3
{g}" = {g"};
theorem :: GROUP_2:4
{g,h}" = {g",h"};
theorem :: GROUP_2:5
({}(the carrier of G))" = {};
theorem :: GROUP_2:6
([#](the carrier of G))" = the carrier of G;
theorem :: GROUP_2:7
A <> {} iff A" <> {};
registration
let G;
let A be empty Subset of G;
cluster A" -> empty;
end;
registration
let G;
let A be non empty Subset of G;
cluster A" -> non empty;
end;
reserve G for non empty multMagma,
A,B,C for Subset of G;
reserve a,b,g,g1,g2,h,h1,h2 for Element of G;
definition
let G;
let A,B;
func A * B -> Subset of G equals
:: GROUP_2:def 2
{g * h : g in A & h in B};
end;
definition
let G be commutative non empty multMagma;
let A,B be Subset of G;
redefine func A * B;
commutativity;
end;
theorem :: GROUP_2:8
x in A * B iff ex g,h st x = g * h & g in A & h in B;
theorem :: GROUP_2:9
A <> {} & B <> {} iff A * B <> {};
theorem :: GROUP_2:10
G is associative implies A * B * C = A * (B * C);
theorem :: GROUP_2:11
for G being Group, A,B being Subset of G holds (A * B)" = B" * A";
theorem :: GROUP_2:12
A * (B \/ C) = A * B \/ A * C;
theorem :: GROUP_2:13
(A \/ B) * C = A * C \/ B * C;
theorem :: GROUP_2:14
A * (B /\ C) c= (A * B) /\ (A * C);
theorem :: GROUP_2:15
(A /\ B) * C c= (A * C) /\ (B * C);
theorem :: GROUP_2:16
{}(the carrier of G) * A = {} & A * {}(the carrier of G) = {};
theorem :: GROUP_2:17
for G being Group, A being Subset of G holds A <> {} implies [#]
(the carrier of G) * A = the carrier of G & A * [#](the carrier of G) = the
carrier of G;
theorem :: GROUP_2:18
{g} * {h} = {g * h};
theorem :: GROUP_2:19
{g} * {g1,g2} = {g * g1,g * g2};
theorem :: GROUP_2:20
{g1,g2} * {g} = {g1 * g,g2 * g};
theorem :: GROUP_2:21
{g,h} * {g1,g2} = {g * g1, g * g2, h * g1, h * g2};
theorem :: GROUP_2:22
for G being Group, A being Subset of G holds (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) implies A * A = A;
theorem :: GROUP_2:23
for G being Group, A being Subset of G holds (for g being
Element of G st g in A holds g" in A) implies A" = A;
theorem :: GROUP_2:24
(for a,b st a in A & b in B holds a * b = b * a) implies A * B = B * A;
theorem :: GROUP_2:25
G is commutative Group implies A * B = B * A;
theorem :: GROUP_2:26
for G being commutative Group, A,B being Subset of G holds (A * B)" = A" * B"
;
definition
let G,g,A;
func g * A -> Subset of G equals
:: GROUP_2:def 3
{g} * A;
func A * g -> Subset of G equals
:: GROUP_2:def 4
A * {g};
end;
theorem :: GROUP_2:27
x in g * A iff ex h st x = g * h & h in A;
theorem :: GROUP_2:28
x in A * g iff ex h st x = h * g & h in A;
theorem :: GROUP_2:29
G is associative implies g * A * B = g * (A * B);
theorem :: GROUP_2:30
G is associative implies A * g * B = A * (g * B);
theorem :: GROUP_2:31
G is associative implies A * B * g = A * (B * g);
theorem :: GROUP_2:32
G is associative implies g * h * A = g * (h * A);
theorem :: GROUP_2:33
G is associative implies g * A * h = g * (A * h);
theorem :: GROUP_2:34
G is associative implies A * g * h = A * (g * h);
theorem :: GROUP_2:35
{}(the carrier of G) * a = {} & a * {}(the carrier of G) = {};
reserve G for Group-like non empty multMagma;
reserve h,g,g1,g2 for Element of G;
reserve A for Subset of G;
theorem :: GROUP_2:36
for G being Group, a being Element of G holds [#](the carrier of G) *
a = the carrier of G & a * [#](the carrier of G) = the carrier of G;
theorem :: GROUP_2:37
1_G * A = A & A * 1_G = A;
theorem :: GROUP_2:38
G is commutative Group implies g * A = A * g;
definition
let G be Group-like non empty multMagma;
mode Subgroup of G -> Group-like non empty multMagma means
:: 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;
end;
reserve H for Subgroup of G;
reserve h,h1,h2 for Element of H;
theorem :: GROUP_2:39
G is finite implies H is finite;
theorem :: GROUP_2:40
x in H implies x in G;
theorem :: GROUP_2:41
h in G;
theorem :: GROUP_2:42
h is Element of G;
theorem :: GROUP_2:43
h1 = g1 & h2 = g2 implies h1 * h2 = g1 * g2;
registration
let G be Group;
cluster -> associative for Subgroup of G;
end;
reserve G,G1,G2,G3 for Group;
reserve a,a1,a2,b,b1,b2,g,g1,g2 for Element of G;
reserve A,B for Subset of G;
reserve H,H1,H2,H3 for Subgroup of G;
reserve h,h1,h2 for Element of H;
theorem :: GROUP_2:44
1_H = 1_G;
theorem :: GROUP_2:45
1_H1 = 1_H2;
theorem :: GROUP_2:46
1_G in H;
theorem :: GROUP_2:47
1_H1 in H2;
theorem :: GROUP_2:48
h = g implies h" = g";
theorem :: GROUP_2:49
inverse_op(H) = inverse_op(G) | the carrier of H;
theorem :: GROUP_2:50
g1 in H & g2 in H implies g1 * g2 in H;
theorem :: GROUP_2:51
g in H implies g" in H;
registration
let G;
cluster strict for Subgroup of G;
end;
theorem :: GROUP_2:52
A <> {} & (for g1,g2 st g1 in A & g2 in A holds g1 * g2 in A) &
(for g st g in A holds g" in A) implies ex H being strict Subgroup of G st the
carrier of H = A;
theorem :: GROUP_2:53
G is commutative Group implies H is commutative;
registration
let G be commutative Group;
cluster -> commutative for Subgroup of G;
end;
theorem :: GROUP_2:54
G is Subgroup of G;
theorem :: GROUP_2:55
G1 is Subgroup of G2 & G2 is Subgroup of G1 implies the
multMagma of G1 = the multMagma of G2;
theorem :: GROUP_2:56
G1 is Subgroup of G2 & G2 is Subgroup of G3 implies G1 is Subgroup of G3;
theorem :: GROUP_2:57
the carrier of H1 c= the carrier of H2 implies H1 is Subgroup of H2;
theorem :: GROUP_2:58
(for g st g in H1 holds g in H2) implies H1 is Subgroup of H2;
theorem :: GROUP_2:59
the carrier of H1 = the carrier of H2 implies the multMagma of
H1 = the multMagma of H2;
theorem :: GROUP_2:60
(for g holds g in H1 iff g in H2) implies the multMagma of H1 =
the multMagma of H2;
definition
let G;
let H1,H2 be strict Subgroup of G;
redefine pred H1 = H2 means
:: GROUP_2:def 6
for g holds g in H1 iff g in H2;
end;
theorem :: GROUP_2:61
for G being Group, H being Subgroup of G st the carrier of G c=
the carrier of H holds the multMagma of H = the multMagma of G;
theorem :: GROUP_2:62
(for g being Element of G holds g in H) implies the multMagma of
H = the multMagma of G;
definition
let G;
func (1).G -> strict Subgroup of G means
:: GROUP_2:def 7
the carrier of it = {1_G};
end;
definition
let G;
func (Omega).G -> strict Subgroup of G equals
:: GROUP_2:def 8
the multMagma of G;
projectivity;
end;
theorem :: GROUP_2:63
(1).H = (1).G;
theorem :: GROUP_2:64
(1).H1 = (1).H2;
theorem :: GROUP_2:65
(1).G is Subgroup of H;
theorem :: GROUP_2:66
for G being strict Group, 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 :: GROUP_2:68
(1).G is finite;
registration
let G;
cluster (1).G -> finite;
cluster strict finite for Subgroup of G;
end;
registration
cluster strict finite for Group;
end;
registration
let G be finite Group;
cluster -> finite for Subgroup of G;
end;
theorem :: GROUP_2:69
card (1).G = 1;
theorem :: GROUP_2:70
for H being strict finite Subgroup of G holds card H = 1 implies H = (1).G;
theorem :: GROUP_2:71
card H c= card G;
theorem :: GROUP_2:72
for G being finite Group, H being Subgroup of G holds card H <= card G;
theorem :: GROUP_2:73
for G being finite Group, H being Subgroup of G holds card G = card H
implies the multMagma of H = the multMagma of G;
definition
let G,H;
func carr(H) -> Subset of G equals
:: GROUP_2:def 9
the carrier of H;
end;
theorem :: GROUP_2:74
g1 in carr(H) & g2 in carr(H) implies g1 * g2 in carr(H);
theorem :: GROUP_2:75
g in carr(H) implies g" in carr(H);
theorem :: GROUP_2:76
carr(H) * carr(H) = carr(H);
theorem :: GROUP_2:77
carr(H)" = carr H;
theorem :: GROUP_2:78
(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 st the carrier
of H = carr H1 * carr H2) implies carr H1 * carr H2 = carr H2 * carr H1);
theorem :: GROUP_2:79
G is commutative Group implies ex H being strict Subgroup of G st the
carrier of H = carr(H1) * carr(H2);
definition
let G,H1,H2;
func H1 /\ H2 -> strict Subgroup of G means
:: GROUP_2:def 10
the carrier of it = carr (H1) /\ carr(H2);
end;
theorem :: GROUP_2:80
(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 holds the carrier of H = (the carrier of H1) /\ (the carrier of H2)
implies H = H1 /\ H2;
theorem :: GROUP_2:81
carr(H1 /\ H2) = carr(H1) /\ carr(H2);
theorem :: GROUP_2:82
x in H1 /\ H2 iff x in H1 & x in H2;
theorem :: GROUP_2:83
for H being strict Subgroup of G holds H /\ H = H;
definition
let G,H1,H2;
redefine func H1 /\ H2;
commutativity;
end;
theorem :: GROUP_2:84
H1 /\ H2 /\ H3 = H1 /\ (H2 /\ H3);
theorem :: GROUP_2:85
(1).G /\ H = (1).G & H /\ (1).G = (1).G;
theorem :: GROUP_2:86
for G being strict Group, H being strict Subgroup of G holds H /\
(Omega).G = H & (Omega).G /\ H = H;
theorem :: GROUP_2:87
for G being strict Group holds (Omega).G /\ (Omega).G = G;
theorem :: GROUP_2:88
H1 /\ H2 is Subgroup of H1 & H1 /\ H2 is Subgroup of H2;
theorem :: GROUP_2:89
for H1 being Subgroup of G holds H1 is Subgroup of H2 iff the
multMagma of (H1 /\ H2) = the multMagma of H1;
theorem :: GROUP_2:90
H1 is Subgroup of H2 implies H1 /\ H3 is Subgroup of H2;
theorem :: GROUP_2:91
H1 is Subgroup of H2 & H1 is Subgroup of H3 implies H1 is Subgroup of
H2 /\ H3;
theorem :: GROUP_2:92
H1 is Subgroup of H2 implies H1 /\ H3 is Subgroup of H2 /\ H3;
theorem :: GROUP_2:93
H1 is finite or H2 is finite implies H1 /\ H2 is finite;
definition
let G,H,A;
func A * H -> Subset of G equals
:: GROUP_2:def 11
A * carr H;
func H * A -> Subset of G equals
:: GROUP_2:def 12
carr H * A;
end;
theorem :: GROUP_2:94
x in A * H iff ex g1,g2 st x = g1 * g2 & g1 in A & g2 in H;
theorem :: GROUP_2:95
x in H * A iff ex g1,g2 st x = g1 * g2 & g1 in H & g2 in A;
theorem :: GROUP_2:96
A * B * H = A * (B * H);
theorem :: GROUP_2:97
A * H * B = A * (H * B);
theorem :: GROUP_2:98
H * A * B = H * (A * B);
theorem :: GROUP_2:99
A * H1 * H2 = A * (H1 * carr H2);
theorem :: GROUP_2:100
H1 * A * H2 = H1 * (A * H2);
theorem :: GROUP_2:101
H1 * carr(H2) * A = H1 * (H2 * A);
theorem :: GROUP_2:102
G is commutative Group implies A * H = H * A;
definition
let G,H,a;
func a * H -> Subset of G equals
:: GROUP_2:def 13
a * carr(H);
func H * a -> Subset of G equals
:: GROUP_2:def 14
carr(H) * a;
end;
theorem :: GROUP_2:103
x in a * H iff ex g st x = a * g & g in H;
theorem :: GROUP_2:104
x in H * a iff ex g st x = g * a & g in H;
theorem :: GROUP_2:105
a * b * H = a * (b * H);
theorem :: GROUP_2:106
a * H * b = a * (H * b);
theorem :: GROUP_2:107
H * a * b = H * (a * b);
theorem :: GROUP_2:108
a in a * H & a in H * a;
theorem :: GROUP_2:109
1_G * H = carr(H) & H * 1_G = carr(H);
theorem :: GROUP_2:110
(1).G * a = {a} & a * (1).G = {a};
theorem :: GROUP_2:111
a * (Omega).G = the carrier of G & (Omega).G * a = the carrier of G;
theorem :: GROUP_2:112
G is commutative Group implies a * H = H * a;
theorem :: GROUP_2:113
a in H iff a * H = carr(H);
theorem :: GROUP_2:114
a * H = b * H iff b" * a in H;
theorem :: GROUP_2:115
a * H = b * H iff a * H meets b * H;
theorem :: GROUP_2:116
a * b * H c= (a * H) * (b * H);
theorem :: GROUP_2:117
carr(H) c= (a * H) * (a" * H) & carr(H) c= (a" * H) * (a * H);
theorem :: GROUP_2:118
a |^ 2 * H c= (a * H) * (a * H);
theorem :: GROUP_2:119
a in H iff H * a = carr(H);
theorem :: GROUP_2:120
H * a = H * b iff b * a" in H;
theorem :: GROUP_2:121
H * a = H * b iff H * a meets H * b;
theorem :: GROUP_2:122
H * a * b c= (H * a) * (H * b);
theorem :: GROUP_2:123
carr(H) c= (H * a) * (H * a") & carr(H) c= (H * a") * (H * a);
theorem :: GROUP_2:124
H * (a |^ 2) c= (H * a) * (H * a);
theorem :: GROUP_2:125
a * (H1 /\ H2) = (a * H1) /\ (a * H2);
theorem :: GROUP_2:126
(H1 /\ H2) * a = (H1 * a) /\ (H2 * a);
theorem :: GROUP_2:127
ex H1 being strict Subgroup of G st the carrier of H1 = a * H2 * a";
theorem :: GROUP_2:128
a * H,b * H are_equipotent;
theorem :: GROUP_2:129
a * H,H * b are_equipotent;
theorem :: GROUP_2:130
H * a,H * b are_equipotent;
theorem :: GROUP_2:131
carr(H),a * H are_equipotent & carr(H),H * a are_equipotent;
theorem :: GROUP_2:132
card(H) = card(a * H) & card(H) = card(H * a);
theorem :: GROUP_2:133
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;
definition
let G,H;
func Left_Cosets H -> Subset-Family of G means
:: GROUP_2:def 15
A in it iff ex a st A = a * H;
func Right_Cosets H -> Subset-Family of G means
:: GROUP_2:def 16
A in it iff ex a st A = H * a;
end;
theorem :: GROUP_2:134
G is finite implies Right_Cosets H is finite & Left_Cosets H is finite;
theorem :: GROUP_2:135
carr H in Left_Cosets H & carr H in Right_Cosets H;
theorem :: GROUP_2:136
Left_Cosets H, Right_Cosets H are_equipotent;
theorem :: GROUP_2:137
union Left_Cosets H = the carrier of G & union Right_Cosets H =
the carrier of G;
theorem :: GROUP_2:138
Left_Cosets (1).G = the set of all {a};
theorem :: GROUP_2:139
Right_Cosets (1).G = the set of all {a};
theorem :: GROUP_2:140
for H being strict Subgroup of G holds Left_Cosets H = the set of all {a}
implies H = (1).G;
theorem :: GROUP_2:141
for H being strict Subgroup of G holds Right_Cosets H = the set of all {a}
implies H = (1).G;
theorem :: GROUP_2:142
Left_Cosets (Omega).G = {the carrier of G} & Right_Cosets
(Omega).G = {the carrier of G};
theorem :: GROUP_2:143
for G being strict Group, H being strict Subgroup of G holds
Left_Cosets H = {the carrier of G} implies H = G;
theorem :: GROUP_2:144
for G being strict Group, H being strict Subgroup of G holds
Right_Cosets H = {the carrier of G} implies H = G;
definition
let G,H;
func Index H -> Cardinal equals
:: GROUP_2:def 17
card Left_Cosets H;
end;
theorem :: GROUP_2:145
Index H = card Left_Cosets H & Index H = card Right_Cosets H;
definition
let G,H;
assume
Left_Cosets(H) is finite;
func index H -> Element of NAT means
:: GROUP_2:def 18
ex B being finite set st B = Left_Cosets H & it = card B;
end;
theorem :: GROUP_2:146
Left_Cosets H is finite implies (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;
::$N Lagrange Theorem for Groups
theorem :: GROUP_2:147
for G being finite Group, H being Subgroup of G holds card G =
card H * index H;
theorem :: GROUP_2:148
for G being finite Group, H being Subgroup of G holds card H divides card G;
theorem :: GROUP_2:149
for G being finite Group, I, H being Subgroup of G, J being Subgroup
of H holds I = J implies index I = index J * index H;
theorem :: GROUP_2:150
index (Omega).G = 1;
theorem :: GROUP_2:151
for G being strict Group, H being strict Subgroup of G holds
Left_Cosets H is finite & index H = 1 implies H = G;
theorem :: GROUP_2:152
Index (1).G = card G;
theorem :: GROUP_2:153
for G being finite Group holds index (1).G = card G;
theorem :: GROUP_2:154
for G being finite Group, H being strict Subgroup of G holds
index H = card G implies H = (1).G;
theorem :: GROUP_2:155
for H being strict Subgroup of G holds Left_Cosets H is finite & Index
H = card G implies G is finite & H = (1).G;
::
:: Auxiliary theorems.
::
theorem :: GROUP_2:156
for X being finite set st (for Y st Y in X ex B being finite set st B
= Y & card B = k & for Z st Z in X & Y <> Z holds Y,Z are_equipotent & Y misses
Z) ex C being finite set st C = union X & card C = k * card X;