:: The Product of the Families of the Groups
:: by Artur Korni{\l}owicz
::
:: Received June 10, 1998
:: Copyright (c) 1998-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 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,
AFINSQ_1, ORDINAL4;
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,
AFINSQ_1,
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, AFINSQ_1;
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, AFINSQ_1, PBOOLE;
requirements NUMERALS, BOOLE, SUBSET;
definitions STRUCT_0, GROUP_1, TARSKI, GROUP_6, XBOOLE_0, PRALG_1, FUNCT_1,
PBOOLE;
equalities FINSEQ_1, BINOP_1, REALSET1, ALGSTR_0;
expansions GROUP_1, TARSKI, FINSEQ_1, FUNCT_1;
theorems PRALG_1, FUNCT_1, CARD_3, FUNCT_2, BINOP_1, TARSKI, ZFMISC_1,
GROUP_1, GROUP_2, GROUP_6, FUNCT_4, FINSEQ_1, FINSEQ_3, ENUMSET1,
RELSET_1, XBOOLE_0, XBOOLE_1, RELAT_1, FUNCOP_1, MONOID_0, PARTFUN1,
AFINSQ_1;
schemes BINOP_1, FUNCT_1, PBOOLE, FUNCT_2, XBOOLE_0;
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 :Def1:
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;
coherence
proof
let f be Function such that
A1: f is multMagma-yielding;
let x be object;
assume x in dom f;
then f.x in rng f by FUNCT_1:def 3;
hence thesis by A1;
end;
end;
registration
let I be set;
cluster multMagma-yielding for ManySortedSet of I;
existence
proof
set H = the non empty multMagma;
set f = I --> H;
take f;
let a be set;
assume a in rng f;
then ex x being object st x in dom f & a = f.x by FUNCT_1:def 3;
hence thesis by FUNCOP_1:7;
end;
end;
registration
cluster multMagma-yielding for Function;
existence
proof
set I = the set,f = the multMagma-yielding ManySortedSet of I;
take f;
thus thesis;
end;
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; :: redefines . (FUNCT_1, definition)
coherence
proof
dom F = I by PARTFUN1:def 2;
then F.i in rng F by FUNCT_1:def 3;
hence thesis by Def1;
end;
end;
registration
let I be set, F be multMagma-Family of I;
cluster Carrier F -> non-empty;
coherence
proof
let i be object;
assume
A1: i in I;
dom F = I by PARTFUN1:def 2;
then F.i in rng F by A1,FUNCT_1:def 3;
then
A2: F.i is non empty multMagma by Def1;
ex R being 1-sorted st R = F.i & (Carrier F).i = the carrier of R by A1,
PRALG_1:def 15;
hence thesis by A2;
end;
end;
Lm1: now
let I be non empty set, i be Element of I, F be multMagma-yielding
ManySortedSet of I, f be Element of product Carrier F;
A1: dom Carrier F = I by PARTFUN1:def 2;
ex R being 1-sorted st R = F.i & (Carrier F).i = the carrier of R by
PRALG_1:def 15;
hence f.i in the carrier of (F.i) by A1,CARD_3:9;
end;
definition
let I be set, F be multMagma-Family of I;
func product F -> strict multMagma means :Def2:
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);
existence
proof
set A = product Carrier F;
defpred P[Element of A, Element of A, set] means for i being set st i in I
ex Fi being non empty multMagma, h being Function st Fi = F.i & h = $3 & h.i =
(the multF of Fi).($1.i,$2.i);
A1: dom Carrier F = I by PARTFUN1:def 2;
A2: for x, y being Element of A ex z being Element of A st P[x,y,z]
proof
let x, y be Element of A;
defpred R[object,object] means
ex Fi being non empty multMagma st Fi = F.$1 &
$2 = (the multF of Fi).(x.$1,y.$1);
A3: for i being object st i in I
ex w being object st w in union rng Carrier F & R[i,w]
proof
let i be object;
assume
A4: i in I;
then reconsider I1 = I as non empty set;
reconsider i1 = i as Element of I1 by A4;
reconsider F1 = F as multMagma-Family of I1;
take w = (the multF of (F1.i1)).(x.i1,y.i1);
A5: (Carrier F).i1 in rng Carrier F by A1,FUNCT_1:def 3;
A6: ex R being 1-sorted st R = F.i1 & (Carrier F1).i1 = the carrier of
R by PRALG_1:def 15;
then
A7: y.i1 in the carrier of (F1.i1) by A1,CARD_3:9;
x.i1 in the carrier of (F1.i1) by A1,A6,CARD_3:9;
then (the multF of (F1.i1)).(x.i1,y.i1) in the carrier of (F1. i1)
by A7,BINOP_1:17;
hence w in union rng Carrier F by A6,A5,TARSKI:def 4;
thus thesis;
end;
consider z being Function such that
A8: dom z = I & rng z c= union rng Carrier F & for x being object st x
in I holds R[x,z.x] from FUNCT_1:sch 6(A3);
A9: for i being object st i in dom Carrier F holds z.i in (Carrier F).i
proof
let i be object;
assume
A10: i in dom Carrier F;
then reconsider I1 = I as non empty set;
A11: ex Fi being non empty multMagma st Fi = F.i & z.i = (the multF of
Fi).(x.i,y.i) by A8,A10;
reconsider i1 = i as Element of I1 by A10;
reconsider F1 = F as multMagma-Family of I1;
A12: ex R being 1-sorted st R = F.i & (Carrier F).i = the carrier of R
by A10,PRALG_1:def 15;
then
A13: y.i1 in the carrier of (F1.i1) by A1,CARD_3:9;
x.i1 in the carrier of (F1.i1) by A1,A12,CARD_3:9;
hence thesis by A11,A12,A13,BINOP_1:17;
end;
dom z = dom Carrier F by A8,PARTFUN1:def 2;
then reconsider z as Element of A by A9,CARD_3:9;
take z;
let i be set;
assume i in I;
then consider Fi being non empty multMagma such that
A14: Fi = F.i and
A15: z.i = (the multF of Fi).(x.i,y.i) by A8;
take Fi, z;
thus Fi = F.i & z = z & z.i = (the multF of Fi).(x.i,y.i) by A14,A15;
end;
consider B being BinOp of A such that
A16: for a, b being Element of A holds P[a,b,B.(a,b)] from BINOP_1:sch
3(A2);
take multMagma (#A,B#);
thus the carrier of multMagma (#A,B#) = product Carrier F;
let f, g be Element of product Carrier F, i be set;
assume i in I;
hence thesis by A16;
end;
uniqueness
proof
let A, B be strict multMagma such that
A17: the carrier of A = product Carrier F and
A18: 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 A).(f,g) & h.i = (the multF of Fi).(f.i,g.i) and
A19: the carrier of B = product Carrier F and
A20: 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 B).(f,g) & h.i = (the multF of Fi).(f.i,g.i);
for x, y being set st x in the carrier of A & y in the carrier of A
holds (the multF of A).(x,y) = (the multF of B).(x,y)
proof
set P = product Carrier F;
let x, y be set such that
A21: x in the carrier of A and
A22: y in the carrier of A;
reconsider x1 = x, y1 = y as Element of P by A17,A21,A22;
[x1,y1] in [:the carrier of A, the carrier of A:] by A21,A22,ZFMISC_1:87;
then reconsider f = (the multF of A).[x1,y1] as Element of P by A17,
FUNCT_2:5;
[x1,y1] in [:the carrier of B, the carrier of B:] by A19,ZFMISC_1:87;
then reconsider g = (the multF of B).[x1,y1] as Element of P by A19,
FUNCT_2:5;
A23: dom Carrier F = I by PARTFUN1:def 2;
then
A24: dom g = I by CARD_3:9;
A25: for i being object st i in I holds f.i = g.i
proof
let i be object;
assume
A26: i in I;
then
A27: ex Gi being non empty multMagma, h2 being Function st Gi = F.i &
h2 = (the multF of B).(x1,y1) & h2.i = (the multF of Gi).(x1.i,y1.i) by A20;
ex Fi being non empty multMagma, h1 being Function st Fi = F.i &
h1 = (the multF of A).(x1,y1) & h1.i = (the multF of Fi).(x1.i,y1.i) by A18,A26
;
hence thesis by A27;
end;
dom f = I by A23,CARD_3:9;
hence thesis by A24,A25,FUNCT_1:2;
end;
hence thesis by A17,A19,BINOP_1:1;
end;
end;
registration
let I be set, F be multMagma-Family of I;
cluster product F -> non empty constituted-Functions;
coherence
proof
A1: the carrier of product F = product Carrier F by Def2;
hence the carrier of product F is non empty;
thus thesis by A1,MONOID_0:80;
end;
end;
registration
let I be empty set, F be multMagma-Family of I;
cluster product F -> trivial;
coherence
proof
now
let f, g be object;
assume f in the carrier of product F & g in the carrier of product F;
then f in product Carrier F & g in product Carrier F by Def2;
then f = {} & g = {};
hence f = g;
end;
hence thesis by ZFMISC_1:def 10;
end;
end;
theorem Th1:
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
proof
let F be multMagma-Family of I, G be non empty multMagma,
p, q be Element of product F, x, y be Element of G such that
A1: i in I and
A2: G = F.i and
A3: f = p and
A4: g = q and
A5: h = p * q and
A6: f.i = x and
A7: g.i = y;
set GP = product F;
q in the carrier of GP;
then
A8: g in product Carrier F by A4,Def2;
p in the carrier of GP;
then f in product Carrier F by A3,Def2;
then
ex Fi being non empty multMagma, m being Function st Fi = F.i & m = (
the multF of GP).(f,g) & m.i = (the multF of Fi).(f.i,g.i) by A1,A8,Def2;
hence thesis by A2,A3,A4,A5,A6,A7;
end;
definition
let I be set, F be multMagma-Family of I;
attr F is Group-like means :Def3:
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 :Def4:
for i being set st i in I
ex Fi being associative non empty multMagma st Fi = F.i;
attr F is commutative means :Def5:
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 :Def6: :: redefines Group-like (GROUP_7, definition)
for i being Element of I holds F. i is Group-like;
compatibility
proof
hereby
assume
A1: F is Group-like;
let i be Element of I;
ex Fi being Group-like non empty multMagma st Fi = F.i by A1;
hence F.i is Group-like;
end;
assume
A2: for i being Element of I holds F.i is Group-like;
let i be set;
assume i in I;
then reconsider i1 = i as Element of I;
reconsider F1 = F.i1 as Group-like non empty multMagma by A2;
take F1;
thus thesis;
end;
redefine attr F is associative means :: redefines associative (GROUP_7, definition)
:Def7:
for i being Element of I holds F .i is associative;
compatibility
proof
hereby
assume
A3: F is associative;
let i be Element of I;
ex Fi being associative non empty multMagma st Fi = F.i by A3;
hence F.i is associative;
end;
assume
A4: for i being Element of I holds F.i is associative;
let i be set;
assume i in I;
then reconsider i1 = i as Element of I;
reconsider Fi = F.i1 as associative non empty multMagma by A4;
take Fi;
thus thesis;
end;
redefine attr F is commutative means :: redefines commutative (GROUP_7, definition)
for i being Element of I holds F.i is commutative;
compatibility
proof
hereby
assume
A5: F is commutative;
let i be Element of I;
ex Fi being commutative non empty multMagma st Fi = F.i by A5;
hence F.i is commutative;
end;
assume
A6: for i being Element of I holds F.i is commutative;
let i be set;
assume i in I;
then reconsider i1 = i as Element of I;
reconsider Fi = F.i1 as commutative non empty multMagma by A6;
take Fi;
thus thesis;
end;
end;
registration
let I be set;
cluster Group-like associative commutative for multMagma-Family of I;
existence
proof
set H = the commutative Group;
set f = I --> H;
f is multMagma-yielding
proof
let i be set;
assume i in rng f;
then ex x being object st x in dom f & i = f.x by FUNCT_1:def 3;
hence thesis by FUNCOP_1:7;
end;
then reconsider f as multMagma-Family of I;
take f;
hereby
let i be set;
assume
A1: i in I;
then reconsider I1 = I as non empty set;
reconsider i1 = i as Element of I1 by A1;
reconsider F1 = f as multMagma-Family of I1;
reconsider Fi = F1.i1 as Group-like non empty multMagma;
take Fi;
thus Fi = f.i;
end;
hereby
let i be set;
assume
A2: i in I;
then reconsider I1 = I as non empty set;
reconsider i1 = i as Element of I1 by A2;
reconsider F1 = f as multMagma-Family of I1;
reconsider Fi = F1.i1 as associative non empty multMagma;
take Fi;
thus Fi = f.i;
end;
let i be set;
assume
A3: i in I;
then reconsider I1 = I as non empty set;
reconsider i1 = i as Element of I1 by A3;
reconsider F1 = f as multMagma-Family of I1;
reconsider Fi = F1.i1 as commutative non empty multMagma;
take Fi;
thus thesis;
end;
end;
registration
let I be set, F be Group-like multMagma-Family of I;
cluster product F -> Group-like;
coherence
proof
defpred P[object,object] means
ex Fi being non empty multMagma, e being Element
of Fi st Fi = F.$1 & $2 = e & for h being Element of Fi holds h * e = h & e * h
= h & ex g being Element of Fi st h * g = e & g * h = e;
set G = product F;
A1: dom Carrier F = I by PARTFUN1:def 2;
A2: for i being object st i in I
ex y being object st y in union rng Carrier F & P[i,y]
proof
let i be object;
assume
A3: i in I;
then reconsider I1 = I as non empty set;
reconsider i1 = i as Element of I1 by A3;
reconsider F1 = F as Group-like multMagma-Family of I1;
A4: ex R being 1-sorted st R = F.i1 & (Carrier F1).i1 = the carrier of R
by PRALG_1:def 15;
F1.i1 is Group-like by Def6;
then consider e being Element of F1.i1 such that
A5: for h being Element of F1.i1 holds h * e = h & e * h = h & ex g
being Element of F1.i1 st h * g = e & g * h = e;
take e;
(Carrier F).i1 in rng Carrier F by A1,FUNCT_1:def 3;
hence e in union rng Carrier F by A4,TARSKI:def 4;
take F1.i1, e;
thus F1.i1 = F.i & e = e;
let h be Element of F1.i1;
thus thesis by A5;
end;
consider ee being Function such that
A6: dom ee = I and
rng ee c= union rng Carrier F and
A7: for x being object st x in I holds P[x,ee.x] from FUNCT_1:sch 6(A2);
now
let i be object;
assume
A8: i in dom ee;
then
A9: ex R being 1-sorted st R = F.i & (Carrier F).i = the carrier of R
by A6,PRALG_1:def 15;
ex Fi being non empty multMagma, e being Element of Fi st Fi = F.i
& ee.i = e & for h being Element of Fi holds h * e = h & e * h = h & ex g
being Element of Fi st h * g = e & g * h = e by A6,A7,A8;
hence ee.i in (Carrier F).i by A9;
end;
then
A10: ee in product Carrier F by A1,A6,CARD_3:9;
then reconsider e1 = ee as Element of G by Def2;
take e1;
let h be Element of G;
reconsider h1 = h as Element of product Carrier F by Def2;
reconsider he = (the multF of G).(h,e1), eh = (the multF of G).(e1,h) as
Element of product Carrier F by Def2;
A11: dom h1 = I by A1,CARD_3:9;
A12: now
let i be object;
assume
A13: i in I;
then consider
Fi being non empty multMagma, e2 being Element of Fi such that
A14: Fi = F.i and
A15: ee.i = e2 and
A16: for h being Element of Fi holds h * e2 = h & e2 * h = h & ex g
being Element of Fi st h * g = e2 & g * h = e2 by A7;
reconsider h2 = h1.i as Element of Fi by A13,A14,Lm1;
A17: ex Gi being non empty multMagma, f being Function st Gi = F.i & f =
(the multF of G).(h1,e1) & f.i = (the multF of Gi).(h1.i,ee.i) by A10,A13,Def2;
h2 * e2 = h2 by A16;
hence he.i = h1.i by A17,A14,A15;
end;
dom he = I by A1,CARD_3:9;
hence h * e1 = h by A11,A12;
A18: now
let i be object;
assume
A19: i in I;
then consider
Fi being non empty multMagma, e2 being Element of Fi such that
A20: Fi = F.i and
A21: ee.i = e2 and
A22: for h being Element of Fi holds h * e2 = h & e2 * h = h & ex g
being Element of Fi st h * g = e2 & g * h = e2 by A7;
reconsider h2 = h1.i as Element of Fi by A19,A20,Lm1;
A23: ex Gi being non empty multMagma, f being Function st Gi = F.i & f =
(the multF of G).(e1,h1) & f.i = (the multF of Gi).(ee.i,h1.i) by A10,A19,Def2;
e2 * h2 = h2 by A22;
hence eh.i = h1.i by A23,A20,A21;
end;
defpred R[object,object] means
ex Fi being non empty multMagma, hi being Element
of Fi st Fi = F.$1 & hi = h1.$1 & ex g being Element of Fi st hi * g = ee.$1 &
g * hi = ee.$1 & $2 = g;
A24: for i being object st i in I
ex y being object st y in union rng Carrier F & R[i,y]
proof
let i be object;
assume
A25: i in I;
then consider
Fi being non empty multMagma, e being Element of Fi such that
A26: Fi = F.i and
A27: ee.i = e and
A28: for h being Element of Fi holds h * e = h & e * h = h & ex g
being Element of Fi st h * g = e & g * h = e by A7;
A29: ex R being 1-sorted st R = F.i & (Carrier F).i = the carrier of R
by A25,PRALG_1:def 15;
reconsider hi = h1.i as Element of Fi by A25,A26,Lm1;
consider g being Element of Fi such that
A30: hi * g = e and
A31: g * hi = e by A28;
take g;
(Carrier F).i in rng Carrier F by A1,A25,FUNCT_1:def 3;
hence g in union rng Carrier F by A26,A29,TARSKI:def 4;
take Fi, hi;
thus Fi = F.i & hi = h1.i by A26;
take g;
thus thesis by A27,A30,A31;
end;
consider gg being Function such that
A32: dom gg = I and
rng gg c= union rng Carrier F and
A33: for x being object st x in I holds R[x,gg.x] from FUNCT_1:sch 6(A24);
now
let i be object;
assume
A34: i in dom gg;
then
A35: ex R being 1-sorted st R = F.i & (Carrier F).i = the carrier of R
by A32,PRALG_1:def 15;
ex Fi being non empty multMagma, hi being Element of Fi st Fi = F.
i & hi = h1.i & ex g being Element of Fi st hi * g = ee.i & g * hi = ee.i &
gg.i = g by A32,A33,A34;
hence gg.i in (Carrier F).i by A35;
end;
then
A36: gg in product Carrier F by A1,A32,CARD_3:9;
then reconsider g1 = gg as Element of G by Def2;
dom eh = I by A1,CARD_3:9;
hence e1 * h = h by A11,A18;
take g1;
reconsider he = (the multF of G).(h,g1), eh = (the multF of G).(g1,h) as
Element of product Carrier F by Def2;
A37: now
let i be object;
assume
A38: i in I;
then
A39: ex Fi being non empty multMagma, hi being Element of Fi st Fi = F.i
& hi = h1.i & ex g being Element of Fi st hi * g = ee.i & g * hi = ee.i & gg.i
= g by A33;
ex Gi being non empty multMagma, h5 being Function st Gi = F.i &
h5 = (the multF of G).(h1,gg) & h5.i = (the multF of Gi).(h1.i,gg.i) by A36,A38
,Def2;
hence he.i = ee.i by A39;
end;
A40: now
let i be object;
assume
A41: i in I;
then
A42: ex Fi being non empty multMagma, hi being Element of Fi st Fi = F.
i & hi = h1.i & ex g being Element of Fi st hi * g = ee.i & g * hi = ee.i &
gg.i = g by A33;
ex Gi being non empty multMagma, h5 being Function st Gi = F.i &
h5 = (the multF of G).(gg,h1) & h5.i = (the multF of Gi).(gg.i,h1.i) by A36,A41
,Def2;
hence eh.i = ee.i by A42;
end;
dom he = I by A1,CARD_3:9;
hence h * g1 = e1 by A6,A37;
dom eh = I by A1,CARD_3:9;
hence thesis by A6,A40;
end;
end;
registration
let I be set, F be associative multMagma-Family of I;
cluster product F -> associative;
coherence
proof
set G = product F;
let x, y, z be Element of G;
reconsider x1 = x, y1 = y, z1 = z as Element of product Carrier F by Def2;
set xy = (the multF of G).(x,y), yz = (the multF of G).(y,z), s = (the
multF of G).(xy,z), t = (the multF of G).(x,yz);
reconsider xy, yz, s, t as Element of product Carrier F by Def2;
A1: dom Carrier F = I by PARTFUN1:def 2;
then
A2: dom t = I by CARD_3:9;
A3: now
let i be object;
assume
A4: i in I;
then consider XY being non empty multMagma, hxy being Function such that
A5: XY = F.i and
A6: hxy = (the multF of G).(x,y) and
A7: hxy.i = (the multF of XY).(x1.i,y1.i) by Def2;
A8: ex YZ being non empty multMagma, hyz being Function st YZ = F.i &
hyz = (the multF of G).(y,z) & hyz.i = (the multF of YZ).(y1.i,z1.i) by A4,Def2
;
reconsider xi = x1.i, yi = y1.i as Element of XY by A4,A5,Lm1;
consider XYZ1 being non empty multMagma, hxyz1 being Function such that
A9: XYZ1 = F.i and
A10: hxyz1 = (the multF of G).(xy,z) and
A11: hxyz1.i = (the multF of XYZ1).(xy.i,z1.i) by A4,Def2;
reconsider zi = z1.i, xiyi = xi*yi as Element of XYZ1 by A4,A5,A9,Lm1;
reconsider xii = xi, yii = yi as Element of XYZ1 by A5,A9;
A12: XYZ1 is associative by A4,A9,Def7;
A13: ex XYZ2 being non empty multMagma, hxyz2 being Function st XYZ2 =
F.i & hxyz2 = (the multF of G).(x,yz) & hxyz2.i = (the multF of XYZ2). (x1.i,
yz.i) by A4,Def2;
thus s.i = xiyi*zi by A6,A7,A10,A11
.= xii*(yii*zi) by A5,A9,A12
.= t.i by A8,A9,A13;
end;
dom s = I by A1,CARD_3:9;
hence thesis by A2,A3;
end;
end;
registration
let I be set, F be commutative multMagma-Family of I;
cluster product F -> commutative;
coherence
proof
set G = product F;
let x, y be Element of G;
reconsider x1 = x, y1 = y, xy = (the multF of G).(x,y), yx = (the multF of
G).(y,x) as Element of product Carrier F by Def2;
A1: dom Carrier F = I by PARTFUN1:def 2;
then
A2: dom yx = I by CARD_3:9;
A3: now
let i be object;
assume
A4: i in I;
then consider XY being non empty multMagma, hxy being Function such that
A5: XY = F.i and
A6: hxy = (the multF of G).(x,y) and
A7: hxy.i = (the multF of XY).(x1.i,y1.i) by Def2;
reconsider xi = x1.i, yi = y1.i as Element of XY by A4,A5,Lm1;
A8: ex YX being non empty multMagma, hyx being Function st YX = F.i &
hyx = (the multF of G).(y,x) & hyx.i = (the multF of YX).(y1.i,x1.i) by A4,Def2
;
A9: ex Fi being commutative non empty multMagma st ( Fi = F.i) by A4,Def5;
thus xy.i = xi * yi by A6,A7
.= yi * xi by A5,A9,GROUP_1:def 12
.= yx.i by A5,A8;
end;
dom xy = I by A1,CARD_3:9;
hence thesis by A2,A3;
end;
end;
theorem
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
proof
let F be multMagma-Family of I, G be non empty multMagma such that
A1: i in I and
A2: G = F.i;
set GP = product F;
given e being Element of GP such that
A3: for h being Element of GP holds h * e = h & e * h = h & ex g being
Element of GP st h * g = e & g * h = e;
reconsider f = e as Element of product Carrier F by Def2;
reconsider ei = f.i as Element of G by A1,A2,Lm1;
take ei;
let h be Element of G;
defpred P[object,object] means
($1 = i implies $2 = h) & ($1 <> i implies ex H
being non empty multMagma, a being Element of H st H = F.$1 & $2 = a);
A4: for j being object st j in I ex k being object st P[j,k]
proof
let j be object such that
A5: j in I;
per cases;
suppose
j = i;
hence thesis;
end;
suppose
A6: j <> i;
j in dom F by A5,PARTFUN1:def 2;
then F.j in rng F by FUNCT_1:def 3;
then reconsider Fj = F.j as non empty multMagma by Def1;
set a = the Element of Fj;
take a;
thus j = i implies a = h by A6;
thus thesis;
end;
end;
consider g being ManySortedSet of I such that
A7: for j being object st j in I holds P[j,g.j] from PBOOLE:sch 3(A4);
A8: dom g = I by PARTFUN1:def 2;
A9: now
let j be object;
assume
A10: j in dom g;
then
A11: ex R being 1-sorted st R = F.j & (Carrier F).j = the carrier of R
by PRALG_1:def 15;
per cases;
suppose
A12: i = j;
then g.j = h by A7,A10;
hence g.j in (Carrier F).j by A2,A11,A12;
end;
suppose
j <> i;
then ex H being non empty multMagma, a being Element of H st H = F.j &
g.j = a by A7,A10;
hence g.j in (Carrier F).j by A11;
end;
end;
dom Carrier F = I by PARTFUN1:def 2;
then reconsider g as Element of product Carrier F by A8,A9,CARD_3:9;
A13: g.i = h by A1,A7;
reconsider g1 = g as Element of GP by Def2;
A14: e * g1 = g1 by A3;
g1 * e = g1 by A3;
hence h * ei = h & ei * h = h by A1,A2,A13,A14,Th1;
consider gg being Element of GP such that
A15: g1 * gg = e and
A16: gg * g1 = e by A3;
reconsider r = gg as Element of product Carrier F by Def2;
reconsider r1 = r.i as Element of G by A1,A2,Lm1;
take r1;
thus thesis by A1,A2,A13,A15,A16,Th1;
end;
theorem
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
proof
let F be multMagma-Family of I, G be non empty multMagma such that
A1: i in I and
A2: G = F.i and
A3: for x, y, z being Element of product F holds (x*y)*z = x*(y*z);
let x, y, z be Element of G;
defpred Y[object,object] means
($1 = i implies $2 = y) & ($1 <> i implies ex H
being non empty multMagma, a being Element of H st H = F.$1 & $2 = a);
A4: for j being object st j in I ex k being object st Y[j,k]
proof
let j be object such that
A5: j in I;
per cases;
suppose
j = i;
hence thesis;
end;
suppose
A6: j <> i;
j in dom F by A5,PARTFUN1:def 2;
then F.j in rng F by FUNCT_1:def 3;
then reconsider Fj = F.j as non empty multMagma by Def1;
set a = the Element of Fj;
take a;
thus j = i implies a = y by A6;
thus thesis;
end;
end;
consider gy being ManySortedSet of I such that
A7: for j being object st j in I holds Y[j,gy.j] from PBOOLE:sch 3(A4);
A8: dom gy = I by PARTFUN1:def 2;
A9: now
let j be object;
assume
A10: j in dom gy;
then
A11: ex R being 1-sorted st R = F.j & (Carrier F).j = the carrier of R
by PRALG_1:def 15;
per cases;
suppose
A12: i = j;
then gy.j = y by A7,A10;
hence gy.j in (Carrier F).j by A2,A11,A12;
end;
suppose
j <> i;
then ex H being non empty multMagma, a being Element of H st H = F.j &
gy.j = a by A7,A10;
hence gy.j in (Carrier F).j by A11;
end;
end;
defpred Z[object,object] means
($1 = i implies $2 = z) & ($1 <> i implies ex H
being non empty multMagma, a being Element of H st H = F.$1 & $2 = a);
A13: for j being object st j in I ex k being object st Z[j,k]
proof
let j be object such that
A14: j in I;
per cases;
suppose
j = i;
hence thesis;
end;
suppose
A15: j <> i;
j in dom F by A14,PARTFUN1:def 2;
then F.j in rng F by FUNCT_1:def 3;
then reconsider Fj = F.j as non empty multMagma by Def1;
set a = the Element of Fj;
take a;
thus j = i implies a = z by A15;
thus thesis;
end;
end;
consider gz being ManySortedSet of I such that
A16: for j being object st j in I holds Z[j,gz.j] from PBOOLE:sch 3(A13);
set GP = product F;
defpred X[object,object] means
($1 = i implies $2 = x) & ($1 <> i implies ex H
being non empty multMagma, a being Element of H st H = F.$1 & $2 = a);
A17: for j being object st j in I ex k being object st X[j,k]
proof
let j be object such that
A18: j in I;
per cases;
suppose
j = i;
hence thesis;
end;
suppose
A19: j <> i;
j in dom F by A18,PARTFUN1:def 2;
then F.j in rng F by FUNCT_1:def 3;
then reconsider Fj = F.j as non empty multMagma by Def1;
set a = the Element of Fj;
take a;
thus j = i implies a = x by A19;
thus thesis;
end;
end;
consider gx being ManySortedSet of I such that
A20: for j being object st j in I holds X[j,gx.j] from PBOOLE:sch 3(A17);
A21: dom gx = I by PARTFUN1:def 2;
A22: now
let j be object;
assume
A23: j in dom gx;
then
A24: ex R being 1-sorted st R = F.j & (Carrier F).j = the carrier of R
by PRALG_1:def 15;
per cases;
suppose
A25: i = j;
then gx.j = x by A20,A23;
hence gx.j in (Carrier F).j by A2,A24,A25;
end;
suppose
j <> i;
then ex H being non empty multMagma, a being Element of H st H = F.j &
gx.j = a by A20,A23;
hence gx.j in (Carrier F).j by A24;
end;
end;
A26: dom gz = I by PARTFUN1:def 2;
A27: now
let j be object;
assume
A28: j in dom gz;
then
A29: ex R being 1-sorted st R = F.j & (Carrier F).j = the carrier of R
by PRALG_1:def 15;
per cases;
suppose
A30: i = j;
then gz.j = z by A16,A28;
hence gz.j in (Carrier F).j by A2,A29,A30;
end;
suppose
j <> i;
then ex H being non empty multMagma, a being Element of H st H = F.j &
gz.j = a by A16,A28;
hence gz.j in (Carrier F).j by A29;
end;
end;
A31: dom Carrier F = I by PARTFUN1:def 2;
then reconsider gx as Element of product Carrier F by A21,A22,CARD_3:9;
reconsider gz as Element of product Carrier F by A26,A31,A27,CARD_3:9;
reconsider gy as Element of product Carrier F by A8,A31,A9,CARD_3:9;
reconsider x1 = gx, y1 = gy, z1 = gz as Element of GP by Def2;
reconsider xy = x1*y1, xyz3 = x1*y1*z1, yz = y1*z1, xyz5 = x1*(y1*z1) as
Element of product Carrier F by Def2;
reconsider xyi = xy.i, yzi = yz.i as Element of G by A1,A2,Lm1;
A32: x1 * y1 * z1 = x1 * (y1 * z1) by A3;
A33: gx.i = x by A1,A20;
then
A34: x * yzi = xyz5.i by A1,A2,Th1;
A35: gz.i = z by A1,A16;
then
A36: xyi * z = xyz3.i by A1,A2,Th1;
A37: gy.i = y by A1,A7;
then xy.i = x * y by A1,A2,A33,Th1;
hence thesis by A1,A2,A32,A37,A35,A36,A34,Th1;
end;
theorem
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
proof
let F be multMagma-Family of I, G be non empty multMagma such that
A1: i in I and
A2: G = F.i and
A3: for x, y being Element of product F holds x*y = y*x;
let x, y be Element of G;
defpred Y[object,object] means
($1 = i implies $2 = y) & ($1 <> i implies ex H
being non empty multMagma, a being Element of H st H = F.$1 & $2 = a);
A4: for j being object st j in I ex k being object st Y[j,k]
proof
let j be object such that
A5: j in I;
per cases;
suppose
j = i;
hence thesis;
end;
suppose
A6: j <> i;
j in dom F by A5,PARTFUN1:def 2;
then F.j in rng F by FUNCT_1:def 3;
then reconsider Fj = F.j as non empty multMagma by Def1;
set a = the Element of Fj;
take a;
thus j = i implies a = y by A6;
thus thesis;
end;
end;
consider gy being ManySortedSet of I such that
A7: for j being object st j in I holds Y[j,gy.j] from PBOOLE:sch 3(A4);
set GP = product F;
defpred X[object,object] means
($1 = i implies $2 = x) & ($1 <> i implies ex H
being non empty multMagma, a being Element of H st H = F.$1 & $2 = a);
A8: for j being object st j in I ex k being object st X[j,k]
proof
let j be object such that
A9: j in I;
per cases;
suppose
j = i;
hence thesis;
end;
suppose
A10: j <> i;
j in dom F by A9,PARTFUN1:def 2;
then F.j in rng F by FUNCT_1:def 3;
then reconsider Fj = F.j as non empty multMagma by Def1;
set a = the Element of Fj;
take a;
thus j = i implies a = x by A10;
thus thesis;
end;
end;
consider gx being ManySortedSet of I such that
A11: for j being object st j in I holds X[j,gx.j] from PBOOLE:sch 3(A8);
A12: dom gy = I by PARTFUN1:def 2;
A13: now
let j be object;
assume
A14: j in dom gy;
then
A15: ex R being 1-sorted st R = F.j & (Carrier F).j = the carrier of R
by PRALG_1:def 15;
per cases;
suppose
A16: i = j;
then gy.j = y by A7,A14;
hence gy.j in (Carrier F).j by A2,A15,A16;
end;
suppose
j <> i;
then ex H being non empty multMagma, a being Element of H st H = F.j &
gy.j = a by A7,A14;
hence gy.j in (Carrier F).j by A15;
end;
end;
A17: dom Carrier F = I by PARTFUN1:def 2;
then reconsider gy as Element of product Carrier F by A12,A13,CARD_3:9;
A18: gy.i = y by A1,A7;
A19: dom gx = I by PARTFUN1:def 2;
now
let j be object;
assume
A20: j in dom gx;
then
A21: ex R being 1-sorted st R = F.j & (Carrier F).j = the carrier of R
by PRALG_1:def 15;
per cases;
suppose
A22: i = j;
then gx.j = x by A11,A20;
hence gx.j in (Carrier F).j by A2,A21,A22;
end;
suppose
j <> i;
then ex H being non empty multMagma, a being Element of H st H = F.j &
gx.j = a by A11,A20;
hence gx.j in (Carrier F).j by A21;
end;
end;
then reconsider gx as Element of product Carrier F by A19,A17,CARD_3:9;
reconsider x1 = gx, y1 = gy as Element of GP by Def2;
A23: x1 * y1 = y1 * x1 by A3;
reconsider xy = x1*y1 as Element of product Carrier F by Def2;
A24: gx.i = x by A1,A11;
then xy.i = x * y by A1,A2,A18,Th1;
hence thesis by A1,A2,A23,A24,A18,Th1;
end;
theorem Th5:
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
proof
let F be Group-like multMagma-Family of I such that
A1: for i being set st i in I ex G being Group-like non empty multMagma
st G = F.i & s.i = 1_G;
set GP = product F;
A2: dom Carrier F = I by PARTFUN1:def 2;
A3: dom s = I by PARTFUN1:def 2;
now
let i be object;
assume
A4: i in dom s;
then
A5: ex R being 1-sorted st R = F.i & (Carrier F).i = the carrier of R
by PRALG_1:def 15;
ex G being Group-like non empty multMagma st ( G = F.i)&( s.i = 1_G)
by A1,A4;
hence s.i in (Carrier F).i by A5;
end;
then
A6: s in product Carrier F by A3,A2,CARD_3:9;
then reconsider e = s as Element of GP by Def2;
now
let h be Element of GP;
reconsider h1 = h, he = h*e, eh = e*h as Element of product Carrier F by
Def2;
A7: dom h1 = I by A2,CARD_3:9;
A8: now
let i be object;
assume
A9: i in I;
then consider G being Group-like non empty multMagma such that
A10: G = F.i and
A11: s.i = 1_G by A1;
reconsider b = h1.i, c = s.i as Element of G by A9,A10,A11,Lm1;
A12: ex Fi being non empty multMagma, m being Function st Fi = F.i & m
= (the multF of GP).(h,s) & m.i = (the multF of Fi).(h1.i,s.i) by A6,A9,Def2;
b * c = b by A11,GROUP_1:def 4;
hence he.i = h1.i by A12,A10;
end;
dom he = I by A2,CARD_3:9;
hence h * e = h by A7,A8;
A13: now
let i be object;
assume
A14: i in I;
then consider G being Group-like non empty multMagma such that
A15: G = F.i and
A16: s.i = 1_G by A1;
reconsider b = h1.i, c = s.i as Element of G by A14,A15,A16,Lm1;
A17: ex Fi being non empty multMagma, m being Function st Fi = F.i & m
= (the multF of GP).(s,h) & m.i = (the multF of Fi).(s.i,h1.i) by A6,A14,Def2;
c * b = b by A16,GROUP_1:def 4;
hence eh.i = h1.i by A17,A15;
end;
dom eh = I by A2,CARD_3:9;
hence e * h = h by A7,A13;
end;
hence thesis by GROUP_1:4;
end;
theorem Th6:
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
proof
let F be Group-like multMagma-Family of I,
G be Group-like non empty multMagma such that
A1: i in I and
A2: G = F.i and
A3: f = 1_product F;
set GP = product F;
f in the carrier of GP by A3;
then
A4: f in product Carrier F by Def2;
then reconsider e = f.i as Element of G by A1,A2,Lm1;
now
let h be Element of G;
defpred P[object,object] means
($1 = i implies $2 = h) & ($1 <> i implies ex H
being Group-like non empty multMagma st H = F.$1 & $2 = 1_H);
A5: for j being object st j in I ex k being object st P[j,k]
proof
let j be object such that
A6: j in I;
per cases;
suppose
j = i;
hence thesis;
end;
suppose
A7: j <> i;
consider Fj being Group-like non empty multMagma such that
A8: Fj = F.j by A6,Def3;
take 1_Fj;
thus j = i implies 1_Fj = h by A7;
thus thesis by A8;
end;
end;
consider g being ManySortedSet of I such that
A9: for j being object st j in I holds P[j,g.j] from PBOOLE:sch 3(A5);
A10: dom g = I by PARTFUN1:def 2;
A11: now
let j be object;
assume
A12: j in dom g;
then
A13: ex R being 1-sorted st R = F.j & (Carrier F).j = the carrier of R
by PRALG_1:def 15;
per cases;
suppose
A14: i = j;
then g.j = h by A9,A12;
hence g.j in (Carrier F).j by A2,A13,A14;
end;
suppose
j <> i;
then ex H being Group-like non empty multMagma st ( H = F.j)&( g.j =
1_H) by A9,A12;
hence g.j in (Carrier F).j by A13;
end;
end;
dom Carrier F = I by PARTFUN1:def 2;
then
A15: g in product Carrier F by A10,A11,CARD_3:9;
then reconsider g1 = g as Element of GP by Def2;
A16: g1 * 1_product F = g1 by GROUP_1:def 4;
A17: g.i = h by A1,A9;
A18: g.i = h by A1,A9;
ex Fi being non empty multMagma, m being Function st Fi = F.i & m =
(the multF of GP).(g,f) & m.i = (the multF of Fi).(g.i,f.i) by A1,A4,A15
,Def2;
hence h * e = h by A2,A3,A16,A18;
A19: 1_product F * g1 = g1 by GROUP_1:def 4;
ex Fi being non empty multMagma, m being Function st Fi = F.i & m =
(the multF of GP).(f,g) & m.i = (the multF of Fi).(f.i,g.i) by A1,A4,A15
,Def2;
hence e * h = h by A2,A3,A19,A17;
end;
hence thesis by GROUP_1:4;
end;
theorem Th7:
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"
proof
let F be associative Group-like multMagma-Family of I, x be Element of
product F such that
A1: x = g and
A2: 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;
set GP = product F;
A3: dom Carrier F = I by PARTFUN1:def 2;
A4: dom s = I by PARTFUN1:def 2;
now
let i be object;
assume
A5: i in dom s;
then
A6: ex R being 1-sorted st R = F.i & (Carrier F).i = the carrier of R
by PRALG_1:def 15;
ex G being Group, y being Element of G st G = F.i & s.i = y" & y =
g.i by A2,A5;
hence s.i in (Carrier F).i by A6;
end;
then
A7: s in product Carrier F by A3,A4,CARD_3:9;
then reconsider f1 = s as Element of GP by Def2;
reconsider II = 1_GP, xf = x * f1, fx = f1 * x, x1 = x as Element of product
Carrier F by Def2;
A8: dom II = I by A3,CARD_3:9;
A9: now
let i be object;
assume
A10: i in I;
then consider G being Group, y being Element of G such that
A11: G = F.i and
A12: s.i = y" and
A13: y = g.i by A2;
A14: ex Fi being non empty multMagma, m being Function st Fi = F.i & m =
(the multF of GP).(s,x) & m.i = (the multF of Fi).(s.i,x1.i) by A7,A10,Def2;
y" * y = 1_G by GROUP_1:def 5;
hence fx.i = II.i by A1,A10,A14,A11,A12,A13,Th6;
end;
dom fx = I by A3,CARD_3:9;
then
A15: f1 * x = 1_GP by A8,A9;
A16: now
let i be object;
assume
A17: i in I;
then consider G being Group, y being Element of G such that
A18: G = F.i and
A19: s.i = y" and
A20: y = g.i by A2;
A21: ex Fi being non empty multMagma, m being Function st Fi = F.i & m =
(the multF of GP).(x,s) & m.i = (the multF of Fi).(x1.i,s.i) by A7,A17,Def2;
y * y" = 1_G by GROUP_1:def 5;
hence xf.i = II.i by A1,A17,A21,A18,A19,A20,Th6;
end;
dom xf = I by A3,CARD_3:9;
then x * f1 = 1_GP by A8,A16;
hence thesis by A15,GROUP_1:def 5;
end;
theorem Th8:
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"
proof
let F be associative Group-like multMagma-Family of I, x be Element of
product F, G be Group, y be Element of G such that
A1: i in I and
A2: G = F.i and
A3: f = x and
A4: g = x" and
A5: f.i = y;
set GP = product F;
A6: (the multF of GP).(g,f) = x" * x by A3,A4
.= 1_GP by GROUP_1:def 5;
x" in the carrier of GP;
then
A7: g in product Carrier F by A4,Def2;
then reconsider gi = g.i as Element of G by A1,A2,Lm1;
x in the carrier of GP;
then
A8: f in product Carrier F by A3,Def2;
then
ex Fi being non empty multMagma, h being Function st Fi = F.i & h = (
the multF of GP).(g,f) & h.i = (the multF of Fi).(g.i,f.i) by A1,A7,Def2;
then
A9: gi * y = 1_G by A1,A2,A5,A6,Th6;
A10: (the multF of GP).(f,g) = x * x" by A3,A4
.= 1_GP by GROUP_1:def 5;
ex Fi being non empty multMagma, h being Function st Fi = F.i & h = (
the multF of GP).(f,g) & h.i = (the multF of Fi).(f.i,g.i) by A1,A8,A7,Def2;
then y * gi = 1_G by A1,A2,A5,A10,Th6;
hence thesis by A9,GROUP_1:def 5;
end;
definition
let I be set, F be associative Group-like multMagma-Family of I;
func sum F -> strict Subgroup of product F means
:Def9:
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;
existence
proof
set GP = product F, CF = Carrier F;
A1: dom CF = I by PARTFUN1:def 2;
reconsider g = 1_GP as Element of product CF by Def2;
A2: dom g = dom CF by CARD_3:9;
defpred P[object] means
ex J being finite Subset of I, f being ManySortedSet
of J st $1 = 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;
consider A being set such that
A3: for x being object holds x in A iff x in product CF & P[x] from
XBOOLE_0:sch 1;
A4: A c= the carrier of GP
proof
let a be object;
assume a in A;
then a in product CF by A3;
hence thesis by Def2;
end;
A5: P[g]
proof
set J = {}I;
dom {} = J;
then reconsider f = {} as ManySortedSet of J by PARTFUN1:def 2
,RELAT_1:def 18;
take J, f;
thus g = g +* {}
.= g +* f;
thus thesis;
end;
then reconsider A as non empty set by A3;
set b = (the multF of GP)||A;
A6: for p be Element of product CF holds dom p = I by PARTFUN1:def 2;
dom b = [:A,A:] & rng b c= A
proof
dom the multF of GP = [:the carrier of GP,the carrier of GP:] by
FUNCT_2:def 1;
hence
A7: dom b = [:A,A:] by A4,RELAT_1:62,ZFMISC_1:96;
let y be object;
assume y in rng b;
then consider x being object such that
A8: x in dom b and
A9: b.x = y by FUNCT_1:def 3;
consider x1, x2 being object such that
A10: x1 in A and
A11: x2 in A and
A12: x = [x1,x2] by A7,A8,ZFMISC_1:def 2;
consider J1 being finite Subset of I, f1 being ManySortedSet of J1 such
that
A13: x1 = g +* f1 and
A14: for j being set st j in J1 ex G being Group-like non empty
multMagma st G = F.j & f1.j in the carrier of G & f1.j <> 1_G by A3,A10;
consider J2 being finite Subset of I, f2 being ManySortedSet of J2 such
that
A15: x2 = g +* f2 and
A16: for j being set st j in J2 ex G being Group-like non empty
multMagma st G = F.j & f2.j in the carrier of G & f2.j <> 1_G by A3,A11;
reconsider x1, x2 as Function by A13,A15;
A17: dom f1 = J1 by PARTFUN1:def 2;
A18: now
let i be object;
assume
A19: i in I;
then
A20: ex R being 1-sorted st R = F.i & CF.i = the carrier of R by
PRALG_1:def 15;
per cases;
suppose
A21: i in J1;
then ex G being Group-like non empty multMagma st G = F.i & f1.i
in the carrier of G & f1.i <> 1_G by A14;
hence x1.i in CF.i by A13,A17,A20,A21,FUNCT_4:13;
end;
suppose
A22: not i in J1;
consider G being Group-like non empty multMagma such that
A23: G = F.i by A19,Def3;
x1.i = g.i by A13,A17,A22,FUNCT_4:11
.= 1_G by A19,A23,Th6;
hence x1.i in CF.i by A20,A23;
end;
end;
A24: dom f2 = J2 by PARTFUN1:def 2;
A25: now
let i be object;
assume
A26: i in I;
then
A27: ex R being 1-sorted st R = F.i & CF.i = the carrier of R by
PRALG_1:def 15;
per cases;
suppose
A28: i in J2;
then ex G being Group-like non empty multMagma st G = F.i & f2.i
in the carrier of G & f2.i <> 1_G by A16;
hence x2.i in CF.i by A15,A24,A27,A28,FUNCT_4:13;
end;
suppose
A29: not i in J2;
consider G being Group-like non empty multMagma such that
A30: G = F.i by A26,Def3;
x2.i = g.i by A15,A24,A29,FUNCT_4:11
.= 1_G by A26,A30,Th6;
hence x2.i in CF.i by A27,A30;
end;
end;
A31: dom x1 = dom g \/ dom f1 by A13,FUNCT_4:def 1
.= I by A2,A1,A17,XBOOLE_1:12;
dom x2 = dom g \/ dom f2 by A15,FUNCT_4:def 1
.= I by A2,A1,A24,XBOOLE_1:12;
then reconsider x2 as Element of product CF by A1,A25,CARD_3:9;
reconsider x1 as Element of product CF by A1,A31,A18,CARD_3:9;
reconsider X1 = x1, X2 = x2 as Element of GP by Def2;
A32: [x1,x2] in [:A,A:] by A10,A11,ZFMISC_1:87;
then
A33: y = X1*X2 by A9,A12,FUNCT_1:49;
then reconsider y1 = y as Element of product CF by Def2;
defpred S[object] means
ex G being Group-like non empty multMagma, k1, k2
being Element of G st G = F.$1 & k1 = x1.$1 & k2 = x2.$1 & k1*k2 = 1_G & f1.$1
<> 1_G & f2.$1 <> 1_G;
consider K being set such that
A34: for k being object holds k in K iff k in I & S[k] from XBOOLE_0:
sch 1;
A35: P[y]
proof
defpred R[object,object] means
ex G being Group-like non empty multMagma,
k1, k2 being Element of G st G = F.$1 & k1 = x1.$1 & k2 = x2.$1 & $2 = k1*k2;
reconsider J = J1 \/ J2 \ K as finite Subset of I;
take J;
A36: dom y1 = I by A6;
A37: for j being object st j in J ex t being object st R[j,t]
proof
let j be object;
assume
A38: j in J;
then consider G being Group-like non empty multMagma such that
A39: G = F.j by Def3;
reconsider k1 = x1.j, k2 = x2.j as Element of G by A38,A39,Lm1;
take k1*k2;
thus thesis by A39;
end;
consider f being ManySortedSet of J such that
A40: for j being object st j in J holds R[j,f.j] from PBOOLE:sch 3(
A37);
take f;
set gf = g +* f;
A41: dom f = J by PARTFUN1:def 2;
A42: now
let i be object;
assume
A43: i in I;
then consider
Fi being non empty multMagma, h being Function such that
A44: Fi = F.i and
A45: h = (the multF of GP).(x1,x2) and
A46: h.i = (the multF of Fi).(x1.i,x2.i) by Def2;
consider FF being Group-like non empty multMagma such that
A47: FF = F.i by A43,Def3;
reconsider Fi as Group-like non empty multMagma by A44,A47;
reconsider x1i = x1.i, x2i = x2.i as Element of Fi by A43,A44,Lm1;
A48: y1.i = x1i * x2i by A9,A12,A32,A45,A46,FUNCT_1:49;
per cases;
suppose
A49: i in J;
then ex GG being Group-like non empty multMagma, k1a, k2a being
Element of GG st GG = F.i & k1a = x1.i & k2a = x2.i & f.i = k1a*k2a by A40;
hence y1.i = gf.i by A33,A41,A44,A45,A46,A49,FUNCT_4:13;
end;
suppose
A50: not i in J;
then
A51: gf.i = g.i by A41,FUNCT_4:11
.= 1_FF by A43,A47,Th6;
now
per cases by A50,XBOOLE_0:def 5;
case
A52: not i in J1 \/ J2;
then not i in J2 by XBOOLE_0:def 3;
then x2.i = g.i by A15,A24,FUNCT_4:11;
then
A53: x2.i = 1_FF by A43,A47,Th6;
not i in J1 by A52,XBOOLE_0:def 3;
then x1.i = g.i by A13,A17,FUNCT_4:11;
then x1.i = 1_FF by A43,A47,Th6;
hence y1.i = gf.i by A44,A47,A48,A51,A53,GROUP_1:def 4;
end;
case
i in K;
then ex GG being Group-like non empty multMagma, k1, k2
being Element of GG st GG = F.i & k1 = x1.i & k2 = x2.i & k1*k2 = 1_GG & f1.i
<> 1_GG & f2.i <> 1_GG by A34;
hence y1.i = gf.i by A33,A43,A47,A51,Th1;
end;
end;
hence y1.i = gf.i;
end;
end;
dom gf = dom g \/ dom f by FUNCT_4:def 1
.= I by A2,A1,A41,XBOOLE_1:12;
hence y = gf by A36,A42,FUNCT_1:2;
let j be set;
assume
A54: j in J;
then consider G being Group-like non empty multMagma, k1, k2 being
Element of G such that
A55: G = F.j and
A56: k1 = x1.j and
A57: k2 = x2.j and
A58: f.j = k1*k2 by A40;
take G;
thus G = F.j by A55;
thus f.j in the carrier of G by A58;
A59: j in J1 \/ J2 by A54,XBOOLE_0:def 5;
per cases by A59,XBOOLE_0:def 3;
suppose
A60: j in J1 & not j in J2;
then
A61: x1.j = f1.j by A13,A17,FUNCT_4:13;
consider G1 being Group-like non empty multMagma such that
A62: G1 = F.j and
f1.j in the carrier of G1 and
A63: f1.j <> 1_G1 by A14,A60;
x2.j = g.j by A15,A24,A60,FUNCT_4:11
.= 1_G1 by A54,A62,Th6;
hence thesis by A55,A56,A57,A58,A61,A62,A63,GROUP_1:def 4;
end;
suppose
A64: not j in J1 & j in J2;
then
A65: x2.j = f2.j by A15,A24,FUNCT_4:13;
consider G2 being Group-like non empty multMagma such that
A66: G2 = F.j and
f2.j in the carrier of G2 and
A67: f2.j <> 1_G2 by A16,A64;
x1.j = g.j by A13,A17,A64,FUNCT_4:11
.= 1_G2 by A54,A66,Th6;
hence thesis by A55,A56,A57,A58,A65,A66,A67,GROUP_1:def 4;
end;
suppose
A68: j in J1 & j in J2;
then
A69: ex G2 being Group-like non empty multMagma st G2 = F.j & f2.j
in the carrier of G2 & f2.j <> 1_G2 by A16;
A70: not j in K by A54,XBOOLE_0:def 5;
ex G1 being Group-like non empty multMagma st G1 = F.j & f1.j
in the carrier of G1 & f1.j <> 1_G1 by A14,A68;
hence thesis by A34,A54,A55,A56,A57,A58,A69,A70;
end;
end;
reconsider ff = X1*X2 as Element of product CF by Def2;
now
reconsider J = {} as finite Subset of I by XBOOLE_1:2;
take J;
thus for j being set st j in J ex G being Group-like non empty
multMagma st G = F.j & ff.j in the carrier of G & ff.j <> 1_G;
end;
hence thesis by A3,A33,A35;
end;
then reconsider b as BinOp of A by FUNCT_2:def 1,RELSET_1:4;
set H = multMagma (#A,b#);
H is Group-like
proof
reconsider e = g as Element of H by A3,A5;
take e;
let h be Element of H;
reconsider h1 = h as Element of GP by A4;
[h,e] in [:A,A:] by ZFMISC_1:87;
hence h * e = h1 * 1_GP by FUNCT_1:49
.= h by GROUP_1:def 4;
[e,h] in [:A,A:] by ZFMISC_1:87;
hence e * h = 1_GP * h1 by FUNCT_1:49
.= h by GROUP_1:def 4;
reconsider h2 = h1, hh = h1" as Element of product Carrier F by Def2;
A71: P[h1"]
proof
consider J being finite Subset of I, f being ManySortedSet of J such
that
A72: h = g +* f and
A73: 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 by A3;
defpred W[object,object] means
ex G being Group, m being Element of G st G =
F.$1 & m = f.$1 & $2 = m";
A74: for i being object st i in J ex j being object st W[i,j]
proof
let i be object;
assume
A75: i in J;
then consider Gg being Group-like non empty multMagma such that
A76: Gg = F.i by Def3;
ex Ga being associative non empty multMagma st Ga = F.i by A75,Def4;
then reconsider G = Gg as Group by A76;
ex GG being Group-like non empty multMagma st GG = F.i & f.i
in the carrier of GG & f.i <> 1_GG by A73,A75;
then reconsider m = f.i as Element of G by A76;
take m";
thus thesis by A76;
end;
consider f9 being ManySortedSet of J such that
A77: for j being object st j in J holds W[j,f9.j] from PBOOLE:sch 3(
A74);
set gf9 = g +* f9;
A78: dom f9 = J by PARTFUN1:def 2;
A79: dom f = J by PARTFUN1:def 2;
A80: now
let i be object;
assume
A81: i in I;
then consider G3 being Group-like non empty multMagma such that
A82: G3 = F.i by Def3;
ex G4 being associative non empty multMagma st G4 = F.i by A81,Def4;
then consider G5 being Group such that
A83: G5 = F.i by A82;
per cases;
suppose
A84: i in J;
then
A85: gf9.i = f9.i by A78,FUNCT_4:13;
A86: ex G being Group, m being Element of G st G = F.i & m = f.i
& f9.i = m" by A77,A84;
h2.i = f.i by A72,A79,A84,FUNCT_4:13;
hence hh.i = gf9.i by A81,A86,A85,Th8;
end;
suppose
A87: not i in J;
then
A88: gf9.i = g.i by A78,FUNCT_4:11
.= 1_G3 by A81,A82,Th6;
A89: 1_G5 = (1_G5)" by GROUP_1:8;
h2.i = g.i by A72,A79,A87,FUNCT_4:11
.= 1_G3 by A81,A82,Th6;
hence hh.i = gf9.i by A81,A82,A83,A88,A89,Th8;
end;
end;
take J;
take f9;
A90: dom hh = I by A6;
dom gf9 = dom g \/ dom f9 by FUNCT_4:def 1
.= I by A2,A1,A78,XBOOLE_1:12;
hence h1" = g +* f9 by A90,A80;
let j be set;
assume
A91: j in J;
then consider G being Group, m being Element of G such that
A92: G = F.j and
A93: m = f.j and
A94: f9.j = m" by A77;
take G;
thus G = F.j & f9.j in the carrier of G by A92,A94;
ex G1 being Group-like non empty multMagma st G1 = F.j & f.j
in the carrier of G1 & f.j <> 1_G1 by A73,A91;
hence thesis by A92,A93,A94,GROUP_1:10;
end;
product CF = the carrier of GP by Def2;
then reconsider h9 = h1" as Element of H by A3,A71;
take h9;
[h,h9] in [:A,A:] by ZFMISC_1:87;
hence h * h9 = h1 * h1" by FUNCT_1:49
.= e by GROUP_1:def 5;
[h9,h] in [:A,A:] by ZFMISC_1:87;
hence h9 * h = h1" * h1 by FUNCT_1:49
.= e by GROUP_1:def 5;
end;
then reconsider H as Group-like non empty multMagma;
reconsider H as strict Subgroup of GP by A4,GROUP_2:def 5;
take H;
let x be object;
hereby
assume x in the carrier of H;
then P[x] by A3;
hence ex g being Element of product CF, 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;
given g being Element of product CF, J being finite Subset of I, f being
ManySortedSet of J such that
A95: g = 1_product F and
A96: x = g +* f and
A97: 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;
A98: dom g = I by A6;
set gf = g +* f;
A99: dom f = J by PARTFUN1:def 2;
A100: now
let i be object;
assume
A101: i in I;
then
A102: ex R being 1-sorted st R = F.i & CF.i = the carrier of R by
PRALG_1:def 15;
per cases;
suppose
A103: i in J;
then ex G being Group-like non empty multMagma st ( G = F.i)&( f.i
in the carrier of G)&( f.i <> 1_G) by A97;
hence gf.i in CF.i by A99,A102,A103,FUNCT_4:13;
end;
suppose
A104: not i in J;
consider G being Group-like non empty multMagma such that
A105: G = F.i by A101,Def3;
gf.i = g.i by A99,A104,FUNCT_4:11
.= 1_G by A95,A101,A105,Th6;
hence gf.i in CF.i by A102,A105;
end;
end;
dom gf = dom g \/ dom f by FUNCT_4:def 1
.= I by A98,A99,XBOOLE_1:12;
then x in product CF by A1,A96,A100,CARD_3:9;
hence thesis by A3,A95,A96,A97;
end;
uniqueness
proof
defpred P[object] means
ex g being Element of product Carrier F, J being
finite Subset of I, f being ManySortedSet of J st g = 1_product F & $1 = 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;
let A, B be strict Subgroup of product F such that
A106: for x being object holds x in the carrier of A iff P[x] and
A107: for x being object holds x in the carrier of B iff P[x];
the carrier of A = the carrier of B from XBOOLE_0:sch 2(A106,A107);
hence thesis by GROUP_2:59;
end;
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;
coherence
proof
A1: (the multF of sum F).(f,g) in the carrier of sum F;
the carrier of sum F c= the carrier of product F by GROUP_2:def 5;
then reconsider
h = (the multF of sum F).(f,g) as Element of product Carrier F
by A1,Def2;
h is Function;
hence thesis;
end;
end;
theorem
for I being finite set,
F being associative Group-like multMagma-Family of I holds
product F = sum F
proof
let I be finite set, F be associative Group-like multMagma-Family of I;
set GP = product F, S = sum F;
A1: the carrier of S = the carrier of GP
proof
reconsider g = 1_GP as Element of product Carrier F by Def2;
thus the carrier of S c= the carrier of GP by GROUP_2:def 5;
let x be object;
assume x in the carrier of GP;
then reconsider f = x as Element of product Carrier F by Def2;
A2: for p be Element of product Carrier F holds dom p = I by PARTFUN1:def 2;
then
A3: dom f = I;
reconsider f as ManySortedSet of I;
ex g being Element of product Carrier F, J being finite Subset of I, f
being ManySortedSet of J st g = 1_GP & 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
proof
deffunc F(object) = f.$1;
defpred P[object] means ex G being Group-like non empty multMagma, m
being Element of G st G = F.$1 & m = f.$1 & m <> 1_G;
consider J being set such that
A4: for j being object holds j in J iff j in I & P[j] from XBOOLE_0:sch
1;
J c= I
by A4;
then reconsider J as Subset of I;
consider ff being ManySortedSet of J such that
A5: for j being object st j in J holds ff.j = F(j) from PBOOLE:sch 4;
A6: dom ff = J by PARTFUN1:def 2;
A7: now
let i be object such that
A8: i in I;
per cases;
suppose
A9: i in J;
hence f.i = ff.i by A5
.= (g +* ff).i by A6,A9,FUNCT_4:13;
end;
suppose
A10: not i in J;
consider G being Group-like non empty multMagma such that
A11: G = F.i by A8,Def3;
f.i is Element of G by A8,A11,Lm1;
hence f.i = 1_G by A4,A8,A10,A11
.= g.i by A8,A11,Th6
.= (g +* ff).i by A6,A10,FUNCT_4:11;
end;
end;
take g, J;
take ff;
thus g = 1_GP;
A12: dom g = I by A2;
dom (g +* ff) = dom g \/ dom ff by FUNCT_4:def 1
.= I by A6,A12,XBOOLE_1:12;
hence x = g +* ff by A3,A7,FUNCT_1:2;
let j be set;
assume
A13: j in J;
then consider
G being Group-like non empty multMagma, m being Element of G
such that
A14: G = F.j and
A15: m = f.j and
A16: m <> 1_G by A4;
take G;
ff.j = f.j by A5,A13;
hence thesis by A14,A15,A16;
end;
hence thesis by Def9;
end;
product F is Subgroup of product F by GROUP_2:54;
hence thesis by A1,GROUP_2:59;
end;
begin :: The product of one, two and three groups
theorem Th10:
for G1 being non empty multMagma holds <*G1*> is multMagma-Family of {1}
proof
let G1 be non empty multMagma;
dom <*G1*> = {1} by FINSEQ_1:2,def 8;
then reconsider A = <*G1*> as ManySortedSet of {1} by PARTFUN1:def 2
,RELAT_1:def 18;
A is multMagma-yielding
proof
let y be set;
assume y in rng A;
then consider x being object such that
A1: x in dom A and
A2: A.x = y by FUNCT_1:def 3;
x = 1 by A1,TARSKI:def 1;
hence thesis by A2;
end;
hence thesis;
end;
registration
let G1 be non empty multMagma;
cluster <*G1*> -> {1} -defined;
coherence by Th10;
end;
registration
let G1 be non empty multMagma;
cluster <*G1*> -> total multMagma-yielding;
coherence by Th10;
end;
theorem Th11:
for G1 being Group-like non empty multMagma holds
<*G1*> is Group-like multMagma-Family of {1}
proof
let G1 be Group-like non empty multMagma;
reconsider A = <*G1*> as multMagma-Family of {1};
A is Group-like
proof
let x be Element of {1};
x = 1 by TARSKI:def 1;
hence thesis;
end;
hence thesis;
end;
registration
let G1 be Group-like non empty multMagma;
cluster <*G1*> -> Group-like;
coherence by Th11;
end;
theorem Th12:
for G1 being associative non empty multMagma holds
<*G1*> is associative multMagma-Family of {1}
proof
let G1 be associative non empty multMagma;
reconsider A = <*G1*> as multMagma-Family of {1};
A is associative
proof
let x be Element of {1};
x = 1 by TARSKI:def 1;
hence thesis;
end;
hence thesis;
end;
registration
let G1 be associative non empty multMagma;
cluster <*G1*> -> associative;
coherence by Th12;
end;
theorem Th13:
for G1 being commutative non empty multMagma holds
<*G1*> is commutative multMagma-Family of {1}
proof
let G1 be commutative non empty multMagma;
reconsider A = <*G1*> as multMagma-Family of {1};
A is commutative
proof
let x be Element of {1};
x = 1 by TARSKI:def 1;
hence thesis;
end;
hence thesis;
end;
registration
let G1 be commutative non empty multMagma;
cluster <*G1*> -> commutative;
coherence by Th13;
end;
theorem
for G1 being Group holds
<*G1*> is Group-like associative multMagma-Family of {1};
theorem
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*>;
coherence by FINSEQ_1:2,PARTFUN1:def 2;
end;
registration
let G1 be non empty multMagma;
cluster -> FinSequence-like for Element of product <*G1*>;
coherence
proof
let x be Element of product <*G1*>;
reconsider y = x as Element of product Carrier <*G1*> by Def2;
y is FinSequence-like;
hence thesis;
end;
end;
definition
let G1 be non empty multMagma, x be Element of G1;
redefine func <*x*> -> Element of product <*G1*>; :: redefines <* (FINSEQ_1, definition)
coherence
proof
set xy = <*x*>, G = <*G1*>;
A1: dom Carrier G = {1} by PARTFUN1:def 2;
A4: for a being object st a in {1} holds xy.a in (Carrier G).a
proof
let a be object;
assume
A5: a in {1};
then
A6: a = 1 by TARSKI:def 1;
then
ex R being 1-sorted st R = G.1 & (Carrier G).1 = the carrier of R by A5,
PRALG_1:def 15;
hence thesis by A6;
end;
dom xy = {1} by FINSEQ_1:2,def 8;
then xy in product Carrier G by A1,A4,CARD_3:9;
hence thesis by Def2;
end;
end;
theorem Th16:
for G1, G2 being non empty multMagma holds
<*G1,G2*> is multMagma-Family of {1,2}
proof
let G1, G2 be non empty multMagma;
dom <*G1,G2*> = {1,2} by FINSEQ_1:2,89;
then reconsider A = <*G1,G2*> as ManySortedSet of {1,2} by PARTFUN1:def 2
,RELAT_1:def 18;
A is multMagma-yielding
proof
let y be set;
assume y in rng A;
then consider x being object such that
A1: x in dom A and
A2: A.x = y by FUNCT_1:def 3;
x = 1 or x = 2 by A1,TARSKI:def 2;
hence thesis by A2;
end;
hence thesis;
end;
registration
let G1, G2 be non empty multMagma;
cluster <*G1,G2*> -> {1,2} -defined;
coherence by Th16;
end;
registration
let G1, G2 be non empty multMagma;
cluster <*G1,G2*> -> total multMagma-yielding;
coherence by Th16;
end;
theorem Th17:
for G1, G2 being Group-like non empty multMagma holds
<*G1,G2*> is Group-like multMagma-Family of {1,2}
proof
let G1, G2 be Group-like non empty multMagma;
reconsider A = <*G1,G2*> as multMagma-Family of {1,2};
A is Group-like
proof
let x be Element of {1,2};
x = 1 or x = 2 by TARSKI:def 2;
hence thesis;
end;
hence thesis;
end;
registration
let G1, G2 be Group-like non empty multMagma;
cluster <*G1,G2*> -> Group-like;
coherence by Th17;
end;
theorem Th18:
for G1, G2 being associative non empty multMagma holds
<*G1,G2*> is associative multMagma-Family of {1,2}
proof
let G1, G2 be associative non empty multMagma;
reconsider A = <*G1,G2*> as multMagma-Family of {1,2};
A is associative
proof
let x be Element of {1,2};
x = 1 or x = 2 by TARSKI:def 2;
hence thesis;
end;
hence thesis;
end;
registration
let G1, G2 be associative non empty multMagma;
cluster <*G1,G2*> -> associative;
coherence by Th18;
end;
theorem Th19:
for G1, G2 being commutative non empty multMagma holds
<*G1,G2*> is commutative multMagma-Family of {1,2}
proof
let G1, G2 be commutative non empty multMagma;
reconsider A = <*G1,G2*> as multMagma-Family of {1,2};
A is commutative
proof
let x be Element of {1,2};
x = 1 or x = 2 by TARSKI:def 2;
hence thesis;
end;
hence thesis;
end;
registration
let G1, G2 be commutative non empty multMagma;
cluster <*G1,G2*> -> commutative;
coherence by Th19;
end;
theorem
for G1, G2 being Group holds
<*G1,G2*> is Group-like associative multMagma-Family of {1,2};
theorem
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*>;
coherence by FINSEQ_1:2,PARTFUN1:def 2;
end;
registration
let G1, G2 be non empty multMagma;
cluster -> FinSequence-like for Element of product <*G1,G2*>;
coherence
proof
let x be Element of product <*G1,G2*>;
reconsider y = x as Element of product Carrier <*G1,G2*> by Def2;
y is FinSequence-like;
hence thesis;
end;
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*>; :: redefines <* (FINSEQ_1, definition)
coherence
proof
set xy = <*x,y*>, G = <*G1,G2*>;
A1: dom Carrier G = {1,2} by PARTFUN1:def 2;
A6: for a being object st a in {1,2} holds xy.a in (Carrier G).a
proof
let a be object;
assume
A7: a in {1,2};
per cases by A7,TARSKI:def 2;
suppose
A8: a = 1;
then
ex R being 1-sorted st R = G.1 & (Carrier G).1 = the carrier of R
by A7,PRALG_1:def 15;
hence thesis by A8;
end;
suppose
A9: a = 2;
then
ex R being 1-sorted st R = G.2 & (Carrier G).2 = the carrier of R
by A7,PRALG_1:def 15;
hence thesis by A9;
end;
end;
dom xy = {1,2} by FINSEQ_1:2,89;
then xy in product Carrier G by A1,A6,CARD_3:9;
hence thesis by Def2;
end;
end;
theorem Th22:
for G1, G2, G3 being non empty multMagma holds
<*G1,G2,G3*> is multMagma-Family of {1,2,3}
proof
let G1, G2, G3 be non empty multMagma;
dom <*G1,G2,G3*> = {1,2,3} by FINSEQ_1:89,FINSEQ_3:1;
then reconsider A = <*G1,G2,G3*> as ManySortedSet of {1,2,3} by
PARTFUN1:def 2,RELAT_1:def 18;
A is multMagma-yielding
proof
let y be set;
assume y in rng A;
then consider x being object such that
A1: x in dom A and
A2: A.x = y by FUNCT_1:def 3;
x = 1 or x = 2 or x = 3 by A1,ENUMSET1:def 1;
hence thesis by A2;
end;
hence thesis;
end;
registration
let G1, G2, G3 be non empty multMagma;
cluster <*G1,G2,G3*> -> {1,2,3} -defined;
coherence by Th22;
end;
registration
let G1, G2, G3 be non empty multMagma;
cluster <*G1,G2,G3*> -> total multMagma-yielding;
coherence by Th22;
end;
theorem Th23:
for G1, G2, G3 being Group-like non empty multMagma holds
<*G1,G2,G3*> is Group-like multMagma-Family of {1,2,3}
proof
let G1, G2, G3 be Group-like non empty multMagma;
reconsider A = <*G1,G2,G3*> as multMagma-Family of {1,2,3};
A is Group-like
proof
let x be Element of {1,2,3};
x = 1 or x = 2 or x = 3 by ENUMSET1:def 1;
hence thesis;
end;
hence thesis;
end;
registration
let G1, G2, G3 be Group-like non empty multMagma;
cluster <*G1,G2,G3*> -> Group-like;
coherence by Th23;
end;
theorem Th24:
for G1, G2, G3 being associative non empty multMagma holds
<*G1,G2,G3*> is associative multMagma-Family of {1,2,3}
proof
let G1, G2, G3 be associative non empty multMagma;
reconsider A = <*G1,G2,G3*> as multMagma-Family of {1,2,3};
A is associative
proof
let x be Element of {1,2,3};
x = 1 or x = 2 or x = 3 by ENUMSET1:def 1;
hence thesis;
end;
hence thesis;
end;
registration
let G1, G2, G3 be associative non empty multMagma;
cluster <*G1,G2,G3*> -> associative;
coherence by Th24;
end;
theorem Th25:
for G1, G2, G3 being commutative non empty multMagma holds
<*G1,G2,G3*> is commutative multMagma-Family of {1,2,3}
proof
let G1, G2, G3 be commutative non empty multMagma;
reconsider A = <*G1,G2,G3*> as multMagma-Family of {1,2,3};
A is commutative
proof
let x be Element of {1,2,3};
x = 1 or x = 2 or x = 3 by ENUMSET1:def 1;
hence thesis;
end;
hence thesis;
end;
registration
let G1, G2, G3 be commutative non empty multMagma;
cluster <*G1,G2,G3*> -> commutative;
coherence by Th25;
end;
theorem
for G1, G2, G3 being Group holds
<*G1,G2,G3*> is Group-like associative multMagma-Family of {1,2,3};
theorem
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*>;
coherence by FINSEQ_3:1,PARTFUN1:def 2;
end;
registration
let G1, G2, G3 be non empty multMagma;
cluster -> FinSequence-like for Element of product <*G1,G2,G3*>;
coherence
proof
let x be Element of product <*G1,G2,G3*>;
reconsider y = x as Element of product Carrier <*G1,G2,G3*> by Def2;
y is FinSequence-like;
hence thesis;
end;
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*>; :: redefines <* (FINSEQ_1, definition)
coherence
proof
set xy = <*x,y,z*>, G = <*G1,G2,G3*>;
A1: dom Carrier G = {1,2,3} by PARTFUN1:def 2;
A8: for a being object st a in {1,2,3} holds xy.a in (Carrier G).a
proof
let a be object;
assume
A9: a in {1,2,3};
per cases by A9,ENUMSET1:def 1;
suppose
A10: a = 1;
then
ex R being 1-sorted st R = G.1 & (Carrier G).1 = the carrier of R
by A9,PRALG_1:def 15;
hence thesis by A10;
end;
suppose
A11: a = 2;
then
ex R being 1-sorted st R = G.2 & (Carrier G).2 = the carrier of R
by A9,PRALG_1:def 15;
hence thesis by A11;
end;
suppose
A12: a = 3;
then
ex R being 1-sorted st R = G.3 & (Carrier G).3 = the carrier of R
by A9,PRALG_1:def 15;
hence thesis by A12;
end;
end;
dom xy = {1,2,3} by FINSEQ_1:89,FINSEQ_3:1;
then xy in product Carrier G by A1,A8,CARD_3:9;
hence thesis by Def2;
end;
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 Th28:
<*x1*> * <*x2*> = <*x1*x2*>
proof
set G = <*G1*>;
A1: G.1 = G1;
reconsider l = <*x1*>, p = <*x2*>, lpl = <*x1*> * <*x2*>, lpp = <*x1*x2*> as
Element of product Carrier G by Def2;
A2: l.1 = x1;
A3: p.1 = x2;
A5: 1 in {1} by TARSKI:def 1;
A6: for k being Nat st 1 <= k & k <= 1 holds lpl.k = lpp.k
proof
let k be Nat;
assume that
A7: 1 <= k and
A8: k <= 1;
k in Seg 1 by A7,A8;
then k = 1 by FINSEQ_1:2,TARSKI:def 1;
hence thesis by A5,A2,A3,A1,Th1;
end;
dom lpl = dom Carrier G by CARD_3:9
.= Seg 1 by FINSEQ_1:2,PARTFUN1:def 2;
then
A9: len lpl = 1 by FINSEQ_1:def 3;
len lpp = 1 by FINSEQ_1:39;
hence thesis by A9,A6;
end;
theorem
<*x1,y1*> * <*x2,y2*> = <*x1*x2,y1*y2*>
proof
set G = <*G1,G2*>;
A1: G.1 = G1;
A2: G.2 = G2;
reconsider l = <*x1,y1*>, p = <*x2,y2*>, lpl = <*x1,y1*> * <*x2,y2*>, lpp =
<*x1*x2,y1*y2*> as Element of product Carrier G by Def2;
A3: 2 in {1,2} by TARSKI:def 2;
A4: l.1 = x1;
A6: p.2 = y2;
A8: p.1 = x2;
A9: l.2 = y1;
A10: 1 in {1,2} by TARSKI:def 2;
A11: for k being Nat st 1 <= k & k <= 2 holds lpl.k = lpp.k
proof
let k be Nat;
assume that
A12: 1 <= k and
A13: k <= 2;
A14: k in Seg 2 by A12,A13;
per cases by A14,FINSEQ_1:2,TARSKI:def 2;
suppose
k = 1;
hence thesis by A10,A4,A8,A1,Th1;
end;
suppose
k = 2;
hence thesis by A3,A9,A6,A2,Th1;
end;
end;
dom lpl = dom Carrier G by CARD_3:9
.= Seg 2 by FINSEQ_1:2,PARTFUN1:def 2;
then
A15: len lpl = 2 by FINSEQ_1:def 3;
len lpp = 2 by FINSEQ_1:44;
hence thesis by A15,A11;
end;
theorem
<*x1,y1,z1*> * <*x2,y2,z2*> = <*x1*x2,y1*y2,z1*z2*>
proof
set G = <*G1,G2,G3*>;
A1: 3 in {1,2,3} by ENUMSET1:def 1;
A2: G.1 = G1;
A3: G.3 = G3;
A4: G.2 = G2;
reconsider l = <*x1,y1,z1*>, p = <*x2,y2,z2*>, lpl = <*x1,y1,z1*> * <*x2,y2,
z2*>, lpp = <*x1*x2,y1*y2,z1*z2*> as Element of product Carrier G by Def2;
A5: 2 in {1,2,3} by ENUMSET1:def 1;
A6: l.1 = x1;
A7: l.3 = z1;
A8: l.2 = y1;
A12: p.3 = z2;
A13: p.2 = y2;
A14: p.1 = x2;
A15: 1 in {1,2,3} by ENUMSET1:def 1;
A16: for k being Nat st 1 <= k & k <= 3 holds lpl.k = lpp.k
proof
let k be Nat;
assume that
A17: 1 <= k and
A18: k <= 3;
A19: k in Seg 3 by A17,A18;
per cases by A19,ENUMSET1:def 1,FINSEQ_3:1;
suppose
k = 1;
hence thesis by A15,A6,A14,A2,Th1;
end;
suppose
k = 2;
hence thesis by A5,A8,A13,A4,Th1;
end;
suppose
k = 3;
hence thesis by A1,A7,A12,A3,Th1;
end;
end;
dom lpl = dom Carrier G by CARD_3:9
.= Seg 3 by FINSEQ_3:1,PARTFUN1:def 2;
then
A20: len lpl = 3 by FINSEQ_1:def 3;
len lpp = 3 by FINSEQ_1:45;
hence thesis by A20,A16;
end;
reserve G1, G2, G3 for Group-like non empty multMagma;
theorem
1_product <*G1*> = <*1_G1*>
proof
set s = <*1_G1*>, f = <*G1*>;
dom s = {1} by FINSEQ_1:2,def 8;
then reconsider s as ManySortedSet of {1} by PARTFUN1:def 2,RELAT_1:def 18;
for i being set st i in {1} ex G being Group-like non empty multMagma
st G = f.i & s.i = 1_G
proof
let i be set;
assume i in {1};
then
A1: i = 1 by TARSKI:def 1;
then reconsider G = f.i as Group-like non empty multMagma;
take G;
thus thesis by A1;
end;
hence thesis by Th5;
end;
theorem
1_product <*G1,G2*> = <*1_G1,1_G2*>
proof
set s = <*1_G1,1_G2*>, f = <*G1,G2*>;
dom s = {1,2} by FINSEQ_1:2,89;
then reconsider s as ManySortedSet of {1,2} by PARTFUN1:def 2,RELAT_1:def 18;
for i being set st i in {1,2} ex G being Group-like non empty multMagma
st G = f.i & s.i = 1_G
proof
let i be set such that
A1: i in {1,2};
per cases by A1,TARSKI:def 2;
suppose
A2: i = 1;
then reconsider G = f.i as Group-like non empty multMagma;
take G;
thus thesis by A2;
end;
suppose
A3: i = 2;
then reconsider G = f.i as Group-like non empty multMagma;
take G;
thus thesis by A3;
end;
end;
hence thesis by Th5;
end;
theorem
1_product <*G1,G2,G3*> = <*1_G1,1_G2,1_G3*>
proof
set s = <*1_G1,1_G2,1_G3*>, f = <*G1,G2,G3*>;
dom s = {1,2,3} by FINSEQ_1:89,FINSEQ_3:1;
then reconsider s as ManySortedSet of {1,2,3} by PARTFUN1:def 2
,RELAT_1:def 18;
for i being set st i in {1,2,3} ex G being Group-like non empty
multMagma st G = f.i & s.i = 1_G
proof
let i be set such that
A1: i in {1,2,3};
per cases by A1,ENUMSET1:def 1;
suppose
A2: i = 1;
then reconsider G = f.i as Group-like non empty multMagma;
take G;
thus thesis by A2;
end;
suppose
A3: i = 2;
then reconsider G = f.i as Group-like non empty multMagma;
take G;
thus thesis by A3;
end;
suppose
A4: i = 3;
then reconsider G = f.i as Group-like non empty multMagma;
take G;
thus thesis by A4;
end;
end;
hence thesis by Th5;
end;
reserve G1, G2, G3 for Group,
x for Element of G1,
y for Element of G2,
z for Element of G3;
theorem
(<*x*> qua Element of product <*G1*>)" = <*x"*>
proof
reconsider G = <*G1*> as associative Group-like multMagma-Family of {1};
reconsider lF = <*x*>, p = <*x"*> as Element of product Carrier G by Def2;
for i being set st i in {1} ex H being Group, z being Element of H st H
= G.i & p.i = z" & z = lF.i
proof
reconsider H = G.1 as Group;
reconsider z = p.1 as Element of H;
let i be set;
assume
A3: i in {1};
take H, z";
thus H = G.i by A3,TARSKI:def 1;
thus p.i = z"" by A3,TARSKI:def 1;
i = 1 by A3,TARSKI:def 1;
hence thesis;
end;
hence thesis by Th7;
end;
theorem
(<*x,y*> qua Element of product <*G1,G2*>)" = <*x",y"*>
proof
set G = <*G1,G2*>;
reconsider lF = <*x,y*>, p = <*x",y"*> as Element of product Carrier G by
Def2;
for i being set st i in {1,2} ex H being Group, z being Element of H st
H = G.i & p.i = z" & z = lF.i
proof
let i be set such that
A5: i in {1,2};
per cases by A5,TARSKI:def 2;
suppose
A6: i = 1;
reconsider H = G.1 as Group;
reconsider z = p.1 as Element of H;
take H, z";
thus H = G.i by A6;
thus p.i = z"" by A6;
thus thesis by A6;
end;
suppose
A7: i = 2;
reconsider H = G.2 as Group;
reconsider z = p.2 as Element of H;
take H, z";
thus H = G.i by A7;
thus p.i = z"" by A7;
thus thesis by A7;
end;
end;
hence thesis by Th7;
end;
theorem
(<*x,y,z*> qua Element of product <*G1,G2,G3*>)" = <*x",y",z" *>
proof
set G = <*G1,G2,G3*>;
reconsider lF = <*x,y,z*>, p = <*x",y",z"*> as Element of product Carrier G
by Def2;
for i being set st i in {1,2,3} ex H being Group, z being Element of H
st H = G.i & p.i = z" & z = lF.i
proof
let i be set such that
A7: i in {1,2,3};
per cases by A7,ENUMSET1:def 1;
suppose
A8: i = 1;
reconsider H = G.1 as Group;
reconsider z = p.1 as Element of H;
take H, z";
thus H = G.i by A8;
thus p.i = z"" by A8;
thus thesis by A8;
end;
suppose
A9: i = 2;
reconsider H = G.2 as Group;
reconsider z = p.2 as Element of H;
take H, z";
thus H = G.i by A9;
thus p.i = z"" by A9;
thus thesis by A9;
end;
suppose
A10: i = 3;
reconsider H = G.3 as Group;
reconsider z = p.3 as Element of H;
take H, z";
thus H = G.i by A10;
thus p.i = z"" by A10;
thus thesis by A10;
end;
end;
hence thesis by Th7;
end;
theorem Th37:
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*>
proof
let f be Function of the carrier of G1, the carrier of product <*G1*> such
that
A1: for x being Element of G1 holds f.x = <*x*>;
now
let a, b be Element of G1;
thus f.(a * b) = <*a * b*> by A1
.= <*a*> * <*b*> by Th28
.= <*a*> * f.b by A1
.= f.a * f.b by A1;
end;
hence thesis by GROUP_6:def 6;
end;
theorem Th38:
for f being Homomorphism of G1, product <*G1*> st
for x being Element of G1 holds f.x = <*x*> holds f is bijective
proof
let f be Homomorphism of G1, product <*G1*> such that
A1: for x being Element of G1 holds f.x = <*x*>;
A2: dom f = the carrier of G1 by FUNCT_2:def 1;
A3: rng f = the carrier of product <*G1*>
proof
thus rng f c= the carrier of product <*G1*>;
let x be object;
assume x in the carrier of product <*G1*>;
then reconsider a = x as Element of product <*G1*>;
A4: 1 in {1} by TARSKI:def 1;
then
A5: ex R being 1-sorted st R = <*G1*>.1 & (Carrier <*G1*>).1 = the
carrier of R by PRALG_1:def 15;
a in the carrier of product <*G1*>;
then
A6: a in product Carrier <*G1*> by Def2;
then
A7: dom a = dom Carrier <*G1*> by CARD_3:9;
then
A8: dom a = {1} by PARTFUN1:def 2;
then a.1 in (Carrier <*G1*>).1 by A6,A7,A4,CARD_3:9;
then reconsider b = a.1 as Element of G1 by A5;
f.b = <*b*> by A1
.= x by A8,FINSEQ_1:2,def 8;
hence thesis by A2,FUNCT_1:def 3;
end;
f is one-to-one
proof
let m, n be object;
assume that
A9: m in dom f and
A10: n in dom f and
A11: f.m = f.n;
reconsider m1 = m, n1 = n as Element of G1 by A9,A10;
<*m1*> = f.m1 by A1
.= <*n1*> by A1,A11;
hence thesis by FINSEQ_1:76;
end;
hence thesis by A3,GROUP_6:60;
end;
theorem
G1, product <*G1*> are_isomorphic
proof
deffunc F(Element of G1) = <*$1*>;
consider f being Function of the carrier of G1,
the carrier of product <*G1*> such that
A1: for x being Element of G1 holds f.x = F(x) from FUNCT_2:sch 4;
reconsider f as Homomorphism of G1, product <*G1*> by A1,Th37;
take f;
thus thesis by A1,Th38;
end;
:: added, SK 15.11.2024
registration
cluster {} -> multMagma-yielding;
coherence;
let X be set, M be non empty multMagma;
cluster X --> M -> multMagma-yielding;
coherence
proof
for y being set st y in rng(X-->M) holds y is non empty multMagma
by TARSKI:def 1;
hence thesis;
end;
end;
registration
let f,g be multMagma-yielding Function;
cluster f +* g -> multMagma-yielding;
coherence
proof
for y being set st y in rng(f+*g) holds y is non empty multMagma
proof
let y be set;
assume y in rng(f+*g);
then y in rng f \/ rng g by TARSKI:def 3, FUNCT_4:17;
then per cases by XBOOLE_0:def 3;
suppose y in rng f;
hence thesis by Def1;
end;
suppose y in rng g;
hence thesis by Def1;
end;
end;
hence thesis;
end;
end;
registration
cluster non empty FinSequence-like multMagma-yielding for Function;
existence
proof
take <* the non empty multMagma *>;
thus thesis;
end;
end;
registration
let p,q be multMagma-yielding FinSequence;
cluster p^q -> multMagma-yielding;
coherence
proof
for x being set st x in rng(p^q) holds x is non empty multMagma
proof
let x be set;
assume x in rng(p^q);
then x in rng p \/ rng q by FINSEQ_1:31;
then per cases by XBOOLE_0:def 3;
suppose x in rng p;
hence thesis by Def1;
end;
suppose x in rng q;
hence thesis by Def1;
end;
end;
hence thesis;
end;
end;
registration
let I be non empty set;
cluster -> non empty for multMagma-Family of I;
coherence;
end;
registration
let X be set, M be non empty Group-like multMagma;
cluster X --> M -> Group-like for multMagma-Family of X;
coherence
proof
let F be multMagma-Family of X;
assume A1: F = X --> M;
now
let i be set;
assume A2: i in X;
take M;
thus M = F.i by A1, A2, FUNCOP_1:7;
end;
hence thesis;
end;
end;
registration
let X be set, M be non empty associative multMagma;
cluster X --> M -> associative for multMagma-Family of X;
coherence
proof
let F be multMagma-Family of X;
assume A1: F = X --> M;
now
let i be set;
assume A2: i in X;
take M;
thus M = F.i by A1, A2, FUNCOP_1:7;
end;
hence thesis;
end;
end;
registration
let X be set, M be non empty commutative multMagma;
cluster X --> M -> commutative for multMagma-Family of X;
coherence
proof
let F be multMagma-Family of X;
assume A1: F = X --> M;
now
let i be set;
assume A2: i in X;
take M;
thus M = F.i by A1, A2, FUNCOP_1:7;
end;
hence thesis;
end;
end;
registration
let M1 be non empty multMagma;
cluster <% M1 %> -> multMagma-yielding;
coherence
proof
for x being set st x in rng <% M1 %> holds x is non empty multMagma
proof
let x be set;
assume x in rng <% M1 %>;
then x in { M1 } by AFINSQ_1:33;
hence thesis by TARSKI:def 1;
end;
hence thesis;
end;
let M2 be non empty multMagma;
cluster <% M1, M2 %> -> multMagma-yielding;
coherence
proof
for x being set st x in rng <% M1, M2 %> holds x is non empty multMagma
proof
let x be set;
assume x in rng <% M1, M2 %>;
then x in { M1, M2 } by AFINSQ_1:98;
hence thesis by TARSKI:def 2;
end;
hence thesis;
end;
let M3 be non empty multMagma;
cluster <% M1, M2, M3 %> -> multMagma-yielding;
coherence
proof
for x being set st x in rng <% M1, M2, M3 %> holds x is non empty multMagma
proof
let x be set;
assume x in rng <% M1, M2, M3 %>;
then x in { M1, M2, M3 } by AFINSQ_1:99;
hence thesis by ENUMSET1:def 1;
end;
hence thesis;
end;
end;