:: Product of Families of Groups and Vector Spaces :: by Anna Lango and Grzegorz Bancerek :: :: Received December 29, 1992 :: Copyright (c) 1992-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 RLVECT_1, ALGSTR_0, XBOOLE_0, STRUCT_0, VECTSP_1, SUPINF_2, BINOP_1, SUBSET_1, FUNCT_1, ARYTM_3, FINSEQOP, ARYTM_1, RELAT_1, GROUP_1, NAT_1, FINSEQ_2, CARD_3, FUNCOP_1, SETWISEO, ZFMISC_1, PARTFUN1, TARSKI, FINSEQ_1, MESFUNC1, MCART_1, FUNCT_6, GROUP_2, NUMBERS, PRVECT_1, PRALG_1, RLVECT_2, YELLOW_6, WAYBEL_3; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, NAT_1, CARD_3, RELAT_1, FUNCT_1, STRUCT_0, ALGSTR_0, PARTFUN1, FUNCT_2, FUNCT_3, BINOP_1, FUNCOP_1, RLVECT_1, GROUP_1, VECTSP_1, FINSEQOP, FINSEQ_1, FUNCT_6, SETWISEO, FINSEQ_2, PRALG_1, YELLOW_6, WAYBEL_3; constructors PARTFUN1, BINOP_1, FUNCT_3, SETWISEO, FUNCT_5, CARD_3, FINSEQOP, FUNCT_6, VECTSP_1, RLVECT_1, RELSET_1, FINSEQ_2, GROUP_1, PRALG_1, YELLOW_6, WAYBEL_3; registrations XBOOLE_0, RELAT_1, FUNCT_1, ORDINAL1, FUNCT_2, FINSEQ_1, FINSEQ_2, CARD_3, STRUCT_0, VECTSP_1, RELSET_1, CARD_1; requirements BOOLE, SUBSET; begin :: Abelian Groups and Fields reserve G for Abelian add-associative right_complementable right_zeroed non empty addLoopStr; theorem :: PRVECT_1:1 0.G is_a_unity_wrt the addF of G; theorem :: PRVECT_1:2 for G being AbGroup holds comp G is_an_inverseOp_wrt the addF of G; reserve GS for non empty addLoopStr; theorem :: PRVECT_1:3 the addF of GS is commutative associative & 0.GS is_a_unity_wrt the addF of GS & comp GS is_an_inverseOp_wrt the addF of GS implies GS is AbGroup; reserve F for Field; theorem :: PRVECT_1:4 0.F is_a_unity_wrt the addF of F; theorem :: PRVECT_1:5 1_F is_a_unity_wrt the multF of F; begin :: The $n$-Product of a Binary and Unary Operation reserve F for Field, n for Nat, D for non empty set, d for Element of D, B for BinOp of D, C for UnOp of D; definition let D,n; let F be BinOp of D; let x,y be Element of n-tuples_on D; redefine func F.:(x,y) -> Element of n-tuples_on D; end; definition let D be non empty set; let F be BinOp of D; let n be Nat; func product(F,n) -> BinOp of n-tuples_on D means :: PRVECT_1:def 1 for x,y being Element of n-tuples_on D holds it.(x,y)=F.:(x,y); end; definition let D; let F be UnOp of D; let n; func product(F,n) -> UnOp of n-tuples_on D means :: PRVECT_1:def 2 for x being Element of n-tuples_on D holds it.x=F*x; end; theorem :: PRVECT_1:6 B is commutative implies product(B,n) is commutative; theorem :: PRVECT_1:7 B is associative implies product(B,n) is associative; theorem :: PRVECT_1:8 d is_a_unity_wrt B implies n |-> d is_a_unity_wrt product(B,n); theorem :: PRVECT_1:9 B is having_a_unity & B is associative & C is_an_inverseOp_wrt B implies product(C,n) is_an_inverseOp_wrt product(B,n); begin :: The $n$-Power of a Group and of a Field definition let F be non empty addLoopStr, n; assume F is Abelian add-associative right_zeroed right_complementable; func n -Group_over F -> strict AbGroup equals :: PRVECT_1:def 3 addLoopStr(# n-tuples_on the carrier of F, product(the addF of F,n), (n |-> 0.F) qua Element of n-tuples_on the carrier of F#); end; registration let F be AbGroup, n; cluster n-Group_over F -> non empty; end; reserve x,y for set; definition let F,n; func n -Mult_over F -> Function of [:the carrier of F,n-tuples_on the carrier of F:], n-tuples_on the carrier of F means :: PRVECT_1:def 4 for x being Element of F, v being Element of n-tuples_on the carrier of F holds it.(x,v) = (the multF of F)[;](x,v); end; definition let F,n; func n -VectSp_over F -> strict ModuleStr over F means :: PRVECT_1:def 5 the addLoopStr of it = n -Group_over F & the lmult of it = n -Mult_over F; end; registration let F,n; cluster n -VectSp_over F -> non empty; end; reserve D for non empty set, H,G for BinOp of D, d for Element of D, t1,t2 for Element of n-tuples_on D; theorem :: PRVECT_1:10 H is_distributive_wrt G implies H[;](d,G.:(t1,t2)) = G.: (H[;](d,t1),H[;](d,t2)); definition let D be non empty set, n be Nat, F be BinOp of D, x be Element of D, v be Element of n-tuples_on D; redefine func F[;](x,v) -> Element of n-tuples_on D; end; registration let F,n; cluster n -VectSp_over F -> vector-distributive scalar-distributive scalar-associative scalar-unital; end; begin :: Sequences of domains reserve x,y,z for set, A for AbGroup; definition mode Domain-Sequence is non empty non-empty FinSequence; end; scheme :: PRVECT_1:sch 1 NEFinSeqLambda {w() -> non empty FinSequence, F(set)->set}: ex p being non empty FinSequence st len p = len w() & for i being Element of dom w() holds p.i = F(i); definition let a be non-empty non empty Function; let f be Element of product a; let i be Element of dom a; redefine func f.i -> Element of a.i; end; begin :: The Product of Families of Operations reserve a for Domain-Sequence, i for Element of dom a, p for FinSequence; definition let a be non-empty non empty Function; mode BinOps of a -> Function means :: PRVECT_1:def 6 dom it = dom a & for i being Element of dom a holds it.i is BinOp of a.i; mode UnOps of a -> Function means :: PRVECT_1:def 7 dom it = dom a & for i being Element of dom a holds it.i is UnOp of a.i; end; registration let a; cluster -> FinSequence-like for BinOps of a; cluster -> FinSequence-like for UnOps of a; end; registration let a; cluster -> Function-yielding for BinOps of a; cluster -> Function-yielding for UnOps of a; end; theorem :: PRVECT_1:11 p is BinOps of a iff len p = len a & for i holds p.i is BinOp of a.i; theorem :: PRVECT_1:12 p is UnOps of a iff len p = len a & for i holds p.i is UnOp of a .i; definition let a; let b be BinOps of a; let i; redefine func b.i -> BinOp of a.i; end; definition let a; let u be UnOps of a; let i; redefine func u.i -> UnOp of a.i; end; theorem :: PRVECT_1:13 for d,d9 being UnOp of product a st for f being Element of product a, i being Element of dom a holds (d.f).i = (d9.f).i holds d = d9; theorem :: PRVECT_1:14 for u being UnOps of a holds doms u = a & product rngs u c= product a; definition let a; let u be UnOps of a; redefine func Frege u -> UnOp of product a; end; theorem :: PRVECT_1:15 for u being UnOps of a for f being Element of product a, i being Element of dom a holds (Frege u).f.i = (u.i).(f.i); theorem :: PRVECT_1:16 for d,d9 being BinOp of product a st for f,g being Element of product a, i being Element of dom a holds (d.(f,g)).i = (d9.(f,g)).i holds d = d9; reserve i for Element of dom a; definition let a; let b be BinOps of a; func [:b:] -> BinOp of product a means :: PRVECT_1:def 8 for f,g being Element of product a, i being Element of dom a holds (it.(f,g)).i = (b.i).(f.i,g.i); end; theorem :: PRVECT_1:17 for b being BinOps of a st for i holds b.i is commutative holds [:b:] is commutative; theorem :: PRVECT_1:18 for b being BinOps of a st for i holds b.i is associative holds [:b:] is associative; theorem :: PRVECT_1:19 for b being BinOps of a, f being Element of product a st for i holds f.i is_a_unity_wrt b.i holds f is_a_unity_wrt [:b:]; theorem :: PRVECT_1:20 for b being BinOps of a, u being UnOps of a st for i holds u.i is_an_inverseOp_wrt b.i & b.i is having_a_unity holds Frege u is_an_inverseOp_wrt [:b:]; begin :: The Product of Groups definition ::: non-empty-addLoopStr-yielding should be replaced ::: by non-Empty addLoopStr-yielding let F be Relation; attr F is non-empty-addLoopStr-yielding means :: PRVECT_1:def 9 x in rng F implies x is non empty addLoopStr; attr F is AbGroup-yielding means :: PRVECT_1:def 10 x in rng F implies x is AbGroup; end; registration cluster AbGroup-yielding -> non-empty-addLoopStr-yielding for Relation; end; registration cluster non-empty-addLoopStr-yielding -> non-Empty 1-sorted-yielding for Relation; end; registration cluster non empty AbGroup-yielding for FinSequence; end; definition mode Group-Sequence is non empty AbGroup-yielding FinSequence; end; definition let g be non empty non-empty-addLoopStr-yielding FinSequence; let i be Element of dom g; redefine func g.i -> non empty addLoopStr; end; definition let g be Group-Sequence; let i be Element of dom g; redefine func g.i -> AbGroup; end; notation let g be non empty non-Empty 1-sorted-yielding FinSequence; synonym carr g for Carrier g; end; registration let f be 1-sorted-yielding FinSequence; cluster Carrier f -> FinSequence-like; end; registration let f be non empty 1-sorted-yielding Function; cluster Carrier f -> non empty; end; registration let f be non-Empty 1-sorted-yielding Function; cluster Carrier f -> non-empty; end; definition let g be non empty non-Empty 1-sorted-yielding FinSequence; redefine func carr g -> Domain-Sequence means :: PRVECT_1:def 11 len it = len g & for j be Element of dom g holds it.j = the carrier of g.j; end; reserve g for Group-Sequence, i for Element of dom carr g; definition let g be non empty non-empty-addLoopStr-yielding FinSequence; let i be Element of dom carr g; redefine func g.i -> non empty addLoopStr; end; definition let g,i; redefine func g.i -> AbGroup; end; definition let g be non-empty-addLoopStr-yielding non empty FinSequence; func addop g -> BinOps of carr g means :: PRVECT_1:def 12 len it = len carr g & for i being Element of dom carr g holds it.i = the addF of g.i; end; definition let g be non-empty-addLoopStr-yielding non empty FinSequence; func complop g -> UnOps of carr g means :: PRVECT_1:def 13 len it = len carr g & for i being Element of dom carr g holds it.i = comp g.i; func zeros g -> Element of product carr g means :: PRVECT_1:def 14 for i being Element of dom carr g holds it.i = 0.(g.i); end; definition let G be non-empty-addLoopStr-yielding non empty FinSequence; func product G -> strict non empty addLoopStr equals :: PRVECT_1:def 15 addLoopStr (# product carr G, [:addop G:], zeros G #); end; registration let G be Group-Sequence; cluster product G -> add-associative right_zeroed right_complementable non empty Abelian; end;