:: by Yuichi Futa and Yasunari Shidama

::

:: Received August 30, 2017

:: Copyright (c) 2017-2018 Association of Mizar Users

theorem :: VECTSP12:1

for K being Field

for V, W being finite-dimensional VectSp of K

for A being Subset of V

for B being Basis of V

for T being linear-transformation of V,W

for l being Linear_Combination of B \ A st A is Basis of (ker T) & A c= B holds

T . (Sum l) = Sum (T @* l)

for V, W being finite-dimensional VectSp of K

for A being Subset of V

for B being Basis of V

for T being linear-transformation of V,W

for l being Linear_Combination of B \ A st A is Basis of (ker T) & A c= B holds

T . (Sum l) = Sum (T @* l)

proof end;

HM11: for F being Field

for X, Y being VectSp of F

for T being linear-transformation of X,Y

for A being Subset of X st T is bijective & A is Basis of X holds

T .: A is Basis of Y

proof end;

theorem HM12: :: VECTSP12:2

for F being Field

for X, Y being VectSp of F

for T being linear-transformation of X,Y

for A being Subset of X st T is bijective holds

( A is Basis of X iff T .: A is Basis of Y )

for X, Y being VectSp of F

for T being linear-transformation of X,Y

for A being Subset of X st T is bijective holds

( A is Basis of X iff T .: A is Basis of Y )

proof end;

HM13: for F being Field

for X, Y being VectSp of F

for T being linear-transformation of X,Y st T is bijective & X is finite-dimensional holds

Y is finite-dimensional

proof end;

theorem HM151: :: VECTSP12:3

for F being Field

for X, Y being VectSp of F

for T being linear-transformation of X,Y st T is bijective holds

( X is finite-dimensional iff Y is finite-dimensional )

for X, Y being VectSp of F

for T being linear-transformation of X,Y st T is bijective holds

( X is finite-dimensional iff Y is finite-dimensional )

proof end;

theorem HM15: :: VECTSP12:4

for F being Field

for X being finite-dimensional VectSp of F

for Y being VectSp of F

for T being linear-transformation of X,Y st T is bijective holds

( Y is finite-dimensional & dim X = dim Y )

for X being finite-dimensional VectSp of F

for Y being VectSp of F

for T being linear-transformation of X,Y st T is bijective holds

( Y is finite-dimensional & dim X = dim Y )

proof end;

theorem :: VECTSP12:5

for F being Field

for X, Y being VectSp of F

for l being Linear_Combination of X

for T being linear-transformation of X,Y st T is one-to-one holds

T @ l = T @* l

for X, Y being VectSp of F

for l being Linear_Combination of X

for T being linear-transformation of X,Y st T is one-to-one holds

T @ l = T @* l

proof end;

theorem FRds1: :: VECTSP12:6

for K being Field

for V being VectSp of K

for W1, W2 being Subspace of V

for I1 being Basis of W1

for I2 being Basis of W2 st V is_the_direct_sum_of W1,W2 holds

I1 /\ I2 = {}

for V being VectSp of K

for W1, W2 being Subspace of V

for I1 being Basis of W1

for I2 being Basis of W2 st V is_the_direct_sum_of W1,W2 holds

I1 /\ I2 = {}

proof end;

theorem FRds2: :: VECTSP12:7

for K being Field

for V being VectSp of K

for W1, W2 being Subspace of V

for I1 being Basis of W1

for I2 being Basis of W2

for I being Subset of V st V is_the_direct_sum_of W1,W2 & I = I1 \/ I2 holds

Lin I = ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #)

for V being VectSp of K

for W1, W2 being Subspace of V

for I1 being Basis of W1

for I2 being Basis of W2

for I being Subset of V st V is_the_direct_sum_of W1,W2 & I = I1 \/ I2 holds

Lin I = ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #)

proof end;

theorem FRds3: :: VECTSP12:8

for K being Field

for V being VectSp of K

for W1, W2 being Subspace of V

for I1 being Basis of W1

for I2 being Basis of W2

for I being Subset of V st V is_the_direct_sum_of W1,W2 & I = I1 \/ I2 holds

I is linearly-independent

for V being VectSp of K

for W1, W2 being Subspace of V

for I1 being Basis of W1

for I2 being Basis of W2

for I being Subset of V st V is_the_direct_sum_of W1,W2 & I = I1 \/ I2 holds

I is linearly-independent

proof end;

theorem :: VECTSP12:9

for K being Field

for V being VectSp of K

for W1, W2 being Subspace of V

for I1 being Basis of W1

for I2 being Basis of W2 st W1 /\ W2 = (0). V holds

I1 \/ I2 is Basis of (W1 + W2)

for V being VectSp of K

for W1, W2 being Subspace of V

for I1 being Basis of W1

for I2 being Basis of W2 st W1 /\ W2 = (0). V holds

I1 \/ I2 is Basis of (W1 + W2)

proof end;

theorem Th38A: :: VECTSP12:10

for K being Field

for V being finite-dimensional VectSp of K

for W being Subspace of V ex S being Linear_Compl of W ex T being linear-transformation of S,(VectQuot (V,W)) st

( T is bijective & ( for v being Vector of V st v in S holds

T . v = v + W ) )

for V being finite-dimensional VectSp of K

for W being Subspace of V ex S being Linear_Compl of W ex T being linear-transformation of S,(VectQuot (V,W)) st

( T is bijective & ( for v being Vector of V st v in S holds

T . v = v + W ) )

proof end;

theorem :: VECTSP12:11

for K being Field

for V being finite-dimensional VectSp of K

for W being Subspace of V holds

( VectQuot (V,W) is finite-dimensional & (dim (VectQuot (V,W))) + (dim W) = dim V )

for V being finite-dimensional VectSp of K

for W being Subspace of V holds

( VectQuot (V,W) is finite-dimensional & (dim (VectQuot (V,W))) + (dim W) = dim V )

proof end;

definition

let K be Ring;

let V, U be VectSp of K;

let W be Subspace of V;

let f be linear-transformation of V,U;

assume A1: the carrier of W c= the carrier of (ker f) ;

ex b_{1} being linear-transformation of (VectQuot (V,W)),U st

for A being Vector of (VectQuot (V,W))

for a being Vector of V st A = a + W holds

b_{1} . A = f . a

for b_{1}, b_{2} being linear-transformation of (VectQuot (V,W)),U st ( for A being Vector of (VectQuot (V,W))

for a being Vector of V st A = a + W holds

b_{1} . A = f . a ) & ( for A being Vector of (VectQuot (V,W))

for a being Vector of V st A = a + W holds

b_{2} . A = f . a ) holds

b_{1} = b_{2}

end;
let V, U be VectSp of K;

let W be Subspace of V;

let f be linear-transformation of V,U;

assume A1: the carrier of W c= the carrier of (ker f) ;

func QFunctional (f,W) -> linear-transformation of (VectQuot (V,W)),U means :Def12: :: VECTSP12:def 1

for A being Vector of (VectQuot (V,W))

for a being Vector of V st A = a + W holds

it . A = f . a;

existence for A being Vector of (VectQuot (V,W))

for a being Vector of V st A = a + W holds

it . A = f . a;

ex b

for A being Vector of (VectQuot (V,W))

for a being Vector of V st A = a + W holds

b

proof end;

uniqueness for b

for a being Vector of V st A = a + W holds

b

for a being Vector of V st A = a + W holds

b

b

proof end;

:: deftheorem Def12 defines QFunctional VECTSP12:def 1 :

for K being Ring

for V, U being VectSp of K

for W being Subspace of V

for f being linear-transformation of V,U st the carrier of W c= the carrier of (ker f) holds

for b_{6} being linear-transformation of (VectQuot (V,W)),U holds

( b_{6} = QFunctional (f,W) iff for A being Vector of (VectQuot (V,W))

for a being Vector of V st A = a + W holds

b_{6} . A = f . a );

for K being Ring

for V, U being VectSp of K

for W being Subspace of V

for f being linear-transformation of V,U st the carrier of W c= the carrier of (ker f) holds

for b

( b

for a being Vector of V st A = a + W holds

b

definition

let K be Ring;

let V, U be VectSp of K;

let f be linear-transformation of V,U;

QFunctional (f,(ker f)) is linear-transformation of (VectQuot (V,(ker f))),U ;

end;
let V, U be VectSp of K;

let f be linear-transformation of V,U;

func CQFunctional f -> linear-transformation of (VectQuot (V,(ker f))),U equals :: VECTSP12:def 2

QFunctional (f,(ker f));

coherence QFunctional (f,(ker f));

QFunctional (f,(ker f)) is linear-transformation of (VectQuot (V,(ker f))),U ;

:: deftheorem defines CQFunctional VECTSP12:def 2 :

for K being Ring

for V, U being VectSp of K

for f being linear-transformation of V,U holds CQFunctional f = QFunctional (f,(ker f));

for K being Ring

for V, U being VectSp of K

for f being linear-transformation of V,U holds CQFunctional f = QFunctional (f,(ker f));

registration

let K be Ring;

let V, U be VectSp of K;

let f be linear-transformation of V,U;

coherence

CQFunctional f is one-to-one

end;
let V, U be VectSp of K;

let f be linear-transformation of V,U;

coherence

CQFunctional f is one-to-one

proof end;

:: 1st isomorphism theorem

theorem :: VECTSP12:12

for K being Ring

for V, U being VectSp of K

for f being linear-transformation of V,U ex T being linear-transformation of (VectQuot (V,(ker f))),(im f) st

( T = CQFunctional f & T is bijective )

for V, U being VectSp of K

for f being linear-transformation of V,U ex T being linear-transformation of (VectQuot (V,(ker f))),(im f) st

( T = CQFunctional f & T is bijective )

proof end;

definition

let K be Ring;

let V, U, W be VectSp of K;

let f be linear-transformation of V,U;

let g be linear-transformation of U,W;

:: original: (#)

redefine func g * f -> linear-transformation of V,W;

correctness

coherence

f (#) g is linear-transformation of V,W;

end;
let V, U, W be VectSp of K;

let f be linear-transformation of V,U;

let g be linear-transformation of U,W;

:: original: (#)

redefine func g * f -> linear-transformation of V,W;

correctness

coherence

f (#) g is linear-transformation of V,W;

proof end;

definition

let K be Ring;

ex b_{1} being non empty FinSequence st

for S being set st S in rng b_{1} holds

S is VectSp of K

end;
mode VectorSpace-Sequence of K -> non empty FinSequence means :Def3: :: VECTSP12:def 3

for S being set st S in rng it holds

S is VectSp of K;

existence for S being set st S in rng it holds

S is VectSp of K;

ex b

for S being set st S in rng b

S is VectSp of K

proof end;

:: deftheorem Def3 defines VectorSpace-Sequence VECTSP12:def 3 :

for K being Ring

for b_{2} being non empty FinSequence holds

( b_{2} is VectorSpace-Sequence of K iff for S being set st S in rng b_{2} holds

S is VectSp of K );

for K being Ring

for b

( b

S is VectSp of K );

registration

let K be Ring;

coherence

for b_{1} being VectorSpace-Sequence of K holds b_{1} is AbGroup-yielding

end;
coherence

for b

proof end;

definition

let K be Ring;

let G be VectorSpace-Sequence of K;

let j be Element of dom G;

:: original: .

redefine func G . j -> VectSp of K;

coherence

G . j is VectSp of K

end;
let G be VectorSpace-Sequence of K;

let j be Element of dom G;

:: original: .

redefine func G . j -> VectSp of K;

coherence

G . j is VectSp of K

proof end;

definition

let K be Ring;

let G be VectorSpace-Sequence of K;

let j be Element of dom (carr G);

:: original: .

redefine func G . j -> VectSp of K;

coherence

G . j is VectSp of K

end;
let G be VectorSpace-Sequence of K;

let j be Element of dom (carr G);

:: original: .

redefine func G . j -> VectSp of K;

coherence

G . j is VectSp of K

proof end;

definition

let K be Ring;

let G be VectorSpace-Sequence of K;

ex b_{1} being MultOps of the carrier of K, carr G st

( len b_{1} = len (carr G) & ( for j being Element of dom (carr G) holds b_{1} . j = the lmult of (G . j) ) )

for b_{1}, b_{2} being MultOps of the carrier of K, carr G st len b_{1} = len (carr G) & ( for j being Element of dom (carr G) holds b_{1} . j = the lmult of (G . j) ) & len b_{2} = len (carr G) & ( for j being Element of dom (carr G) holds b_{2} . j = the lmult of (G . j) ) holds

b_{1} = b_{2}

end;
let G be VectorSpace-Sequence of K;

func multop G -> MultOps of the carrier of K, carr G means :Def8: :: VECTSP12:def 4

( len it = len (carr G) & ( for j being Element of dom (carr G) holds it . j = the lmult of (G . j) ) );

existence ( len it = len (carr G) & ( for j being Element of dom (carr G) holds it . j = the lmult of (G . j) ) );

ex b

( len b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def8 defines multop VECTSP12:def 4 :

for K being Ring

for G being VectorSpace-Sequence of K

for b_{3} being MultOps of the carrier of K, carr G holds

( b_{3} = multop G iff ( len b_{3} = len (carr G) & ( for j being Element of dom (carr G) holds b_{3} . j = the lmult of (G . j) ) ) );

for K being Ring

for G being VectorSpace-Sequence of K

for b

( b

definition

let K be Ring;

let G be VectorSpace-Sequence of K;

ModuleStr(# (product (carr G)),[:(addop G):],(zeros G),[:(multop G):] #) is non empty strict ModuleStr over K ;

end;
let G be VectorSpace-Sequence of K;

func product G -> non empty strict ModuleStr over K equals :: VECTSP12:def 5

ModuleStr(# (product (carr G)),[:(addop G):],(zeros G),[:(multop G):] #);

coherence ModuleStr(# (product (carr G)),[:(addop G):],(zeros G),[:(multop G):] #);

ModuleStr(# (product (carr G)),[:(addop G):],(zeros G),[:(multop G):] #) is non empty strict ModuleStr over K ;

:: deftheorem defines product VECTSP12:def 5 :

for K being Ring

for G being VectorSpace-Sequence of K holds product G = ModuleStr(# (product (carr G)),[:(addop G):],(zeros G),[:(multop G):] #);

for K being Ring

for G being VectorSpace-Sequence of K holds product G = ModuleStr(# (product (carr G)),[:(addop G):],(zeros G),[:(multop G):] #);

Lm3: for K being Ring

for G being VectorSpace-Sequence of K

for v1, w1 being Element of product (carr G)

for i being Element of dom (carr G) holds

( ([:(addop G):] . (v1,w1)) . i = the addF of (G . i) . ((v1 . i),(w1 . i)) & ( for vi, wi being Vector of (G . i) st vi = v1 . i & wi = w1 . i holds

([:(addop G):] . (v1,w1)) . i = vi + wi ) )

proof end;

Lm4: for K being Ring

for G being VectorSpace-Sequence of K

for r being Element of K

for v being Element of product (carr G)

for i being Element of dom (carr G) holds

( ([:(multop G):] . (r,v)) . i = the lmult of (G . i) . (r,(v . i)) & ( for vi being Vector of (G . i) st vi = v . i holds

([:(multop G):] . (r,v)) . i = r * vi ) )

proof end;

Lm5: for K being Ring

for G being VectorSpace-Sequence of K holds

( product G is vector-distributive & product G is scalar-distributive & product G is scalar-associative & product G is scalar-unital )

proof end;

registration

let K be Ring;

let G be VectorSpace-Sequence of K;

( product G is Abelian & product G is add-associative & product G is right_zeroed & product G is right_complementable & product G is vector-distributive & product G is scalar-distributive & product G is scalar-associative & product G is scalar-unital )

end;
let G be VectorSpace-Sequence of K;

cluster product G -> non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital ;

coherence ( product G is Abelian & product G is add-associative & product G is right_zeroed & product G is right_complementable & product G is vector-distributive & product G is scalar-distributive & product G is scalar-associative & product G is scalar-unital )

proof end;

definition

let K be Ring;

let G, F be non empty ModuleStr over K;

ex b_{1} being Function of [: the carrier of K,[: the carrier of G, the carrier of F:]:],[: the carrier of G, the carrier of F:] st

for r being Element of K

for g being Vector of G

for f being Vector of F holds b_{1} . (r,[g,f]) = [(r * g),(r * f)]

for b_{1}, b_{2} being Function of [: the carrier of K,[: the carrier of G, the carrier of F:]:],[: the carrier of G, the carrier of F:] st ( for r being Element of K

for g being Vector of G

for f being Vector of F holds b_{1} . (r,[g,f]) = [(r * g),(r * f)] ) & ( for r being Element of K

for g being Vector of G

for f being Vector of F holds b_{2} . (r,[g,f]) = [(r * g),(r * f)] ) holds

b_{1} = b_{2}

end;
let G, F be non empty ModuleStr over K;

func prod_MLT (G,F) -> Function of [: the carrier of K,[: the carrier of G, the carrier of F:]:],[: the carrier of G, the carrier of F:] means :YDef2: :: VECTSP12:def 6

for r being Element of K

for g being Vector of G

for f being Vector of F holds it . (r,[g,f]) = [(r * g),(r * f)];

existence for r being Element of K

for g being Vector of G

for f being Vector of F holds it . (r,[g,f]) = [(r * g),(r * f)];

ex b

for r being Element of K

for g being Vector of G

for f being Vector of F holds b

proof end;

uniqueness for b

for g being Vector of G

for f being Vector of F holds b

for g being Vector of G

for f being Vector of F holds b

b

proof end;

:: deftheorem YDef2 defines prod_MLT VECTSP12:def 6 :

for K being Ring

for G, F being non empty ModuleStr over K

for b_{4} being Function of [: the carrier of K,[: the carrier of G, the carrier of F:]:],[: the carrier of G, the carrier of F:] holds

( b_{4} = prod_MLT (G,F) iff for r being Element of K

for g being Vector of G

for f being Vector of F holds b_{4} . (r,[g,f]) = [(r * g),(r * f)] );

for K being Ring

for G, F being non empty ModuleStr over K

for b

( b

for g being Vector of G

for f being Vector of F holds b

definition

let K be Ring;

let G, F be non empty ModuleStr over K;

coherence

ModuleStr(# [: the carrier of G, the carrier of F:],(prod_ADD (G,F)),(prod_ZERO (G,F)),(prod_MLT (G,F)) #) is non empty strict ModuleStr over K;

end;
let G, F be non empty ModuleStr over K;

func [:G,F:] -> non empty strict ModuleStr over K equals :: VECTSP12:def 7

ModuleStr(# [: the carrier of G, the carrier of F:],(prod_ADD (G,F)),(prod_ZERO (G,F)),(prod_MLT (G,F)) #);

correctness ModuleStr(# [: the carrier of G, the carrier of F:],(prod_ADD (G,F)),(prod_ZERO (G,F)),(prod_MLT (G,F)) #);

coherence

ModuleStr(# [: the carrier of G, the carrier of F:],(prod_ADD (G,F)),(prod_ZERO (G,F)),(prod_MLT (G,F)) #) is non empty strict ModuleStr over K;

proof end;

:: deftheorem defines [: VECTSP12:def 7 :

for K being Ring

for G, F being non empty ModuleStr over K holds [:G,F:] = ModuleStr(# [: the carrier of G, the carrier of F:],(prod_ADD (G,F)),(prod_ZERO (G,F)),(prod_MLT (G,F)) #);

for K being Ring

for G, F being non empty ModuleStr over K holds [:G,F:] = ModuleStr(# [: the carrier of G, the carrier of F:],(prod_ADD (G,F)),(prod_ZERO (G,F)),(prod_MLT (G,F)) #);

registration

let K be Ring;

let G, F be non empty Abelian ModuleStr over K;

correctness

coherence

[:G,F:] is Abelian ;

end;
let G, F be non empty Abelian ModuleStr over K;

correctness

coherence

[:G,F:] is Abelian ;

proof end;

registration

let K be Ring;

let G, F be non empty add-associative ModuleStr over K;

correctness

coherence

[:G,F:] is add-associative ;

end;
let G, F be non empty add-associative ModuleStr over K;

correctness

coherence

[:G,F:] is add-associative ;

proof end;

registration

let K be Ring;

let G, F be non empty right_zeroed ModuleStr over K;

correctness

coherence

[:G,F:] is right_zeroed ;

end;
let G, F be non empty right_zeroed ModuleStr over K;

correctness

coherence

[:G,F:] is right_zeroed ;

proof end;

registration

let K be Ring;

let G, F be non empty right_complementable ModuleStr over K;

correctness

coherence

[:G,F:] is right_complementable ;

end;
let G, F be non empty right_complementable ModuleStr over K;

correctness

coherence

[:G,F:] is right_complementable ;

proof end;

theorem :: VECTSP12:13

for K being Ring

for G, F being non empty ModuleStr over K holds

( ( for x being set holds

( x is Vector of [:G,F:] iff ex x1 being Vector of G ex x2 being Vector of F st x = [x1,x2] ) ) & ( for x, y being Vector of [:G,F:]

for x1, y1 being Vector of G

for x2, y2 being Vector of F st x = [x1,x2] & y = [y1,y2] holds

x + y = [(x1 + y1),(x2 + y2)] ) & 0. [:G,F:] = [(0. G),(0. F)] & ( for x being Vector of [:G,F:]

for x1 being Vector of G

for x2 being Vector of F

for a being Element of K st x = [x1,x2] holds

a * x = [(a * x1),(a * x2)] ) ) by YDef2, PRVECT_3:def 1, SUBSET_1:43, ZFMISC_1:87;

for G, F being non empty ModuleStr over K holds

( ( for x being set holds

( x is Vector of [:G,F:] iff ex x1 being Vector of G ex x2 being Vector of F st x = [x1,x2] ) ) & ( for x, y being Vector of [:G,F:]

for x1, y1 being Vector of G

for x2, y2 being Vector of F st x = [x1,x2] & y = [y1,y2] holds

x + y = [(x1 + y1),(x2 + y2)] ) & 0. [:G,F:] = [(0. G),(0. F)] & ( for x being Vector of [:G,F:]

for x1 being Vector of G

for x2 being Vector of F

for a being Element of K st x = [x1,x2] holds

a * x = [(a * x1),(a * x2)] ) ) by YDef2, PRVECT_3:def 1, SUBSET_1:43, ZFMISC_1:87;

theorem :: VECTSP12:14

for K being Ring

for G, F being non empty right_complementable add-associative right_zeroed ModuleStr over K

for x being Vector of [:G,F:]

for x1 being Vector of G

for x2 being Vector of F st x = [x1,x2] holds

- x = [(- x1),(- x2)]

for G, F being non empty right_complementable add-associative right_zeroed ModuleStr over K

for x being Vector of [:G,F:]

for x1 being Vector of G

for x2 being Vector of F st x = [x1,x2] holds

- x = [(- x1),(- x2)]

proof end;

registration

let K be Ring;

let G, F be non empty vector-distributive ModuleStr over K;

correctness

coherence

[:G,F:] is vector-distributive ;

end;
let G, F be non empty vector-distributive ModuleStr over K;

correctness

coherence

[:G,F:] is vector-distributive ;

proof end;

registration

let K be Ring;

let G, F be non empty scalar-distributive ModuleStr over K;

correctness

coherence

[:G,F:] is scalar-distributive ;

end;
let G, F be non empty scalar-distributive ModuleStr over K;

correctness

coherence

[:G,F:] is scalar-distributive ;

proof end;

registration

let K be Ring;

let G, F be non empty scalar-associative ModuleStr over K;

correctness

coherence

[:G,F:] is scalar-associative ;

end;
let G, F be non empty scalar-associative ModuleStr over K;

correctness

coherence

[:G,F:] is scalar-associative ;

proof end;

registration

let K be Ring;

let G, F be non empty scalar-unital ModuleStr over K;

correctness

coherence

[:G,F:] is scalar-unital ;

end;
let G, F be non empty scalar-unital ModuleStr over K;

correctness

coherence

[:G,F:] is scalar-unital ;

proof end;

definition

let K be Ring;

let G be VectSp of K;

:: original: <*

redefine func <*G*> -> VectorSpace-Sequence of K;

correctness

coherence

<*G*> is VectorSpace-Sequence of K;

end;
let G be VectSp of K;

:: original: <*

redefine func <*G*> -> VectorSpace-Sequence of K;

correctness

coherence

<*G*> is VectorSpace-Sequence of K;

proof end;

definition

let K be Ring;

let G, F be VectSp of K;

:: original: <*

redefine func <*G,F*> -> VectorSpace-Sequence of K;

correctness

coherence

<*G,F*> is VectorSpace-Sequence of K;

end;
let G, F be VectSp of K;

:: original: <*

redefine func <*G,F*> -> VectorSpace-Sequence of K;

correctness

coherence

<*G,F*> is VectorSpace-Sequence of K;

proof end;

theorem :: VECTSP12:15

for K being Ring

for X being VectSp of K ex I being Function of X,(product <*X*>) st

( I is one-to-one & I is onto & ( for x being Vector of X holds I . x = <*x*> ) & ( for v, w being Vector of X holds I . (v + w) = (I . v) + (I . w) ) & ( for v being Vector of X

for r being Element of the carrier of K holds I . (r * v) = r * (I . v) ) & I . (0. X) = 0. (product <*X*>) )

for X being VectSp of K ex I being Function of X,(product <*X*>) st

( I is one-to-one & I is onto & ( for x being Vector of X holds I . x = <*x*> ) & ( for v, w being Vector of X holds I . (v + w) = (I . v) + (I . w) ) & ( for v being Vector of X

for r being Element of the carrier of K holds I . (r * v) = r * (I . v) ) & I . (0. X) = 0. (product <*X*>) )

proof end;

definition

let K be Ring;

let G, F be VectorSpace-Sequence of K;

:: original: ^

redefine func G ^ F -> VectorSpace-Sequence of K;

correctness

coherence

G ^ F is VectorSpace-Sequence of K;

end;
let G, F be VectorSpace-Sequence of K;

:: original: ^

redefine func G ^ F -> VectorSpace-Sequence of K;

correctness

coherence

G ^ F is VectorSpace-Sequence of K;

proof end;

theorem Th12: :: VECTSP12:16

for K being Ring

for X, Y being VectSp of K ex I being Function of [:X,Y:],(product <*X,Y*>) st

( I is one-to-one & I is onto & ( for x being Vector of X

for y being Vector of Y holds I . (x,y) = <*x,y*> ) & ( for v, w being Vector of [:X,Y:] holds I . (v + w) = (I . v) + (I . w) ) & ( for v being Vector of [:X,Y:]

for r being Element of K holds I . (r * v) = r * (I . v) ) & I . (0. [:X,Y:]) = 0. (product <*X,Y*>) )

for X, Y being VectSp of K ex I being Function of [:X,Y:],(product <*X,Y*>) st

( I is one-to-one & I is onto & ( for x being Vector of X

for y being Vector of Y holds I . (x,y) = <*x,y*> ) & ( for v, w being Vector of [:X,Y:] holds I . (v + w) = (I . v) + (I . w) ) & ( for v being Vector of [:X,Y:]

for r being Element of K holds I . (r * v) = r * (I . v) ) & I . (0. [:X,Y:]) = 0. (product <*X,Y*>) )

proof end;

theorem :: VECTSP12:17

for K being Ring

for X, Y being VectorSpace-Sequence of K ex I being Function of [:(product X),(product Y):],(product (X ^ Y)) st

( I is one-to-one & I is onto & ( for x being Vector of (product X)

for y being Vector of (product Y) ex x1, y1 being FinSequence st

( x = x1 & y = y1 & I . (x,y) = x1 ^ y1 ) ) & ( for v, w being Vector of [:(product X),(product Y):] holds I . (v + w) = (I . v) + (I . w) ) & ( for v being Vector of [:(product X),(product Y):]

for r being Element of the carrier of K holds I . (r * v) = r * (I . v) ) & I . (0. [:(product X),(product Y):]) = 0. (product (X ^ Y)) )

for X, Y being VectorSpace-Sequence of K ex I being Function of [:(product X),(product Y):],(product (X ^ Y)) st

( I is one-to-one & I is onto & ( for x being Vector of (product X)

for y being Vector of (product Y) ex x1, y1 being FinSequence st

( x = x1 & y = y1 & I . (x,y) = x1 ^ y1 ) ) & ( for v, w being Vector of [:(product X),(product Y):] holds I . (v + w) = (I . v) + (I . w) ) & ( for v being Vector of [:(product X),(product Y):]

for r being Element of the carrier of K holds I . (r * v) = r * (I . v) ) & I . (0. [:(product X),(product Y):]) = 0. (product (X ^ Y)) )

proof end;

theorem :: VECTSP12:18

for K being Ring

for G, F being VectSp of K holds

( ( for x being set holds

( x is Vector of (product <*G,F*>) iff ex x1 being Vector of G ex x2 being Vector of F st x = <*x1,x2*> ) ) & ( for x, y being Vector of (product <*G,F*>)

for x1, y1 being Vector of G

for x2, y2 being Vector of F st x = <*x1,x2*> & y = <*y1,y2*> holds

x + y = <*(x1 + y1),(x2 + y2)*> ) & 0. (product <*G,F*>) = <*(0. G),(0. F)*> & ( for x being Vector of (product <*G,F*>)

for x1 being Vector of G

for x2 being Vector of F st x = <*x1,x2*> holds

- x = <*(- x1),(- x2)*> ) & ( for x being Vector of (product <*G,F*>)

for x1 being Vector of G

for x2 being Vector of F

for a being Element of K st x = <*x1,x2*> holds

a * x = <*(a * x1),(a * x2)*> ) )

for G, F being VectSp of K holds

( ( for x being set holds

( x is Vector of (product <*G,F*>) iff ex x1 being Vector of G ex x2 being Vector of F st x = <*x1,x2*> ) ) & ( for x, y being Vector of (product <*G,F*>)

for x1, y1 being Vector of G

for x2, y2 being Vector of F st x = <*x1,x2*> & y = <*y1,y2*> holds

x + y = <*(x1 + y1),(x2 + y2)*> ) & 0. (product <*G,F*>) = <*(0. G),(0. F)*> & ( for x being Vector of (product <*G,F*>)

for x1 being Vector of G

for x2 being Vector of F st x = <*x1,x2*> holds

- x = <*(- x1),(- x2)*> ) & ( for x being Vector of (product <*G,F*>)

for x1 being Vector of G

for x2 being Vector of F

for a being Element of K st x = <*x1,x2*> holds

a * x = <*(a * x1),(a * x2)*> ) )

proof end;