:: The Product of the Families of the Groups
:: by Artur Korni{\l}owicz
::
:: Received June 10, 1998
:: Copyright (c) 1998-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 FUNCT_1, PBOOLE, RELAT_1, XBOOLE_0, ALGSTR_0, PRALG_1, FUNCOP_1,
SUBSET_1, RLVECT_2, STRUCT_0, CARD_3, TARSKI, BINOP_1, ZFMISC_1,
MONOID_0, GROUP_1, SEMI_AF1, GROUP_2, FINSET_1, FUNCT_4, REALSET1,
FINSEQ_1, NAT_1, XXREAL_0, GROUP_6, FUNCT_2, WELLORD1, GROUP_7, PARTFUN1;
notations TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1,
ORDINAL1, NAT_1, FINSEQ_1, RELSET_1, PARTFUN1, FUNCT_2, FUNCT_4,
FINSET_1, BINOP_1, REALSET1, XXREAL_0, PBOOLE, FUNCOP_1, STRUCT_0,
ALGSTR_0, MONOID_0, GROUP_1, GROUP_2, GROUP_6, CARD_3, PRALG_1;
constructors BINOP_1, XXREAL_0, REALSET1, GROUP_6, MONOID_0, PRALG_1, PRALG_2,
RELSET_1, FUNCT_4;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, FINSET_1, XREAL_0,
FINSEQ_1, REALSET1, STRUCT_0, GROUP_1, GROUP_2, MONOID_0, ORDINAL1,
CARD_3, FUNCOP_1, RELSET_1, FUNCT_4;
requirements NUMERALS, BOOLE, SUBSET;
begin :: The product of the families of the groups
reserve i, I for set,
f, g, h for Function,
s for ManySortedSet of I;
definition
let R be Relation;
attr R is multMagma-yielding means
:: GROUP_7:def 1
for y being set st y in rng R holds y is non empty multMagma;
end;
registration
cluster multMagma-yielding -> 1-sorted-yielding for Function;
end;
registration
let I be set;
cluster multMagma-yielding for ManySortedSet of I;
end;
registration
cluster multMagma-yielding for Function;
end;
definition
let I be set;
mode multMagma-Family of I is multMagma-yielding ManySortedSet of I;
end;
definition
let I be non empty set, F be multMagma-Family of I, i be Element of I;
redefine func F.i -> non empty multMagma;
end;
registration
let I be set, F be multMagma-Family of I;
cluster Carrier F -> non-empty;
end;
definition
let I be set, F be multMagma-Family of I;
func product F -> strict multMagma means
:: GROUP_7:def 2
the carrier of it = product
Carrier F & for f, g being Element of product Carrier F, i being set st i in I
ex Fi being non empty multMagma, h being Function st Fi = F.i & h = (the multF
of it).(f,g) & h.i = (the multF of Fi).(f.i,g.i);
end;
registration
let I be set, F be multMagma-Family of I;
cluster product F -> non empty constituted-Functions;
end;
theorem :: GROUP_7:1
for F being multMagma-Family of I, G being non empty multMagma, p
, q being Element of product F, x, y being Element of G st i in I & G = F.i & f
= p & g = q & h = p * q & f.i = x & g.i = y holds x * y = h.i;
definition
let I be set, F be multMagma-Family of I;
attr F is Group-like means
:: GROUP_7:def 3
for i being set st i in I ex Fi being
Group-like non empty multMagma st Fi = F.i;
attr F is associative means
:: GROUP_7:def 4
for i being set st i in I ex Fi being
associative non empty multMagma st Fi = F.i;
attr F is commutative means
:: GROUP_7:def 5
for i being set st i in I ex Fi being
commutative non empty multMagma st Fi = F.i;
end;
definition
let I be non empty set, F be multMagma-Family of I;
redefine attr F is Group-like means
:: GROUP_7:def 6
for i being Element of I holds F. i is Group-like;
redefine attr F is associative means
:: GROUP_7:def 7
for i being Element of I holds F .i is associative;
redefine attr F is commutative means
:: GROUP_7:def 8
for i being Element of I holds F.i is commutative;
end;
registration
let I be set;
cluster Group-like associative commutative for multMagma-Family of I;
end;
registration
let I be set, F be Group-like multMagma-Family of I;
cluster product F -> Group-like;
end;
registration
let I be set, F be associative multMagma-Family of I;
cluster product F -> associative;
end;
registration
let I be set, F be commutative multMagma-Family of I;
cluster product F -> commutative;
end;
theorem :: GROUP_7:2
for F being multMagma-Family of I, G being non empty multMagma st i in
I & G = F.i & product F is Group-like holds G is Group-like;
theorem :: GROUP_7:3
for F being multMagma-Family of I, G being non empty multMagma st i in
I & G = F.i & product F is associative holds G is associative;
theorem :: GROUP_7:4
for F being multMagma-Family of I, G being non empty multMagma st i in
I & G = F.i & product F is commutative holds G is commutative;
theorem :: GROUP_7:5
for F being Group-like multMagma-Family of I st for i being set
st i in I ex G being Group-like non empty multMagma st G = F.i & s.i = 1_G
holds s = 1_product F;
theorem :: GROUP_7:6
for F being Group-like multMagma-Family of I, G being Group-like
non empty multMagma st i in I & G = F.i & f = 1_product F holds f.i = 1_G;
theorem :: GROUP_7:7
for F being associative Group-like multMagma-Family of I, x
being Element of product F st x = g & for i being set st i in I ex G being
Group, y being Element of G st G = F.i & s.i = y" & y = g.i holds s = x";
theorem :: GROUP_7:8
for F being associative Group-like multMagma-Family of I, x
being Element of product F, G being Group, y being Element of G st i in I & G =
F.i & f = x & g = x" & f.i = y holds g.i = y";
definition
let I be set, F be associative Group-like multMagma-Family of I;
func sum F -> strict Subgroup of product F means
:: GROUP_7:def 9
for x being object
holds x in the carrier of it iff ex g being Element of product Carrier F, J
being finite Subset of I, f being ManySortedSet of J st g = 1_product F & x = g
+* f & for j being set st j in J ex G being Group-like non empty multMagma st
G = F.j & f.j in the carrier of G & f.j <> 1_G;
end;
registration
let I be set, F be associative Group-like multMagma-Family of I, f, g be
Element of sum F;
cluster (the multF of sum F).(f,g) -> Function-like Relation-like;
end;
theorem :: GROUP_7:9
for I being finite set, F being associative Group-like
multMagma-Family of I holds product F = sum F;
begin :: The product of one, two and three groups
theorem :: GROUP_7:10
for G1 being non empty multMagma holds <*G1*> is multMagma-Family of {1};
registration
let G1 be non empty multMagma;
cluster <*G1*> -> {1} -defined;
end;
registration
let G1 be non empty multMagma;
cluster <*G1*> -> total multMagma-yielding;
end;
theorem :: GROUP_7:11
for G1 being Group-like non empty multMagma holds <*G1*> is
Group-like multMagma-Family of {1};
registration
let G1 be Group-like non empty multMagma;
cluster <*G1*> -> Group-like;
end;
theorem :: GROUP_7:12
for G1 being associative non empty multMagma holds <*G1*> is
associative multMagma-Family of {1};
registration
let G1 be associative non empty multMagma;
cluster <*G1*> -> associative;
end;
theorem :: GROUP_7:13
for G1 being commutative non empty multMagma holds <*G1*> is
commutative multMagma-Family of {1};
registration
let G1 be commutative non empty multMagma;
cluster <*G1*> -> commutative;
end;
theorem :: GROUP_7:14
for G1 being Group holds <*G1*> is Group-like associative
multMagma-Family of {1};
theorem :: GROUP_7:15
for G1 being commutative Group holds <*G1*> is commutative
Group-like associative multMagma-Family of {1};
registration
let G1 be non empty multMagma;
cluster -> FinSequence-like for Element of product Carrier <*G1*>;
end;
registration
let G1 be non empty multMagma;
cluster -> FinSequence-like for Element of product <*G1*>;
end;
definition
let G1 be non empty multMagma, x be Element of G1;
redefine func <*x*> -> Element of product <*G1*>;
end;
theorem :: GROUP_7:16
for G1, G2 being non empty multMagma holds <*G1,G2*> is
multMagma-Family of {1,2};
registration
let G1, G2 be non empty multMagma;
cluster <*G1,G2*> -> {1,2} -defined;
end;
registration
let G1, G2 be non empty multMagma;
cluster <*G1,G2*> -> total multMagma-yielding;
end;
theorem :: GROUP_7:17
for G1, G2 being Group-like non empty multMagma holds <*G1,G2
*> is Group-like multMagma-Family of {1,2};
registration
let G1, G2 be Group-like non empty multMagma;
cluster <*G1,G2*> -> Group-like;
end;
theorem :: GROUP_7:18
for G1, G2 being associative non empty multMagma holds <*G1,G2
*> is associative multMagma-Family of {1,2};
registration
let G1, G2 be associative non empty multMagma;
cluster <*G1,G2*> -> associative;
end;
theorem :: GROUP_7:19
for G1, G2 being commutative non empty multMagma holds <*G1,G2
*> is commutative multMagma-Family of {1,2};
registration
let G1, G2 be commutative non empty multMagma;
cluster <*G1,G2*> -> commutative;
end;
theorem :: GROUP_7:20
for G1, G2 being Group holds <*G1,G2*> is Group-like associative
multMagma-Family of {1,2};
theorem :: GROUP_7:21
for G1, G2 being commutative Group holds <*G1,G2*> is Group-like
associative commutative multMagma-Family of {1,2};
registration
let G1, G2 be non empty multMagma;
cluster -> FinSequence-like for Element of product Carrier <*G1,G2*>;
end;
registration
let G1, G2 be non empty multMagma;
cluster -> FinSequence-like for Element of product <*G1,G2*>;
end;
definition
let G1, G2 be non empty multMagma, x be Element of G1, y be Element of G2;
redefine func <*x,y*> -> Element of product <*G1,G2*>;
end;
theorem :: GROUP_7:22
for G1, G2, G3 being non empty multMagma holds <*G1,G2,G3*> is
multMagma-Family of {1,2,3};
registration
let G1, G2, G3 be non empty multMagma;
cluster <*G1,G2,G3*> -> {1,2,3} -defined;
end;
registration
let G1, G2, G3 be non empty multMagma;
cluster <*G1,G2,G3*> -> total multMagma-yielding;
end;
theorem :: GROUP_7:23
for G1, G2, G3 being Group-like non empty multMagma holds <*G1
,G2,G3*> is Group-like multMagma-Family of {1,2,3};
registration
let G1, G2, G3 be Group-like non empty multMagma;
cluster <*G1,G2,G3*> -> Group-like;
end;
theorem :: GROUP_7:24
for G1, G2, G3 being associative non empty multMagma holds <*
G1,G2,G3*> is associative multMagma-Family of {1,2,3};
registration
let G1, G2, G3 be associative non empty multMagma;
cluster <*G1,G2,G3*> -> associative;
end;
theorem :: GROUP_7:25
for G1, G2, G3 being commutative non empty multMagma holds <*
G1,G2,G3*> is commutative multMagma-Family of {1,2,3};
registration
let G1, G2, G3 be commutative non empty multMagma;
cluster <*G1,G2,G3*> -> commutative;
end;
theorem :: GROUP_7:26
for G1, G2, G3 being Group holds <*G1,G2,G3*> is Group-like
associative multMagma-Family of {1,2,3};
theorem :: GROUP_7:27
for G1, G2, G3 being commutative Group holds <*G1,G2,G3*> is
Group-like associative commutative multMagma-Family of {1,2,3};
registration
let G1, G2, G3 be non empty multMagma;
cluster -> FinSequence-like for Element of product Carrier <*G1,G2,G3*>;
end;
registration
let G1, G2, G3 be non empty multMagma;
cluster -> FinSequence-like for Element of product <*G1,G2,G3*>;
end;
definition
let G1, G2, G3 be non empty multMagma, x be Element of G1, y be Element of
G2, z be Element of G3;
redefine func <*x,y,z*> -> Element of product <*G1,G2,G3*>;
end;
reserve G1, G2, G3 for non empty multMagma,
x1, x2 for Element of G1,
y1, y2 for Element of G2,
z1, z2 for Element of G3;
theorem :: GROUP_7:28
<*x1*> * <*x2*> = <*x1*x2*>;
theorem :: GROUP_7:29
<*x1,y1*> * <*x2,y2*> = <*x1*x2,y1*y2*>;
theorem :: GROUP_7:30
<*x1,y1,z1*> * <*x2,y2,z2*> = <*x1*x2,y1*y2,z1*z2*>;
reserve G1, G2, G3 for Group-like non empty multMagma;
theorem :: GROUP_7:31
1_product <*G1*> = <*1_G1*>;
theorem :: GROUP_7:32
1_product <*G1,G2*> = <*1_G1,1_G2*>;
theorem :: GROUP_7:33
1_product <*G1,G2,G3*> = <*1_G1,1_G2,1_G3*>;
reserve G1, G2, G3 for Group,
x for Element of G1,
y for Element of G2,
z for Element of G3;
theorem :: GROUP_7:34
(<*x*> qua Element of product <*G1*>)" = <*x"*>;
theorem :: GROUP_7:35
(<*x,y*> qua Element of product <*G1,G2*>)" = <*x",y"*>;
theorem :: GROUP_7:36
(<*x,y,z*> qua Element of product <*G1,G2,G3*>)" = <*x",y",z" *>;
theorem :: GROUP_7:37
for f being Function of the carrier of G1, the carrier of
product <*G1*> st for x being Element of G1 holds f.x = <*x*> holds f is
Homomorphism of G1, product <*G1*>;
theorem :: GROUP_7:38
for f being Homomorphism of G1, product <*G1*> st for x being
Element of G1 holds f.x = <*x*> holds f is bijective;
theorem :: GROUP_7:39
G1, product <*G1*> are_isomorphic;