:: Product of Families of Groups and Vector Spaces
:: by Anna Lango and Grzegorz Bancerek
::
:: Received December 29, 1992
:: Copyright (c) 1992-2016 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;
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;
constructors PARTFUN1, BINOP_1, FUNCT_3, SETWISEO, FUNCT_5, CARD_3, FINSEQOP,
FUNCT_6, VECTSP_1, RLVECT_1, RELSET_1, FINSEQ_2, GROUP_1;
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
let F be Relation;
attr F is AbGroup-yielding means
:: PRVECT_1:def 9
x in rng F implies x is AbGroup;
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 Group-Sequence;
let i be Element of dom g;
redefine func g.i -> AbGroup;
end;
definition
let g be Group-Sequence;
func carr g -> Domain-Sequence means
:: PRVECT_1:def 10
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,i;
redefine func g.i -> AbGroup;
end;
definition
let g;
func addop g -> BinOps of carr g means
:: PRVECT_1:def 11
len it = len carr g & for i holds it.i = the addF of g.i;
func complop g -> UnOps of carr g means
:: PRVECT_1:def 12
len it = len carr g & for i holds it.i = comp g.i;
func zeros g -> Element of product carr g means
:: PRVECT_1:def 13
for i holds it.i = 0.(g.i);
end;
definition
let G be Group-Sequence;
func product G -> strict AbGroup equals
:: PRVECT_1:def 14
addLoopStr(# product carr G, [:addop G:], zeros G #);
end;