:: The Product of the Families of the Groups
:: by Artur Korni{\l}owicz
::
:: Received June 10, 1998
:: Copyright (c) 1998-2012 Association of Mizar Users


begin

definition
let R be Relation;
attrR is multMagma-yielding  means :Def1: :: GROUP_7:def 1
 for y being set st y in rng R holds
y is non empty multMagma ;
end;

:: deftheorem Def1 defines multMagma-yielding GROUP_7:def_1_:_
 for R being Relation holds
( R is multMagma-yielding iff for y being set st y in rng R holds
y is non empty multMagma );

registration
cluster Relation-like Function-like multMagma-yielding  ->  1-sorted-yielding for set ;
coherence
 for b1 being Function st b1 is multMagma-yielding holds
b1 is 1-sorted-yielding
proofend;
end;

registration
let I be set ;
cluster Relation-like I -defined Function-like total multMagma-yielding for set ;
existence
 ex b1 being ManySortedSet of I st b1 is multMagma-yielding
proofend;
end;

registration
cluster Relation-like Function-like multMagma-yielding for set ;
existence
 ex b1 being Function st b1 is multMagma-yielding
proofend;
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 ;
let F be multMagma-Family of I;
let i be Element of I;
:: original:.
redefine funcF . i ->  non empty multMagma ;
coherence
 F . i is non empty multMagma
proofend;
end;

registration
let I be set ;
let F be multMagma-Family of I;
cluster Carrier F -> V2() ;
coherence
 Carrier F is non-empty
proofend;
end;

Lm1: now__::_thesis:_for_I_being_non_empty_set_
for_i_being_Element_of_I
for_F_being_multMagma-yielding_ManySortedSet_of_I
for_f_being_Element_of_product_(Carrier_F)_holds_f_._i_in_the_carrier_of_(F_._i)
let I be non empty set ; ::_thesis: for i being Element of I
for F being multMagma-yielding ManySortedSet of I
for f being Element of product (Carrier F) holds f . i in the carrier of (F . i)
let i be Element of I; ::_thesis: for F being multMagma-yielding ManySortedSet of I
for f being Element of product (Carrier F) holds f . i in the carrier of (F . i)
let F be multMagma-yielding ManySortedSet of I; ::_thesis: for f being Element of product (Carrier F) holds f . i in the carrier of (F . i)
let f be Element of product (Carrier F); ::_thesis: f . i in the carrier of (F . i)
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_13;
hence  f . i in the carrier of (F . i) by A1, CARD_3:9; ::_thesis: verum
end;

definition
let I be set ;
let F be multMagma-Family of I;
func product F ->  strict multMagma  means :Def2: :: GROUP_7:def 2
( the carrier of it = product (Carrier F) & ( for f, g being Element of product (Carrier F)
for i being set st i in I holds
ex Fi being non empty multMagma ex 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
 ex b1 being strict multMagma st
( the carrier of b1 = product (Carrier F) & ( for f, g being Element of product (Carrier F)
for i being set st i in I holds
ex Fi being non empty multMagma ex h being Function st
( Fi = F . i & h = the multF of b1 . (f,g) & h . i = the multF of Fi . ((f . i),(g . i)) ) ) )
proofend;
uniqueness
 for b1, b2 being strict multMagma st the carrier of b1 = product (Carrier F) & ( for f, g being Element of product (Carrier F)
for i being set st i in I holds
ex Fi being non empty multMagma ex h being Function st
( Fi = F . i & h = the multF of b1 . (f,g) & h . i = the multF of Fi . ((f . i),(g . i)) ) ) & the carrier of b2 = product (Carrier F) & ( for f, g being Element of product (Carrier F)
for i being set st i in I holds
ex Fi being non empty multMagma ex h being Function st
( Fi = F . i & h = the multF of b2 . (f,g) & h . i = the multF of Fi . ((f . i),(g . i)) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def2 defines product GROUP_7:def_2_:_
 for I being set
for F being multMagma-Family of I
for b3 being strict multMagma holds
( b3 = product F iff ( the carrier of b3 = product (Carrier F) & ( for f, g being Element of product (Carrier F)
for i being set st i in I holds
ex Fi being non empty multMagma ex h being Function st
( Fi = F . i & h = the multF of b3 . (f,g) & h . i = the multF of Fi . ((f . i),(g . i)) ) ) ) );

registration
let I be set ;
let F be multMagma-Family of I;
cluster product F ->  non empty strict constituted-Functions ;
coherence
 ( not product F is empty & product F is constituted-Functions )
proofend;
end;

theorem Th4: :: GROUP_7:1
for I, i being set
for f, g, h being Function
for F being multMagma-Family of I
for G being non empty multMagma
for p, q being Element of (product F)
for 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
proofend;

definition
let I be set ;
let F be multMagma-Family of I;
attrF is Group-like  means :Def3: :: GROUP_7:def 3
 for i being set st i in I holds
ex Fi being non empty Group-like multMagma st Fi = F . i;
attrF is associative  means :Def4: :: GROUP_7:def 4
 for i being set st i in I holds
ex Fi being non empty associative multMagma st Fi = F . i;
attrF is commutative  means :Def5: :: GROUP_7:def 5
 for i being set st i in I holds
ex Fi being non empty commutative multMagma st Fi = F . i;
end;

:: deftheorem Def3 defines Group-like GROUP_7:def_3_:_
 for I being set
for F being multMagma-Family of I holds
( F is Group-like iff for i being set st i in I holds
ex Fi being non empty Group-like multMagma st Fi = F . i );

:: deftheorem Def4 defines associative GROUP_7:def_4_:_
 for I being set
for F being multMagma-Family of I holds
( F is associative iff for i being set st i in I holds
ex Fi being non empty associative multMagma st Fi = F . i );

:: deftheorem Def5 defines commutative GROUP_7:def_5_:_
 for I being set
for F being multMagma-Family of I holds
( F is commutative iff for i being set st i in I holds
ex Fi being non empty commutative multMagma st Fi = F . i );

definition
let I be non empty set ;
let F be multMagma-Family of I;
redefine attr F is Group-like  means :Def6: :: GROUP_7:def 6
 for i being Element of I holds F . i is Group-like ;
compatibility
 ( F is Group-like iff for i being Element of I holds F . i is Group-like )
proofend;
redefine attr F is associative  means :Def7: :: GROUP_7:def 7
 for i being Element of I holds F . i is associative ;
compatibility
 ( F is associative iff for i being Element of I holds F . i is associative )
proofend;
redefine attr F is commutative  means :: GROUP_7:def 8
 for i being Element of I holds F . i is commutative ;
compatibility
 ( F is commutative iff for i being Element of I holds F . i is commutative )
proofend;
end;

:: deftheorem Def6 defines Group-like GROUP_7:def_6_:_
 for I being non empty set
for F being multMagma-Family of I holds
( F is Group-like iff for i being Element of I holds F . i is Group-like );

:: deftheorem Def7 defines associative GROUP_7:def_7_:_
 for I being non empty set
for F being multMagma-Family of I holds
( F is associative iff for i being Element of I holds F . i is associative );

:: deftheorem  defines commutative GROUP_7:def_8_:_
 for I being non empty set
for F being multMagma-Family of I holds
( F is commutative iff for i being Element of I holds F . i is commutative );

registration
let I be set ;
cluster Relation-like I -defined Function-like total 1-sorted-yielding multMagma-yielding Group-like associative commutative for set ;
existence
 ex b1 being multMagma-Family of I st
( b1 is Group-like & b1 is associative & b1 is commutative )
proofend;
end;

registration
let I be set ;
let F be Group-like multMagma-Family of I;
cluster product F ->  strict Group-like ;
coherence
 product F is Group-like
proofend;
end;

registration
let I be set ;
let F be associative multMagma-Family of I;
cluster product F ->  strict associative ;
coherence
 product F is associative
proofend;
end;

registration
let I be set ;
let F be commutative multMagma-Family of I;
cluster product F ->  strict commutative ;
coherence
 product F is commutative
proofend;
end;

theorem :: GROUP_7:2
for I, i being set
for F being multMagma-Family of I
for G being non empty multMagma st i in I & G = F . i & product F is Group-like holds
G is Group-like
proofend;

theorem :: GROUP_7:3
for I, i being set
for F being multMagma-Family of I
for G being non empty multMagma st i in I & G = F . i & product F is associative holds
G is associative
proofend;

theorem :: GROUP_7:4
for I, i being set
for F being multMagma-Family of I
for G being non empty multMagma st i in I & G = F . i & product F is commutative holds
G is commutative
proofend;

theorem Th8: :: GROUP_7:5
for I being set
for s being ManySortedSet of I
for F being Group-like multMagma-Family of I st ( for i being set st i in I holds
ex G being non empty Group-like multMagma st
( G = F . i & s . i = 1_ G ) ) holds
s = 1_ (product F)
proofend;

theorem Th9: :: GROUP_7:6
for I, i being set
for f being Function
for F being Group-like multMagma-Family of I
for G being non empty Group-like multMagma st i in I & G = F . i & f = 1_ (product F) holds
f . i = 1_ G
proofend;

theorem Th10: :: GROUP_7:7
for I being set
for g being Function
for s being ManySortedSet of I
for F being Group-like associative multMagma-Family of I
for x being Element of (product F) st x = g & ( for i being set st i in I holds
ex G being Group ex y being Element of G st
( G = F . i & s . i = y " & y = g . i ) ) holds
s = x "
proofend;

theorem Th11: :: GROUP_7:8
for I, i being set
for f, g being Function
for F being Group-like associative multMagma-Family of I
for x being Element of (product F)
for G being Group
for y being Element of G st i in I & G = F . i & f = x & g = x " & f . i = y holds
g . i = y "
proofend;

definition
let I be set ;
let F be Group-like associative multMagma-Family of I;
func sum F ->  strict Subgroup of product F means :Def9: :: GROUP_7:def 9
 for x being set holds
( x in the carrier of it iff ex g being Element of product (Carrier F) ex J being finite Subset of I ex f being ManySortedSet of J st
( g = 1_ (product F) & x = g +* f & ( for j being set st j in J holds
ex G being non empty Group-like multMagma st
( G = F . j &amp; f . j in the carrier of G &amp; f . j <> 1_ G ) ) ) );
existence
 ex b1 being strict Subgroup of product F st
for x being set holds
( x in the carrier of b1 iff ex g being Element of product (Carrier F) ex J being finite Subset of I ex f being ManySortedSet of J st
( g = 1_ (product F) &amp; x = g +* f &amp; ( for j being set st j in J holds
ex G being non empty Group-like multMagma st
( G = F . j &amp; f . j in the carrier of G &amp; f . j <> 1_ G ) ) ) )
proofend;
uniqueness
 for b1, b2 being strict Subgroup of product F st ( for x being set holds
( x in the carrier of b1 iff ex g being Element of product (Carrier F) ex J being finite Subset of I ex f being ManySortedSet of J st
( g = 1_ (product F) &amp; x = g +* f &amp; ( for j being set st j in J holds
ex G being non empty Group-like multMagma st
( G = F . j &amp; f . j in the carrier of G &amp; f . j <> 1_ G ) ) ) ) ) &amp; ( for x being set holds
( x in the carrier of b2 iff ex g being Element of product (Carrier F) ex J being finite Subset of I ex f being ManySortedSet of J st
( g = 1_ (product F) &amp; x = g +* f &amp; ( for j being set st j in J holds
ex G being non empty Group-like multMagma st
( G = F . j &amp; f . j in the carrier of G &amp; f . j <> 1_ G ) ) ) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def9 defines sum GROUP_7:def_9_:_
 for I being set
for F being Group-like associative multMagma-Family of I
for b3 being strict Subgroup of product F holds
( b3 = sum F iff for x being set holds
( x in the carrier of b3 iff ex g being Element of product (Carrier F) ex J being finite Subset of I ex f being ManySortedSet of J st
( g = 1_ (product F) &amp; x = g +* f &amp; ( for j being set st j in J holds
ex G being non empty Group-like multMagma st
( G = F . j &amp; f . j in the carrier of G &amp; f . j <> 1_ G ) ) ) ) );

registration
let I be set ;
let F be Group-like associative multMagma-Family of I;
let f, g be Element of (sum F);
cluster the multF of (sum F) . (f,g) ->  Relation-like Function-like ;
coherence
 ( the multF of (sum F) . (f,g) is Function-like &amp; the multF of (sum F) . (f,g) is Relation-like )
proofend;
end;

theorem :: GROUP_7:9
for I being finite set
for F being Group-like associative multMagma-Family of I holds product F = sum F
proofend;

begin

theorem Th13: :: GROUP_7:10
for G1 being non empty multMagma holds <*G1*> is multMagma-Family of {1}
proofend;

registration
let G1 be non empty multMagma ;
cluster<*G1*> -> {1} -defined ;
coherence
 <*G1*> is {1} -defined by Th13;
end;

registration
let G1 be non empty multMagma ;
cluster<*G1*> ->  total multMagma-yielding ;
coherence
 ( <*G1*> is total &amp; <*G1*> is multMagma-yielding ) by Th13;
end;

theorem Th14: :: GROUP_7:11
for G1 being non empty Group-like multMagma holds <*G1*> is Group-like multMagma-Family of {1}
proofend;

registration
let G1 be non empty Group-like multMagma ;
cluster<*G1*> ->  Group-like ;
coherence
 <*G1*> is Group-like by Th14;
end;

theorem Th15: :: GROUP_7:12
for G1 being non empty associative multMagma holds <*G1*> is associative multMagma-Family of {1}
proofend;

registration
let G1 be non empty associative multMagma ;
cluster<*G1*> ->  associative ;
coherence
 <*G1*> is associative by Th15;
end;

theorem Th16: :: GROUP_7:13
for G1 being non empty commutative multMagma holds <*G1*> is commutative multMagma-Family of {1}
proofend;

registration
let G1 be non empty commutative multMagma ;
cluster<*G1*> ->  commutative ;
coherence
 <*G1*> is commutative by Th16;
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 Group-like associative commutative multMagma-Family of {1} ;

registration
let G1 be non empty multMagma ;
cluster  ->  FinSequence-like for Element of product (Carrier <*G1*>);
coherence
 for b1 being Element of product (Carrier <*G1*>) holds b1 is FinSequence-like
proofend;
end;

registration
let G1 be non empty multMagma ;
cluster  ->  FinSequence-like for Element of the carrier of (product <*G1*>);
coherence
 for b1 being Element of (product <*G1*>) holds b1 is FinSequence-like
proofend;
end;

definition
let G1 be non empty multMagma ;
let x be Element of G1;
:: original:<*
redefine func<*x*> ->  Element of (product <*G1*>);
coherence
 <*x*> is Element of (product <*G1*>)
proofend;
end;

theorem Th19: :: GROUP_7:16
for G1, G2 being non empty multMagma holds <*G1,G2*> is multMagma-Family of {1,2}
proofend;

registration
let G1, G2 be non empty multMagma ;
cluster<*G1,G2*> -> {1,2} -defined ;
coherence
 <*G1,G2*> is {1,2} -defined by Th19;
end;

registration
let G1, G2 be non empty multMagma ;
cluster<*G1,G2*> ->  total multMagma-yielding ;
coherence
 ( <*G1,G2*> is total &amp; <*G1,G2*> is multMagma-yielding ) by Th19;
end;

theorem Th20: :: GROUP_7:17
for G1, G2 being non empty Group-like multMagma holds <*G1,G2*> is Group-like multMagma-Family of {1,2}
proofend;

registration
let G1, G2 be non empty Group-like multMagma ;
cluster<*G1,G2*> ->  Group-like ;
coherence
 <*G1,G2*> is Group-like by Th20;
end;

theorem Th21: :: GROUP_7:18
for G1, G2 being non empty associative multMagma holds <*G1,G2*> is associative multMagma-Family of {1,2}
proofend;

registration
let G1, G2 be non empty associative multMagma ;
cluster<*G1,G2*> ->  associative ;
coherence
 <*G1,G2*> is associative by Th21;
end;

theorem Th22: :: GROUP_7:19
for G1, G2 being non empty commutative multMagma holds <*G1,G2*> is commutative multMagma-Family of {1,2}
proofend;

registration
let G1, G2 be non empty commutative multMagma ;
cluster<*G1,G2*> ->  commutative ;
coherence
 <*G1,G2*> is commutative by Th22;
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*>);
coherence
 for b1 being Element of product (Carrier <*G1,G2*>) holds b1 is FinSequence-like
proofend;
end;

registration
let G1, G2 be non empty multMagma ;
cluster  ->  FinSequence-like for Element of the carrier of (product <*G1,G2*>);
coherence
 for b1 being Element of (product <*G1,G2*>) holds b1 is FinSequence-like
proofend;
end;

definition
let G1, G2 be non empty multMagma ;
let x be Element of G1;
let y be Element of G2;
:: original:<*
redefine func<*x,y*> ->  Element of (product <*G1,G2*>);
coherence
 <*x,y*> is Element of (product <*G1,G2*>)
proofend;
end;

theorem Th25: :: GROUP_7:22
for G1, G2, G3 being non empty multMagma holds <*G1,G2,G3*> is multMagma-Family of {1,2,3}
proofend;

registration
let G1, G2, G3 be non empty multMagma ;
cluster<*G1,G2,G3*> -> {1,2,3} -defined ;
coherence
 <*G1,G2,G3*> is {1,2,3} -defined by Th25;
end;

registration
let G1, G2, G3 be non empty multMagma ;
cluster<*G1,G2,G3*> ->  total multMagma-yielding ;
coherence
 ( <*G1,G2,G3*> is total &amp; <*G1,G2,G3*> is multMagma-yielding ) by Th25;
end;

theorem Th26: :: GROUP_7:23
for G1, G2, G3 being non empty Group-like multMagma holds <*G1,G2,G3*> is Group-like multMagma-Family of {1,2,3}
proofend;

registration
let G1, G2, G3 be non empty Group-like multMagma ;
cluster<*G1,G2,G3*> ->  Group-like ;
coherence
 <*G1,G2,G3*> is Group-like by Th26;
end;

theorem Th27: :: GROUP_7:24
for G1, G2, G3 being non empty associative multMagma holds <*G1,G2,G3*> is associative multMagma-Family of {1,2,3}
proofend;

registration
let G1, G2, G3 be non empty associative multMagma ;
cluster<*G1,G2,G3*> ->  associative ;
coherence
 <*G1,G2,G3*> is associative by Th27;
end;

theorem Th28: :: GROUP_7:25
for G1, G2, G3 being non empty commutative multMagma holds <*G1,G2,G3*> is commutative multMagma-Family of {1,2,3}
proofend;

registration
let G1, G2, G3 be non empty commutative multMagma ;
cluster<*G1,G2,G3*> ->  commutative ;
coherence
 <*G1,G2,G3*> is commutative by Th28;
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*>);
coherence
 for b1 being Element of product (Carrier <*G1,G2,G3*>) holds b1 is FinSequence-like
proofend;
end;

registration
let G1, G2, G3 be non empty multMagma ;
cluster  ->  FinSequence-like for Element of the carrier of (product <*G1,G2,G3*>);
coherence
 for b1 being Element of (product <*G1,G2,G3*>) holds b1 is FinSequence-like
proofend;
end;

definition
let G1, G2, G3 be non empty multMagma ;
let x be Element of G1;
let y be Element of G2;
let z be Element of G3;
:: original:<*
redefine func<*x,y,z*> ->  Element of (product <*G1,G2,G3*>);
coherence
 <*x,y,z*> is Element of (product <*G1,G2,G3*>)
proofend;
end;

theorem Th31: :: GROUP_7:28
for G1 being non empty multMagma
for x1, x2 being Element of G1 holds <*x1*> * <*x2*> = <*(x1 * x2)*>
proofend;

theorem :: GROUP_7:29
for G1, G2 being non empty multMagma
for x1, x2 being Element of G1
for y1, y2 being Element of G2 holds <*x1,y1*> * <*x2,y2*> = <*(x1 * x2),(y1 * y2)*>
proofend;

theorem :: GROUP_7:30
for G1, G2, G3 being non empty multMagma
for x1, x2 being Element of G1
for y1, y2 being Element of G2
for z1, z2 being Element of G3 holds <*x1,y1,z1*> * <*x2,y2,z2*> = <*(x1 * x2),(y1 * y2),(z1 * z2)*>
proofend;

theorem :: GROUP_7:31
for G1 being non empty Group-like multMagma holds 1_ (product <*G1*>) = <*(1_ G1)*>
proofend;

theorem :: GROUP_7:32
for G1, G2 being non empty Group-like multMagma holds 1_ (product <*G1,G2*>) = <*(1_ G1),(1_ G2)*>
proofend;

theorem :: GROUP_7:33
for G1, G2, G3 being non empty Group-like multMagma holds 1_ (product <*G1,G2,G3*>) = <*(1_ G1),(1_ G2),(1_ G3)*>
proofend;

theorem :: GROUP_7:34
for G1 being Group
for x being Element of G1 holds <*x*> " = <*(x ")*>
proofend;

theorem :: GROUP_7:35
for G1, G2 being Group
for x being Element of G1
for y being Element of G2 holds <*x,y*> " = <*(x "),(y ")*>
proofend;

theorem :: GROUP_7:36
for G1, G2, G3 being Group
for x being Element of G1
for y being Element of G2
for z being Element of G3 holds <*x,y,z*> " = <*(x "),(y "),(z ")*>
proofend;

theorem Th40: :: GROUP_7:37
for G1 being Group
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*>)
proofend;

theorem Th41: :: GROUP_7:38
for G1 being Group
for f being Homomorphism of G1,(product <*G1*>) st ( for x being Element of G1 holds f . x = <*x*> ) holds
f is bijective
proofend;

theorem :: GROUP_7:39
for G1 being Group holds G1, product <*G1*> are_isomorphic
proofend;