:: by Wojciech A. Trybulec

::

:: Received July 27, 1990

:: Copyright (c) 1990-2019 Association of Mizar Users

definition

let GF be non empty ZeroStr ;

let V be non empty ModuleStr over GF;

ex b_{1} being Element of Funcs ( the carrier of V, the carrier of GF) ex T being finite Subset of V st

for v being Element of V st not v in T holds

b_{1} . v = 0. GF

end;
let V be non empty ModuleStr over GF;

mode Linear_Combination of V -> Element of Funcs ( the carrier of V, the carrier of GF) means :Def1: :: VECTSP_6:def 1

ex T being finite Subset of V st

for v being Element of V st not v in T holds

it . v = 0. GF;

existence ex T being finite Subset of V st

for v being Element of V st not v in T holds

it . v = 0. GF;

ex b

for v being Element of V st not v in T holds

b

proof end;

:: deftheorem Def1 defines Linear_Combination VECTSP_6:def 1 :

for GF being non empty ZeroStr

for V being non empty ModuleStr over GF

for b_{3} being Element of Funcs ( the carrier of V, the carrier of GF) holds

( b_{3} is Linear_Combination of V iff ex T being finite Subset of V st

for v being Element of V st not v in T holds

b_{3} . v = 0. GF );

for GF being non empty ZeroStr

for V being non empty ModuleStr over GF

for b

( b

for v being Element of V st not v in T holds

b

definition

let GF be non empty ZeroStr ;

let V be non empty ModuleStr over GF;

let L be Linear_Combination of V;

{ v where v is Element of V : L . v <> 0. GF } is finite Subset of V

end;
let V be non empty ModuleStr over GF;

let L be Linear_Combination of V;

func Carrier L -> finite Subset of V equals :: VECTSP_6:def 2

{ v where v is Element of V : L . v <> 0. GF } ;

coherence { v where v is Element of V : L . v <> 0. GF } ;

{ v where v is Element of V : L . v <> 0. GF } is finite Subset of V

proof end;

:: deftheorem defines Carrier VECTSP_6:def 2 :

for GF being non empty ZeroStr

for V being non empty ModuleStr over GF

for L being Linear_Combination of V holds Carrier L = { v where v is Element of V : L . v <> 0. GF } ;

for GF being non empty ZeroStr

for V being non empty ModuleStr over GF

for L being Linear_Combination of V holds Carrier L = { v where v is Element of V : L . v <> 0. GF } ;

theorem :: VECTSP_6:1

for x being set

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for L being Linear_Combination of V holds

( x in Carrier L iff ex v being Element of V st

( x = v & L . v <> 0. GF ) ) ;

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for L being Linear_Combination of V holds

( x in Carrier L iff ex v being Element of V st

( x = v & L . v <> 0. GF ) ) ;

theorem :: VECTSP_6:2

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for v being Element of V

for L being Linear_Combination of V holds

( L . v = 0. GF iff not v in Carrier L )

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for v being Element of V

for L being Linear_Combination of V holds

( L . v = 0. GF iff not v in Carrier L )

proof end;

definition

let GF be non empty ZeroStr ;

let V be non empty ModuleStr over GF;

existence

ex b_{1} being Linear_Combination of V st Carrier b_{1} = {}

for b_{1}, b_{2} being Linear_Combination of V st Carrier b_{1} = {} & Carrier b_{2} = {} holds

b_{1} = b_{2}

end;
let V be non empty ModuleStr over GF;

existence

ex b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def3 defines ZeroLC VECTSP_6:def 3 :

for GF being non empty ZeroStr

for V being non empty ModuleStr over GF

for b_{3} being Linear_Combination of V holds

( b_{3} = ZeroLC V iff Carrier b_{3} = {} );

for GF being non empty ZeroStr

for V being non empty ModuleStr over GF

for b

( b

theorem Th3: :: VECTSP_6:3

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for v being Element of V holds (ZeroLC V) . v = 0. GF

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for v being Element of V holds (ZeroLC V) . v = 0. GF

proof end;

definition

let GF be non empty ZeroStr ;

let V be non empty ModuleStr over GF;

let A be Subset of V;

ex b_{1} being Linear_Combination of V st Carrier b_{1} c= A

end;
let V be non empty ModuleStr over GF;

let A be Subset of V;

mode Linear_Combination of A -> Linear_Combination of V means :Def4: :: VECTSP_6:def 4

Carrier it c= A;

existence Carrier it c= A;

ex b

proof end;

:: deftheorem Def4 defines Linear_Combination VECTSP_6:def 4 :

for GF being non empty ZeroStr

for V being non empty ModuleStr over GF

for A being Subset of V

for b_{4} being Linear_Combination of V holds

( b_{4} is Linear_Combination of A iff Carrier b_{4} c= A );

for GF being non empty ZeroStr

for V being non empty ModuleStr over GF

for A being Subset of V

for b

( b

theorem :: VECTSP_6:4

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for A, B being Subset of V

for l being Linear_Combination of A st A c= B holds

l is Linear_Combination of B

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for A, B being Subset of V

for l being Linear_Combination of A st A c= B holds

l is Linear_Combination of B

proof end;

theorem Th5: :: VECTSP_6:5

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for A being Subset of V holds ZeroLC V is Linear_Combination of A

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for A being Subset of V holds ZeroLC V is Linear_Combination of A

proof end;

theorem Th6: :: VECTSP_6:6

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for l being Linear_Combination of {} the carrier of V holds l = ZeroLC V

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for l being Linear_Combination of {} the carrier of V holds l = ZeroLC V

proof end;

theorem :: VECTSP_6:7

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for L being Linear_Combination of V holds L is Linear_Combination of Carrier L by Def4;

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for L being Linear_Combination of V holds L is Linear_Combination of Carrier L by Def4;

definition

let GF be non empty addLoopStr ;

let V be non empty ModuleStr over GF;

let F be FinSequence of the carrier of V;

let f be Function of V,GF;

ex b_{1} being FinSequence of V st

( len b_{1} = len F & ( for i being Nat st i in dom b_{1} holds

b_{1} . i = (f . (F /. i)) * (F /. i) ) )

for b_{1}, b_{2} being FinSequence of V st len b_{1} = len F & ( for i being Nat st i in dom b_{1} holds

b_{1} . i = (f . (F /. i)) * (F /. i) ) & len b_{2} = len F & ( for i being Nat st i in dom b_{2} holds

b_{2} . i = (f . (F /. i)) * (F /. i) ) holds

b_{1} = b_{2}

end;
let V be non empty ModuleStr over GF;

let F be FinSequence of the carrier of V;

let f be Function of V,GF;

func f (#) F -> FinSequence of V means :Def5: :: VECTSP_6:def 5

( len it = len F & ( for i being Nat st i in dom it holds

it . i = (f . (F /. i)) * (F /. i) ) );

existence ( len it = len F & ( for i being Nat st i in dom it holds

it . i = (f . (F /. i)) * (F /. i) ) );

ex b

( len b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def5 defines (#) VECTSP_6:def 5 :

for GF being non empty addLoopStr

for V being non empty ModuleStr over GF

for F being FinSequence of the carrier of V

for f being Function of V,GF

for b_{5} being FinSequence of V holds

( b_{5} = f (#) F iff ( len b_{5} = len F & ( for i being Nat st i in dom b_{5} holds

b_{5} . i = (f . (F /. i)) * (F /. i) ) ) );

for GF being non empty addLoopStr

for V being non empty ModuleStr over GF

for F being FinSequence of the carrier of V

for f being Function of V,GF

for b

( b

b

theorem Th8: :: VECTSP_6:8

for i being Element of NAT

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for v being Element of V

for F being FinSequence of V

for f being Function of V,GF st i in dom F & v = F . i holds

(f (#) F) . i = (f . v) * v

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for v being Element of V

for F being FinSequence of V

for f being Function of V,GF st i in dom F & v = F . i holds

(f (#) F) . i = (f . v) * v

proof end;

theorem :: VECTSP_6:9

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for f being Function of V,GF holds f (#) (<*> the carrier of V) = <*> the carrier of V

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for f being Function of V,GF holds f (#) (<*> the carrier of V) = <*> the carrier of V

proof end;

theorem Th10: :: VECTSP_6:10

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for v being Element of V

for f being Function of V,GF holds f (#) <*v*> = <*((f . v) * v)*>

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for v being Element of V

for f being Function of V,GF holds f (#) <*v*> = <*((f . v) * v)*>

proof end;

theorem Th11: :: VECTSP_6:11

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for v1, v2 being Element of V

for f being Function of V,GF holds f (#) <*v1,v2*> = <*((f . v1) * v1),((f . v2) * v2)*>

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for v1, v2 being Element of V

for f being Function of V,GF holds f (#) <*v1,v2*> = <*((f . v1) * v1),((f . v2) * v2)*>

proof end;

theorem :: VECTSP_6:12

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for v1, v2, v3 being Element of V

for f being Function of V,GF holds f (#) <*v1,v2,v3*> = <*((f . v1) * v1),((f . v2) * v2),((f . v3) * v3)*>

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for v1, v2, v3 being Element of V

for f being Function of V,GF holds f (#) <*v1,v2,v3*> = <*((f . v1) * v1),((f . v2) * v2),((f . v3) * v3)*>

proof end;

theorem Th13: :: VECTSP_6:13

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for F, G being FinSequence of V

for f being Function of V,GF holds f (#) (F ^ G) = (f (#) F) ^ (f (#) G)

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for F, G being FinSequence of V

for f being Function of V,GF holds f (#) (F ^ G) = (f (#) F) ^ (f (#) G)

proof end;

definition

let GF be non empty addLoopStr ;

let V be non empty ModuleStr over GF;

let L be Linear_Combination of V;

assume A1: ( V is Abelian & V is add-associative & V is right_zeroed & V is right_complementable ) ;

ex b_{1} being Element of V ex F being FinSequence of the carrier of V st

( F is one-to-one & rng F = Carrier L & b_{1} = Sum (L (#) F) )

for b_{1}, b_{2} being Element of V st ex F being FinSequence of the carrier of V st

( F is one-to-one & rng F = Carrier L & b_{1} = Sum (L (#) F) ) & ex F being FinSequence of the carrier of V st

( F is one-to-one & rng F = Carrier L & b_{2} = Sum (L (#) F) ) holds

b_{1} = b_{2}

end;
let V be non empty ModuleStr over GF;

let L be Linear_Combination of V;

assume A1: ( V is Abelian & V is add-associative & V is right_zeroed & V is right_complementable ) ;

func Sum L -> Element of V means :Def6: :: VECTSP_6:def 6

ex F being FinSequence of the carrier of V st

( F is one-to-one & rng F = Carrier L & it = Sum (L (#) F) );

existence ex F being FinSequence of the carrier of V st

( F is one-to-one & rng F = Carrier L & it = Sum (L (#) F) );

ex b

( F is one-to-one & rng F = Carrier L & b

proof end;

uniqueness for b

( F is one-to-one & rng F = Carrier L & b

( F is one-to-one & rng F = Carrier L & b

b

proof end;

:: deftheorem Def6 defines Sum VECTSP_6:def 6 :

for GF being non empty addLoopStr

for V being non empty ModuleStr over GF

for L being Linear_Combination of V st V is Abelian & V is add-associative & V is right_zeroed & V is right_complementable holds

for b_{4} being Element of V holds

( b_{4} = Sum L iff ex F being FinSequence of the carrier of V st

( F is one-to-one & rng F = Carrier L & b_{4} = Sum (L (#) F) ) );

for GF being non empty addLoopStr

for V being non empty ModuleStr over GF

for L being Linear_Combination of V st V is Abelian & V is add-associative & V is right_zeroed & V is right_complementable holds

for b

( b

( F is one-to-one & rng F = Carrier L & b

Lm1: for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF holds Sum (ZeroLC V) = 0. V

proof end;

theorem :: VECTSP_6:14

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for A being Subset of V st 0. GF <> 1. GF holds

( ( A <> {} & A is linearly-closed ) iff for l being Linear_Combination of A holds Sum l in A )

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for A being Subset of V st 0. GF <> 1. GF holds

( ( A <> {} & A is linearly-closed ) iff for l being Linear_Combination of A holds Sum l in A )

proof end;

theorem :: VECTSP_6:15

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF holds Sum (ZeroLC V) = 0. V by Lm1;

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF holds Sum (ZeroLC V) = 0. V by Lm1;

theorem :: VECTSP_6:16

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for l being Linear_Combination of {} the carrier of V holds Sum l = 0. V

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for l being Linear_Combination of {} the carrier of V holds Sum l = 0. V

proof end;

theorem Th17: :: VECTSP_6:17

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for v being Element of V

for l being Linear_Combination of {v} holds Sum l = (l . v) * v

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for v being Element of V

for l being Linear_Combination of {v} holds Sum l = (l . v) * v

proof end;

theorem Th18: :: VECTSP_6:18

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for v1, v2 being Element of V st v1 <> v2 holds

for l being Linear_Combination of {v1,v2} holds Sum l = ((l . v1) * v1) + ((l . v2) * v2)

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for v1, v2 being Element of V st v1 <> v2 holds

for l being Linear_Combination of {v1,v2} holds Sum l = ((l . v1) * v1) + ((l . v2) * v2)

proof end;

theorem :: VECTSP_6:19

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for L being Linear_Combination of V st Carrier L = {} holds

Sum L = 0. V

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for L being Linear_Combination of V st Carrier L = {} holds

Sum L = 0. V

proof end;

theorem :: VECTSP_6:20

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for v being Element of V

for L being Linear_Combination of V st Carrier L = {v} holds

Sum L = (L . v) * v

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for v being Element of V

for L being Linear_Combination of V st Carrier L = {v} holds

Sum L = (L . v) * v

proof end;

theorem :: VECTSP_6:21

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for v1, v2 being Element of V

for L being Linear_Combination of V st Carrier L = {v1,v2} & v1 <> v2 holds

Sum L = ((L . v1) * v1) + ((L . v2) * v2)

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for v1, v2 being Element of V

for L being Linear_Combination of V st Carrier L = {v1,v2} & v1 <> v2 holds

Sum L = ((L . v1) * v1) + ((L . v2) * v2)

proof end;

definition

let GF be non empty ZeroStr ;

let V be non empty ModuleStr over GF;

let L1, L2 be Linear_Combination of V;

( L1 = L2 iff for v being Element of V holds L1 . v = L2 . v ) by FUNCT_2:63;

end;
let V be non empty ModuleStr over GF;

let L1, L2 be Linear_Combination of V;

:: original: =

redefine pred L1 = L2 means :: VECTSP_6:def 7

for v being Element of V holds L1 . v = L2 . v;

compatibility redefine pred L1 = L2 means :: VECTSP_6:def 7

for v being Element of V holds L1 . v = L2 . v;

( L1 = L2 iff for v being Element of V holds L1 . v = L2 . v ) by FUNCT_2:63;

:: deftheorem defines = VECTSP_6:def 7 :

for GF being non empty ZeroStr

for V being non empty ModuleStr over GF

for L1, L2 being Linear_Combination of V holds

( L1 = L2 iff for v being Element of V holds L1 . v = L2 . v );

for GF being non empty ZeroStr

for V being non empty ModuleStr over GF

for L1, L2 being Linear_Combination of V holds

( L1 = L2 iff for v being Element of V holds L1 . v = L2 . v );

definition

let GF be non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr ;

let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF;

let L1, L2 be Linear_Combination of V;

coherence

L1 + L2 is Linear_Combination of V

end;
let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF;

let L1, L2 be Linear_Combination of V;

coherence

L1 + L2 is Linear_Combination of V

proof end;

:: deftheorem defines + VECTSP_6:def 8 :

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for L1, L2 being Linear_Combination of V holds L1 + L2 = L1 + L2;

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for L1, L2 being Linear_Combination of V holds L1 + L2 = L1 + L2;

theorem Th22: :: VECTSP_6:22

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for v being Element of V

for L1, L2 being Linear_Combination of V holds (L1 + L2) . v = (L1 . v) + (L2 . v)

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for v being Element of V

for L1, L2 being Linear_Combination of V holds (L1 + L2) . v = (L1 . v) + (L2 . v)

proof end;

theorem Th23: :: VECTSP_6:23

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for L1, L2 being Linear_Combination of V holds Carrier (L1 + L2) c= (Carrier L1) \/ (Carrier L2)

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for L1, L2 being Linear_Combination of V holds Carrier (L1 + L2) c= (Carrier L1) \/ (Carrier L2)

proof end;

theorem Th24: :: VECTSP_6:24

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for A being Subset of V

for L1, L2 being Linear_Combination of V st L1 is Linear_Combination of A & L2 is Linear_Combination of A holds

L1 + L2 is Linear_Combination of A

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for A being Subset of V

for L1, L2 being Linear_Combination of V st L1 is Linear_Combination of A & L2 is Linear_Combination of A holds

L1 + L2 is Linear_Combination of A

proof end;

theorem :: VECTSP_6:25

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for L1, L2 being Linear_Combination of V holds L1 + L2 = L2 + L1

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for L1, L2 being Linear_Combination of V holds L1 + L2 = L2 + L1

proof end;

theorem :: VECTSP_6:26

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for L1, L2, L3 being Linear_Combination of V holds L1 + (L2 + L3) = (L1 + L2) + L3

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for L1, L2, L3 being Linear_Combination of V holds L1 + (L2 + L3) = (L1 + L2) + L3

proof end;

theorem :: VECTSP_6:27

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for L being Linear_Combination of V holds

( L + (ZeroLC V) = L & (ZeroLC V) + L = L )

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for L being Linear_Combination of V holds

( L + (ZeroLC V) = L & (ZeroLC V) + L = L )

proof end;

definition

let GF be non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr ;

let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF;

let a be Element of GF;

let L be Linear_Combination of V;

ex b_{1} being Linear_Combination of V st

for v being Element of V holds b_{1} . v = a * (L . v)

for b_{1}, b_{2} being Linear_Combination of V st ( for v being Element of V holds b_{1} . v = a * (L . v) ) & ( for v being Element of V holds b_{2} . v = a * (L . v) ) holds

b_{1} = b_{2}

end;
let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF;

let a be Element of GF;

let L be Linear_Combination of V;

func a * L -> Linear_Combination of V means :Def9: :: VECTSP_6:def 9

for v being Element of V holds it . v = a * (L . v);

existence for v being Element of V holds it . v = a * (L . v);

ex b

for v being Element of V holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def9 defines * VECTSP_6:def 9 :

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for a being Element of GF

for L, b_{5} being Linear_Combination of V holds

( b_{5} = a * L iff for v being Element of V holds b_{5} . v = a * (L . v) );

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for a being Element of GF

for L, b

( b

theorem Th28: :: VECTSP_6:28

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for a being Element of GF

for L being Linear_Combination of V holds Carrier (a * L) c= Carrier L

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for a being Element of GF

for L being Linear_Combination of V holds Carrier (a * L) c= Carrier L

proof end;

theorem Th29: :: VECTSP_6:29

for GF being Field

for V being VectSp of GF

for a being Element of GF

for L being Linear_Combination of V st a <> 0. GF holds

Carrier (a * L) = Carrier L

for V being VectSp of GF

for a being Element of GF

for L being Linear_Combination of V st a <> 0. GF holds

Carrier (a * L) = Carrier L

proof end;

theorem Th30: :: VECTSP_6:30

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for L being Linear_Combination of V holds (0. GF) * L = ZeroLC V

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for L being Linear_Combination of V holds (0. GF) * L = ZeroLC V

proof end;

theorem Th31: :: VECTSP_6:31

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for a being Element of GF

for A being Subset of V

for L being Linear_Combination of V st L is Linear_Combination of A holds

a * L is Linear_Combination of A

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for a being Element of GF

for A being Subset of V

for L being Linear_Combination of V st L is Linear_Combination of A holds

a * L is Linear_Combination of A

proof end;

theorem :: VECTSP_6:32

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for a, b being Element of GF

for L being Linear_Combination of V holds (a + b) * L = (a * L) + (b * L)

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for a, b being Element of GF

for L being Linear_Combination of V holds (a + b) * L = (a * L) + (b * L)

proof end;

theorem :: VECTSP_6:33

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for a being Element of GF

for L1, L2 being Linear_Combination of V holds a * (L1 + L2) = (a * L1) + (a * L2)

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for a being Element of GF

for L1, L2 being Linear_Combination of V holds a * (L1 + L2) = (a * L1) + (a * L2)

proof end;

theorem Th34: :: VECTSP_6:34

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for a, b being Element of GF

for L being Linear_Combination of V holds a * (b * L) = (a * b) * L

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for a, b being Element of GF

for L being Linear_Combination of V holds a * (b * L) = (a * b) * L

proof end;

theorem :: VECTSP_6:35

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for L being Linear_Combination of V holds (1. GF) * L = L

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for L being Linear_Combination of V holds (1. GF) * L = L

proof end;

definition

let GF be non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr ;

let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF;

let L be Linear_Combination of V;

correctness

coherence

(- (1. GF)) * L is Linear_Combination of V;

;

involutiveness

for b_{1}, b_{2} being Linear_Combination of V st b_{1} = (- (1. GF)) * b_{2} holds

b_{2} = (- (1. GF)) * b_{1}

end;
let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF;

let L be Linear_Combination of V;

correctness

coherence

(- (1. GF)) * L is Linear_Combination of V;

;

involutiveness

for b

b

proof end;

:: deftheorem defines - VECTSP_6:def 10 :

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for L being Linear_Combination of V holds - L = (- (1. GF)) * L;

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for L being Linear_Combination of V holds - L = (- (1. GF)) * L;

Lm2: for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for a being Element of GF holds (- (1. GF)) * a = - a

proof end;

theorem Th36: :: VECTSP_6:36

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for v being Element of V

for L being Linear_Combination of V holds (- L) . v = - (L . v)

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for v being Element of V

for L being Linear_Combination of V holds (- L) . v = - (L . v)

proof end;

theorem :: VECTSP_6:37

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for L1, L2 being Linear_Combination of V st L1 + L2 = ZeroLC V holds

L2 = - L1

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for L1, L2 being Linear_Combination of V st L1 + L2 = ZeroLC V holds

L2 = - L1

proof end;

Lm3: for GF being Field holds - (1. GF) <> 0. GF

proof end;

theorem Th38: :: VECTSP_6:38

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for L being Linear_Combination of V holds Carrier (- L) = Carrier L

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for L being Linear_Combination of V holds Carrier (- L) = Carrier L

proof end;

theorem :: VECTSP_6:39

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for A being Subset of V

for L being Linear_Combination of V st L is Linear_Combination of A holds

- L is Linear_Combination of A by Th31;

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for A being Subset of V

for L being Linear_Combination of V st L is Linear_Combination of A holds

- L is Linear_Combination of A by Th31;

definition

let GF be non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr ;

let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF;

let L1, L2 be Linear_Combination of V;

coherence

L1 + (- L2) is Linear_Combination of V ;

end;
let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF;

let L1, L2 be Linear_Combination of V;

coherence

L1 + (- L2) is Linear_Combination of V ;

:: deftheorem defines - VECTSP_6:def 11 :

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for L1, L2 being Linear_Combination of V holds L1 - L2 = L1 + (- L2);

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for L1, L2 being Linear_Combination of V holds L1 - L2 = L1 + (- L2);

theorem Th40: :: VECTSP_6:40

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for v being Element of V

for L1, L2 being Linear_Combination of V holds (L1 - L2) . v = (L1 . v) - (L2 . v)

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for v being Element of V

for L1, L2 being Linear_Combination of V holds (L1 - L2) . v = (L1 . v) - (L2 . v)

proof end;

theorem :: VECTSP_6:41

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for L1, L2 being Linear_Combination of V holds Carrier (L1 - L2) c= (Carrier L1) \/ (Carrier L2)

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for L1, L2 being Linear_Combination of V holds Carrier (L1 - L2) c= (Carrier L1) \/ (Carrier L2)

proof end;

theorem :: VECTSP_6:42

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for A being Subset of V

for L1, L2 being Linear_Combination of V st L1 is Linear_Combination of A & L2 is Linear_Combination of A holds

L1 - L2 is Linear_Combination of A

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for A being Subset of V

for L1, L2 being Linear_Combination of V st L1 is Linear_Combination of A & L2 is Linear_Combination of A holds

L1 - L2 is Linear_Combination of A

proof end;

theorem Th43: :: VECTSP_6:43

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for L being Linear_Combination of V holds L - L = ZeroLC V

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for L being Linear_Combination of V holds L - L = ZeroLC V

proof end;

theorem Th44: :: VECTSP_6:44

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for L1, L2 being Linear_Combination of V holds Sum (L1 + L2) = (Sum L1) + (Sum L2)

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for L1, L2 being Linear_Combination of V holds Sum (L1 + L2) = (Sum L1) + (Sum L2)

proof end;

theorem :: VECTSP_6:45

for GF being Field

for V being VectSp of GF

for L being Linear_Combination of V

for a being Element of GF holds Sum (a * L) = a * (Sum L)

for V being VectSp of GF

for L being Linear_Combination of V

for a being Element of GF holds Sum (a * L) = a * (Sum L)

proof end;

theorem Th46: :: VECTSP_6:46

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for L being Linear_Combination of V holds Sum (- L) = - (Sum L)

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for L being Linear_Combination of V holds Sum (- L) = - (Sum L)

proof end;

theorem :: VECTSP_6:47

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for L1, L2 being Linear_Combination of V holds Sum (L1 - L2) = (Sum L1) - (Sum L2)

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for L1, L2 being Linear_Combination of V holds Sum (L1 - L2) = (Sum L1) - (Sum L2)

proof end;

theorem :: VECTSP_6:48

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for a being Element of GF holds (- (1. GF)) * a = - a by Lm2;

for a being Element of GF holds (- (1. GF)) * a = - a by Lm2;

:: Auxiliary theorems.

::