:: Product of Families of Groups and Vector Spaces
:: by Anna Lango and Grzegorz Bancerek
::
:: Received December 29, 1992
:: Copyright (c) 1992 Association of Mizar Users
deffunc H1( 1-sorted ) -> set = the carrier of $1;
deffunc H2( addLoopStr ) -> M5([:the carrier of $1,the carrier of $1:],the carrier of $1) = the addF of $1;
deffunc H3( non empty addLoopStr ) -> M5(the carrier of $1,the carrier of $1) = comp $1;
deffunc H4( addLoopStr ) -> Element of the carrier of $1 = 0. $1;
theorem :: PRVECT_1:1
canceled;
theorem :: PRVECT_1:2
canceled;
theorem Th3: :: PRVECT_1:3
theorem Th4: :: PRVECT_1:4
Lm1:
for G being non empty right_complementable Abelian add-associative right_zeroed addLoopStr holds comp G is_an_inverseOp_wrt the addF of G
theorem :: PRVECT_1:5
Lm2:
for GS being non empty addLoopStr st the addF of GS is commutative & the addF of GS is associative holds
( GS is Abelian & GS is add-associative )
Lm3:
for GS being non empty addLoopStr st 0. GS is_a_unity_wrt the addF of GS holds
GS is right_zeroed
Lm4:
for F being Field holds the multF of F is associative
theorem :: PRVECT_1:6
canceled;
theorem :: PRVECT_1:7
canceled;
theorem :: PRVECT_1:8
canceled;
theorem :: PRVECT_1:9
canceled;
theorem :: PRVECT_1:10
theorem Th11: :: PRVECT_1:11
Lm5:
for F being Field holds the multF of F is_distributive_wrt the addF of F
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 :
Def1:
:: PRVECT_1:def 1
for
x,
y being
Element of
n -tuples_on D holds
it . x,
y = F .: x,
y;
existence
ex b1 being BinOp of n -tuples_on D st
for x, y being Element of n -tuples_on D holds b1 . x,y = F .: x,y
uniqueness
for b1, b2 being BinOp of n -tuples_on D st ( for x, y being Element of n -tuples_on D holds b1 . x,y = F .: x,y ) & ( for x, y being Element of n -tuples_on D holds b2 . x,y = F .: x,y ) holds
b1 = b2
end;
:: deftheorem Def1 defines product PRVECT_1:def 1 :
:: deftheorem Def2 defines product PRVECT_1:def 2 :
theorem :: PRVECT_1:12
canceled;
theorem :: PRVECT_1:13
canceled;
theorem Th14: :: PRVECT_1:14
theorem Th15: :: PRVECT_1:15
theorem Th16: :: PRVECT_1:16
theorem Th17: :: PRVECT_1:17
:: deftheorem Def3 defines -Group_over PRVECT_1:def 3 :
definition
let F be
Field;
let n be
Nat;
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 :
Def4:
:: PRVECT_1:def 4
for
x being
Element of
F for
v being
Element of
n -tuples_on the
carrier of
F holds
it . x,
v = the
multF of
F [;] x,
v;
existence
ex b1 being Function of [:the carrier of F,(n -tuples_on the carrier of F):],n -tuples_on the carrier of F st
for x being Element of F
for v being Element of n -tuples_on the carrier of F holds b1 . x,v = the multF of F [;] x,v
uniqueness
for b1, b2 being Function of [:the carrier of F,(n -tuples_on the carrier of F):],n -tuples_on the carrier of F st ( for x being Element of F
for v being Element of n -tuples_on the carrier of F holds b1 . x,v = the multF of F [;] x,v ) & ( for x being Element of F
for v being Element of n -tuples_on the carrier of F holds b2 . x,v = the multF of F [;] x,v ) holds
b1 = b2
end;
:: deftheorem Def4 defines -Mult_over PRVECT_1:def 4 :
:: deftheorem Def5 defines -VectSp_over PRVECT_1:def 5 :
theorem Th18: :: PRVECT_1:18
:: deftheorem PRVECT_1:def 6 :
canceled;
:: deftheorem PRVECT_1:def 7 :
canceled;
:: deftheorem Def8 defines BinOps PRVECT_1:def 8 :
:: deftheorem Def9 defines UnOps PRVECT_1:def 9 :
theorem Th19: :: PRVECT_1:19
theorem Th20: :: PRVECT_1:20
theorem :: PRVECT_1:21
theorem Th22: :: PRVECT_1:22
theorem Th23: :: PRVECT_1:23
theorem Th24: :: PRVECT_1:24
definition
let a be
Domain-Sequence;
let b be
BinOps of
a;
func [:b:] -> BinOp of
product a means :
Def10:
:: PRVECT_1:def 10
for
f,
g being
Element of
product a for
i being
Element of
dom a holds
(it . f,g) . i = (b . i) . (f . i),
(g . i);
existence
ex b1 being BinOp of product a st
for f, g being Element of product a
for i being Element of dom a holds (b1 . f,g) . i = (b . i) . (f . i),(g . i)
uniqueness
for b1, b2 being BinOp of product a st ( for f, g being Element of product a
for i being Element of dom a holds (b1 . f,g) . i = (b . i) . (f . i),(g . i) ) & ( for f, g being Element of product a
for i being Element of dom a holds (b2 . f,g) . i = (b . i) . (f . i),(g . i) ) holds
b1 = b2
end;
:: deftheorem Def10 defines [: PRVECT_1:def 10 :
theorem Th25: :: PRVECT_1:25
theorem Th26: :: PRVECT_1:26
theorem Th27: :: PRVECT_1:27
theorem Th28: :: PRVECT_1:28
:: deftheorem Def11 defines AbGroup-yielding PRVECT_1:def 11 :
:: deftheorem Def12 defines carr PRVECT_1:def 12 :
:: deftheorem Def13 defines addop PRVECT_1:def 13 :
:: deftheorem Def14 defines complop PRVECT_1:def 14 :
:: deftheorem Def15 defines zeros PRVECT_1:def 15 :
:: deftheorem defines product PRVECT_1:def 16 :