Volume 10, 1998

University of Bialystok

Copyright (c) 1998 Association of Mizar Users

### The abstract of the Mizar article:

### The Product of the Families of the Groups

**by****Artur Kornilowicz**- Received June 10, 1998
- MML identifier: GROUP_7

- [ Mizar article, MML identifier index ]

environ vocabulary FINSEQ_1, FUNCT_1, PBOOLE, RELAT_1, VECTSP_1, PRALG_1, RLVECT_2, ZF_REFLE, CARD_3, TARSKI, BINOP_1, GROUP_1, REALSET1, BOOLE, SEMI_AF1, GROUP_2, FINSET_1, FUNCT_4, GROUP_6, WELLORD1, GROUP_7; notation TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, PARTFUN1, XREAL_0, NAT_1, FINSEQ_1, FUNCT_2, FUNCT_4, FINSET_1, BINOP_1, STRUCT_0, VECTSP_1, GROUP_1, GROUP_2, GROUP_6, PBOOLE, CARD_3, PRALG_1, PRALG_2; constructors BINOP_1, GROUP_6, PRALG_2, ENUMSET1, XCMPLX_0, MEMBERED; clusters STRUCT_0, PRALG_2, GROUP_1, FINSET_1, RELAT_1, GROUP_2, FINSEQ_1, MOD_2, RELSET_1, ARYTM_3, MEMBERED; requirements NUMERALS, BOOLE, SUBSET; begin :: Preliminaries reserve a, b, c, d, e, f for set; theorem :: GROUP_7:1 <*a*> = <*b*> implies a = b; theorem :: GROUP_7:2 <*a,b*> = <*c,d*> implies a = c & b = d; theorem :: GROUP_7:3 <*a,b,c*> = <*d,e,f*> implies a = d & b = e & c = f; 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 HGrStr-yielding means :: GROUP_7:def 1 for y being set st y in rng R holds y is non empty HGrStr; end; definition cluster HGrStr-yielding -> 1-sorted-yielding Function; end; definition let I be set; cluster HGrStr-yielding ManySortedSet of I; end; definition cluster HGrStr-yielding Function; end; definition let I be set; mode HGrStr-Family of I is HGrStr-yielding ManySortedSet of I; end; definition let I be non empty set, F be HGrStr-Family of I, i be Element of I; redefine func F.i -> non empty HGrStr; end; definition let I be set, F be HGrStr-Family of I; cluster Carrier F -> non-empty; end; definition let I be set, F be HGrStr-Family of I; func product F -> strict HGrStr 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 HGrStr, h being Function st Fi = F.i & h = (the mult of it).(f,g) & h.i = (the mult of Fi).(f.i,g.i); end; definition let I be set, F be HGrStr-Family of I; cluster product F -> non empty; end; definition let I be set, F be HGrStr-Family of I; cluster -> Function-like Relation-like Element of product F; end; definition let I be set, F be HGrStr-Family of I, f, g be Element of product Carrier F; cluster (the mult of product F).(f,g) -> Function-like Relation-like; end; theorem :: GROUP_7:4 for F being HGrStr-Family of I, G being non empty HGrStr, 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 HGrStr-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 HGrStr) 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 HGrStr) 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 HGrStr) st Fi = F.i; end; definition let I be non empty set, F be HGrStr-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; definition let I be set; cluster Group-like associative commutative HGrStr-Family of I; end; definition let I be set, F be Group-like HGrStr-Family of I; cluster product F -> Group-like; end; definition let I be set, F be associative HGrStr-Family of I; cluster product F -> associative; end; definition let I be set, F be commutative HGrStr-Family of I; cluster product F -> commutative; end; theorem :: GROUP_7:5 for F being HGrStr-Family of I, G being non empty HGrStr st i in I & G = F.i & product F is Group-like holds G is Group-like; theorem :: GROUP_7:6 for F being HGrStr-Family of I, G being non empty HGrStr st i in I & G = F.i & product F is associative holds G is associative; theorem :: GROUP_7:7 for F being HGrStr-Family of I, G being non empty HGrStr st i in I & G = F.i & product F is commutative holds G is commutative; theorem :: GROUP_7:8 for F being Group-like HGrStr-Family of I st for i being set st i in I ex G being Group-like (non empty HGrStr) st G = F.i & s.i = 1.G holds s = 1.product F; theorem :: GROUP_7:9 for F being Group-like HGrStr-Family of I, G being Group-like (non empty HGrStr) st i in I & G = F.i & f = 1.product F holds f.i = 1.G; theorem :: GROUP_7:10 for F being associative Group-like HGrStr-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:11 for F being associative Group-like HGrStr-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 HGrStr-Family of I; func sum F -> strict Subgroup of product F means :: GROUP_7:def 9 for x being set 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 HGrStr) st G = F.j & f.j in the carrier of G & f.j <> 1.G; end; definition let I be set, F be associative Group-like HGrStr-Family of I, f, g be Element of sum F; cluster (the mult of sum F).(f,g) -> Function-like Relation-like; end; theorem :: GROUP_7:12 for I being finite set, F being associative Group-like HGrStr-Family of I holds product F = sum F; begin :: The product of one, two and three groups theorem :: GROUP_7:13 for G1 being non empty HGrStr holds <*G1*> is HGrStr-Family of {1}; definition let G1 be non empty HGrStr; redefine func <*G1*> -> HGrStr-Family of {1}; end; theorem :: GROUP_7:14 for G1 being Group-like (non empty HGrStr) holds <*G1*> is Group-like HGrStr-Family of {1}; definition let G1 be Group-like (non empty HGrStr); redefine func <*G1*> -> Group-like HGrStr-Family of {1}; end; theorem :: GROUP_7:15 for G1 being associative (non empty HGrStr) holds <*G1*> is associative HGrStr-Family of {1}; definition let G1 be associative (non empty HGrStr); redefine func <*G1*> -> associative HGrStr-Family of {1}; end; theorem :: GROUP_7:16 for G1 being commutative (non empty HGrStr) holds <*G1*> is commutative HGrStr-Family of {1}; definition let G1 be commutative (non empty HGrStr); redefine func <*G1*> -> commutative HGrStr-Family of {1}; end; theorem :: GROUP_7:17 for G1 being Group holds <*G1*> is Group-like associative HGrStr-Family of {1}; definition let G1 be Group; redefine func <*G1*> -> Group-like associative HGrStr-Family of {1}; end; theorem :: GROUP_7:18 for G1 being commutative Group holds <*G1*> is commutative Group-like associative HGrStr-Family of {1}; definition let G1 be commutative Group; redefine func <*G1*> -> Group-like associative commutative HGrStr-Family of {1}; end; definition let G1 be non empty HGrStr; cluster -> FinSequence-like Element of product Carrier <*G1*>; end; definition let G1 be non empty HGrStr; cluster -> FinSequence-like Element of product <*G1*>; end; definition let G1 be non empty HGrStr, x be Element of G1; redefine func <*x*> -> Element of product <*G1*>; end; theorem :: GROUP_7:19 for G1, G2 being non empty HGrStr holds <*G1,G2*> is HGrStr-Family of {1,2}; definition let G1, G2 be non empty HGrStr; redefine func <*G1,G2*> -> HGrStr-Family of {1,2}; end; theorem :: GROUP_7:20 for G1, G2 being Group-like (non empty HGrStr) holds <*G1,G2*> is Group-like HGrStr-Family of {1,2}; definition let G1, G2 be Group-like (non empty HGrStr); redefine func <*G1,G2*> -> Group-like HGrStr-Family of {1,2}; end; theorem :: GROUP_7:21 for G1, G2 being associative (non empty HGrStr) holds <*G1,G2*> is associative HGrStr-Family of {1,2}; definition let G1, G2 be associative (non empty HGrStr); redefine func <*G1,G2*> -> associative HGrStr-Family of {1,2}; end; theorem :: GROUP_7:22 for G1, G2 being commutative (non empty HGrStr) holds <*G1,G2*> is commutative HGrStr-Family of {1,2}; definition let G1, G2 be commutative (non empty HGrStr); redefine func <*G1,G2*> -> commutative HGrStr-Family of {1,2}; end; theorem :: GROUP_7:23 for G1, G2 being Group holds <*G1,G2*> is Group-like associative HGrStr-Family of {1,2}; definition let G1, G2 be Group; redefine func <*G1,G2*> -> Group-like associative HGrStr-Family of {1,2}; end; theorem :: GROUP_7:24 for G1, G2 being commutative Group holds <*G1,G2*> is Group-like associative commutative HGrStr-Family of {1,2}; definition let G1, G2 be commutative Group; redefine func <*G1,G2*> -> Group-like associative commutative HGrStr-Family of {1,2}; end; definition let G1, G2 be non empty HGrStr; cluster -> FinSequence-like Element of product Carrier <*G1,G2*>; end; definition let G1, G2 be non empty HGrStr; cluster -> FinSequence-like Element of product <*G1,G2*>; end; definition let G1, G2 be non empty HGrStr, x be Element of G1, y be Element of G2; redefine func <*x,y*> -> Element of product <*G1,G2*>; end; theorem :: GROUP_7:25 for G1, G2, G3 being non empty HGrStr holds <*G1,G2,G3*> is HGrStr-Family of {1,2,3}; definition let G1, G2, G3 be non empty HGrStr; redefine func <*G1,G2,G3*> -> HGrStr-Family of {1,2,3}; end; theorem :: GROUP_7:26 for G1, G2, G3 being Group-like (non empty HGrStr) holds <*G1,G2,G3*> is Group-like HGrStr-Family of {1,2,3}; definition let G1, G2, G3 be Group-like (non empty HGrStr); redefine func <*G1,G2,G3*> -> Group-like HGrStr-Family of {1,2,3}; end; theorem :: GROUP_7:27 for G1, G2, G3 being associative (non empty HGrStr) holds <*G1,G2,G3*> is associative HGrStr-Family of {1,2,3}; definition let G1, G2, G3 be associative (non empty HGrStr); redefine func <*G1,G2,G3*> -> associative HGrStr-Family of {1,2,3}; end; theorem :: GROUP_7:28 for G1, G2, G3 being commutative (non empty HGrStr) holds <*G1,G2,G3*> is commutative HGrStr-Family of {1,2,3}; definition let G1, G2, G3 be commutative (non empty HGrStr); redefine func <*G1,G2,G3*> -> commutative HGrStr-Family of {1,2,3}; end; theorem :: GROUP_7:29 for G1, G2, G3 being Group holds <*G1,G2,G3*> is Group-like associative HGrStr-Family of {1,2,3}; definition let G1, G2, G3 be Group; redefine func <*G1,G2,G3*> -> Group-like associative HGrStr-Family of {1,2,3}; end; theorem :: GROUP_7:30 for G1, G2, G3 being commutative Group holds <*G1,G2,G3*> is Group-like associative commutative HGrStr-Family of {1,2,3}; definition let G1, G2, G3 be commutative Group; redefine func <*G1,G2,G3*> -> Group-like associative commutative HGrStr-Family of {1,2,3}; end; definition let G1, G2, G3 be non empty HGrStr; cluster -> FinSequence-like Element of product Carrier <*G1,G2,G3*>; end; definition let G1, G2, G3 be non empty HGrStr; cluster -> FinSequence-like Element of product <*G1,G2,G3*>; end; definition let G1, G2, G3 be non empty HGrStr, 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 HGrStr, x1, x2 for Element of G1, y1, y2 for Element of G2, z1, z2 for Element of G3; theorem :: GROUP_7:31 <*x1*> * <*x2*> = <*x1*x2*>; theorem :: GROUP_7:32 <*x1,y1*> * <*x2,y2*> = <*x1*x2,y1*y2*>; theorem :: GROUP_7:33 <*x1,y1,z1*> * <*x2,y2,z2*> = <*x1*x2,y1*y2,z1*z2*>; reserve G1, G2, G3 for Group-like (non empty HGrStr); theorem :: GROUP_7:34 1.product <*G1*> = <*1.G1*>; theorem :: GROUP_7:35 1.product <*G1,G2*> = <*1.G1,1.G2*>; theorem :: GROUP_7:36 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:37 (<*x*> qua Element of product <*G1*>)" = <*x"*>; theorem :: GROUP_7:38 (<*x,y*> qua Element of product <*G1,G2*>)" = <*x",y"*>; theorem :: GROUP_7:39 (<*x,y,z*> qua Element of product <*G1,G2,G3*>)" = <*x",y",z" *>; theorem :: GROUP_7:40 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:41 for f being Homomorphism of G1, product <*G1*> st for x being Element of G1 holds f.x = <*x*> holds f is_isomorphism; theorem :: GROUP_7:42 G1, product <*G1*> are_isomorphic;

Back to top