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

begin

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

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

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

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

theorem :: PRVECT_1:1

canceled;

theorem :: PRVECT_1:2

canceled;

theorem Th3: :: PRVECT_1:3

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 Th4: :: PRVECT_1:4

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

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 )

proof end;

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

proof end;

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

proof end;

theorem :: PRVECT_1:6

canceled;

theorem :: PRVECT_1:7

canceled;

theorem :: PRVECT_1:8

canceled;

theorem :: PRVECT_1:9

canceled;

theorem :: PRVECT_1:10

for F being Field holds 0. F is_a_unity_wrt the addF of F

proof end;

theorem Th11: :: PRVECT_1:11

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;

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 func F .: (x,y) -> Element of n -tuples_on D;
coherence
F .: (x,y) is Element of n -tuples_on D by FINSEQ_2:140;

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 b₁ being BinOp of (n -tuples_on D) st
for x, y being Element of n -tuples_on D holds b₁ . (x,y) = F .: (x,y)

proof end;

uniqueness
for b₁, b₂ being BinOp of (n -tuples_on D) st ( for x, y being Element of n -tuples_on D holds b₁ . (x,y) = F .: (x,y) ) & ( for x, y being Element of n -tuples_on D holds b₂ . (x,y) = F .: (x,y) ) holds
b₁ = b₂

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 b₄ being BinOp of (n -tuples_on D) holds
( b₄ = product (F,n) iff for x, y being Element of n -tuples_on D holds b₄ . (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 b₁ being UnOp of (n -tuples_on D) st
for x being Element of n -tuples_on D holds b₁ . x = F * x

proof end;

uniqueness
for b₁, b₂ being UnOp of (n -tuples_on D) st ( for x being Element of n -tuples_on D holds b₁ . x = F * x ) & ( for x being Element of n -tuples_on D holds b₂ . x = F * x ) holds
b₁ = b₂

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 b₄ being UnOp of (n -tuples_on D) holds
( b₄ = product (F,n) iff for x being Element of n -tuples_on D holds b₄ . x = F * x );

definition

let D be non empty set ;
let n be Nat;
let x be Element of D;
:: original: |->
redefine func n |-> x -> Element of n -tuples_on D;
correctness
coherence
n |-> x is Element of n -tuples_on D;
by FINSEQ_2:132;

end;

theorem :: PRVECT_1:12

canceled;

theorem :: PRVECT_1:13

canceled;

theorem Th14: :: PRVECT_1:14

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 Th15: :: PRVECT_1:15

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 Th16: :: PRVECT_1:16

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 Th17: :: PRVECT_1:17

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;

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 ) ;
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 b₁ 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 b₁ . (x,v) = the multF of F [;] (x,v)

proof end;

uniqueness
for b₁, b₂ 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 b₁ . (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 b₂ . (x,v) = the multF of F [;] (x,v) ) holds
b₁ = b₂

proof end;

end;

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

definition

let F be Field;
let n be Nat;
func n -VectSp_over F -> strict VectSpStr of 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 b₁ being strict VectSpStr of F st
( addLoopStr(# the carrier of b₁, the addF of b₁, the ZeroF of b₁ #) = n -Group_over F & the lmult of b₁ = n -Mult_over F )

proof end;

uniqueness
for b₁, b₂ being strict VectSpStr of F st addLoopStr(# the carrier of b₁, the addF of b₁, the ZeroF of b₁ #) = n -Group_over F & the lmult of b₁ = n -Mult_over F & addLoopStr(# the carrier of b₂, the addF of b₂, the ZeroF of b₂ #) = n -Group_over F & the lmult of b₂ = n -Mult_over F holds
b₁ = b₂ ;

end;

:: deftheorem Def5 defines -VectSp_over PRVECT_1:def 5 :
for F being Field
for n being Nat
for b₃ being strict VectSpStr of F holds
( b₃ = n -VectSp_over F iff ( addLoopStr(# the carrier of b₃, the addF of b₃, the ZeroF of b₃ #) = n -Group_over F & the lmult of b₃ = 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 Th18: :: PRVECT_1:18

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

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;

begin

definition

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

end;

scheme :: PRVECT_1:sch 1
NEFinSeqLambda{ F₁() -> non empty FinSequence, F₂( set ) -> set } :

ex p being non empty FinSequence st
( len p = len F₁() & ( for i being Element of dom F₁() holds p . i = F₂(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:18;

end;

begin

definition

let a be non-empty non empty Function;
canceled;
canceled;
mode BinOps of a -> Function means :Def8: :: PRVECT_1:def 8
( dom it = dom a & ( for i being Element of dom a holds it . i is BinOp of (a . i) ) );
existence
ex b₁ being Function st
( dom b₁ = dom a & ( for i being Element of dom a holds b₁ . i is BinOp of (a . i) ) )

proof end;

mode UnOps of a -> Function means :Def9: :: PRVECT_1:def 9
( dom it = dom a & ( for i being Element of dom a holds it . i is UnOp of (a . i) ) );
existence
ex b₁ being Function st
( dom b₁ = dom a & ( for i being Element of dom a holds b₁ . i is UnOp of (a . i) ) )

proof end;

end;

:: deftheorem PRVECT_1:def 6 :
canceled;

:: deftheorem PRVECT_1:def 7 :
canceled;

:: deftheorem Def8 defines BinOps PRVECT_1:def 8 :
for a being non-empty non empty Function
for b₂ being Function holds
( b₂ is BinOps of a iff ( dom b₂ = dom a & ( for i being Element of dom a holds b₂ . i is BinOp of (a . i) ) ) );

:: deftheorem Def9 defines UnOps PRVECT_1:def 9 :
for a being non-empty non empty Function
for b₂ being Function holds
( b₂ is UnOps of a iff ( dom b₂ = dom a & ( for i being Element of dom a holds b₂ . i is UnOp of (a . i) ) ) );

registration

let a be Domain-Sequence;
cluster -> FinSequence-like BinOps of a;
coherence
for b₁ being BinOps of a holds b₁ is FinSequence-like

proof end;

cluster -> FinSequence-like UnOps of a;
coherence
for b₁ being UnOps of a holds b₁ is FinSequence-like

proof end;

end;

theorem Th19: :: PRVECT_1:19

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 Th20: :: PRVECT_1:20

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

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

end;

theorem :: PRVECT_1:21

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 Th22: :: PRVECT_1:22

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 Th23: :: PRVECT_1:23

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;

definition

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

proof end;

end;

theorem Th24: :: PRVECT_1:24

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 :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 b₁ being BinOp of (product a) st
for f, g being Element of product a
for i being Element of dom a holds (b₁ . (f,g)) . i = (b . i) . ((f . i),(g . i))

proof end;

uniqueness
for b₁, b₂ being BinOp of (product a) st ( for f, g being Element of product a
for i being Element of dom a holds (b₁ . (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 (b₂ . (f,g)) . i = (b . i) . ((f . i),(g . i)) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def10 defines [: PRVECT_1:def 10 :
for a being Domain-Sequence
for b being BinOps of a
for b₃ being BinOp of (product a) holds
( b₃ = [:b:] iff for f, g being Element of product a
for i being Element of dom a holds (b₃ . (f,g)) . i = (b . i) . ((f . i),(g . i)) );

theorem Th25: :: PRVECT_1:25

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 Th26: :: PRVECT_1:26

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 Th27: :: PRVECT_1:27

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 Th28: :: PRVECT_1:28

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;

begin

definition

let F be Relation;
attr F is AbGroup-yielding means :Def11: :: PRVECT_1:def 11
for x being set st x in rng F holds
x is AbGroup;

end;

:: deftheorem Def11 defines AbGroup-yielding PRVECT_1:def 11 :
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 Function-like non empty V33() countable FinSequence-like FinSubsequence-like AbGroup-yielding set ;
existence
ex b₁ being FinSequence st
( not b₁ is empty & b₁ is AbGroup-yielding )

proof end;

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 func g . i -> AbGroup;
coherence
g . i is AbGroup

proof end;

end;

definition

let g be Group-Sequence;
func carr g -> Domain-Sequence means :Def12: :: PRVECT_1:def 12
( len it = len g & ( for j being Element of dom g holds it . j = the carrier of (g . j) ) );
existence
ex b₁ being Domain-Sequence st
( len b₁ = len g & ( for j being Element of dom g holds b₁ . j = the carrier of (g . j) ) )

proof end;

uniqueness
for b₁, b₂ being Domain-Sequence st len b₁ = len g & ( for j being Element of dom g holds b₁ . j = the carrier of (g . j) ) & len b₂ = len g & ( for j being Element of dom g holds b₂ . j = the carrier of (g . j) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def12 defines carr PRVECT_1:def 12 :
for g being Group-Sequence
for b₂ being Domain-Sequence holds
( b₂ = carr g iff ( len b₂ = len g & ( for j being Element of dom g holds b₂ . j = the carrier of (g . j) ) ) );

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 Group-Sequence;
func addop g -> BinOps of carr g means :Def13: :: PRVECT_1:def 13
( len it = len (carr g) & ( for i being Element of dom (carr g) holds it . i = the addF of (g . i) ) );
existence
ex b₁ being BinOps of carr g st
( len b₁ = len (carr g) & ( for i being Element of dom (carr g) holds b₁ . i = the addF of (g . i) ) )

proof end;

uniqueness
for b₁, b₂ being BinOps of carr g st len b₁ = len (carr g) & ( for i being Element of dom (carr g) holds b₁ . i = the addF of (g . i) ) & len b₂ = len (carr g) & ( for i being Element of dom (carr g) holds b₂ . i = the addF of (g . i) ) holds
b₁ = b₂

proof end;

func complop g -> UnOps of carr g means :Def14: :: PRVECT_1:def 14
( len it = len (carr g) & ( for i being Element of dom (carr g) holds it . i = comp (g . i) ) );
existence
ex b₁ being UnOps of carr g st
( len b₁ = len (carr g) & ( for i being Element of dom (carr g) holds b₁ . i = comp (g . i) ) )

proof end;

uniqueness
for b₁, b₂ being UnOps of carr g st len b₁ = len (carr g) & ( for i being Element of dom (carr g) holds b₁ . i = comp (g . i) ) & len b₂ = len (carr g) & ( for i being Element of dom (carr g) holds b₂ . i = comp (g . i) ) holds
b₁ = b₂

proof end;

func zeros g -> Element of product (carr g) means :Def15: :: PRVECT_1:def 15
for i being Element of dom (carr g) holds it . i = 0. (g . i);
existence
ex b₁ being Element of product (carr g) st
for i being Element of dom (carr g) holds b₁ . i = 0. (g . i)

proof end;

uniqueness
for b₁, b₂ being Element of product (carr g) st ( for i being Element of dom (carr g) holds b₁ . i = 0. (g . i) ) & ( for i being Element of dom (carr g) holds b₂ . i = 0. (g . i) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def13 defines addop PRVECT_1:def 13 :
for g being Group-Sequence
for b₂ being BinOps of carr g holds
( b₂ = addop g iff ( len b₂ = len (carr g) & ( for i being Element of dom (carr g) holds b₂ . i = the addF of (g . i) ) ) );

:: deftheorem Def14 defines complop PRVECT_1:def 14 :
for g being Group-Sequence
for b₂ being UnOps of carr g holds
( b₂ = complop g iff ( len b₂ = len (carr g) & ( for i being Element of dom (carr g) holds b₂ . i = comp (g . i) ) ) );

:: deftheorem Def15 defines zeros PRVECT_1:def 15 :
for g being Group-Sequence
for b₂ being Element of product (carr g) holds
( b₂ = zeros g iff for i being Element of dom (carr g) holds b₂ . i = 0. (g . i) );

definition

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

proof end;

end;

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