:: Linear Combinations in Vector Space
:: by Wojciech A. Trybulec
::
:: Received July 27, 1990
:: Copyright (c) 1990-2011 Association of Mizar Users

begin

definition

let GF be non empty ZeroStr ;
let V be non empty VectSpStr of GF;
canceled;
canceled;
canceled;
mode Linear_Combination of V -> Element of Funcs ( the carrier of V, the carrier of GF) means :Def4: :: VECTSP_6:def 4
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 b₁ 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₁ . v = 0. GF

proof end;

end;

:: deftheorem VECTSP_6:def 1 :
canceled;

:: deftheorem VECTSP_6:def 2 :
canceled;

:: deftheorem VECTSP_6:def 3 :
canceled;

:: deftheorem Def4 defines Linear_Combination VECTSP_6:def 4 :
for GF being non empty ZeroStr
for V being non empty VectSpStr of GF
for b₃ being Element of Funcs ( the carrier of V, the carrier of GF) holds
( b₃ 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₃ . v = 0. GF );

definition

let GF be non empty ZeroStr ;
let V be non empty VectSpStr of GF;
let L be Linear_Combination of V;
func Carrier L -> finite Subset of V equals :: VECTSP_6:def 5
{ v where v is Element of V : L . v <> 0. GF } ;
coherence
{ v where v is Element of V : L . v <> 0. GF } is finite Subset of V

proof end;

end;

:: deftheorem defines Carrier VECTSP_6:def 5 :
for GF being non empty ZeroStr
for V being non empty VectSpStr of 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

canceled;

theorem :: VECTSP_6:2

canceled;

theorem :: VECTSP_6:3

canceled;

theorem :: VECTSP_6:4

canceled;

theorem :: VECTSP_6:5

canceled;

theorem :: VECTSP_6:6

canceled;

theorem :: VECTSP_6:7

canceled;

theorem :: VECTSP_6:8

canceled;

theorem :: VECTSP_6:9

canceled;

theorem :: VECTSP_6:10

canceled;

theorem :: VECTSP_6:11

canceled;

theorem :: VECTSP_6:12

canceled;

theorem :: VECTSP_6:13

canceled;

theorem :: VECTSP_6:14

canceled;

theorem :: VECTSP_6:15

canceled;

theorem :: VECTSP_6:16

canceled;

theorem :: VECTSP_6:17

canceled;

theorem :: VECTSP_6:18

canceled;

theorem :: VECTSP_6:19

for x being set
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr of 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:20

for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr of 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 VectSpStr of GF;
func ZeroLC V -> Linear_Combination of V means :Def6: :: VECTSP_6:def 6
Carrier it = {} ;
existence
ex b₁ being Linear_Combination of V st Carrier b₁ = {}

proof end;

uniqueness
for b₁, b₂ being Linear_Combination of V st Carrier b₁ = {} & Carrier b₂ = {} holds
b₁ = b₂

proof end;

end;

:: deftheorem Def6 defines ZeroLC VECTSP_6:def 6 :
for GF being non empty ZeroStr
for V being non empty VectSpStr of GF
for b₃ being Linear_Combination of V holds
( b₃ = ZeroLC V iff Carrier b₃ = {} );

theorem :: VECTSP_6:21

canceled;

theorem Th22: :: VECTSP_6:22

for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr of 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 VectSpStr of GF;
let A be Subset of V;
mode Linear_Combination of A -> Linear_Combination of V means :Def7: :: VECTSP_6:def 7
Carrier it c= A;
existence
ex b₁ being Linear_Combination of V st Carrier b₁ c= A

proof end;

end;

:: deftheorem Def7 defines Linear_Combination VECTSP_6:def 7 :
for GF being non empty ZeroStr
for V being non empty VectSpStr of GF
for A being Subset of V
for b₄ being Linear_Combination of V holds
( b₄ is Linear_Combination of A iff Carrier b₄ c= A );

theorem :: VECTSP_6:23

canceled;

theorem :: VECTSP_6:24

canceled;

theorem :: VECTSP_6:25

for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr of 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 Th26: :: VECTSP_6:26

for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr of GF
for A being Subset of V holds ZeroLC V is Linear_Combination of A

proof end;

theorem Th27: :: VECTSP_6:27

for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr of GF
for l being Linear_Combination of {} the carrier of V holds l = ZeroLC V

proof end;

theorem :: VECTSP_6:28

for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr of GF
for L being Linear_Combination of V holds L is Linear_Combination of Carrier L by Def7;

definition

let GF be non empty addLoopStr ;
let V be non empty VectSpStr of GF;
let F be FinSequence of the carrier of V;
let f be Function of V,GF;
func f (#) F -> FinSequence of V means :Def8: :: VECTSP_6:def 8
( len it = len F & ( for i being Nat st i in dom it holds
it . i = (f . (F /. i)) * (F /. i) ) );
existence
ex b₁ being FinSequence of V st
( len b₁ = len F & ( for i being Nat st i in dom b₁ holds
b₁ . i = (f . (F /. i)) * (F /. i) ) )

proof end;

uniqueness
for b₁, b₂ being FinSequence of V st len b₁ = len F & ( for i being Nat st i in dom b₁ holds
b₁ . i = (f . (F /. i)) * (F /. i) ) & len b₂ = len F & ( for i being Nat st i in dom b₂ holds
b₂ . i = (f . (F /. i)) * (F /. i) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def8 defines (#) VECTSP_6:def 8 :
for GF being non empty addLoopStr
for V being non empty VectSpStr of GF
for F being FinSequence of the carrier of V
for f being Function of V,GF
for b₅ being FinSequence of V holds
( b₅ = f (#) F iff ( len b₅ = len F & ( for i being Nat st i in dom b₅ holds
b₅ . i = (f . (F /. i)) * (F /. i) ) ) );

theorem :: VECTSP_6:29

canceled;

theorem :: VECTSP_6:30

canceled;

theorem :: VECTSP_6:31

canceled;

theorem Th32: :: VECTSP_6:32

for i being Element of NAT
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr of 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:33

for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr of GF
for f being Function of V,GF holds f (#) (<*> the carrier of V) = <*> the carrier of V

proof end;

theorem Th34: :: VECTSP_6:34

for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr of GF
for v being Element of V
for f being Function of V,GF holds f (#) <*v*> = <*((f . v) * v)*>

proof end;

theorem Th35: :: VECTSP_6:35

for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr of 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:36

for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr of 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 Th37: :: VECTSP_6:37

for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr of 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 VectSpStr of 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 :Def9: :: VECTSP_6:def 9
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 b₁ being Element of V ex F being FinSequence of the carrier of V st
( F is one-to-one & rng F = Carrier L & b₁ = Sum (L (#) F) )

proof end;

uniqueness
for b₁, b₂ 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₁ = Sum (L (#) F) ) & ex F being FinSequence of the carrier of V st
( F is one-to-one & rng F = Carrier L & b₂ = Sum (L (#) F) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def9 defines Sum VECTSP_6:def 9 :
for GF being non empty addLoopStr
for V being non empty VectSpStr of 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₄ being Element of V holds
( b₄ = Sum L iff ex F being FinSequence of the carrier of V st
( F is one-to-one & rng F = Carrier L & b₄ = Sum (L (#) F) ) );

Lm1: for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr of GF holds Sum (ZeroLC V) = 0. V

proof end;

theorem :: VECTSP_6:38

canceled;

theorem :: VECTSP_6:39

canceled;

theorem :: VECTSP_6:40

for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr of 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:41

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

theorem :: VECTSP_6:42

for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr of GF
for l being Linear_Combination of {} the carrier of V holds Sum l = 0. V

proof end;

theorem Th43: :: VECTSP_6:43

for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr of GF
for v being Element of V
for l being Linear_Combination of {v} holds Sum l = (l . v) * v

proof end;

theorem Th44: :: VECTSP_6:44

for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr of 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:45

for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr of GF
for L being Linear_Combination of V st Carrier L = {} holds
Sum L = 0. V

proof end;

theorem :: VECTSP_6:46

for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr of 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:47

for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr of 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 VectSpStr of GF;
let L1, L2 be Linear_Combination of V;
:: original: =
redefine pred L1 = L2 means :: VECTSP_6:def 10
for v being Element of V holds L1 . v = L2 . v;
compatibility
( L1 = L2 iff for v being Element of V holds L1 . v = L2 . v ) by FUNCT_2:113;

end;

:: deftheorem defines = VECTSP_6:def 10 :
for GF being non empty ZeroStr
for V being non empty VectSpStr of 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 associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ;
let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr of GF;
let L1, L2 be Linear_Combination of V;
func L1 + L2 -> Linear_Combination of V equals :: VECTSP_6:def 11
L1 + L2;
coherence
L1 + L2 is Linear_Combination of V

proof end;

end;

:: deftheorem defines + VECTSP_6:def 11 :
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr of GF
for L1, L2 being Linear_Combination of V holds L1 + L2 = L1 + L2;

theorem ThDef11: :: VECTSP_6:48

for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr of 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:49

canceled;

theorem :: VECTSP_6:50

canceled;

theorem Th51: :: VECTSP_6:51

for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr of GF
for L1, L2 being Linear_Combination of V holds Carrier (L1 + L2) c= (Carrier L1) \/ (Carrier L2)

proof end;

theorem Th52: :: VECTSP_6:52

for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr of 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 Th53: :: VECTSP_6:53

for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr of GF
for L1, L2 being Linear_Combination of V holds L1 + L2 = L2 + L1

proof end;

theorem :: VECTSP_6:54

for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr of GF
for L1, L2, L3 being Linear_Combination of V holds L1 + (L2 + L3) = (L1 + L2) + L3

proof end;

theorem :: VECTSP_6:55

for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr of 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 associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ;
let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr of GF;
let a be Element of GF;
let L be Linear_Combination of V;
func a * L -> Linear_Combination of V means :Def12: :: VECTSP_6:def 12
for v being Element of V holds it . v = a * (L . v);
existence
ex b₁ being Linear_Combination of V st
for v being Element of V holds b₁ . v = a * (L . v)

proof end;

uniqueness
for b₁, b₂ being Linear_Combination of V st ( for v being Element of V holds b₁ . v = a * (L . v) ) & ( for v being Element of V holds b₂ . v = a * (L . v) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def12 defines * VECTSP_6:def 12 :
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr of GF
for a being Element of GF
for L, b₅ being Linear_Combination of V holds
( b₅ = a * L iff for v being Element of V holds b₅ . v = a * (L . v) );

theorem :: VECTSP_6:56

canceled;

theorem :: VECTSP_6:57

canceled;

theorem Th58: :: VECTSP_6:58

for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr of GF
for a being Element of GF
for L being Linear_Combination of V holds Carrier (a * L) c= Carrier L

proof end;

theorem Th59: :: VECTSP_6:59

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

proof end;

theorem Th60: :: VECTSP_6:60

for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr of GF
for L being Linear_Combination of V holds (0. GF) * L = ZeroLC V

proof end;

theorem Th61: :: VECTSP_6:61

for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr of 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:62

for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr of 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:63

for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr of 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 Th64: :: VECTSP_6:64

for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr of 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:65

for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr of GF
for L being Linear_Combination of V holds (1. GF) * L = L

proof end;

definition

let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ;
let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr of GF;
let L be Linear_Combination of V;
func - L -> Linear_Combination of V equals :: VECTSP_6:def 13
(- (1. GF)) * L;
correctness
coherence
(- (1. GF)) * L is Linear_Combination of V;
;
involutiveness
for b₁, b₂ being Linear_Combination of V st b₁ = (- (1. GF)) * b₂ holds
b₂ = (- (1. GF)) * b₁

proof end;

end;

:: deftheorem defines - VECTSP_6:def 13 :
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr of GF
for L being Linear_Combination of V holds - L = (- (1. GF)) * L;

Lm2: for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for a being Element of GF holds (- (1. GF)) * a = - a

proof end;

theorem :: VECTSP_6:66

canceled;

theorem Th67: :: VECTSP_6:67

for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr of GF
for v being Element of V
for L being Linear_Combination of V holds (- L) . v = - (L . v)

proof end;

theorem :: VECTSP_6:68

for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr of 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 Th69: :: VECTSP_6:69

for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr of GF
for L being Linear_Combination of V holds Carrier (- L) = Carrier L

proof end;

theorem :: VECTSP_6:70

for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr of 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 Th61;

definition

let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ;
let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr of GF;
let L1, L2 be Linear_Combination of V;
func L1 - L2 -> Linear_Combination of V equals :: VECTSP_6:def 14
L1 + (- L2);
coherence
L1 + (- L2) is Linear_Combination of V ;

end;

:: deftheorem defines - VECTSP_6:def 14 :
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr of GF
for L1, L2 being Linear_Combination of V holds L1 - L2 = L1 + (- L2);

theorem :: VECTSP_6:71

canceled;

theorem :: VECTSP_6:72

canceled;

theorem Th73: :: VECTSP_6:73

for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr of 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:74

for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr of GF
for L1, L2 being Linear_Combination of V holds Carrier (L1 - L2) c= (Carrier L1) \/ (Carrier L2)

proof end;

theorem :: VECTSP_6:75

for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr of 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 Th76: :: VECTSP_6:76

for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr of GF
for L being Linear_Combination of V holds L - L = ZeroLC V

proof end;

theorem Th77: :: VECTSP_6:77

for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr of GF
for L1, L2 being Linear_Combination of V holds Sum (L1 + L2) = (Sum L1) + (Sum L2)

proof end;

theorem :: VECTSP_6:78

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)

proof end;

theorem Th79: :: VECTSP_6:79

for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr of GF
for L being Linear_Combination of V holds Sum (- L) = - (Sum L)

proof end;

theorem :: VECTSP_6:80

for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr of GF
for L1, L2 being Linear_Combination of V holds Sum (L1 - L2) = (Sum L1) - (Sum L2)

proof end;

theorem :: VECTSP_6:81

for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for a being Element of GF holds (- (1. GF)) * a = - a by Lm2;

theorem :: VECTSP_6:82

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