:: The Product of the Families of the Groups :: by Artur Korni{\l}owicz :: :: Received June 10, 1998 :: Copyright (c) 1998-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies FUNCT_1, PBOOLE, RELAT_1, XBOOLE_0, ALGSTR_0, PRALG_1, FUNCOP_1, SUBSET_1, RLVECT_2, STRUCT_0, CARD_3, TARSKI, BINOP_1, ZFMISC_1, MONOID_0, GROUP_1, SEMI_AF1, GROUP_2, FINSET_1, FUNCT_4, REALSET1, FINSEQ_1, NAT_1, XXREAL_0, GROUP_6, FUNCT_2, WELLORD1, GROUP_7, PARTFUN1; notations TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, NAT_1, FINSEQ_1, RELSET_1, PARTFUN1, FUNCT_2, FUNCT_4, FINSET_1, BINOP_1, REALSET1, XXREAL_0, PBOOLE, FUNCOP_1, STRUCT_0, ALGSTR_0, MONOID_0, GROUP_1, GROUP_2, GROUP_6, CARD_3, PRALG_1; constructors BINOP_1, XXREAL_0, REALSET1, GROUP_6, MONOID_0, PRALG_1, PRALG_2, RELSET_1, FUNCT_4; registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, FINSET_1, XREAL_0, FINSEQ_1, REALSET1, STRUCT_0, GROUP_1, GROUP_2, MONOID_0, ORDINAL1, CARD_3, FUNCOP_1, RELSET_1, FUNCT_4; requirements NUMERALS, BOOLE, SUBSET; begin :: The product of the families of the groups reserve i, I for set, f, g, h for Function, s for ManySortedSet of I; definition let R be Relation; attr R is multMagma-yielding means :: GROUP_7:def 1 for y being set st y in rng R holds y is non empty multMagma; end; registration cluster multMagma-yielding -> 1-sorted-yielding for Function; end; registration let I be set; cluster multMagma-yielding for ManySortedSet of I; end; registration cluster multMagma-yielding for Function; end; definition let I be set; mode multMagma-Family of I is multMagma-yielding ManySortedSet of I; end; definition let I be non empty set, F be multMagma-Family of I, i be Element of I; redefine func F.i -> non empty multMagma; end; registration let I be set, F be multMagma-Family of I; cluster Carrier F -> non-empty; end; definition let I be set, F be multMagma-Family of I; func product F -> strict multMagma means :: GROUP_7:def 2 the carrier of it = product Carrier F & for f, g being Element of product Carrier F, i being set st i in I ex Fi being non empty multMagma, h being Function st Fi = F.i & h = (the multF of it).(f,g) & h.i = (the multF of Fi).(f.i,g.i); end; registration let I be set, F be multMagma-Family of I; cluster product F -> non empty constituted-Functions; end; theorem :: GROUP_7:1 for F being multMagma-Family of I, G being non empty multMagma, p , q being Element of product F, x, y being Element of G st i in I & G = F.i & f = p & g = q & h = p * q & f.i = x & g.i = y holds x * y = h.i; definition let I be set, F be multMagma-Family of I; attr F is Group-like means :: GROUP_7:def 3 for i being set st i in I ex Fi being Group-like non empty multMagma st Fi = F.i; attr F is associative means :: GROUP_7:def 4 for i being set st i in I ex Fi being associative non empty multMagma st Fi = F.i; attr F is commutative means :: GROUP_7:def 5 for i being set st i in I ex Fi being commutative non empty multMagma st Fi = F.i; end; definition let I be non empty set, F be multMagma-Family of I; redefine attr F is Group-like means :: GROUP_7:def 6 for i being Element of I holds F. i is Group-like; redefine attr F is associative means :: GROUP_7:def 7 for i being Element of I holds F .i is associative; redefine attr F is commutative means :: GROUP_7:def 8 for i being Element of I holds F.i is commutative; end; registration let I be set; cluster Group-like associative commutative for multMagma-Family of I; end; registration let I be set, F be Group-like multMagma-Family of I; cluster product F -> Group-like; end; registration let I be set, F be associative multMagma-Family of I; cluster product F -> associative; end; registration let I be set, F be commutative multMagma-Family of I; cluster product F -> commutative; end; theorem :: GROUP_7:2 for F being multMagma-Family of I, G being non empty multMagma st i in I & G = F.i & product F is Group-like holds G is Group-like; theorem :: GROUP_7:3 for F being multMagma-Family of I, G being non empty multMagma st i in I & G = F.i & product F is associative holds G is associative; theorem :: GROUP_7:4 for F being multMagma-Family of I, G being non empty multMagma st i in I & G = F.i & product F is commutative holds G is commutative; theorem :: GROUP_7:5 for F being Group-like multMagma-Family of I st for i being set st i in I ex G being Group-like non empty multMagma st G = F.i & s.i = 1_G holds s = 1_product F; theorem :: GROUP_7:6 for F being Group-like multMagma-Family of I, G being Group-like non empty multMagma st i in I & G = F.i & f = 1_product F holds f.i = 1_G; theorem :: GROUP_7:7 for F being associative Group-like multMagma-Family of I, x being Element of product F st x = g & for i being set st i in I ex G being Group, y being Element of G st G = F.i & s.i = y" & y = g.i holds s = x"; theorem :: GROUP_7:8 for F being associative Group-like multMagma-Family of I, x being Element of product F, G being Group, y being Element of G st i in I & G = F.i & f = x & g = x" & f.i = y holds g.i = y"; definition let I be set, F be associative Group-like multMagma-Family of I; func sum F -> strict Subgroup of product F means :: GROUP_7:def 9 for x being object holds x in the carrier of it iff ex g being Element of product Carrier F, J being finite Subset of I, f being ManySortedSet of J st g = 1_product F & x = g +* f & for j being set st j in J ex G being Group-like non empty multMagma st G = F.j & f.j in the carrier of G & f.j <> 1_G; end; registration let I be set, F be associative Group-like multMagma-Family of I, f, g be Element of sum F; cluster (the multF of sum F).(f,g) -> Function-like Relation-like; end; theorem :: GROUP_7:9 for I being finite set, F being associative Group-like multMagma-Family of I holds product F = sum F; begin :: The product of one, two and three groups theorem :: GROUP_7:10 for G1 being non empty multMagma holds <*G1*> is multMagma-Family of {1}; registration let G1 be non empty multMagma; cluster <*G1*> -> {1} -defined; end; registration let G1 be non empty multMagma; cluster <*G1*> -> total multMagma-yielding; end; theorem :: GROUP_7:11 for G1 being Group-like non empty multMagma holds <*G1*> is Group-like multMagma-Family of {1}; registration let G1 be Group-like non empty multMagma; cluster <*G1*> -> Group-like; end; theorem :: GROUP_7:12 for G1 being associative non empty multMagma holds <*G1*> is associative multMagma-Family of {1}; registration let G1 be associative non empty multMagma; cluster <*G1*> -> associative; end; theorem :: GROUP_7:13 for G1 being commutative non empty multMagma holds <*G1*> is commutative multMagma-Family of {1}; registration let G1 be commutative non empty multMagma; cluster <*G1*> -> commutative; end; theorem :: GROUP_7:14 for G1 being Group holds <*G1*> is Group-like associative multMagma-Family of {1}; theorem :: GROUP_7:15 for G1 being commutative Group holds <*G1*> is commutative Group-like associative multMagma-Family of {1}; registration let G1 be non empty multMagma; cluster -> FinSequence-like for Element of product Carrier <*G1*>; end; registration let G1 be non empty multMagma; cluster -> FinSequence-like for Element of product <*G1*>; end; definition let G1 be non empty multMagma, x be Element of G1; redefine func <*x*> -> Element of product <*G1*>; end; theorem :: GROUP_7:16 for G1, G2 being non empty multMagma holds <*G1,G2*> is multMagma-Family of {1,2}; registration let G1, G2 be non empty multMagma; cluster <*G1,G2*> -> {1,2} -defined; end; registration let G1, G2 be non empty multMagma; cluster <*G1,G2*> -> total multMagma-yielding; end; theorem :: GROUP_7:17 for G1, G2 being Group-like non empty multMagma holds <*G1,G2 *> is Group-like multMagma-Family of {1,2}; registration let G1, G2 be Group-like non empty multMagma; cluster <*G1,G2*> -> Group-like; end; theorem :: GROUP_7:18 for G1, G2 being associative non empty multMagma holds <*G1,G2 *> is associative multMagma-Family of {1,2}; registration let G1, G2 be associative non empty multMagma; cluster <*G1,G2*> -> associative; end; theorem :: GROUP_7:19 for G1, G2 being commutative non empty multMagma holds <*G1,G2 *> is commutative multMagma-Family of {1,2}; registration let G1, G2 be commutative non empty multMagma; cluster <*G1,G2*> -> commutative; end; theorem :: GROUP_7:20 for G1, G2 being Group holds <*G1,G2*> is Group-like associative multMagma-Family of {1,2}; theorem :: GROUP_7:21 for G1, G2 being commutative Group holds <*G1,G2*> is Group-like associative commutative multMagma-Family of {1,2}; registration let G1, G2 be non empty multMagma; cluster -> FinSequence-like for Element of product Carrier <*G1,G2*>; end; registration let G1, G2 be non empty multMagma; cluster -> FinSequence-like for Element of product <*G1,G2*>; end; definition let G1, G2 be non empty multMagma, x be Element of G1, y be Element of G2; redefine func <*x,y*> -> Element of product <*G1,G2*>; end; theorem :: GROUP_7:22 for G1, G2, G3 being non empty multMagma holds <*G1,G2,G3*> is multMagma-Family of {1,2,3}; registration let G1, G2, G3 be non empty multMagma; cluster <*G1,G2,G3*> -> {1,2,3} -defined; end; registration let G1, G2, G3 be non empty multMagma; cluster <*G1,G2,G3*> -> total multMagma-yielding; end; theorem :: GROUP_7:23 for G1, G2, G3 being Group-like non empty multMagma holds <*G1 ,G2,G3*> is Group-like multMagma-Family of {1,2,3}; registration let G1, G2, G3 be Group-like non empty multMagma; cluster <*G1,G2,G3*> -> Group-like; end; theorem :: GROUP_7:24 for G1, G2, G3 being associative non empty multMagma holds <* G1,G2,G3*> is associative multMagma-Family of {1,2,3}; registration let G1, G2, G3 be associative non empty multMagma; cluster <*G1,G2,G3*> -> associative; end; theorem :: GROUP_7:25 for G1, G2, G3 being commutative non empty multMagma holds <* G1,G2,G3*> is commutative multMagma-Family of {1,2,3}; registration let G1, G2, G3 be commutative non empty multMagma; cluster <*G1,G2,G3*> -> commutative; end; theorem :: GROUP_7:26 for G1, G2, G3 being Group holds <*G1,G2,G3*> is Group-like associative multMagma-Family of {1,2,3}; theorem :: GROUP_7:27 for G1, G2, G3 being commutative Group holds <*G1,G2,G3*> is Group-like associative commutative multMagma-Family of {1,2,3}; registration let G1, G2, G3 be non empty multMagma; cluster -> FinSequence-like for Element of product Carrier <*G1,G2,G3*>; end; registration let G1, G2, G3 be non empty multMagma; cluster -> FinSequence-like for Element of product <*G1,G2,G3*>; end; definition let G1, G2, G3 be non empty multMagma, x be Element of G1, y be Element of G2, z be Element of G3; redefine func <*x,y,z*> -> Element of product <*G1,G2,G3*>; end; reserve G1, G2, G3 for non empty multMagma, x1, x2 for Element of G1, y1, y2 for Element of G2, z1, z2 for Element of G3; theorem :: GROUP_7:28 <*x1*> * <*x2*> = <*x1*x2*>; theorem :: GROUP_7:29 <*x1,y1*> * <*x2,y2*> = <*x1*x2,y1*y2*>; theorem :: GROUP_7:30 <*x1,y1,z1*> * <*x2,y2,z2*> = <*x1*x2,y1*y2,z1*z2*>; reserve G1, G2, G3 for Group-like non empty multMagma; theorem :: GROUP_7:31 1_product <*G1*> = <*1_G1*>; theorem :: GROUP_7:32 1_product <*G1,G2*> = <*1_G1,1_G2*>; theorem :: GROUP_7:33 1_product <*G1,G2,G3*> = <*1_G1,1_G2,1_G3*>; reserve G1, G2, G3 for Group, x for Element of G1, y for Element of G2, z for Element of G3; theorem :: GROUP_7:34 (<*x*> qua Element of product <*G1*>)" = <*x"*>; theorem :: GROUP_7:35 (<*x,y*> qua Element of product <*G1,G2*>)" = <*x",y"*>; theorem :: GROUP_7:36 (<*x,y,z*> qua Element of product <*G1,G2,G3*>)" = <*x",y",z" *>; theorem :: GROUP_7:37 for f being Function of the carrier of G1, the carrier of product <*G1*> st for x being Element of G1 holds f.x = <*x*> holds f is Homomorphism of G1, product <*G1*>; theorem :: GROUP_7:38 for f being Homomorphism of G1, product <*G1*> st for x being Element of G1 holds f.x = <*x*> holds f is bijective; theorem :: GROUP_7:39 G1, product <*G1*> are_isomorphic;