:: Subgroup and Cosets of Subgroups. Lagrange theorem
:: by Wojciech A. Trybulec
::
:: Received July 23, 1990
:: Copyright (c) 1990-2026 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;
definitions FUNCT_1, GROUP_1, STRUCT_0, TARSKI, XBOOLE_0;
equalities STRUCT_0, XBOOLE_0, BINOP_1, REALSET1, SUBSET_1, ALGSTR_0;
expansions GROUP_1, STRUCT_0, TARSKI, XBOOLE_0;
theorems CARD_1, CARD_2, ENUMSET1, FINSET_1, FINSUB_1, FUNCT_1, FUNCT_2,
GROUP_1, TARSKI, WELLORD2, ZFMISC_1, RELAT_1, RELSET_1, XBOOLE_0,
XBOOLE_1, XCMPLX_1, NAT_D, STRUCT_0, NAT_1;
schemes FUNCT_1, SUBSET_1, SETWISEO, CLASSES1;
begin
reserve x for object;
reserve G for non empty 1-sorted;
reserve A for Subset of G;
Lm1: x in A implies x is Element of G;
theorem
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
{g" : g in A};
coherence
proof
set F = {g" : g in A};
F c= the carrier of G
proof
let x be object;
assume x in F;
then ex g st x = g" & g in A;
hence thesis;
end;
hence thesis;
end;
involutiveness
proof
let R, B be Subset of G;
assume
A1: R = {g" : g in B};
thus B c= {g" : g in R}
proof
let a be object;
assume
A2: a in B;
then reconsider a as Element of G;
a"" = a & a" in R by A1,A2;
hence thesis;
end;
let a be object;
assume a in {g" : g in R};
then consider g such that
A3: a = g" and
A4: g in R;
ex h st g = h" & h in B by A1,A4;
hence thesis by A3;
end;
end;
theorem Th2:
x in A" iff ex g st x = g" & g in A;
theorem
{g}" = {g"}
proof
thus {g}" c= {g"}
proof
let x be object;
assume x in {g}";
then consider h such that
A1: x = h" and
A2: h in {g};
h = g by A2,TARSKI:def 1;
hence thesis by A1,TARSKI:def 1;
end;
let x be object;
assume x in {g"};
then
A3: x = g" by TARSKI:def 1;
g in {g} by TARSKI:def 1;
hence thesis by A3;
end;
theorem
{g,h}" = {g",h"}
proof
thus {g,h}" c= {g",h"}
proof
let x be object;
assume x in {g,h}";
then consider a such that
A1: x = a" and
A2: a in {g,h};
a = g or a = h by A2,TARSKI:def 2;
hence thesis by A1,TARSKI:def 2;
end;
let x be object;
assume x in {g",h"};
then
A3: x = g" or x = h" by TARSKI:def 2;
g in {g,h} & h in {g,h} by TARSKI:def 2;
hence thesis by A3;
end;
theorem
({}(the carrier of G))" = {}
proof
thus ({}(the carrier of G))" c= {}
proof
let x be object;
assume x in ({}(the carrier of G))";
then ex a st x = a" & a in {}the carrier of G;
hence thesis;
end;
thus thesis;
end;
theorem
([#](the carrier of G))" = the carrier of G
proof
thus ([#](the carrier of G))" c= the carrier of G;
let x be object;
assume x in the carrier of G;
then reconsider a = x as Element of G;
a"" in ([#](the carrier of G))";
hence thesis;
end;
theorem Th7:
A <> {} iff A" <> {}
proof
set x = the Element of A";
thus A <> {} implies A" <> {}
proof
set x = the Element of A;
assume
A1: A <> {};
then reconsider x as Element of G by Lm1;
x" in A" by A1;
hence thesis;
end;
assume A" <> {};
then ex a st x = a" & a in A by Th2;
hence thesis;
end;
registration
let G;
let A be empty Subset of G;
cluster A" -> empty;
coherence by Th7;
end;
registration
let G;
let A be non empty Subset of G;
cluster A" -> non empty;
coherence by Th7;
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
{g * h : g in A & h in B};
coherence
proof
set S = {g * h : g in A & h in B};
S c= the carrier of G
proof
let x be object;
assume x in S;
then ex g,h st x = g * h & g in A & h in B;
hence thesis;
end;
hence thesis;
end;
end;
definition
let G be commutative non empty multMagma;
let A,B be Subset of G;
redefine func A * B; :: redefines * (GROUP_2, definition)
commutativity
proof
let A,B be Subset of G;
thus A*B c= B*A
proof
let x be object;
assume x in A*B;
then ex g,h being Element of G st x = g*h & g in A & h in B;
hence thesis;
end;
let x be object;
assume x in B*A;
then ex g,h being Element of G st x = g*h & g in B & h in A;
hence thesis;
end;
end;
theorem Th8:
x in A * B iff ex g,h st x = g * h & g in A & h in B;
theorem Th9:
A <> {} & B <> {} iff A * B <> {}
proof
thus A <> {} & B <> {} implies A * B <> {}
proof
assume
A1: A <> {};
then reconsider x = the Element of A as Element of G by TARSKI:def 3;
assume
A2: B <> {};
then reconsider y = the Element of B as Element of G by TARSKI:def 3;
x * y in A * B by A1,A2;
hence thesis;
end;
set x = the Element of A * B;
assume A * B <> {};
then ex a,b st x = a * b & a in A & b in B by Th8;
hence thesis;
end;
theorem Th10:
G is associative implies A * B * C = A * (B * C)
proof
assume
A1: G is associative;
thus A * B * C c= A * (B * C)
proof
let x be object;
assume x in A * B * C;
then consider g,h such that
A2: x = g * h and
A3: g in A * B and
A4: h in C;
consider g1,g2 such that
A5: g = g1 * g2 and
A6: g1 in A and
A7: g2 in B by A3;
x = g1 * (g2 * h) & g2 * h in B * C by A1,A2,A4,A5,A7;
hence thesis by A6;
end;
let x be object;
assume x in A * (B * C);
then consider g,h such that
A8: x = g * h and
A9: g in A and
A10: h in B * C;
consider g1,g2 such that
A11: h = g1 * g2 and
A12: g1 in B and
A13: g2 in C by A10;
A14: g * g1 in A * B by A9,A12;
x = g * g1 * g2 by A1,A8,A11;
hence thesis by A13,A14;
end;
theorem
for G being Group, A,B being Subset of G holds (A * B)" = B" * A"
proof
let G be Group, A,B be Subset of G;
thus (A * B)" c= B" * A"
proof
let x be object;
assume x in (A * B)";
then consider g being Element of G such that
A1: x = g" and
A2: g in A * B;
consider g1,g2 being Element of G such that
A3: g = g1 * g2 and
A4: g1 in A & g2 in B by A2;
A5: g1" in A" & g2" in B" by A4;
x = g2" * g1" by A1,A3,GROUP_1:17;
hence thesis by A5;
end;
let x be object;
assume x in B" * A";
then consider g1,g2 being Element of G such that
A6: x = g1 * g2 and
A7: g1 in B" and
A8: g2 in A";
consider b being Element of G such that
A9: g2 = b" and
A10: b in A by A8;
consider a being Element of G such that
A11: g1 = a" and
A12: a in B by A7;
A13: b * a in A * B by A12,A10;
x = (b * a)" by A6,A11,A9,GROUP_1:17;
hence thesis by A13;
end;
theorem
A * (B \/ C) = A * B \/ A * C
proof
thus A * (B \/ C) c= A * B \/ A * C
proof
let x be object;
assume x in A * (B \/ C);
then consider g1,g2 such that
A1: x = g1 * g2 & g1 in A and
A2: g2 in B \/ C;
g2 in B or g2 in C by A2,XBOOLE_0:def 3;
then x in A * B or x in A * C by A1;
hence thesis by XBOOLE_0:def 3;
end;
let x be object;
assume
A3: x in A * B \/ A * C;
now
per cases by A3,XBOOLE_0:def 3;
suppose
x in A * B;
then consider g1,g2 such that
A4: x = g1 * g2 & g1 in A and
A5: g2 in B;
g2 in B \/ C by A5,XBOOLE_0:def 3;
hence thesis by A4;
end;
suppose
x in A * C;
then consider g1,g2 such that
A6: x = g1 * g2 & g1 in A and
A7: g2 in C;
g2 in B \/ C by A7,XBOOLE_0:def 3;
hence thesis by A6;
end;
end;
hence thesis;
end;
theorem
(A \/ B) * C = A * C \/ B * C
proof
thus (A \/ B) * C c= A * C \/ B * C
proof
let x be object;
assume x in (A \/ B) * C;
then consider g1,g2 such that
A1: x = g1 * g2 and
A2: g1 in A \/ B and
A3: g2 in C;
g1 in A or g1 in B by A2,XBOOLE_0:def 3;
then x in A * C or x in B * C by A1,A3;
hence thesis by XBOOLE_0:def 3;
end;
let x be object;
assume
A4: x in A * C \/ B * C;
now
per cases by A4,XBOOLE_0:def 3;
suppose
x in A * C;
then consider g1,g2 such that
A5: x = g1 * g2 and
A6: g1 in A and
A7: g2 in C;
g1 in A \/ B by A6,XBOOLE_0:def 3;
hence thesis by A5,A7;
end;
suppose
x in B * C;
then consider g1,g2 such that
A8: x = g1 * g2 and
A9: g1 in B and
A10: g2 in C;
g1 in A \/ B by A9,XBOOLE_0:def 3;
hence thesis by A8,A10;
end;
end;
hence thesis;
end;
theorem
A * (B /\ C) c= (A * B) /\ (A * C)
proof
let x be object;
assume x in A * (B /\ C);
then consider g1,g2 such that
A1: x = g1 * g2 & g1 in A and
A2: g2 in B /\ C;
g2 in C by A2,XBOOLE_0:def 4;
then
A3: x in A * C by A1;
g2 in B by A2,XBOOLE_0:def 4;
then x in A * B by A1;
hence thesis by A3,XBOOLE_0:def 4;
end;
theorem
(A /\ B) * C c= (A * C) /\ (B * C)
proof
let x be object;
assume x in (A /\ B) * C;
then consider g1,g2 such that
A1: x = g1 * g2 and
A2: g1 in A /\ B and
A3: g2 in C;
g1 in B by A2,XBOOLE_0:def 4;
then
A4: x in B * C by A1,A3;
g1 in A by A2,XBOOLE_0:def 4;
then x in A * C by A1,A3;
hence thesis by A4,XBOOLE_0:def 4;
end;
theorem Th16:
{}(the carrier of G) * A = {} & A * {}(the carrier of G) = {}
proof
A1: now
set x = the Element of A * {}(the carrier of G);
assume A * {}(the carrier of G) <> {};
then ex g1,g2 st x = g1 * g2 & g1 in A & g2 in {}(the carrier of G) by Th8;
hence contradiction;
end;
now
set x = the Element of {}(the carrier of G) * A;
assume {}(the carrier of G) * A <> {};
then ex g1,g2 st x = g1 * g2 & g1 in {}(the carrier of G) & g2 in A by Th8;
hence contradiction;
end;
hence thesis by A1;
end;
theorem Th17:
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
proof
let G be Group, A be Subset of G;
set y = the Element of A;
assume
A1: A <> {};
then reconsider y as Element of G by Lm1;
thus [#](the carrier of G) * A = the carrier of G
proof
set y = the Element of A;
reconsider y as Element of G by A1,Lm1;
thus [#](the carrier of G) * A c= the carrier of G;
let x be object;
assume x in the carrier of G;
then reconsider a = x as Element of G;
(a * y") * y = a * (y" * y) by GROUP_1:def 3
.= a * 1_G by GROUP_1:def 5
.= a by GROUP_1:def 4;
hence thesis by A1;
end;
thus A * [#](the carrier of G) c= the carrier of G;
let x be object;
assume x in the carrier of G;
then reconsider a = x as Element of G;
y * (y" * a) = (y * y") * a by GROUP_1:def 3
.= 1_G * a by GROUP_1:def 5
.= a by GROUP_1:def 4;
hence thesis by A1;
end;
theorem Th18:
{g} * {h} = {g * h}
proof
thus {g} * {h} c= {g * h}
proof
let x be object;
assume x in {g} * {h};
then consider g1,g2 such that
A1: x = g1 * g2 and
A2: g1 in {g} & g2 in {h};
g1 = g & g2 = h by A2,TARSKI:def 1;
hence thesis by A1,TARSKI:def 1;
end;
let x be object;
assume x in {g * h};
then
A3: x = g * h by TARSKI:def 1;
g in {g} & h in {h} by TARSKI:def 1;
hence thesis by A3;
end;
theorem
{g} * {g1,g2} = {g * g1, g * g2}
proof
thus {g} * {g1,g2} c= {g * g1, g * g2}
proof
let x be object;
assume x in {g} * {g1,g2};
then consider h1,h2 such that
A1: x = h1 * h2 and
A2: h1 in {g} and
A3: h2 in {g1,g2};
A4: h2 = g1 or h2 = g2 by A3,TARSKI:def 2;
h1 = g by A2,TARSKI:def 1;
hence thesis by A1,A4,TARSKI:def 2;
end;
let x be object;
A5: g2 in {g1,g2 } by TARSKI:def 2;
assume x in {g * g1,g * g2};
then
A6: x = g * g1 or x = g * g2 by TARSKI:def 2;
g in {g} & g1 in {g1,g2} by TARSKI:def 1,def 2;
hence thesis by A6,A5;
end;
theorem
{g1,g2} * {g} = {g1 * g, g2 * g}
proof
thus {g1,g2} * {g} c= {g1 * g, g2 * g}
proof
let x be object;
assume x in {g1,g2} * {g};
then consider h1,h2 such that
A1: x = h1 * h2 and
A2: h1 in {g1,g2} and
A3: h2 in {g};
A4: h1 = g1 or h1 = g2 by A2,TARSKI:def 2;
h2 = g by A3,TARSKI:def 1;
hence thesis by A1,A4,TARSKI:def 2;
end;
let x be object;
A5: g2 in {g1,g2 } by TARSKI:def 2;
assume x in {g1 * g,g2 * g};
then
A6: x = g1 * g or x = g2 * g by TARSKI:def 2;
g in {g} & g1 in {g1,g2} by TARSKI:def 1,def 2;
hence thesis by A6,A5;
end;
theorem
{g,h} * {g1,g2} = {g * g1, g * g2, h * g1, h * g2}
proof
set A = {g,h} * {g1,g2};
set B = {g * g1, g * g2, h * g1, h * g2};
thus A c= B
proof
let x be object;
assume x in A;
then consider h1,h2 such that
A1: x = h1 * h2 and
A2: h1 in {g,h} and
A3: h2 in {g1,g2};
A4: h2 = g1 or h2 = g2 by A3,TARSKI:def 2;
h1 = g or h1 = h by A2,TARSKI:def 2;
hence thesis by A1,A4,ENUMSET1:def 2;
end;
let x be object;
A5: g1 in {g1,g2} & g2 in {g1,g2} by TARSKI:def 2;
assume x in B;
then
A6: x = g * g1 or x = g * g2 or x = h * g1 or x = h * g2 by ENUMSET1:def 2;
g in {g,h} & h in {g,h} by TARSKI:def 2;
hence thesis by A6,A5;
end;
theorem Th22:
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
proof
let G be Group, A be Subset of G such that
A1: for g1,g2 being Element of G st g1 in A & g2 in A holds g1 * g2 in A and
A2: for g being Element of G st g in A holds g" in A;
thus A * A c= A
proof
let x be object;
assume x in A * A;
then ex g1,g2 being Element of G st x = g1 * g2 & g1 in A & g2 in A;
hence thesis by A1;
end;
let x be object;
assume
A3: x in A;
then reconsider a = x as Element of G;
a" in A by A2,A3;
then a" * a in A by A1,A3;
then
A4: 1_G in A by GROUP_1:def 5;
1_G * a = a by GROUP_1:def 4;
hence thesis by A3,A4;
end;
theorem Th23:
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
proof
let G be Group, A be Subset of G;
assume
A1: for g being Element of G st g in A holds g" in A;
thus A" c= A
proof
let x be object;
assume x in A";
then ex g being Element of G st x = g" & g in A;
hence thesis by A1;
end;
let x be object;
assume
A2: x in A;
then reconsider a = x as Element of G;
A3: x = a"";
a" in A by A1,A2;
hence thesis by A3;
end;
theorem
(for a,b st a in A & b in B holds a * b = b * a) implies A * B = B * A
proof
assume
A1: for a,b st a in A & b in B holds a * b = b * a;
thus A * B c= B * A
proof
let x be object;
assume x in A * B;
then consider a,b such that
A2: x = a * b and
A3: a in A & b in B;
x = b * a by A1,A2,A3;
hence thesis by A3;
end;
let x be object;
assume x in B * A;
then consider b,a such that
A4: x = b * a and
A5: b in B & a in A;
x = a * b by A1,A4,A5;
hence thesis by A5;
end;
Lm2: for A be commutative Group, a, b be Element of A holds a * b = b * a;
theorem Th25:
G is commutative Group implies A * B = B * A
proof
assume
A1: G is commutative Group;
thus A * B c= B * A
proof
let x be object;
assume x in A * B;
then consider g,h such that
A2: x = g * h and
A3: g in A & h in B;
x = h * g by A1,A2,Lm2;
hence thesis by A3;
end;
let x be object;
assume x in B * A;
then consider g,h such that
A4: x = g * h and
A5: g in B & h in A;
x = h * g by A1,A4,Lm2;
hence thesis by A5;
end;
theorem
for G being commutative Group, A,B being Subset of G holds (A * B)" = A" * B"
proof
let G be commutative Group, A,B be Subset of G;
thus (A * B)" c= A" * B"
proof
let x be object;
assume x in (A * B)";
then consider g being Element of G such that
A1: x = g" and
A2: g in A * B;
consider g1,g2 being Element of G such that
A3: g = g1 * g2 and
A4: g1 in A & g2 in B by A2;
A5: g1" in A" & g2" in B" by A4;
x = g1" * g2" by A1,A3,GROUP_1:47;
hence thesis by A5;
end;
let x be object;
assume x in A" * B";
then consider g1,g2 being Element of G such that
A6: x = g1 * g2 and
A7: g1 in A" and
A8: g2 in B";
consider b being Element of G such that
A9: g2 = b" and
A10: b in B by A8;
consider a being Element of G such that
A11: g1 = a" and
A12: a in A by A7;
A13: a * b in A * B by A12,A10;
x = (a * b)" by A6,A11,A9,GROUP_1:47;
hence thesis by A13;
end;
definition
let G,g,A;
func g * A -> Subset of G equals
{g} * A;
correctness;
func A * g -> Subset of G equals
A * {g};
correctness;
end;
theorem Th27:
x in g * A iff ex h st x = g * h & h in A
proof
thus x in g * A implies ex h st x = g * h & h in A
proof
assume x in g * A;
then consider g1,g2 such that
A1: x = g1 * g2 and
A2: g1 in {g} and
A3: g2 in A;
g1 = g by A2,TARSKI:def 1;
hence thesis by A1,A3;
end;
given h such that
A4: x = g * h & h in A;
g in {g} by TARSKI:def 1;
hence thesis by A4;
end;
theorem Th28:
x in A * g iff ex h st x = h * g & h in A
proof
thus x in A * g implies ex h st x = h * g & h in A
proof
assume x in A * g;
then consider g1,g2 such that
A1: x = g1 * g2 & g1 in A and
A2: g2 in {g};
g2 = g by A2,TARSKI:def 1;
hence thesis by A1;
end;
given h such that
A3: x = h * g & h in A;
g in {g} by TARSKI:def 1;
hence thesis by A3;
end;
theorem
G is associative implies g * A * B = g * (A * B) by Th10;
theorem
G is associative implies A * g * B = A * (g * B) by Th10;
theorem
G is associative implies A * B * g = A * (B * g) by Th10;
theorem Th32:
G is associative implies g * h * A = g * (h * A)
proof
assume
A1: G is associative;
thus g * h * A = {g} * {h} * A by Th18
.= g * (h * A) by A1,Th10;
end;
theorem
G is associative implies g * A * h = g * (A * h) by Th10;
theorem Th34:
G is associative implies A * g * h = A * (g * h)
proof
assume G is associative;
hence A * g * h = A * ({g} * {h}) by Th10
.= A * (g * h) by Th18;
end;
theorem
{}(the carrier of G) * a = {} & a * {}(the carrier of G) = {} by Th16;
reserve G for Group-like non empty multMagma;
reserve h,g,g1,g2 for Element of G;
reserve A for Subset of G;
theorem
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 by Th17;
theorem Th37:
1_G * A = A & A * 1_G = A
proof
thus 1_G * A = A
proof
thus 1_G * A c= A
proof
let x be object;
assume x in 1_G * A;
then ex h st x = 1_G * h & h in A by Th27;
hence thesis by GROUP_1:def 4;
end;
let x be object;
assume
A1: x in A;
then reconsider a = x as Element of G;
1_G * a = a by GROUP_1:def 4;
hence thesis by A1,Th27;
end;
thus A * 1_G c= A
proof
let x be object;
assume x in A * 1_G;
then ex h st x = h * 1_G & h in A by Th28;
hence thesis by GROUP_1:def 4;
end;
let x be object;
assume
A2: x in A;
then reconsider a = x as Element of G;
a * 1_G = a by GROUP_1:def 4;
hence thesis by A2,Th28;
end;
theorem
G is commutative Group implies g * A = A * g by Th25;
definition
let G be Group-like non empty multMagma;
mode Subgroup of G -> Group-like non empty multMagma means
:Def5:
the
carrier of it c= the carrier of G & the multF of it = (the multF of G)||the
carrier of it;
existence
proof
take G;
dom(the multF of G) = [:the carrier of G,the carrier of G:] by
FUNCT_2:def 1;
hence thesis by RELAT_1:68;
end;
end;
reserve H for Subgroup of G;
reserve h,h1,h2 for Element of H;
theorem Th39:
G is finite implies H is finite
proof
assume
A1: G is finite;
the carrier of H c= the carrier of G by Def5;
hence the carrier of H is finite by A1;
end;
theorem Th40:
x in H implies x in G
proof
assume x in H;
then
A1: x in the carrier of H;
the carrier of H c= the carrier of G by Def5;
hence thesis by A1;
end;
theorem Th41:
h in G by Th40,STRUCT_0:def 5;
theorem Th42:
h is Element of G by Th41,STRUCT_0:def 5;
theorem Th43:
h1 = g1 & h2 = g2 implies h1 * h2 = g1 * g2
proof
assume
A1: h1 = g1 & h2 = g2;
h1 * h2 = ((the multF of G)||the carrier of H).[h1,h2] by Def5;
hence thesis by A1,FUNCT_1:49;
end;
registration
let G be Group;
cluster -> associative for Subgroup of G;
coherence
proof
let H be Subgroup of G;
let x, y, z be Element of H;
y*z in the carrier of H & the carrier of H c= the carrier of G by Def5;
then reconsider
a = x, b = y, c = z, ab = x*y, bc = y*z as Element of G;
thus x*y*z = ab*c by Th43
.= a*b*c by Th43
.= a*(b*c) by GROUP_1:def 3
.= a*bc by Th43
.= x*(y*z) by Th43;
end;
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 Th44:
1_H = 1_G
proof
set h = the Element of H;
reconsider g = h, g9 = 1_H as Element of G by Th42;
h * 1_H = h by GROUP_1:def 4;
then g * g9 = g by Th43;
hence thesis by GROUP_1:7;
end;
theorem
1_H1 = 1_H2
proof
thus 1_H1 = 1_G by Th44
.= 1_H2 by Th44;
end;
theorem Th46:
1_G in H
proof
1_H in H;
hence thesis by Th44;
end;
theorem
1_H1 in H2
proof
1_H1 = 1_G by Th44;
hence thesis by Th46;
end;
theorem Th48:
h = g implies h" = g"
proof
reconsider g9 = h" as Element of G by Th42;
A1: h * h" = 1_H by GROUP_1:def 5;
assume h = g;
then g * g9 = 1_H by A1,Th43
.= 1_G by Th44;
hence thesis by GROUP_1:12;
end;
theorem
inverse_op(H) = inverse_op(G) | the carrier of H
proof
the carrier of H c= the carrier of G by Def5;
then
A1: (the carrier of G) /\ (the carrier of H) = the carrier of H by XBOOLE_1:28;
A2: now
let x be object;
assume x in dom(inverse_op(H));
then reconsider a = x as Element of H;
reconsider b = a as Element of G by Th42;
thus inverse_op(H).x = a" by GROUP_1:def 6
.= b" by Th48
.= inverse_op(G).x by GROUP_1:def 6;
end;
dom(inverse_op(H)) = the carrier of H & dom(inverse_op(G)) = the carrier
of G by FUNCT_2:def 1;
hence thesis by A1,A2,FUNCT_1:46;
end;
theorem Th50:
g1 in H & g2 in H implies g1 * g2 in H
proof
assume g1 in H & g2 in H;
then reconsider h1 = g1, h2 = g2 as Element of H;
h1 * h2 in H;
hence thesis by Th43;
end;
theorem Th51:
g in H implies g" in H
proof
assume g in H;
then reconsider h = g as Element of H;
h" in H;
hence thesis by Th48;
end;
registration
let G;
cluster strict for Subgroup of G;
existence
proof
set H = multMagma (#the carrier of G, the multF of G#);
reconsider H as Group-like non empty multMagma;
the multF of H = (the multF of G)||the carrier of H by RELSET_1:19;
then H is Subgroup of G by Def5;
hence thesis;
end;
end;
theorem Th52:
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
proof
assume that
A1: A <> {} and
A2: for g1,g2 st g1 in A & g2 in A holds g1 * g2 in A and
A3: for g st g in A holds g" in A;
reconsider D = A as non empty set by A1;
set o = (the multF of G)||A;
A4: dom o = dom(the multF of G) /\ [:A,A:] by RELAT_1:61;
dom(the multF of G) = [:the carrier of G,the carrier of G:] by FUNCT_2:def 1;
then
A5: dom o = [:A,A:] by A4,XBOOLE_1:28;
rng o c= A
proof
let x be object;
assume x in rng o;
then consider y being object such that
A6: y in dom o and
A7: o.y = x by FUNCT_1:def 3;
consider y1,y2 being object such that
A8: [y1,y2] = y by A4,A6,RELAT_1:def 1;
A9: y1 in A & y2 in A by A5,A6,A8,ZFMISC_1:87;
reconsider y1,y2 as Element of G by A4,A6,A8,ZFMISC_1:87;
x = y1 * y2 by A6,A7,A8,FUNCT_1:47;
hence thesis by A2,A9;
end;
then reconsider o as BinOp of D by A5,FUNCT_2:def 1,RELSET_1:4;
set H = multMagma (# D,o #);
A10: now
let g1,g2;
let h1,h2 be Element of H;
A11: h1 * h2 = ((the multF of G)||A).[h1,h2];
assume g1 = h1 & g2 = h2;
hence g1 * g2 = h1 * h2 by A11,FUNCT_1:49;
end;
H is Group-like
proof
set a = the Element of H;
reconsider x = a as Element of G by Lm1;
x" in A by A3;
then x * x" in A by A2;
then reconsider t = 1_G as Element of H by GROUP_1:def 5;
take t;
let a be Element of H;
reconsider x = a as Element of G by Lm1;
thus a * t = x * 1_G by A10
.= a by GROUP_1:def 4;
thus t * a = 1_G * x by A10
.= a by GROUP_1:def 4;
reconsider s = x" as Element of H by A3;
take s;
thus a * s = x * x" by A10
.= t by GROUP_1:def 5;
thus s * a = x" * x by A10
.= t by GROUP_1:def 5;
end;
then reconsider H as Group-like non empty multMagma;
reconsider H as strict Subgroup of G by Def5;
take H;
thus thesis;
end;
theorem Th53:
G is commutative Group implies H is commutative
proof
assume
A1: G is commutative Group;
thus for h1,h2 holds h1 * h2 = h2 * h1
proof
let h1,h2;
reconsider g1 = h1, g2 = h2 as Element of G by Th42;
thus h1 * h2 = g1 * g2 by Th43
.= g2 * g1 by A1,Lm2
.= h2 * h1 by Th43;
end;
end;
registration
let G be commutative Group;
cluster -> commutative for Subgroup of G;
coherence by Th53;
end;
theorem Th54:
G is Subgroup of G
proof
dom(the multF of G) = [:the carrier of G,the carrier of G:] by FUNCT_2:def 1;
hence
the carrier of G c= the carrier of G & the multF of G = (the multF of G
)||the carrier of G by RELAT_1:68;
end;
theorem Th55:
G1 is Subgroup of G2 & G2 is Subgroup of G1 implies
the multMagma of G1 = the multMagma of G2
proof
assume that
A1: G1 is Subgroup of G2 and
A2: G2 is Subgroup of G1;
set g = the multF of G2;
set f = the multF of G1;
set B = the carrier of G2;
set A = the carrier of G1;
A3: A c= B & B c= A by A1,A2,Def5;
then
A4: A = B;
f = g||A by A1,Def5
.= (f||B)||A by A2,Def5
.= f||B by A4,RELAT_1:72
.= g by A2,Def5;
hence thesis by A3,XBOOLE_0:def 10;
end;
theorem Th56:
G1 is Subgroup of G2 & G2 is Subgroup of G3 implies G1 is Subgroup of G3
proof
assume that
A1: G1 is Subgroup of G2 and
A2: G2 is Subgroup of G3;
set h = the multF of G3;
set C = the carrier of G3;
set B = the carrier of G2;
set A = the carrier of G1;
A3: A c= B by A1,Def5;
then
A4: [:A,A:] c= [:B,B:] by ZFMISC_1:96;
B c= C by A2,Def5;
then
A5: A c= C by A3;
the multF of G1 = (the multF of G2)||A by A1,Def5
.= (h||B)||A by A2,Def5
.= h||A by A4,FUNCT_1:51;
hence thesis by A5,Def5;
end;
theorem Th57:
the carrier of H1 c= the carrier of H2 implies H1 is Subgroup of H2
proof
set A = the carrier of H1;
set B = the carrier of H2;
set h = the multF of G;
assume
A1: the carrier of H1 c= the carrier of H2;
hence the carrier of H1 c= the carrier of H2;
A2: [:A,A:] c= [:B,B:] by A1,ZFMISC_1:96;
the multF of H1 = h||A & the multF of H2 = h||B by Def5;
hence thesis by A2,FUNCT_1:51;
end;
theorem Th58:
(for g st g in H1 holds g in H2) implies H1 is Subgroup of H2
proof
assume
A1: for g st g in H1 holds g in H2;
the carrier of H1 c= the carrier of H2
proof
let x be object;
assume x in the carrier of H1;
then reconsider g = x as Element of H1;
reconsider g as Element of G by Th42;
g in H1;
then g in H2 by A1;
hence thesis;
end;
hence thesis by Th57;
end;
theorem Th59:
the carrier of H1 = the carrier of H2 implies
the multMagma of H1 = the multMagma of H2
proof
assume the carrier of H1 = the carrier of H2;
then H1 is Subgroup of H2 & H2 is Subgroup of H1 by Th57;
hence thesis by Th55;
end;
theorem Th60:
(for g holds g in H1 iff g in H2) implies
the multMagma of H1 = the multMagma of H2
proof
assume for g holds g in H1 iff g in H2;
then H1 is Subgroup of H2 & H2 is Subgroup of H1 by Th58;
hence thesis by Th55;
end;
definition
let G;
let H1,H2 be strict Subgroup of G;
redefine pred H1 = H2 means :: redefines = (XBOOLE_0, redefinition) → = (HIDDEN, definition)
for g holds g in H1 iff g in H2;
compatibility by Th60;
end;
theorem Th61:
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
proof
let G be Group, H be Subgroup of G;
assume
A1: the carrier of G c= the carrier of H;
A2: G is Subgroup of G by Th54;
the carrier of H c= the carrier of G by Def5;
then the carrier of G = the carrier of H by A1;
hence thesis by A2,Th59;
end;
theorem Th62:
(for g being Element of G holds g in H) implies
the multMagma of H = the multMagma of G
proof
assume for g being Element of G holds g in H;
then
A1: for g be Element of G holds ( g in H implies g in G) &( g in G implies g
in H);
G is Subgroup of G by Th54;
hence thesis by A1,Th60;
end;
definition
let G;
func (1).G -> strict Subgroup of G means
:Def7:
the carrier of it = {1_G};
existence
proof
A1: now
let g;
assume g in {1_G};
then g = 1_G by TARSKI:def 1;
then g" = 1_G by GROUP_1:8;
hence g" in {1_G} by TARSKI:def 1;
end;
now
let g1,g2;
assume g1 in {1_G} & g2 in {1_G};
then g1 = 1_G & g2 = 1_G by TARSKI:def 1;
then g1 * g2 = 1_G by GROUP_1:def 4;
hence g1 * g2 in {1_G} by TARSKI:def 1;
end;
hence thesis by A1,Th52;
end;
uniqueness by Th59;
end;
definition
let G;
func (Omega).G -> strict Subgroup of G equals
the multMagma of G;
coherence
proof
set H = the multMagma of G;
reconsider H as Group-like non empty multMagma;
dom(the multF of G) = [:the carrier of G,the carrier of G:]
by FUNCT_2:def 1;
then the multF of H = (the multF of G)||the carrier of H by RELAT_1:68;
hence thesis by Def5;
end;
projectivity;
end;
theorem Th63:
(1).H = (1).G
proof
A1: 1_H = 1_G by Th44;
(1).H is Subgroup of G & the carrier of (1).H = {1_H} by Def7,Th56;
hence thesis by A1,Def7;
end;
theorem
(1).H1 = (1).H2
proof
thus (1).H1 = (1).G by Th63
.= (1).H2 by Th63;
end;
theorem Th65:
(1).G is Subgroup of H
proof
(1).G = (1).H by Th63;
hence thesis;
end;
theorem
for G being strict Group, H being Subgroup of G holds
H is Subgroup of (Omega).G;
theorem
for G being strict Group holds G is Subgroup of (Omega).G;
theorem Th68:
(1).G is finite
proof
the carrier of (1).G = {1_G} by Def7;
hence thesis;
end;
registration
let G;
cluster (1).G -> finite;
coherence by Th68;
cluster strict finite for Subgroup of G;
existence
proof
take (1).G;
thus thesis;
end;
end;
registration
cluster strict finite for Group;
existence
proof
set G = the Group;
take (1).G;
thus thesis;
end;
end;
registration
let G be finite Group;
cluster -> finite for Subgroup of G;
coherence by Th39;
end;
theorem Th69:
card (1).G = 1
proof
the carrier of (1).G = {1_G} by Def7;
hence thesis by CARD_1:30;
end;
theorem Th70:
for H being strict finite Subgroup of G holds card H = 1 implies H = (1).G
proof
let H be strict finite Subgroup of G;
assume card H = 1;
then consider x being object such that
A1: the carrier of H = {x} by CARD_2:42;
1_G in H by Th46;
then 1_G in the carrier of H;
then x = 1_G by A1,TARSKI:def 1;
hence thesis by A1,Def7;
end;
theorem
card H c= card G by Def5,CARD_1:11;
theorem
for G being finite Group, H being Subgroup of G holds card H <= card G
by Def5,NAT_1:43;
theorem
for G being finite Group, H being Subgroup of G holds card G = card H
implies the multMagma of H = the multMagma of G
proof
let G be finite Group, H be Subgroup of G;
assume
A1: card G = card H;
A2: the carrier of H c= the carrier of G by Def5;
the carrier of H = the carrier of G
proof
assume the carrier of H <> the carrier of G;
then the carrier of H c< the carrier of G by A2;
hence thesis by A1,CARD_2:48;
end;
hence thesis by Th61;
end;
definition
let G,H;
func carr(H) -> Subset of G equals
the carrier of H;
coherence by Def5;
end;
registration let G be Group, H be Subgroup of G;
cluster carr H -> non empty;
coherence;
end;
theorem Th74:
g1 in carr(H) & g2 in carr(H) implies g1 * g2 in carr(H)
proof
assume g1 in carr(H) & g2 in carr(H);
then g1 in H & g2 in H;
then g1 * g2 in H by Th50;
hence thesis;
end;
theorem Th75:
g in carr(H) implies g" in carr(H)
proof
assume g in carr(H);
then g in H;
then g" in H by Th51;
hence thesis;
end;
theorem
carr(H) * carr(H) = carr(H)
proof
A1: g in carr(H) implies g" in carr(H) by Th75;
g1 in carr(H) & g2 in carr(H) implies g1 * g2 in carr(H) by Th74;
hence thesis by A1,Th22;
end;
theorem
carr(H)" = carr H
proof
g in carr H implies g" in carr H by Th75;
hence thesis by Th23;
end;
theorem Th78:
(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)
proof
thus 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)
proof
assume
A1: carr H1 * carr H2 = carr H2 * carr H1;
A2: now
let g;
assume
A3: g in carr H1 * carr H2;
then consider a,b such that
A4: g = a * b and
a in carr H1 and
b in carr H2;
consider b1,a1 such that
A5: a * b = b1 * a1 and
A6: b1 in carr H2 & a1 in carr H1 by A1,A3,A4;
A7: a1" in carr H1 & b1" in carr H2 by A6,Th75;
g" = a1" * b1" by A4,A5,GROUP_1:17;
hence g" in carr H1 * carr H2 by A7;
end;
A8: now
let g1,g2;
assume that
A9: g1 in carr(H1) * carr(H2) and
A10: g2 in carr(H1) * carr(H2);
consider a1,b1 such that
A11: g1 = a1 * b1 and
A12: a1 in carr(H1) and
A13: b1 in carr(H2) by A9;
consider a2,b2 such that
A14: g2 = a2 * b2 and
A15: a2 in carr H1 and
A16: b2 in carr H2 by A10;
b1 * a2 in carr H1 * carr H2 by A1,A13,A15;
then consider a,b such that
A17: b1 * a2 = a * b and
A18: a in carr H1 and
A19: b in carr H2;
A20: b * b2 in carr H2 by A16,A19,Th74;
g1 * g2 = a1 * b1 * a2 * b2 by A11,A14,GROUP_1:def 3
.= a1 * (b1 * a2) * b2 by GROUP_1:def 3;
then
A21: g1 * g2 = a1 * a * b * b2 by A17,GROUP_1:def 3
.= a1 * a * (b * b2) by GROUP_1:def 3;
a1 * a in carr H1 by A12,A18,Th74;
hence g1 * g2 in carr H1 * carr H2 by A21,A20;
end;
carr H1 * carr H2 <> {} by Th9;
hence thesis by A8,A2,Th52;
end;
given H such that
A22: the carrier of H = carr H1 * carr H2;
thus carr H1 * carr H2 c= carr H2 * carr H1
proof
let x be object;
assume
A23: x in carr H1 * carr H2;
then reconsider y = x as Element of G;
y" in carr H by A22,A23,Th75;
then consider a,b such that
A24: y" = a * b and
A25: a in carr H1 & b in carr H2 by A22;
A26: y = y"" .= b" * a" by A24,GROUP_1:17;
a" in carr H1 & b" in carr H2 by A25,Th75;
hence thesis by A26;
end;
let x be object;
assume
A27: x in carr H2 * carr H1;
then reconsider y = x as Element of G;
consider a,b such that
A28: x = a * b & a in carr H2 and
A29: b in carr H1 by A27;
now
A30: b" in carr H1 by A29,Th75;
assume
A31: not y" in carr H;
y" = b" * a" & a" in carr H2 by A28,Th75,GROUP_1:17;
hence contradiction by A22,A31,A30;
end;
then y"" in carr H by Th75;
hence thesis by A22;
end;
theorem
G is commutative Group implies ex H being strict Subgroup of G st
the carrier of H = carr(H1) * carr(H2)
proof
assume G is commutative Group;
then carr(H1) * carr(H2) = carr(H2) * carr(H1) by Th25;
hence thesis by Th78;
end;
definition
let G,H1,H2;
func H1 /\ H2 -> strict Subgroup of G means
:Def10:
the carrier of it = carr (H1) /\ carr(H2);
existence
proof
set A = carr(H1) /\ carr(H2);
1_G in H2 by Th46;
then
A1: 1_G in the carrier of H2;
A2: now
let g1,g2;
assume
A3: g1 in A & g2 in A;
then g1 in carr(H2) & g2 in carr(H2) by XBOOLE_0:def 4;
then
A4: g1 * g2 in carr(H2) by Th74;
g1 in carr(H1) & g2 in carr(H1) by A3,XBOOLE_0:def 4;
then g1 * g2 in carr(H1) by Th74;
hence g1 * g2 in A by A4,XBOOLE_0:def 4;
end;
A5: now
let g;
assume
A6: g in A;
then g in carr(H2) by XBOOLE_0:def 4;
then
A7: g" in carr(H2) by Th75;
g in carr(H1) by A6,XBOOLE_0:def 4;
then g" in carr(H1) by Th75;
hence g" in A by A7,XBOOLE_0:def 4;
end;
1_G in H1 by Th46;
then 1_G in the carrier of H1;
then A <> {} by A1,XBOOLE_0:def 4;
hence thesis by A2,A5,Th52;
end;
uniqueness by Th59;
end;
theorem Th80:
(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
proof
A1: the carrier of H1 = carr(H1) & the carrier of H2 = carr(H2);
thus for H being Subgroup of G st H = H1 /\ H2 holds the carrier of H = (the
carrier of H1) /\ (the carrier of H2)
proof
let H be Subgroup of G;
assume H = H1 /\ H2;
hence the carrier of H = carr(H1) /\ carr(H2) by Def10
.= (the carrier of H1) /\ (the carrier of H2);
end;
let H be strict Subgroup of G;
assume the carrier of H = (the carrier of H1) /\ (the carrier of H2);
hence thesis by A1,Def10;
end;
theorem
carr(H1 /\ H2) = carr(H1) /\ carr(H2) by Def10;
theorem Th82:
x in H1 /\ H2 iff x in H1 & x in H2
proof
thus x in H1 /\ H2 implies x in H1 & x in H2
proof
assume x in H1 /\ H2;
then x in the carrier of H1 /\ H2;
then x in carr(H1) /\ carr(H2) by Def10;
then x in carr(H1) & x in carr(H2) by XBOOLE_0:def 4;
hence thesis;
end;
assume x in H1 & x in H2;
then x in carr(H2) & x in carr(H1);
then x in carr(H1) /\ carr(H2) by XBOOLE_0:def 4;
then x in carr(H1 /\ H2) by Def10;
hence thesis;
end;
theorem
for H being strict Subgroup of G holds H /\ H = H
proof
let H be strict Subgroup of G;
the carrier of H /\ H = carr(H) /\ carr(H) by Def10
.= the carrier of H;
hence thesis by Th59;
end;
definition
let G,H1,H2;
redefine func H1 /\ H2; :: redefines /\ (GROUP_2, definition)
commutativity
proof let H1,H2;
the carrier of H1 /\ H2 = carr(H2) /\ carr(H1) by Def10
.= the carrier of H2 /\ H1 by Def10;
hence thesis by Th59;
end;
end;
theorem
H1 /\ H2 /\ H3 = H1 /\ (H2 /\ H3)
proof
the carrier of H1 /\ H2 /\ H3 = carr(H1 /\ H2) /\ carr(H3) by Def10
.= carr(H1) /\ carr(H2) /\ carr(H3) by Def10
.= carr(H1) /\ (carr(H2) /\ carr(H3)) by XBOOLE_1:16
.= carr(H1) /\ carr(H2 /\ H3) by Def10
.= the carrier of H1 /\ (H2 /\ H3) by Def10;
hence thesis by Th59;
end;
Lm3: for H1 being Subgroup of G holds H1 is Subgroup of H2 iff the multMagma
of (H1 /\ H2) = the multMagma of H1
proof
let H1 be Subgroup of G;
thus H1 is Subgroup of H2 implies the multMagma of (H1 /\ H2) = the
multMagma of H1
proof
assume H1 is Subgroup of H2;
then
A1: the carrier of H1 c= the carrier of H2 by Def5;
the carrier of H1 /\ H2 = carr(H1) /\ carr (H2) by Def10;
hence thesis by A1,Th59,XBOOLE_1:28;
end;
assume the multMagma of (H1 /\ H2) = the multMagma of H1;
then the carrier of H1 = carr(H1) /\ carr(H2) by Def10
.= (the carrier of H1) /\ (the carrier of H2);
hence thesis by Th57,XBOOLE_1:17;
end;
theorem
(1).G /\ H = (1).G & H /\ (1).G = (1).G
proof
A1: (1).G is Subgroup of H by Th65;
hence (1).G /\ H = (1).G by Lm3;
thus thesis by A1,Lm3;
end;
theorem
for G being strict Group, H being strict Subgroup of G holds
H /\ (Omega).G = H & (Omega).G /\ H = H by Lm3;
theorem
for G being strict Group holds (Omega).G /\ (Omega).G = G by Lm3;
Lm4: H1 /\ H2 is Subgroup of H1
proof
the carrier of H1 /\ H2 = (the carrier of H1) /\ (the carrier of H2) by Th80;
hence thesis by Th57,XBOOLE_1:17;
end;
theorem
H1 /\ H2 is Subgroup of H1 & H1 /\ H2 is Subgroup of H2 by Lm4;
theorem
for H1 being Subgroup of G holds H1 is Subgroup of H2 iff
the multMagma of (H1 /\ H2) = the multMagma of H1 by Lm3;
theorem
H1 is Subgroup of H2 implies H1 /\ H3 is Subgroup of H2
proof
assume
A1: H1 is Subgroup of H2;
H1 /\ H3 is Subgroup of H1 by Lm4;
hence thesis by A1,Th56;
end;
theorem
H1 is Subgroup of H2 & H1 is Subgroup of H3 implies
H1 is Subgroup of H2 /\ H3
proof
assume
A1: H1 is Subgroup of H2 & H1 is Subgroup of H3;
now
let g;
assume g in H1;
then g in H2 & g in H3 by A1,Th40;
hence g in H2 /\ H3 by Th82;
end;
hence thesis by Th58;
end;
theorem
H1 is Subgroup of H2 implies H1 /\ H3 is Subgroup of H2 /\ H3
proof
assume H1 is Subgroup of H2;
then the carrier of H1 c= the carrier of H2 by Def5;
then (the carrier of H1) /\ (the carrier of H3) c= (the carrier of H2) /\ (
the carrier of H3) by XBOOLE_1:26;
then
the carrier of H1 /\ H3 c= (the carrier of H2) /\ (the carrier of H3) by Th80
;
then the carrier of H1 /\ H3 c= the carrier of H2 /\ H3 by Th80;
hence thesis by Th57;
end;
theorem
H1 is finite or H2 is finite implies H1 /\ H2 is finite
proof
assume
A1: H1 is finite or H2 is finite;
H1 /\ H2 is Subgroup of H1 & H1 /\ H2 is Subgroup of H2 by Lm4;
hence thesis by A1;
end;
definition
let G,H,A;
func A * H -> Subset of G equals
A * carr H;
correctness;
func H * A -> Subset of G equals
carr H * A;
correctness;
end;
theorem
x in A * H iff ex g1,g2 st x = g1 * g2 & g1 in A & g2 in H
proof
thus x in A * H implies ex g1,g2 st x = g1 * g2 & g1 in A & g2 in H
proof
assume x in A * H;
then consider g1,g2 such that
A1: x = g1 * g2 & g1 in A and
A2: g2 in carr H;
g2 in H by A2;
hence thesis by A1;
end;
given g1,g2 such that
A3: x = g1 * g2 & g1 in A and
A4: g2 in H;
g2 in carr H by A4;
hence thesis by A3;
end;
theorem
x in H * A iff ex g1,g2 st x = g1 * g2 & g1 in H & g2 in A
proof
thus x in H * A implies ex g1,g2 st x = g1 * g2 & g1 in H & g2 in A
proof
assume x in H * A;
then consider g1,g2 such that
A1: x = g1 * g2 and
A2: g1 in carr H and
A3: g2 in A;
g1 in H by A2;
hence thesis by A1,A3;
end;
given g1,g2 such that
A4: x = g1 * g2 and
A5: g1 in H and
A6: g2 in A;
g1 in carr H by A5;
hence thesis by A4,A6;
end;
theorem
A * B * H = A * (B * H) by Th10;
theorem
A * H * B = A * (H * B) by Th10;
theorem
H * A * B = H * (A * B) by Th10;
theorem
A * H1 * H2 = A * (H1 * carr H2) by Th10;
theorem
H1 * A * H2 = H1 * (A * H2) by Th10;
theorem
H1 * carr(H2) * A = H1 * (H2 * A) by Th10;
theorem
G is commutative Group implies A * H = H * A by Th25;
definition
let G,H,a;
func a * H -> Subset of G equals
a * carr(H);
correctness;
func H * a -> Subset of G equals
carr(H) * a;
correctness;
end;
theorem Th103:
x in a * H iff ex g st x = a * g & g in H
proof
thus x in a * H implies ex g st x = a * g & g in H
proof
assume x in a * H;
then consider g such that
A1: x = a * g & g in carr(H) by Th27;
take g;
thus thesis by A1;
end;
given g such that
A2: x = a * g and
A3: g in H;
g in carr(H) by A3;
hence thesis by A2,Th27;
end;
theorem Th104:
x in H * a iff ex g st x = g * a & g in H
proof
thus x in H * a implies ex g st x = g * a & g in H
proof
assume x in H * a;
then consider g such that
A1: x = g * a & g in carr(H) by Th28;
take g;
thus thesis by A1;
end;
given g such that
A2: x = g * a and
A3: g in H;
g in carr(H) by A3;
hence thesis by A2,Th28;
end;
theorem
a * b * H = a * (b * H) by Th32;
theorem
a * H * b = a * (H * b) by Th10;
theorem
H * a * b = H * (a * b) by Th34;
theorem Th108:
a in a * H & a in H * a
proof
A1: 1_G * a = a by GROUP_1:def 4;
1_G in H & a * 1_G = a by Th46,GROUP_1:def 4;
hence thesis by A1,Th103,Th104;
end;
theorem
1_G * H = carr(H) & H * 1_G = carr(H) by Th37;
theorem Th110:
(1).G * a = {a} & a * (1).G = {a}
proof
A1: the carrier of (1).G = {1_G} by Def7;
hence (1).G * a = {1_G * a} by Th18
.= {a} by GROUP_1:def 4;
thus a * (1).G = {a * 1_G} by A1,Th18
.= {a} by GROUP_1:def 4;
end;
theorem Th111:
a * (Omega).G = the carrier of G & (Omega).G * a = the carrier of G
proof
[#](the carrier of G) * a = the carrier of G by Th17;
hence thesis by Th17;
end;
theorem
G is commutative Group implies a * H = H * a by Th25;
theorem Th113:
a in H iff a * H = carr(H)
proof
thus a in H implies a * H = carr(H)
proof
assume
A1: a in H;
thus a * H c= carr(H)
proof
let x be object;
assume x in a * H;
then consider g such that
A2: x = a * g and
A3: g in H by Th103;
a * g in H by A1,A3,Th50;
hence thesis by A2;
end;
let x be object;
assume
A4: x in carr(H);
then
A5: x in H;
reconsider b = x as Element of G by A4;
A6: a * (a" * b) = a * a" * b by GROUP_1:def 3
.= 1_G * b by GROUP_1:def 5
.= x by GROUP_1:def 4;
a" in H by A1,Th51;
then a" * b in H by A5,Th50;
hence thesis by A6,Th103;
end;
assume
A7: a * H = carr(H);
a * 1_G = a & 1_G in H by Th46,GROUP_1:def 4;
then a in carr(H) by A7,Th103;
hence thesis;
end;
theorem Th114:
a * H = b * H iff b" * a in H
proof
thus a * H = b * H implies b" * a in H
proof
assume
A1: a * H = b * H;
b" * a * H = b" * (a * H) by Th32
.= b" * b * H by A1,Th32
.= 1_G * H by GROUP_1:def 5
.= carr(H) by Th37;
hence thesis by Th113;
end;
assume
A2: b" * a in H;
thus a * H = 1_G * (a * H) by Th37
.= 1_G * a * H by Th32
.= b * b" * a * H by GROUP_1:def 5
.= b * (b" * a) * H by GROUP_1:def 3
.= b * ((b" * a) * H) by Th32
.= b * H by A2,Th113;
end;
theorem Th115:
a * H = b * H iff a * H meets b * H
proof
a * H <> {} by Th108;
hence a * H = b * H implies a * H meets b * H;
assume a * H meets b * H;
then consider x being object such that
A1: x in a * H and
A2: x in b * H by XBOOLE_0:3;
reconsider x as Element of G by A2;
consider g such that
A3: x = a * g and
A4: g in H by A1,Th103;
A5: g" in H by A4,Th51;
consider h being Element of G such that
A6: x = b * h and
A7: h in H by A2,Th103;
a = b * h * g" by A3,A6,GROUP_1:14
.= b * (h * g") by GROUP_1:def 3;
then b" * a = h * g" by GROUP_1:13;
then b" * a in H by A7,A5,Th50;
hence thesis by Th114;
end;
theorem Th116:
a * b * H c= (a * H) * (b * H)
proof
let x be object;
assume x in a * b * H;
then consider g such that
A1: x = a * b * g and
A2: g in H by Th103;
A3: x = a * 1_G * b * g by A1,GROUP_1:def 4
.= (a * 1_G) * (b * g) by GROUP_1:def 3;
1_G in H by Th46;
then
A4: a * 1_G in a * H by Th103;
b * g in b * H by A2,Th103;
hence thesis by A3,A4;
end;
theorem
carr(H) c= (a * H) * (a" * H) & carr(H) c= (a" * H) * (a * H)
proof
A1: a" * a * H = 1_G * H by GROUP_1:def 5
.= carr(H) by Th37;
a * a" * H = 1_G * H by GROUP_1:def 5
.= carr(H) by Th37;
hence thesis by A1,Th116;
end;
theorem
a |^ 2 * H c= (a * H) * (a * H)
proof
a |^ 2 * H = a * a * H by GROUP_1:27;
hence thesis by Th116;
end;
theorem Th119:
a in H iff H * a = carr(H)
proof
thus a in H implies H * a = carr(H)
proof
assume
A1: a in H;
thus H * a c= carr(H)
proof
let x be object;
assume x in H * a;
then consider g such that
A2: x = g * a and
A3: g in H by Th104;
g * a in H by A1,A3,Th50;
hence thesis by A2;
end;
let x be object;
assume
A4: x in carr(H);
then
A5: x in H;
reconsider b = x as Element of G by A4;
A6: (b * a") * a = b * (a" * a) by GROUP_1:def 3
.= b * 1_G by GROUP_1:def 5
.= x by GROUP_1:def 4;
a" in H by A1,Th51;
then b * a" in H by A5,Th50;
hence thesis by A6,Th104;
end;
assume
A7: H * a = carr(H);
1_G * a = a & 1_G in H by Th46,GROUP_1:def 4;
then a in carr(H) by A7,Th104;
hence thesis;
end;
theorem Th120:
H * a = H * b iff b * a" in H
proof
thus H * a = H * b implies b * a" in H
proof
assume
A1: H * a = H * b;
carr(H) = H * 1_G by Th37
.= H * (a * a") by GROUP_1:def 5
.= H * b * a" by A1,Th34
.= H * (b * a") by Th34;
hence thesis by Th119;
end;
assume b * a" in H;
hence H * a = H * (b * a") * a by Th119
.= H * (b * a" * a) by Th34
.= H * (b * (a" * a)) by GROUP_1:def 3
.= H * (b * (1_G)) by GROUP_1:def 5
.= H * b by GROUP_1:def 4;
end;
theorem
H * a = H * b iff H * a meets H * b
proof
H * a <> {} by Th108;
hence H * a = H * b implies H * a meets H * b;
assume H * a meets H * b;
then consider x being object such that
A1: x in H * a and
A2: x in H * b by XBOOLE_0:3;
reconsider x as Element of G by A2;
consider g such that
A3: x = g * a and
A4: g in H by A1,Th104;
A5: g" in H by A4,Th51;
consider h being Element of G such that
A6: x = h * b and
A7: h in H by A2,Th104;
a = g" * (h * b) by A3,A6,GROUP_1:13
.= g" * h * b by GROUP_1:def 3;
then a * b" = g" * h by GROUP_1:14;
then a * b" in H by A7,A5,Th50;
hence thesis by Th120;
end;
theorem Th122:
H * a * b c= (H * a) * (H * b)
proof
let x be object;
1_G in H by Th46;
then
A1: 1_G * b in H * b by Th104;
assume x in H * a * b;
then x in H * (a * b) by Th34;
then consider g such that
A2: x = g * (a * b) and
A3: g in H by Th104;
A4: x = g * a * b by A2,GROUP_1:def 3
.= g * a * (1_G * b) by GROUP_1:def 4;
g * a in H * a by A3,Th104;
hence thesis by A1,A4;
end;
theorem
carr(H) c= (H * a) * (H * a") & carr(H) c= (H * a") * (H * a)
proof
A1: H * a"* a = H * (a"* a) by Th34
.= H * 1_G by GROUP_1:def 5
.= carr(H) by Th37;
H * a * a" = H * (a * a") by Th34
.= H * 1_G by GROUP_1:def 5
.= carr(H) by Th37;
hence thesis by A1,Th122;
end;
theorem
H * (a |^ 2) c= (H * a) * (H * a)
proof
a |^ 2 = a * a & H * a * a = H * (a * a) by Th34,GROUP_1:27;
hence thesis by Th122;
end;
theorem
a * (H1 /\ H2) = (a * H1) /\ (a * H2)
proof
thus a * (H1 /\ H2) c= (a * H1) /\ (a * H2)
proof
let x be object;
assume x in a * (H1 /\ H2);
then consider g such that
A1: x = a * g and
A2: g in H1 /\ H2 by Th103;
g in H2 by A2,Th82;
then
A3: x in a * H2 by A1,Th103;
g in H1 by A2,Th82;
then x in a * H1 by A1,Th103;
hence thesis by A3,XBOOLE_0:def 4;
end;
let x be object;
assume
A4: x in (a * H1) /\ (a * H2);
then x in a * H1 by XBOOLE_0:def 4;
then consider g such that
A5: x = a * g and
A6: g in H1 by Th103;
x in a * H2 by A4,XBOOLE_0:def 4;
then consider g1 such that
A7: x = a * g1 and
A8: g1 in H2 by Th103;
g = g1 by A5,A7,GROUP_1:6;
then g in H1 /\ H2 by A6,A8,Th82;
hence thesis by A5,Th103;
end;
theorem
(H1 /\ H2) * a = (H1 * a) /\ (H2 * a)
proof
thus (H1 /\ H2) * a c= (H1 * a) /\ (H2 * a)
proof
let x be object;
assume x in (H1 /\ H2) * a;
then consider g such that
A1: x = g * a and
A2: g in H1 /\ H2 by Th104;
g in H2 by A2,Th82;
then
A3: x in H2 * a by A1,Th104;
g in H1 by A2,Th82;
then x in H1 * a by A1,Th104;
hence thesis by A3,XBOOLE_0:def 4;
end;
let x be object;
assume
A4: x in (H1 * a) /\ (H2 * a);
then x in H1 * a by XBOOLE_0:def 4;
then consider g such that
A5: x = g * a and
A6: g in H1 by Th104;
x in H2 * a by A4,XBOOLE_0:def 4;
then consider g1 such that
A7: x = g1 * a and
A8: g1 in H2 by Th104;
g = g1 by A5,A7,GROUP_1:6;
then g in H1 /\ H2 by A6,A8,Th82;
hence thesis by A5,Th104;
end;
theorem
ex H1 being strict Subgroup of G st the carrier of H1 = a * H2 * a"
proof
set A = a * H2 * a";
set x = the Element of a * H2;
A1: a * H2 <> {} by Th108;
then reconsider x as Element of G by Lm1;
A2: now
let g;
assume g in A;
then consider g1 such that
A3: g = g1 * a" and
A4: g1 in a * H2 by Th28;
consider g2 such that
A5: g1 = a * g2 and
A6: g2 in H2 by A4,Th103;
g2" in H2 by A6,Th51;
then
A7: g2" * a" in H2 * a" by Th104;
g" = a"" * (a * g2)" by A3,A5,GROUP_1:17
.= a * (g2" * a") by GROUP_1:17;
then g" in a * (H2 * a") by A7,Th27;
hence g" in A by Th10;
end;
A8: now
let g1,g2;
assume that
A9: g1 in A and
A10: g2 in A;
consider g such that
A11: g1 = g * a" and
A12: g in a * H2 by A9,Th28;
consider h being Element of G such that
A13: g = a * h and
A14: h in H2 by A12,Th103;
A = a * (H2 * a") by Th10;
then consider b such that
A15: g2 = a * b and
A16: b in H2 * a" by A10,Th27;
consider c being Element of G such that
A17: b = c * a" and
A18: c in H2 by A16,Th104;
h * c in H2 by A14,A18,Th50;
then
A19: a * (h * c) in a * H2 by Th103;
g1 * g2 = (a * h) * (a" * (a * (c * a"))) by A11,A15,A13,A17,GROUP_1:def 3
.= (a * h) * (a" * a * (c * a")) by GROUP_1:def 3
.= (a * h) * (1_G * (c * a")) by GROUP_1:def 5
.= (a * h) * (c * a") by GROUP_1:def 4
.= a * h * c * a" by GROUP_1:def 3
.= a * (h * c) * a" by GROUP_1:def 3;
hence g1 * g2 in A by A19,Th28;
end;
x * a" in A by A1,Th28;
hence thesis by A8,A2,Th52;
end;
theorem Th128:
a * H, b * H are_equipotent
proof
defpred P[object,object] means ex g1 st $1 = g1 & $2 = b * a" * g1;
A1: for x being object st x in a * H ex y being object st P[x,y]
proof
let x be object;
assume x in a * H;
then reconsider g = x as Element of G;
reconsider y = b * a" * g as set;
take y;
take g;
thus thesis;
end;
consider f being Function such that
A2: dom f = a * H and
A3: for x being object st x in a * H holds P[x,f.x] from CLASSES1:sch 1(A1);
A4: rng f = b * H
proof
thus rng f c= b * H
proof
let x be object;
assume x in rng f;
then consider y being object such that
A5: y in dom f and
A6: f.y = x by FUNCT_1:def 3;
consider g such that
A7: y = g and
A8: x = b * a" * g by A2,A3,A5,A6;
consider g1 such that
A9: g = a * g1 and
A10: g1 in H by A2,A5,A7,Th103;
x = b * a" * a * g1 by A8,A9,GROUP_1:def 3
.= b * (a" * a) * g1 by GROUP_1:def 3
.= b * 1_G * g1 by GROUP_1:def 5
.= b * g1 by GROUP_1:def 4;
hence thesis by A10,Th103;
end;
let x be object;
assume x in b * H;
then consider g such that
A11: x = b * g and
A12: g in H by Th103;
A13: a * g in dom f by A2,A12,Th103;
then ex g1 st g1 = a * g & f.(a * g) = b * a" * g1 by A2,A3;
then f.(a * g) = b * a" * a * g by GROUP_1:def 3
.= b * (a" * a) * g by GROUP_1:def 3
.= b * 1_G * g by GROUP_1:def 5
.= x by A11,GROUP_1:def 4;
hence thesis by A13,FUNCT_1:def 3;
end;
f is one-to-one
proof
let x,y be object;
assume that
A14: x in dom f & y in dom f and
A15: f.x = f.y;
( ex g1 st x = g1 & f.x = b * a" * g1)& ex g2 st y = g2 & f.y = b * a
" * g2 by A2,A3,A14;
hence thesis by A15,GROUP_1:6;
end;
hence thesis by A2,A4,WELLORD2:def 4;
end;
theorem Th129:
a * H, H * b are_equipotent
proof
defpred P[object,object] means ex g1 st $1 = g1 & $2 = a" * g1 * b;
A1: for x being object st x in a * H ex y being object st P[x,y]
proof
let x be object;
assume x in a * H;
then reconsider g = x as Element of G;
reconsider y = a" * g * b as set;
take y;
take g;
thus thesis;
end;
consider f being Function such that
A2: dom f = a * H and
A3: for x being object st x in a * H holds P[x,f.x] from CLASSES1:sch 1(A1);
A4: rng f = H * b
proof
thus rng f c= H * b
proof
let x be object;
assume x in rng f;
then consider y being object such that
A5: y in dom f and
A6: f.y = x by FUNCT_1:def 3;
consider g such that
A7: y = g and
A8: x = a" * g * b by A2,A3,A5,A6;
consider g1 such that
A9: g = a * g1 and
A10: g1 in H by A2,A5,A7,Th103;
x = a" * a * g1 * b by A8,A9,GROUP_1:def 3
.= 1_G * g1 * b by GROUP_1:def 5
.= g1 * b by GROUP_1:def 4;
hence thesis by A10,Th104;
end;
let x be object;
assume x in H * b;
then consider g such that
A11: x = g * b and
A12: g in H by Th104;
A13: a * g in dom f by A2,A12,Th103;
then ex g1 st g1 = a * g & f.(a * g) = a" * g1 * b by A2,A3;
then f.(a * g) = a" * a * g * b by GROUP_1:def 3
.= 1_G * g * b by GROUP_1:def 5
.= x by A11,GROUP_1:def 4;
hence thesis by A13,FUNCT_1:def 3;
end;
f is one-to-one
proof
let x,y be object;
assume that
A14: x in dom f and
A15: y in dom f and
A16: f.x = f.y;
consider g2 such that
A17: y = g2 and
A18: f.y = a" * g2 * b by A2,A3,A15;
consider g1 such that
A19: x = g1 and
A20: f.x = a" * g1 * b by A2,A3,A14;
a" * g1 = a" * g2 by A16,A20,A18,GROUP_1:6;
hence thesis by A19,A17,GROUP_1:6;
end;
hence thesis by A2,A4,WELLORD2:def 4;
end;
theorem Th130:
H * a, H * b are_equipotent
proof
H * a,b * H are_equipotent & b * H,H * b are_equipotent by Th129;
hence thesis by WELLORD2:15;
end;
theorem Th131:
carr(H), a * H are_equipotent & carr(H), H * a are_equipotent
proof
carr(H) = 1_G * H & carr(H) = H * 1_G by Th37;
hence thesis by Th128,Th130;
end;
theorem
card(H) = card(a * H) & card(H) = card(H * a)
by Th131,CARD_1:5;
theorem Th133:
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
let H be finite Subgroup of G;
reconsider B = a * H, C = H * a as finite set by Th131,CARD_1:38;
take B,C;
carr(H),a * H are_equipotent & carr(H),H * a are_equipotent by Th131;
hence thesis by CARD_1:5;
end;
definition
let G,H;
func Left_Cosets H -> Subset-Family of G means
:Def15:
A in it iff ex a st A = a * H;
existence
proof
defpred P[set] means ex a st $1 = a * H;
ex F be Subset-Family of G st for A being Subset of G holds A in F iff
P[A] from SUBSET_1:sch 3;
hence thesis;
end;
uniqueness
proof
defpred P[set] means ex a st $1 = a * H;
let F1,F2 be Subset-Family of G;
assume
A1: for A holds A in F1 iff P[A];
assume
A2: for A holds A in F2 iff P[A];
thus thesis from SUBSET_1:sch 4(A1,A2);
end;
func Right_Cosets H -> Subset-Family of G means
:Def16:
A in it iff ex a st A = H * a;
existence
proof
defpred P[set] means ex a st $1 = H * a;
ex F be Subset-Family of G st for A being Subset of G holds A in F iff
P[A] from SUBSET_1:sch 3;
hence thesis;
end;
uniqueness
proof
defpred P[set] means ex a st $1 = H * a;
let F1,F2 be Subset-Family of G;
assume
A3: for A holds A in F1 iff P[A];
assume
A4: for A holds A in F2 iff P[A];
thus thesis from SUBSET_1:sch 4(A3,A4);
end;
end;
theorem
G is finite implies Right_Cosets H is finite & Left_Cosets H is finite;
theorem Th135:
carr H in Left_Cosets H & carr H in Right_Cosets H
proof
carr H = 1_G * H & carr H = H * 1_G by Th37;
hence thesis by Def15,Def16;
end;
registration let G, H;
cluster Left_Cosets H -> non empty;
coherence by Th135;
cluster Right_Cosets H -> non empty;
coherence by Th135;
end;
theorem Th136:
Left_Cosets H, Right_Cosets H are_equipotent
proof
defpred P[object,object] means ex g st $1 = g * H & $2 = H * g";
A1: for x being object st x in Left_Cosets H ex y being object st P[x,y]
proof
let x be object;
assume x in Left_Cosets H;
then consider g such that
A2: x = g * H by Def15;
reconsider y = H * g" as set;
take y;
take g;
thus thesis by A2;
end;
consider f being Function such that
A3: dom f = Left_Cosets H and
A4: for x being object st x in Left_Cosets H holds P[x,f.x]
from CLASSES1:sch 1(A1);
A5: rng f = Right_Cosets H
proof
thus rng f c= Right_Cosets H
proof
let x be object;
assume x in rng f;
then consider y being object such that
A6: y in dom f and
A7: f.y = x by FUNCT_1:def 3;
ex g st y = g * H & f.y = H * g" by A3,A4,A6;
hence thesis by A7,Def16;
end;
let x be object;
assume
A8: x in Right_Cosets H;
then reconsider A = x as Subset of G;
consider g such that
A9: A = H * g by A8,Def16;
A10: g" * H in Left_Cosets H by Def15;
then
A11: f.(g" * H) in rng f by A3,FUNCT_1:def 3;
consider a such that
A12: g" * H = a * H and
A13: f.(g" * H) = H * a" by A4,A10;
a" * g" in H by A12,Th114;
hence thesis by A9,A11,A13,Th120;
end;
f is one-to-one
proof
let x,y be object;
assume that
A14: x in dom f and
A15: y in dom f and
A16: f.x = f.y;
consider b such that
A17: y = b * H and
A18: f.y = H * b" by A3,A4,A15;
consider a such that
A19: x = a * H and
A20: f.x = H * a" by A3,A4,A14;
b" * a"" in H by A16,A20,A18,Th120;
hence thesis by A19,A17,Th114;
end;
hence thesis by A3,A5,WELLORD2:def 4;
end;
theorem Th137:
union Left_Cosets H = the carrier of G &
union Right_Cosets H = the carrier of G
proof
thus union Left_Cosets H = the carrier of G
proof
set h = the Element of H;
reconsider g = h as Element of G by Th42;
thus union Left_Cosets H c= the carrier of G;
let x be object;
assume x in the carrier of G;
then reconsider a = x as Element of G;
A1: a = a * 1_G by GROUP_1:def 4
.= a * (g" * g) by GROUP_1:def 5
.= a * g" * g by GROUP_1:def 3;
A2: a * g" * H in Left_Cosets H by Def15;
h in H;
then a in a * g" * H by A1,Th103;
hence thesis by A2,TARSKI:def 4;
end;
set h = the Element of H;
reconsider g = h as Element of G by Th42;
thus union Right_Cosets H c= the carrier of G;
let x be object;
assume x in the carrier of G;
then reconsider a = x as Element of G;
A3: a = 1_G * a by GROUP_1:def 4
.= g * g" * a by GROUP_1:def 5
.= g * (g" * a) by GROUP_1:def 3;
A4: H * (g" * a) in Right_Cosets H by Def16;
h in H;
then a in H * (g" * a) by A3,Th104;
hence thesis by A4,TARSKI:def 4;
end;
theorem Th138:
Left_Cosets (1).G = the set of all {a}
proof
set A = the set of all {a};
thus Left_Cosets (1).G c= A
proof
let x be object;
assume
A1: x in Left_Cosets (1).G;
then reconsider X = x as Subset of G;
consider g such that
A2: X = g * (1).G by A1,Def15;
x = {g} by A2,Th110;
hence thesis;
end;
let x be object;
assume x in A;
then consider a such that
A3: x = {a};
a * (1).G = {a} by Th110;
hence thesis by A3,Def15;
end;
theorem
Right_Cosets (1).G = the set of all {a}
proof
set A = the set of all {a};
thus Right_Cosets (1).G c= A
proof
let x be object;
assume
A1: x in Right_Cosets (1).G;
then reconsider X = x as Subset of G;
consider g such that
A2: X = (1).G * g by A1,Def16;
x = {g} by A2,Th110;
hence thesis;
end;
let x be object;
assume x in A;
then consider a such that
A3: x = {a};
(1).G * a = {a} by Th110;
hence thesis by A3,Def16;
end;
theorem
for H being strict Subgroup of G holds Left_Cosets H = the set of all {a}
implies H = (1).G
proof
let H be strict Subgroup of G;
assume
A1: Left_Cosets H = the set of all {a};
A2: the carrier of H c= {1_G}
proof
set a = the Element of G;
let x be object;
assume x in the carrier of H;
then reconsider h = x as Element of H;
A3: h in H;
reconsider h as Element of G by Th42;
a * H in Left_Cosets H by Def15;
then consider b such that
A4: a * H = {b} by A1;
a * h in a * H by A3,Th103;
then
A5: a * h = b by A4,TARSKI:def 1;
1_G in H by Th46;
then a * 1_G in a * H by Th103;
then a * 1_G = b by A4,TARSKI:def 1;
then h = 1_G by A5,GROUP_1:6;
hence thesis by TARSKI:def 1;
end;
1_G in H by Th46;
then 1_G in the carrier of H;
then {1_G} c= the carrier of H by ZFMISC_1:31;
then {1_G} = the carrier of H by A2;
hence thesis by Def7;
end;
theorem
for H being strict Subgroup of G holds Right_Cosets H = the set of all {a}
implies H = (1).G
proof
let H be strict Subgroup of G;
assume
A1: Right_Cosets H = the set of all {a};
A2: the carrier of H c= {1_G}
proof
set a = the Element of G;
let x be object;
assume x in the carrier of H;
then reconsider h = x as Element of H;
A3: h in H;
reconsider h as Element of G by Th42;
H * a in Right_Cosets H by Def16;
then consider b such that
A4: H * a = {b} by A1;
h * a in H * a by A3,Th104;
then
A5: h * a = b by A4,TARSKI:def 1;
1_G in H by Th46;
then 1_G * a in H * a by Th104;
then 1_G * a = b by A4,TARSKI:def 1;
then h = 1_G by A5,GROUP_1:6;
hence thesis by TARSKI:def 1;
end;
1_G in H by Th46;
then 1_G in the carrier of H;
then {1_G} c= the carrier of H by ZFMISC_1:31;
then {1_G} = the carrier of H by A2;
hence thesis by Def7;
end;
theorem Th142:
Left_Cosets (Omega).G = {the carrier of G} &
Right_Cosets (Omega).G = {the carrier of G}
proof
set a = the Element of G;
A1: Left_Cosets (Omega).G c= {the carrier of G}
proof
let x be object;
assume
A2: x in Left_Cosets (Omega).G;
then reconsider X = x as Subset of G;
consider a such that
A3: X = a * (Omega).G by A2,Def15;
a * (Omega).G = the carrier of G by Th111;
hence thesis by A3,TARSKI:def 1;
end;
A4: Right_Cosets (Omega).G c= {the carrier of G}
proof
let x be object;
assume
A5: x in Right_Cosets (Omega).G;
then reconsider X = x as Subset of G;
consider a such that
A6: X = (Omega).G * a by A5,Def16;
(Omega).G * a = the carrier of G by Th111;
hence thesis by A6,TARSKI:def 1;
end;
(Omega). G * a = the carrier of G by Th111;
then the carrier of G in Right_Cosets(Omega).G by Def16;
then
A7: {the carrier of G} c= Right_Cosets(Omega).G by ZFMISC_1:31;
a * (Omega).G = the carrier of G by Th111;
then the carrier of G in Left_Cosets (Omega).G by Def15;
then {the carrier of G} c= Left_Cosets (Omega).G by ZFMISC_1:31;
hence thesis by A7,A1,A4;
end;
theorem Th143:
for G being strict Group, H being strict Subgroup of G holds
Left_Cosets H = {the carrier of G} implies H = G
proof
let G be strict Group, H be strict Subgroup of G;
assume Left_Cosets H = {the carrier of G};
then
A1: the carrier of G in Left_Cosets H by TARSKI:def 1;
then reconsider T = the carrier of G as Subset of G;
consider a being Element of G such that
A2: T = a * H by A1,Def15;
now
let g be Element of G;
ex b being Element of G st a * g = a * b & b in H by A2,Th103;
hence g in H by GROUP_1:6;
end;
hence thesis by Th62;
end;
theorem
for G being strict Group, H being strict Subgroup of G holds
Right_Cosets H = {the carrier of G} implies H = G
proof
let G be strict Group, H be strict Subgroup of G;
assume Right_Cosets H = {the carrier of G};
then
A1: the carrier of G in Right_Cosets H by TARSKI:def 1;
then reconsider T = the carrier of G as Subset of G;
consider a being Element of G such that
A2: T = H * a by A1,Def16;
now
let g be Element of G;
ex b being Element of G st g * a = b * a & b in H by A2,Th104;
hence g in H by GROUP_1:6;
end;
hence thesis by Th62;
end;
definition
let G,H;
func Index H -> Cardinal equals
card Left_Cosets H;
correctness;
end;
theorem
Index H = card Left_Cosets H & Index H = card Right_Cosets H
by Th136,CARD_1:5;
definition
let G,H;
assume
A1: Left_Cosets(H) is finite;
func index H -> Element of NAT means
:Def18:
ex B being finite set st B = Left_Cosets H & it = card B;
existence
proof
reconsider B = Left_Cosets(H) as finite set by A1;
take card B, B;
thus thesis;
end;
uniqueness;
end;
theorem
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
proof
assume Left_Cosets H is finite;
then reconsider B = Left_Cosets H as finite set;
hereby
take B;
thus B = Left_Cosets H & index H = card B by Def18;
end;
then reconsider C = Right_Cosets H as finite set by Th136,CARD_1:38;
take C;
index H = card B & B, C are_equipotent by Def18,Th136;
hence thesis by CARD_1:5;
end;
Lm5: 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
proof
let X be finite set;
per cases;
suppose
A1: X = {};
reconsider E = {} as finite set;
assume
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;
take E;
thus thesis by A1,CARD_1:27,ZFMISC_1:2;
end;
suppose
X <> {};
then reconsider D = X as non empty set;
defpred P[Element of Fin D] means (for Y st Y in $1 ex B being finite set
st B = Y & card B = k & for Z st Z in $1 & Y <> Z holds Y,Z are_equipotent & Y
misses Z) implies ex C being finite set st C = union $1 & card C = k * card $1;
A2: for S being Element of Fin D, s being Element of D st P[S] & not s in
S holds P[S \/ {.s.}]
proof
let S be Element of Fin D, s be Element of D;
assume that
A3: (for Y st Y in S ex B being finite set st B = Y & card B = k &
for Z st Z in S & Y <> Z holds Y,Z are_equipotent & Y misses Z) implies ex C
being finite set st C = union S & card C = k * card S and
A4: not s in S and
A5: for Y st Y in S \/ {s} ex B being finite set st B = Y & card B =
k & for Z st Z in S \/ {s} & Y <> Z holds Y,Z are_equipotent & Y misses Z;
A6: card(S \/ {s}) = card S + 1 by A4,CARD_2:41;
now
let Y;
assume Y in S;
then Y in S \/ {s} by XBOOLE_0:def 3;
then ex B being finite set st B = Y & card B = k & for Z st Z in S \/
{s} & Y <> Z holds Y,Z are_equipotent & Y misses Z by A5;
hence Y is finite;
end;
then reconsider D1 = union S as finite set by FINSET_1:7;
A7: now
let Y,Z;
assume Y in S;
then Y in S \/ {s} by XBOOLE_0:def 3;
then consider B being finite set such that
A8: B = Y & card B = k and
A9: for Z st Z in S \/ {s} & Y <> Z holds Y,Z are_equipotent & Y
misses Z by A5;
take B;
thus B = Y & card B = k by A8;
let Z;
assume that
A10: Z in S and
A11: Y <> Z;
Z in S \/ {s} by A10,XBOOLE_0:def 3;
hence Y,Z are_equipotent & Y misses Z by A9,A11;
end;
s in {s} by TARSKI:def 1;
then s in S \/ {s} by XBOOLE_0:def 3;
then
A12: ex B being finite set st B = s & card B = k & for Z st Z in S \/ {s}
& s <> Z holds s,Z are_equipotent & s misses Z by A5;
then reconsider T = s as finite set;
A13: union{s} = s by ZFMISC_1:25;
then
A14: union(S \/ {s}) = D1 \/ T by ZFMISC_1:78;
then reconsider D2 = union(S \/ {s}) as finite set;
take D2;
thus D2 = union(S \/ {s});
now
assume union S meets union{s};
then consider x being object such that
A15: x in union S and
A16: x in union{s} by XBOOLE_0:3;
consider Y such that
A17: x in Y and
A18: Y in S by A15,TARSKI:def 4;
consider Z such that
A19: x in Z and
A20: Z in {s} by A16,TARSKI:def 4;
A21: Z in S \/ {s} by A20,XBOOLE_0:def 3;
Y in S \/ {s} by A18,XBOOLE_0:def 3;
then
A22: ex B being finite set st B = Y & card B = k & for Z st Z in S \/ {
s} & Y <> Z holds Y,Z are_equipotent & Y misses Z by A5;
Z <> Y by A4,A18,A20,TARSKI:def 1;
then Y misses Z by A21,A22;
hence contradiction by A17,A19,XBOOLE_0:3;
end;
hence card D2 = k * card S + k * 1 by A3,A13,A12,A14,A7,CARD_2:40
.= k * card(S \/ {s}) by A6;
end;
A23: X is Element of Fin D by FINSUB_1:def 5;
A24: P[{}.D] by ZFMISC_1:2;
for B being Element of Fin D holds P[B] from SETWISEO:sch 2(A24,A2 );
hence thesis by A23;
end;
end;
::$N Lagrange Theorem for Groups
::$L https://en.wikipedia.org/wiki/Lagrange's_theorem_(group_theory) Lagrange Theorem for Groups
theorem Th147:
for G being finite Group, H being Subgroup of G holds
card G = card H * index H
proof
let G be finite Group, H be Subgroup of G;
reconsider C = Left_Cosets H as finite set;
now
let X be set;
assume
A1: X in C;
then reconsider x = X as Subset of G;
x is finite;
then reconsider B = X as finite set;
take B;
thus B = X;
consider a being Element of G such that
A2: x = a * H by A1,Def15;
ex B,C being finite set st B = a * H & C = H * a & card H = card B &
card H = card C by Th133;
hence card B = card H by A2;
let Y;
assume that
A3: Y in C and
A4: X <> Y;
reconsider y = Y as Subset of G by A3;
A5: ex b being Element of G st y = b * H by A3,Def15;
hence X,Y are_equipotent by A2,Th128;
thus X misses Y by A2,A4,A5,Th115;
end;
then
A6: ex D being finite set st D = union C & card D = card H * card C by Lm5;
union Left_Cosets H = the carrier of G by Th137;
hence thesis by A6,Def18;
end;
theorem
for G being finite Group, H being Subgroup of G holds card H divides card G
proof
let G be finite Group, H being Subgroup of G;
card G = card H * index H by Th147;
hence thesis by NAT_D:def 3;
end;
theorem
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
proof
let G be finite Group, I, H be Subgroup of G, J be Subgroup of H;
assume
A1: I = J;
card G = card H * index H & card H = card J * index J by Th147;
then card I * (index J * index H) = card I * index I by A1,Th147;
hence thesis by XCMPLX_1:5;
end;
theorem
index (Omega).G = 1
proof
Left_Cosets (Omega).G = {the carrier of G} by Th142;
hence index (Omega).G = card{the carrier of G} by Def18
.= 1 by CARD_1:30;
end;
theorem
for G being strict Group, H being strict Subgroup of G holds
Left_Cosets H is finite & index H = 1 implies H = G
proof
let G be strict Group, H be strict Subgroup of G;
assume that
A1: Left_Cosets H is finite and
A2: index H = 1;
reconsider B = Left_Cosets H as finite set by A1;
card B = 1 by A2,Def18;
then consider x being object such that
A3: Left_Cosets H = {x} by CARD_2:42;
union {x} = x & union Left_Cosets H = the carrier of G by Th137,ZFMISC_1:25;
hence thesis by A3,Th143;
end;
theorem
Index (1).G = card G
proof
deffunc F(object) = {$1};
consider f being Function such that
A1: dom f = the carrier of G and
A2: for x being object st x in the carrier of G holds f.x = F(x)
from FUNCT_1:sch 3;
A3: rng f = Left_Cosets (1).G
proof
thus rng f c= Left_Cosets (1).G
proof
let x be object;
assume x in rng f;
then consider y being object such that
A4: y in dom f and
A5: f.y = x by FUNCT_1:def 3;
reconsider y as Element of G by A1,A4;
x = {y} by A2,A5;
then x in the set of all {a};
hence thesis by Th138;
end;
let x be object;
assume x in Left_Cosets (1).G;
then x in the set of all {a} by Th138;
then consider a such that
A6: x = {a};
f.a = {a} by A2;
hence thesis by A1,A6,FUNCT_1:def 3;
end;
f is one-to-one
proof
let x,y be object;
assume that
A7: x in dom f & y in dom f and
A8: f.x = f.y;
f.y = {y} & f.x = {x} by A1,A2,A7;
hence thesis by A8,ZFMISC_1:3;
end;
then the carrier of G,Left_Cosets (1).G are_equipotent
by A1,A3,WELLORD2:def 4;
hence thesis by CARD_1:5;
end;
theorem
for G being finite Group holds index (1).G = card G
proof
let G be finite Group;
thus card G = card (1).G * index (1).G by Th147
.= 1 * index (1).G by Th69
.= index (1).G;
end;
theorem Th154:
for G being finite Group, H being strict Subgroup of G holds
index H = card G implies H = (1).G
proof
let G be finite Group, H be strict Subgroup of G;
assume index H = card G;
then 1 * card G = card H * card G by Th147;
hence thesis by Th70,XCMPLX_1:5;
end;
theorem
for H being strict Subgroup of G holds Left_Cosets H is finite &
Index H = card G implies G is finite & H = (1).G
proof
let H be strict Subgroup of G;
assume that
A1: Left_Cosets H is finite and
A2: Index H = card G;
thus
A3: G is finite by A1,A2;
ex B being finite set st B = Left_Cosets H & index H = card B by A1,Def18;
hence thesis by A2,A3,Th154;
end;
::
:: Auxiliary theorems.
::
theorem
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 by Lm5;