:: VECTSP_6 semantic presentation

definition

let c₁ be non empty ZeroStr ;
let c₂ be non empty VectSpStr of c₁;
canceled;
canceled;
canceled;
mode Linear_Combination of c₂ -> Element of Funcs the carrier of a₂,the carrier of a₁ means :Def4: :: VECTSP_6:def 4
ex b₁ being finite Subset of a₂ st
for b₂ being Element of a₂ st not b₂ in b₁ holds
a₃ . b₂ = 0. a₁;
existence

proof end;

end;

:: deftheorem Def1 VECTSP_6:def 1 :

:: deftheorem Def2 VECTSP_6:def 2 :

:: deftheorem Def3 VECTSP_6:def 3 :

:: deftheorem Def4 defines Linear_Combination VECTSP_6:def 4 :

definition

let c₁ be non empty ZeroStr ;
let c₂ be non empty VectSpStr of c₁;
let c₃ be Linear_Combination of c₂;
func Carrier c₃ -> finite Subset of a₂ equals :: VECTSP_6:def 5
{ b₁ where B is Element of a₂ : a₃ . b₁ <> 0. a₁ } ;
coherence

proof end;

end;

:: deftheorem Def5 defines Carrier VECTSP_6:def 5 :

theorem Th1: :: VECTSP_6:1

canceled;

theorem Th2: :: VECTSP_6:2

canceled;

theorem Th3: :: VECTSP_6:3

canceled;

theorem Th4: :: VECTSP_6:4

canceled;

theorem Th5: :: VECTSP_6:5

canceled;

theorem Th6: :: VECTSP_6:6

canceled;

theorem Th7: :: VECTSP_6:7

canceled;

theorem Th8: :: VECTSP_6:8

canceled;

theorem Th9: :: VECTSP_6:9

canceled;

theorem Th10: :: VECTSP_6:10

canceled;

theorem Th11: :: VECTSP_6:11

canceled;

theorem Th12: :: VECTSP_6:12

canceled;

theorem Th13: :: VECTSP_6:13

canceled;

theorem Th14: :: VECTSP_6:14

canceled;

theorem Th15: :: VECTSP_6:15

canceled;

theorem Th16: :: VECTSP_6:16

canceled;

theorem Th17: :: VECTSP_6:17

canceled;

theorem Th18: :: VECTSP_6:18

canceled;

theorem Th19: :: VECTSP_6:19

for b₁ being set
for b₂ being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b₃ being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of b₂
for b₄ being Linear_Combination of b₃ holds
( b₁ in Carrier b₄ iff ex b₅ being Element of b₃ st
( b₁ = b₅ & b₄ . b₅ <> 0. b₂ ) ) ;

theorem Th20: :: VECTSP_6:20

for b₁ being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b₂ being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of b₁
for b₃ being Element of b₂
for b₄ being Linear_Combination of b₂ holds
( b₄ . b₃ = 0. b₁ iff not b₃ in Carrier b₄ )

proof end;

definition

let c₁ be non empty ZeroStr ;
let c₂ be non empty VectSpStr of c₁;
func ZeroLC c₂ -> Linear_Combination of a₂ means :Def6: :: VECTSP_6:def 6
Carrier a₃ = {} ;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def6 defines ZeroLC VECTSP_6:def 6 :

theorem Th21: :: VECTSP_6:21

canceled;

theorem Th22: :: VECTSP_6:22

proof end;

definition

let c₁ be non empty ZeroStr ;
let c₂ be non empty VectSpStr of c₁;
let c₃ be Subset of c₂;
mode Linear_Combination of c₃ -> Linear_Combination of a₂ means :Def7: :: VECTSP_6:def 7
Carrier a₄ c= a₃;
existence

proof end;

end;

:: deftheorem Def7 defines Linear_Combination VECTSP_6:def 7 :

theorem Th23: :: VECTSP_6:23

canceled;

theorem Th24: :: VECTSP_6:24

canceled;

theorem Th25: :: VECTSP_6:25

for b₁ being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b₂ being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of b₁
for b₃, b₄ being Subset of b₂
for b₅ being Linear_Combination of b₃ st b₃ c= b₄ holds
b₅ is Linear_Combination of b₄

proof end;

theorem Th26: :: VECTSP_6:26

proof end;

theorem Th27: :: VECTSP_6:27

for b₁ being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b₂ being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of b₁
for b₃ being Linear_Combination of {} the carrier of b₂ holds b₃ = ZeroLC b₂

proof end;

theorem Th28: :: VECTSP_6:28

for b₁ being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b₂ being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of b₁
for b₃ being Linear_Combination of b₂ holds b₃ is Linear_Combination of Carrier b₃ by Def7;

definition

let c₁ be non empty LoopStr ;
let c₂ be non empty VectSpStr of c₁;
let c₃ be FinSequence of the carrier of c₂;
let c₄ be Function of the carrier of c₂,the carrier of c₁;
func c₄ (#) c₃ -> FinSequence of the carrier of a₂ means :Def8: :: VECTSP_6:def 8
( len a₅ = len a₃ & ( for b₁ being Nat st b₁ in dom a₅ holds
a₅ . b₁ = (a₄ . (a₃ /. b₁)) * (a₃ /. b₁) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def8 defines (#) VECTSP_6:def 8 :

theorem Th29: :: VECTSP_6:29

canceled;

theorem Th30: :: VECTSP_6:30

canceled;

theorem Th31: :: VECTSP_6:31

canceled;

theorem Th32: :: VECTSP_6:32

for b₁ being Nat
for b₂ being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b₃ being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of b₂
for b₄ being Element of b₃
for b₅ being FinSequence of the carrier of b₃
for b₆ being Function of the carrier of b₃,the carrier of b₂ st b₁ in dom b₅ & b₄ = b₅ . b₁ holds
(b₆ (#) b₅) . b₁ = (b₆ . b₄) * b₄

proof end;

theorem Th33: :: VECTSP_6:33

for b₁ being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b₂ being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of b₁
for b₃ being Function of the carrier of b₂,the carrier of b₁ holds b₃ (#) (<*> the carrier of b₂) = <*> the carrier of b₂

proof end;

theorem Th34: :: VECTSP_6:34

for b₁ being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b₂ being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of b₁
for b₃ being Element of b₂
for b₄ being Function of the carrier of b₂,the carrier of b₁ holds b₄ (#) <*b₃*> = <*((b₄ . b₃) * b₃)*>

proof end;

theorem Th35: :: VECTSP_6:35

for b₁ being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b₂ being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of b₁
for b₃, b₄ being Element of b₂
for b₅ being Function of the carrier of b₂,the carrier of b₁ holds b₅ (#) <*b₃,b₄*> = <*((b₅ . b₃) * b₃),((b₅ . b₄) * b₄)*>

proof end;

theorem Th36: :: VECTSP_6:36

for b₁ being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b₂ being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of b₁
for b₃, b₄, b₅ being Element of b₂
for b₆ being Function of the carrier of b₂,the carrier of b₁ holds b₆ (#) <*b₃,b₄,b₅*> = <*((b₆ . b₃) * b₃),((b₆ . b₄) * b₄),((b₆ . b₅) * b₅)*>

proof end;

theorem Th37: :: VECTSP_6:37

for b₁ being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b₂ being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of b₁
for b₃, b₄ being FinSequence of the carrier of b₂
for b₅ being Function of the carrier of b₂,the carrier of b₁ holds b₅ (#) (b₃ ^ b₄) = (b₅ (#) b₃) ^ (b₅ (#) b₄)

proof end;

definition

let c₁ be non empty LoopStr ;
let c₂ be non empty VectSpStr of c₁;
let c₃ be Linear_Combination of c₂;
assume E12: ( c₂ is Abelian & c₂ is add-associative & c₂ is right_zeroed & c₂ is right_complementable ) ;
func Sum c₃ -> Element of a₂ means :Def9: :: VECTSP_6:def 9
ex b₁ being FinSequence of the carrier of a₂ st
( b₁ is one-to-one & rng b₁ = Carrier a₃ & a₄ = Sum (a₃ (#) b₁) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def9 defines Sum VECTSP_6:def 9 :

Lemma13: for b₁ being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b₂ being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of b₁ holds Sum (ZeroLC b₂) = 0. b₂

proof end;

theorem Th38: :: VECTSP_6:38

canceled;

theorem Th39: :: VECTSP_6:39

canceled;

theorem Th40: :: VECTSP_6:40

for b₁ being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b₂ being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of b₁
for b₃ being Subset of b₂ st 0. b₁ <> 1. b₁ holds
( ( b₃ <> {} & b₃ is lineary-closed ) iff for b₄ being Linear_Combination of b₃ holds Sum b₄ in b₃ )

proof end;

theorem Th41: :: VECTSP_6:41

theorem Th42: :: VECTSP_6:42

for b₁ being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b₂ being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of b₁
for b₃ being Linear_Combination of {} the carrier of b₂ holds Sum b₃ = 0. b₂

proof end;

theorem Th43: :: VECTSP_6:43

proof end;

theorem Th44: :: VECTSP_6:44

for b₁ being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b₂ being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of b₁
for b₃, b₄ being Element of b₂ st b₃ <> b₄ holds
for b₅ being Linear_Combination of {b₃,b₄} holds Sum b₅ = ((b₅ . b₃) * b₃) + ((b₅ . b₄) * b₄)

proof end;

theorem Th45: :: VECTSP_6:45

for b₁ being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b₂ being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of b₁
for b₃ being Linear_Combination of b₂ st Carrier b₃ = {} holds
Sum b₃ = 0. b₂

proof end;

theorem Th46: :: VECTSP_6:46

for b₁ being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b₂ being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of b₁
for b₃ being Element of b₂
for b₄ being Linear_Combination of b₂ st Carrier b₄ = {b₃} holds
Sum b₄ = (b₄ . b₃) * b₃

proof end;

theorem Th47: :: VECTSP_6:47

for b₁ being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b₂ being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of b₁
for b₃, b₄ being Element of b₂
for b₅ being Linear_Combination of b₂ st Carrier b₅ = {b₃,b₄} & b₃ <> b₄ holds
Sum b₅ = ((b₅ . b₃) * b₃) + ((b₅ . b₄) * b₄)

proof end;

definition

let c₁ be non empty ZeroStr ;
let c₂ be non empty VectSpStr of c₁;
let c₃, c₄ be Linear_Combination of c₂;
redefine pred = as c₃ = c₄ means :: VECTSP_6:def 10
for b₁ being Element of a₂ holds a₃ . b₁ = a₄ . b₁;
compatibility by FUNCT_2:113;

end;

:: deftheorem Def10 defines = VECTSP_6:def 10 :

definition

let c₁ be non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr ;
let c₂ be non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of c₁;
let c₃, c₄ be Linear_Combination of c₂;
func c₃ + c₄ -> Linear_Combination of a₂ means :Def11: :: VECTSP_6:def 11
for b₁ being Element of a₂ holds a₅ . b₁ = (a₃ . b₁) + (a₄ . b₁);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def11 defines + VECTSP_6:def 11 :

theorem Th48: :: VECTSP_6:48

canceled;

theorem Th49: :: VECTSP_6:49

canceled;

theorem Th50: :: VECTSP_6:50

canceled;

theorem Th51: :: VECTSP_6:51

for b₁ being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b₂ being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of b₁
for b₃, b₄ being Linear_Combination of b₂ holds Carrier (b₃ + b₄) c= (Carrier b₃) \/ (Carrier b₄)

proof end;

theorem Th52: :: VECTSP_6:52

for b₁ being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b₂ being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of b₁
for b₃ being Subset of b₂
for b₄, b₅ being Linear_Combination of b₂ st b₄ is Linear_Combination of b₃ & b₅ is Linear_Combination of b₃ holds
b₄ + b₅ is Linear_Combination of b₃

proof end;

theorem Th53: :: VECTSP_6:53

for b₁ being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b₂ being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of b₁
for b₃, b₄ being Linear_Combination of b₂ holds b₃ + b₄ = b₄ + b₃

proof end;

theorem Th54: :: VECTSP_6:54

for b₁ being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b₂ being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of b₁
for b₃, b₄, b₅ being Linear_Combination of b₂ holds b₃ + (b₄ + b₅) = (b₃ + b₄) + b₅

proof end;

theorem Th55: :: VECTSP_6:55

for b₁ being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b₂ being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of b₁
for b₃ being Linear_Combination of b₂ holds
( b₃ + (ZeroLC b₂) = b₃ & (ZeroLC b₂) + b₃ = b₃ )

proof end;

definition

let c₁ be non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr ;
let c₂ be non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of c₁;
let c₃ be Element of c₁;
let c₄ be Linear_Combination of c₂;
func c₃ * c₄ -> Linear_Combination of a₂ means :Def12: :: VECTSP_6:def 12
for b₁ being Element of a₂ holds a₅ . b₁ = a₃ * (a₄ . b₁);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def12 defines * VECTSP_6:def 12 :

theorem Th56: :: VECTSP_6:56

canceled;

theorem Th57: :: VECTSP_6:57

canceled;

theorem Th58: :: VECTSP_6:58

for b₁ being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b₂ being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of b₁
for b₃ being Element of b₁
for b₄ being Linear_Combination of b₂ holds Carrier (b₃ * b₄) c= Carrier b₄

proof end;

theorem Th59: :: VECTSP_6:59

for b₁ being Field
for b₂ being VectSp of b₁
for b₃ being Element of b₁
for b₄ being Linear_Combination of b₂ st b₃ <> 0. b₁ holds
Carrier (b₃ * b₄) = Carrier b₄

proof end;

theorem Th60: :: VECTSP_6:60

proof end;

theorem Th61: :: VECTSP_6:61

for b₁ being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b₂ being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of b₁
for b₃ being Element of b₁
for b₄ being Subset of b₂
for b₅ being Linear_Combination of b₂ st b₅ is Linear_Combination of b₄ holds
b₃ * b₅ is Linear_Combination of b₄

proof end;

theorem Th62: :: VECTSP_6:62

for b₁ being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b₂ being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of b₁
for b₃, b₄ being Element of b₁
for b₅ being Linear_Combination of b₂ holds (b₃ + b₄) * b₅ = (b₃ * b₅) + (b₄ * b₅)

proof end;

theorem Th63: :: VECTSP_6:63

for b₁ being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b₂ being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of b₁
for b₃ being Element of b₁
for b₄, b₅ being Linear_Combination of b₂ holds b₃ * (b₄ + b₅) = (b₃ * b₄) + (b₃ * b₅)

proof end;

theorem Th64: :: VECTSP_6:64

for b₁ being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b₂ being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of b₁
for b₃, b₄ being Element of b₁
for b₅ being Linear_Combination of b₂ holds b₃ * (b₄ * b₅) = (b₃ * b₄) * b₅

proof end;

theorem Th65: :: VECTSP_6:65

proof end;

definition

let c₁ be non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr ;
let c₂ be non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of c₁;
let c₃ be Linear_Combination of c₂;
func - c₃ -> Linear_Combination of a₂ equals :: VECTSP_6:def 13
(- (1. a₁)) * a₃;
correctness ;
involutiveness

proof end;

end;

:: deftheorem Def13 defines - VECTSP_6:def 13 :

Lemma26: for b₁ being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b₂ being Element of b₁ holds (- (1. b₁)) * b₂ = - b₂

proof end;

theorem Th66: :: VECTSP_6:66

canceled;

theorem Th67: :: VECTSP_6:67

proof end;

theorem Th68: :: VECTSP_6:68

for b₁ being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b₂ being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of b₁
for b₃, b₄ being Linear_Combination of b₂ st b₃ + b₄ = ZeroLC b₂ holds
b₄ = - b₃

proof end;

Lemma28: for b₁ being Field holds - (1. b₁) <> 0. b₁

proof end;

Lemma29: for b₁ being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b₂ being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of b₁
for b₃ being Linear_Combination of b₂ holds Carrier (- b₃) c= Carrier b₃
by Th58;

theorem Th69: :: VECTSP_6:69

for b₁ being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b₂ being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of b₁
for b₃ being Linear_Combination of b₂ holds Carrier (- b₃) = Carrier b₃

proof end;

theorem Th70: :: VECTSP_6:70

for b₁ being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b₂ being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of b₁
for b₃ being Subset of b₂
for b₄ being Linear_Combination of b₂ st b₄ is Linear_Combination of b₃ holds
- b₄ is Linear_Combination of b₃ by Th61;

definition

let c₁ be non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr ;
let c₂ be non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of c₁;
let c₃, c₄ be Linear_Combination of c₂;
func c₃ - c₄ -> Linear_Combination of a₂ equals :: VECTSP_6:def 14
a₃ + (- a₄);
coherence ;

end;

:: deftheorem Def14 defines - VECTSP_6:def 14 :

theorem Th71: :: VECTSP_6:71

canceled;

theorem Th72: :: VECTSP_6:72

canceled;

theorem Th73: :: VECTSP_6:73

for b₁ being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b₂ being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of b₁
for b₃ being Element of b₂
for b₄, b₅ being Linear_Combination of b₂ holds (b₄ - b₅) . b₃ = (b₄ . b₃) - (b₅ . b₃)

proof end;

theorem Th74: :: VECTSP_6:74

for b₁ being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b₂ being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of b₁
for b₃, b₄ being Linear_Combination of b₂ holds Carrier (b₃ - b₄) c= (Carrier b₃) \/ (Carrier b₄)

proof end;

theorem Th75: :: VECTSP_6:75

for b₁ being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b₂ being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of b₁
for b₃ being Subset of b₂
for b₄, b₅ being Linear_Combination of b₂ st b₄ is Linear_Combination of b₃ & b₅ is Linear_Combination of b₃ holds
b₄ - b₅ is Linear_Combination of b₃

proof end;

theorem Th76: :: VECTSP_6:76

proof end;

theorem Th77: :: VECTSP_6:77

for b₁ being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b₂ being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of b₁
for b₃, b₄ being Linear_Combination of b₂ holds Sum (b₃ + b₄) = (Sum b₃) + (Sum b₄)

proof end;

theorem Th78: :: VECTSP_6:78

for b₁ being Field
for b₂ being VectSp of b₁
for b₃ being Linear_Combination of b₂
for b₄ being Element of b₁ holds Sum (b₄ * b₃) = b₄ * (Sum b₃)

proof end;

theorem Th79: :: VECTSP_6:79

proof end;

theorem Th80: :: VECTSP_6:80

for b₁ being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b₂ being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of b₁
for b₃, b₄ being Linear_Combination of b₂ holds Sum (b₃ - b₄) = (Sum b₃) - (Sum b₄)

proof end;

theorem Th81: :: VECTSP_6:81

for b₁ being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b₂ being Element of b₁ holds (- (1. b₁)) * b₂ = - b₂ by Lemma26;

theorem Th82: :: VECTSP_6:82

for b₁ being Field holds - (1. b₁) <> 0. b₁ by Lemma28;