:: 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


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
proof end;

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

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
proof end;

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
proof end;

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
by BINOP_1:3;

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

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

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

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

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 func F .: (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)
proof end;
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
proof end;
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
proof end;
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
proof end;
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
proof end;

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
proof end;

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)
proof end;

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)
proof end;

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 ) ;
func n -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
proof end;
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;
cluster n -Group_over F -> strict ;
coherence
not n -Group_over F is empty ;
end;

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)
proof end;
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
proof end;
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;
func n -VectSp_over F -> strict ModuleStr 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 ModuleStr 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 )
proof end;
uniqueness
for b1, b2 being strict ModuleStr 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 ModuleStr 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;
cluster n -VectSp_over F -> non empty strict ;
coherence
not n -VectSp_over F is empty
proof end;
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)))
proof end;

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 func F [;] (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;
cluster n -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 )
proof end;
end;

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) ) )
proof end;

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 func f . i -> Element of a . i;
coherence
f . i is Element of a . i by CARD_3:9;
end;

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) ) )
proof end;
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) ) )
proof end;
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
proof end;
cluster -> FinSequence-like for UnOps of a;
coherence
for b1 being UnOps of a holds b1 is FinSequence-like
proof end;
end;

registration
let a be Domain-Sequence;
cluster -> Function-yielding for BinOps of a;
coherence
for b1 being BinOps of a holds b1 is Function-yielding
proof end;
cluster -> Function-yielding for UnOps of a;
coherence
for b1 being UnOps of a holds b1 is Function-yielding
proof end;
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) ) ) )
proof end;

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) ) ) )
proof end;

definition
let a be Domain-Sequence;
let b be BinOps of a;
let i be Element of dom a;
:: original: .
redefine func b . 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 func u . 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
proof end;

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 )
proof end;

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)
proof end;
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)
proof 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
proof end;

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))
proof end;
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
proof end;
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
proof end;

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
proof end;

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:]
proof end;

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:]
proof end;

definition
let F be Relation;
::: by non-Empty addLoopStr-yielding
attr F is non-empty-addLoopStr-yielding means :DefAA: :: PRVECT_1:def 9
 for x being set st x in rng F holds
x is non empty addLoopStr ;
attr F is AbGroup-yielding means :Def9: :: PRVECT_1:def 10
 for x being set st x in rng F holds
x is AbGroup;
end;

:: deftheorem DefAA defines non-empty-addLoopStr-yielding PRVECT_1:def 9 :
for F being Relation holds
( F is non-empty-addLoopStr-yielding iff for x being set st x in rng F holds
x is non empty addLoopStr );

:: deftheorem Def9 defines AbGroup-yielding PRVECT_1:def 10 :
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 AbGroup-yielding -> non-empty-addLoopStr-yielding for set ;
coherence
for b1 being Relation st b1 is AbGroup-yielding holds
b1 is non-empty-addLoopStr-yielding ;
end;

registration
cluster Relation-like non-empty-addLoopStr-yielding -> 1-sorted-yielding non-Empty for set ;
coherence
for b1 being Relation st b1 is non-empty-addLoopStr-yielding holds
( b1 is non-Empty & b1 is 1-sorted-yielding )
proof end;
end;

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

definition
let g be Group-Sequence;
let i be Element of dom g;
:: original: .
redefine func g . i -> AbGroup;
coherence
g . i is AbGroup
proof end;
end;

notation
let g be non empty 1-sorted-yielding non-Empty FinSequence;
synonym carr g for Carrier g;
end;

registration
let f be 1-sorted-yielding FinSequence;
cluster carr f -> FinSequence-like ;
coherence
Carrier f is FinSequence-like
proof end;
end;

registration
let f be non empty 1-sorted-yielding Function;
cluster carr f -> non empty ;
coherence
not Carrier f is empty
proof end;
end;

registration
let f be 1-sorted-yielding non-Empty Function;
cluster carr f -> non-empty ;
coherence
Carrier f is non-empty
proof end;
end;

definition
let g be non empty 1-sorted-yielding non-Empty FinSequence;
:: original: carr
redefine func carr g -> Domain-Sequence means :Def10: :: PRVECT_1:def 11
( len it = len g & ( for j being Element of dom g holds it . j = the carrier of (g . j) ) );
coherence
carr g is Domain-Sequence ;
compatibility
for b1 being Domain-Sequence holds
( b1 = carr g iff ( len b1 = len g & ( for j being Element of dom g holds b1 . j = the carrier of (g . j) ) ) )
proof end;
end;

:: deftheorem Def10 defines carr PRVECT_1:def 11 :
for g being non empty 1-sorted-yielding non-Empty FinSequence
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 non empty non-empty-addLoopStr-yielding FinSequence;
let i be Element of dom (carr g);
:: original: .
redefine func g . i -> non empty addLoopStr ;
coherence
g . i is non empty addLoopStr
proof end;
end;

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

definition
let g be non empty non-empty-addLoopStr-yielding FinSequence;
func addop g -> BinOps of carr g means :Def11: :: 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) ) );
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) ) )
proof end;
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
proof end;
end;

:: deftheorem Def11 defines addop PRVECT_1:def 12 :
for g being non empty non-empty-addLoopStr-yielding FinSequence
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) ) ) );

definition
let g be non empty non-empty-addLoopStr-yielding FinSequence;
func complop g -> UnOps of carr g means :Def12: :: PRVECT_1:def 13
( 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) ) )
proof end;
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
proof end;
func zeros g -> Element of product (carr g) means :Def13: :: PRVECT_1:def 14
 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)
proof end;
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
proof end;
end;

:: deftheorem Def12 defines complop PRVECT_1:def 13 :
for g being non empty non-empty-addLoopStr-yielding FinSequence
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 14 :
for g being non empty non-empty-addLoopStr-yielding FinSequence
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 non empty non-empty-addLoopStr-yielding FinSequence;
func product G -> non empty strict addLoopStr equals :: PRVECT_1:def 15
 addLoopStr(# (product (carr G)),[:(addop G):],(zeros G) #);
coherence
addLoopStr(# (product (carr G)),[:(addop G):],(zeros G) #) is non empty strict addLoopStr ;
end;

:: deftheorem defines product PRVECT_1:def 15 :
for G being non empty non-empty-addLoopStr-yielding FinSequence holds product G = addLoopStr(# (product (carr G)),[:(addop G):],(zeros G) #);

registration
let G be Group-Sequence;
cluster product G -> non empty strict right_complementable Abelian add-associative right_zeroed ;
coherence
( product G is add-associative & product G is right_zeroed & product G is right_complementable & not product G is empty & product G is Abelian )
proof end;
end;