:: Product of Families of Groups and Vector Spaces
:: by Anna Lango and Grzegorz Bancerek
::
:: Received December 29, 1992
:: Copyright (c) 1992-2012 Association of Mizar Users


begin

deffunc H1( 1-sorted ) ->  set = the carrier of $1;

deffunc H2( addLoopStr ) ->  Element of bool [:[: the carrier of $1, the carrier of $1:], the carrier of $1:] = the addF of $1;

deffunc H3( non empty addLoopStr ) ->  Element of bool [: the carrier of $1, the carrier of $1:] = comp $1;

deffunc H4( addLoopStr ) ->  Element of the carrier of $1 = 0. $1;

theorem Th1: :: PRVECT_1:1
for G being non empty right_complementable Abelian add-associative right_zeroed addLoopStr holds 0. G is_a_unity_wrt the addF of G
proofend;

theorem Th2: :: PRVECT_1:2
for G being AbGroup holds comp G is_an_inverseOp_wrt the addF of G
proofend;

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
proofend;

theorem :: PRVECT_1:3
for GS being non empty addLoopStr st the addF of GS is commutative & the addF of GS is associative & 0. GS is_a_unity_wrt the addF of GS & comp GS is_an_inverseOp_wrt the addF of GS holds
GS is AbGroup
proofend;

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 )
proofend;

Lm3:  for GS being non empty addLoopStr st 0. GS is_a_unity_wrt the addF of GS holds
GS is right_zeroed
proofend;

Lm4:  for F being Field holds the multF of F is associative
proofend;

theorem :: PRVECT_1:4
for F being Field holds 0. F is_a_unity_wrt the addF of F
proofend;

theorem Th5: :: PRVECT_1:5
for F being Field holds 1_ F is_a_unity_wrt the multF of F
proofend;

Lm5:  for F being Field holds the multF of F is_distributive_wrt the addF of F
proofend;

begin

definition
let D be non empty set ;
let n be Nat;
let F be BinOp of D;
let x, y be Element of n -tuples_on D;
:: original:.:
redefine funcF .: (x,y) ->  Element of n -tuples_on D;
coherence
 F .: (x,y) is Element of n -tuples_on D by FINSEQ_2:120;
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 :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)
proofend;
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
proofend;
end;

:: deftheorem Def1 defines product PRVECT_1:def_1_:_
 for D being non empty set
for F being BinOp of D
for n being Nat
for b4 being BinOp of (n -tuples_on D) holds
( b4 = product (F,n) iff for x, y being Element of n -tuples_on D holds b4 . (x,y) = F .: (x,y) );

definition
let D be non empty set ;
let F be UnOp of D;
let n be Nat;
func product (F,n) ->  UnOp of (n -tuples_on D) means :Def2: :: PRVECT_1:def 2
 for x being Element of n -tuples_on D holds it . x = F * x;
existence
 ex b1 being UnOp of (n -tuples_on D) st
for x being Element of n -tuples_on D holds b1 . x = F * x
proofend;
uniqueness
 for b1, b2 being UnOp of (n -tuples_on D) st ( for x being Element of n -tuples_on D holds b1 . x = F * x ) & ( for x being Element of n -tuples_on D holds b2 . x = F * x ) holds
b1 = b2
proofend;
end;

:: deftheorem Def2 defines product PRVECT_1:def_2_:_
 for D being non empty set
for F being UnOp of D
for n being Nat
for b4 being UnOp of (n -tuples_on D) holds
( b4 = product (F,n) iff for x being Element of n -tuples_on D holds b4 . x = F * x );

theorem Th6: :: PRVECT_1:6
for n being Nat
for D being non empty set
for B being BinOp of D st B is commutative holds
product (B,n) is commutative
proofend;

theorem Th7: :: PRVECT_1:7
for n being Nat
for D being non empty set
for B being BinOp of D st B is associative holds
product (B,n) is associative
proofend;

theorem Th8: :: PRVECT_1:8
for n being Nat
for D being non empty set
for d being Element of D
for B being BinOp of D st d is_a_unity_wrt B holds
n |-> d is_a_unity_wrt product (B,n)
proofend;

theorem Th9: :: PRVECT_1:9
for n being Nat
for D being non empty set
for B being BinOp of D
for C being UnOp of D st B is having_a_unity & B is associative & C is_an_inverseOp_wrt B holds
product (C,n) is_an_inverseOp_wrt product (B,n)
proofend;

begin

definition
let F be non empty addLoopStr ;
let n be Nat;
assume A1: ( F is Abelian & F is add-associative & F is right_zeroed & F is right_complementable ) ;
funcn -Group_over F ->  strict AbGroup equals :Def3: :: PRVECT_1:def 3
 addLoopStr(# (n -tuples_on the carrier of F),(product ( the addF of F,n)),(n |-> (0. F)) #);
coherence
 addLoopStr(# (n -tuples_on the carrier of F),(product ( the addF of F,n)),(n |-> (0. F)) #) is strict AbGroup
proofend;
end;

:: deftheorem Def3 defines -Group_over PRVECT_1:def_3_:_
 for F being non empty addLoopStr
for n being Nat st F is Abelian & F is add-associative & F is right_zeroed & F is right_complementable holds
n -Group_over F = addLoopStr(# (n -tuples_on the carrier of F),(product ( the addF of F,n)),(n |-> (0. F)) #);

registration
let F be AbGroup;
let n be Nat;
clustern -Group_over F ->  strict ;
coherence
 not n -Group_over F is empty ;
end;

definition
let F be Field;
let n be Nat;
funcn -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)
proofend;
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
proofend;
end;

:: deftheorem Def4 defines -Mult_over PRVECT_1:def_4_:_
 for F being Field
for n being Nat
for b3 being Function of [: the carrier of F,(n -tuples_on the carrier of F):],(n -tuples_on the carrier of F) holds
( b3 = n -Mult_over F iff for x being Element of F
for v being Element of n -tuples_on the carrier of F holds b3 . (x,v) = the multF of F [;] (x,v) );

definition
let F be Field;
let n be Nat;
funcn -VectSp_over F ->  strict VectSpStr over F means :Def5: :: PRVECT_1:def 5
( addLoopStr(# the carrier of it, the addF of it, the ZeroF of it #) = n -Group_over F & the lmult of it = n -Mult_over F );
existence
 ex b1 being strict VectSpStr over F st
( addLoopStr(# the carrier of b1, the addF of b1, the ZeroF of b1 #) = n -Group_over F & the lmult of b1 = n -Mult_over F )
proofend;
uniqueness
 for b1, b2 being strict VectSpStr over F st addLoopStr(# the carrier of b1, the addF of b1, the ZeroF of b1 #) = n -Group_over F & the lmult of b1 = n -Mult_over F & addLoopStr(# the carrier of b2, the addF of b2, the ZeroF of b2 #) = n -Group_over F & the lmult of b2 = n -Mult_over F holds
b1 = b2 ;
end;

:: deftheorem Def5 defines -VectSp_over PRVECT_1:def_5_:_
 for F being Field
for n being Nat
for b3 being strict VectSpStr over F holds
( b3 = n -VectSp_over F iff ( addLoopStr(# the carrier of b3, the addF of b3, the ZeroF of b3 #) = n -Group_over F & the lmult of b3 = n -Mult_over F ) );

registration
let F be Field;
let n be Nat;
clustern -VectSp_over F ->  non empty strict ;
coherence
 not n -VectSp_over F is empty
proofend;
end;

theorem Th10: :: PRVECT_1:10
for n being Nat
for D being non empty set
for H, G being BinOp of D
for d being Element of D
for t1, t2 being Element of n -tuples_on D st H is_distributive_wrt G holds
H [;] (d,(G .: (t1,t2))) = G .: ((H [;] (d,t1)),(H [;] (d,t2)))
proofend;

definition
let D be non empty set ;
let n be Nat;
let F be BinOp of D;
let x be Element of D;
let v be Element of n -tuples_on D;
:: original:[;]
redefine funcF [;] (x,v) ->  Element of n -tuples_on D;
coherence
 F [;] (x,v) is Element of n -tuples_on D by FINSEQ_2:121;
end;

registration
let F be Field;
let n be Nat;
clustern -VectSp_over F ->  strict vector-distributive scalar-distributive scalar-associative scalar-unital ;
coherence
 ( n -VectSp_over F is vector-distributive & n -VectSp_over F is scalar-distributive & n -VectSp_over F is scalar-associative & n -VectSp_over F is scalar-unital )
proofend;
end;

begin

definition
mode Domain-Sequence is non-empty non empty FinSequence;
end;

scheme :: PRVECT_1:sch 1
NEFinSeqLambda{ F1() ->  non empty FinSequence, F2( set ) ->  set } :
 ex p being non empty FinSequence st
( len p = len F1() & ( for i being Element of dom F1() holds p . i = F2(i) ) )
proofend;

definition
let a be non-empty non empty Function;
let f be Element of product a;
let i be Element of dom a;
:: original:.
redefine funcf . i ->  Element of a . i;
coherence
 f . i is Element of a . i by CARD_3:9;
end;

begin

definition
let a be non-empty non empty Function;
mode BinOps of a ->  Function means :Def6: :: PRVECT_1:def 6
( dom it = dom a & ( for i being Element of dom a holds it . i is BinOp of (a . i) ) );
existence
 ex b1 being Function st
( dom b1 = dom a & ( for i being Element of dom a holds b1 . i is BinOp of (a . i) ) )
proofend;
mode UnOps of a ->  Function means :Def7: :: PRVECT_1:def 7
( dom it = dom a & ( for i being Element of dom a holds it . i is UnOp of (a . i) ) );
existence
 ex b1 being Function st
( dom b1 = dom a & ( for i being Element of dom a holds b1 . i is UnOp of (a . i) ) )
proofend;
end;

:: deftheorem Def6 defines BinOps PRVECT_1:def_6_:_
 for a being non-empty non empty Function
for b2 being Function holds
( b2 is BinOps of a iff ( dom b2 = dom a & ( for i being Element of dom a holds b2 . i is BinOp of (a . i) ) ) );

:: deftheorem Def7 defines UnOps PRVECT_1:def_7_:_
 for a being non-empty non empty Function
for b2 being Function holds
( b2 is UnOps of a iff ( dom b2 = dom a & ( for i being Element of dom a holds b2 . i is UnOp of (a . i) ) ) );

registration
let a be Domain-Sequence;
cluster  ->  FinSequence-like for BinOps of a;
coherence
 for b1 being BinOps of a holds b1 is FinSequence-like
proofend;
cluster  ->  FinSequence-like for UnOps of a;
coherence
 for b1 being UnOps of a holds b1 is FinSequence-like
proofend;
end;

theorem Th11: :: PRVECT_1:11
for a being Domain-Sequence
for p being FinSequence holds
( p is BinOps of a iff ( len p = len a & ( for i being Element of dom a holds p . i is BinOp of (a . i) ) ) )
proofend;

theorem Th12: :: PRVECT_1:12
for a being Domain-Sequence
for p being FinSequence holds
( p is UnOps of a iff ( len p = len a & ( for i being Element of dom a holds p . i is UnOp of (a . i) ) ) )
proofend;

definition
let a be Domain-Sequence;
let b be BinOps of a;
let i be Element of dom a;
:: original:.
redefine funcb . i ->  BinOp of (a . i);
coherence
 b . i is BinOp of (a . i) by Th11;
end;

definition
let a be Domain-Sequence;
let u be UnOps of a;
let i be Element of dom a;
:: original:.
redefine funcu . i ->  UnOp of (a . i);
coherence
 u . i is UnOp of (a . i) by Th12;
end;

theorem :: PRVECT_1:13
for a being Domain-Sequence
for d, d9 being UnOp of (product a) st ( for f being Element of product a
for i being Element of dom a holds (d . f) . i = (d9 . f) . i ) holds
d = d9
proofend;

theorem Th14: :: PRVECT_1:14
for a being Domain-Sequence
for u being UnOps of a holds
( doms u = a & product (rngs u) c= product a )
proofend;

definition
let a be Domain-Sequence;
let u be UnOps of a;
:: original:Frege
redefine func Frege u ->  UnOp of (product a);
coherence
 Frege u is UnOp of (product a)
proofend;
end;

theorem Th15: :: PRVECT_1:15
for a being Domain-Sequence
for u being UnOps of a
for f being Element of product a
for i being Element of dom a holds ((Frege u) . f) . i = (u . i) . (f . i)
proofend;

definition
let F be functional non empty set ;
let b be BinOp of F;
let f, g be Element of F;
:: original:.
redefine funcb . (f,g) ->  Element of F;
coherence
 b . (f,g) is Element of F
proofend;
end;

theorem Th16: :: PRVECT_1:16
for a being Domain-Sequence
for d, d9 being BinOp of (product a) st ( for f, g being Element of product a
for i being Element of dom a holds (d . (f,g)) . i = (d9 . (f,g)) . i ) holds
d = d9
proofend;

definition
let a be Domain-Sequence;
let b be BinOps of a;
func[:b:] ->  BinOp of (product a) means :Def8: :: PRVECT_1:def 8
 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))
proofend;
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
proofend;
end;

:: deftheorem Def8 defines [: PRVECT_1:def_8_:_
 for a being Domain-Sequence
for b being BinOps of a
for b3 being BinOp of (product a) holds
( b3 = [:b:] iff for f, g being Element of product a
for i being Element of dom a holds (b3 . (f,g)) . i = (b . i) . ((f . i),(g . i)) );

theorem Th17: :: PRVECT_1:17
for a being Domain-Sequence
for b being BinOps of a st ( for i being Element of dom a holds b . i is commutative ) holds
[:b:] is commutative
proofend;

theorem Th18: :: PRVECT_1:18
for a being Domain-Sequence
for b being BinOps of a st ( for i being Element of dom a holds b . i is associative ) holds
[:b:] is associative
proofend;

theorem Th19: :: PRVECT_1:19
for a being Domain-Sequence
for b being BinOps of a
for f being Element of product a st ( for i being Element of dom a holds f . i is_a_unity_wrt b . i ) holds
f is_a_unity_wrt [:b:]
proofend;

theorem Th20: :: PRVECT_1:20
for a being Domain-Sequence
for b being BinOps of a
for u being UnOps of a st ( for i being Element of dom a holds
( u . i is_an_inverseOp_wrt b . i & b . i is having_a_unity ) ) holds
Frege u is_an_inverseOp_wrt [:b:]
proofend;

begin

definition
let F be Relation;
attrF is AbGroup-yielding  means :Def9: :: PRVECT_1:def 9
 for x being set st x in rng F holds
x is AbGroup;
end;

:: deftheorem Def9 defines AbGroup-yielding PRVECT_1:def_9_:_
 for F being Relation holds
( F is AbGroup-yielding iff for x being set st x in rng F holds
x is AbGroup );

registration
cluster Relation-like NAT -defined Function-like non empty V36() countable FinSequence-like FinSubsequence-like AbGroup-yielding for set ;
existence
 ex b1 being FinSequence st
( not b1 is empty & b1 is AbGroup-yielding )
proofend;
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;
:: original:.
redefine funcg . i ->  AbGroup;
coherence
 g . i is AbGroup
proofend;
end;

definition
let g be Group-Sequence;
func carr g ->  Domain-Sequence means :Def10: :: PRVECT_1:def 10
( len it = len g & ( for j being Element of dom g holds it . j = the carrier of (g . j) ) );
existence
 ex b1 being Domain-Sequence st
( len b1 = len g & ( for j being Element of dom g holds b1 . j = the carrier of (g . j) ) )
proofend;
uniqueness
 for b1, b2 being Domain-Sequence st len b1 = len g & ( for j being Element of dom g holds b1 . j = the carrier of (g . j) ) & len b2 = len g & ( for j being Element of dom g holds b2 . j = the carrier of (g . j) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def10 defines carr PRVECT_1:def_10_:_
 for g being Group-Sequence
for b2 being Domain-Sequence holds
( b2 = carr g iff ( len b2 = len g & ( for j being Element of dom g holds b2 . j = the carrier of (g . j) ) ) );

definition
let g be Group-Sequence;
let i be Element of dom (carr g);
:: original:.
redefine funcg . i ->  AbGroup;
coherence
 g . i is AbGroup
proofend;
end;

definition
let g be Group-Sequence;
func addop g ->  BinOps of carr g means :Def11: :: PRVECT_1:def 11
( len it = len (carr g) & ( for i being Element of dom (carr g) holds it . i = the addF of (g . i) ) );
existence
 ex b1 being BinOps of carr g st
( len b1 = len (carr g) & ( for i being Element of dom (carr g) holds b1 . i = the addF of (g . i) ) )
proofend;
uniqueness
 for b1, b2 being BinOps of carr g st len b1 = len (carr g) & ( for i being Element of dom (carr g) holds b1 . i = the addF of (g . i) ) & len b2 = len (carr g) & ( for i being Element of dom (carr g) holds b2 . i = the addF of (g . i) ) holds
b1 = b2
proofend;
func complop g ->  UnOps of carr g means :Def12: :: PRVECT_1:def 12
( len it = len (carr g) & ( for i being Element of dom (carr g) holds it . i = comp (g . i) ) );
existence
 ex b1 being UnOps of carr g st
( len b1 = len (carr g) & ( for i being Element of dom (carr g) holds b1 . i = comp (g . i) ) )
proofend;
uniqueness
 for b1, b2 being UnOps of carr g st len b1 = len (carr g) & ( for i being Element of dom (carr g) holds b1 . i = comp (g . i) ) & len b2 = len (carr g) & ( for i being Element of dom (carr g) holds b2 . i = comp (g . i) ) holds
b1 = b2
proofend;
func zeros g ->  Element of product (carr g) means :Def13: :: PRVECT_1:def 13
 for i being Element of dom (carr g) holds it . i = 0. (g . i);
existence
 ex b1 being Element of product (carr g) st
for i being Element of dom (carr g) holds b1 . i = 0. (g . i)
proofend;
uniqueness
 for b1, b2 being Element of product (carr g) st ( for i being Element of dom (carr g) holds b1 . i = 0. (g . i) ) & ( for i being Element of dom (carr g) holds b2 . i = 0. (g . i) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def11 defines addop PRVECT_1:def_11_:_
 for g being Group-Sequence
for b2 being BinOps of carr g holds
( b2 = addop g iff ( len b2 = len (carr g) & ( for i being Element of dom (carr g) holds b2 . i = the addF of (g . i) ) ) );

:: deftheorem Def12 defines complop PRVECT_1:def_12_:_
 for g being Group-Sequence
for b2 being UnOps of carr g holds
( b2 = complop g iff ( len b2 = len (carr g) & ( for i being Element of dom (carr g) holds b2 . i = comp (g . i) ) ) );

:: deftheorem Def13 defines zeros PRVECT_1:def_13_:_
 for g being Group-Sequence
for b2 being Element of product (carr g) holds
( b2 = zeros g iff for i being Element of dom (carr g) holds b2 . i = 0. (g . i) );

definition
let G be Group-Sequence;
func product G ->  strict AbGroup equals :: PRVECT_1:def 14
 addLoopStr(# (product (carr G)),[:(addop G):],(zeros G) #);
coherence
 addLoopStr(# (product (carr G)),[:(addop G):],(zeros G) #) is strict AbGroup
proofend;
end;

:: deftheorem  defines product PRVECT_1:def_14_:_
 for G being Group-Sequence holds product G = addLoopStr(# (product (carr G)),[:(addop G):],(zeros G) #);