:: RLVECT_2 semantic presentation

definition

let c₁ be 1-sorted ;
let c₂ be set ;
assume E1: c₂ in c₁ ;
func vector c₁,c₂ -> Element of a₁ equals :Def1: :: RLVECT_2:def 1
a₂;
coherence by E1, RLVECT_1:def 1;

end;

:: deftheorem Def1 defines vector RLVECT_2:def 1 :

theorem Th1: :: RLVECT_2:1

canceled;

theorem Th2: :: RLVECT_2:2

canceled;

theorem Th3: :: RLVECT_2:3

for b₁ being non empty 1-sorted
for b₂ being Element of b₁ holds vector b₁,b₂ = b₂

proof end;

theorem Th4: :: RLVECT_2:4

for b₁ being non empty Abelian add-associative right_zeroed right_complementable LoopStr
for b₂, b₃, b₄ being FinSequence of the carrier of b₁ st len b₂ = len b₃ & len b₂ = len b₄ & ( for b₅ being Nat st b₅ in dom b₂ holds
b₄ . b₅ = (b₂ /. b₅) + (b₃ /. b₅) ) holds
Sum b₄ = (Sum b₂) + (Sum b₃)

proof end;

theorem Th5: :: RLVECT_2:5

for b₁ being RealLinearSpace
for b₂ being Real
for b₃, b₄ being FinSequence of the carrier of b₁ st len b₃ = len b₄ & ( for b₅ being Nat st b₅ in dom b₃ holds
b₄ . b₅ = b₂ * (b₃ /. b₅) ) holds
Sum b₄ = b₂ * (Sum b₃)

proof end;

theorem Th6: :: RLVECT_2:6

for b₁ being non empty Abelian add-associative right_zeroed right_complementable LoopStr
for b₂, b₃ being FinSequence of the carrier of b₁ st len b₂ = len b₃ & ( for b₄ being Nat st b₄ in dom b₂ holds
b₃ . b₄ = - (b₂ /. b₄) ) holds
Sum b₃ = - (Sum b₂)

proof end;

theorem Th7: :: RLVECT_2:7

for b₁ being non empty Abelian add-associative right_zeroed right_complementable LoopStr
for b₂, b₃, b₄ being FinSequence of the carrier of b₁ st len b₂ = len b₃ & len b₂ = len b₄ & ( for b₅ being Nat st b₅ in dom b₂ holds
b₄ . b₅ = (b₂ /. b₅) - (b₃ /. b₅) ) holds
Sum b₄ = (Sum b₂) - (Sum b₃)

proof end;

Lemma5: for b₁, b₂ being Nat st b₁ < b₂ holds
b₂ - 1 is Nat
by NAT_1:60;

theorem Th8: :: RLVECT_2:8

for b₁ being non empty Abelian add-associative right_zeroed right_complementable LoopStr
for b₂, b₃ being FinSequence of the carrier of b₁
for b₄ being Permutation of dom b₂ st len b₂ = len b₃ & ( for b₅ being Nat st b₅ in dom b₃ holds
b₃ . b₅ = b₂ . (b₄ . b₅) ) holds
Sum b₂ = Sum b₃

proof end;

theorem Th9: :: RLVECT_2:9

for b₁ being non empty Abelian add-associative right_zeroed right_complementable LoopStr
for b₂, b₃ being FinSequence of the carrier of b₁
for b₄ being Permutation of dom b₂ st b₃ = b₂ * b₄ holds
Sum b₂ = Sum b₃

proof end;

registration

let c₁ be 1-sorted ;
cluster empty finite Element of bool the carrier of a₁;
existence

proof end;

end;

definition

let c₁ be 1-sorted ;
let c₂, c₃ be finite Subset of c₁;
redefine func \/ as c₂ \/ c₃ -> finite Subset of a₁;
coherence

proof end;

redefine func /\ as c₂ /\ c₃ -> finite Subset of a₁;
coherence

proof end;

redefine func \ as c₂ \ c₃ -> finite Subset of a₁;
coherence

proof end;

redefine func \+\ as c₂ \+\ c₃ -> finite Subset of a₁;
coherence

proof end;

end;

definition

let c₁ be non empty LoopStr ;
let c₂ be finite Subset of c₁;
assume E7: ( c₁ is Abelian & c₁ is add-associative & c₁ is right_zeroed ) ;
canceled;
canceled;
func Sum c₂ -> Element of a₁ means :Def4: :: RLVECT_2:def 4
ex b₁ being FinSequence of the carrier of a₁ st
( rng b₁ = a₂ & b₁ is one-to-one & a₃ = Sum b₁ );
existence

proof end;

uniqueness by E7, RLVECT_1:59;

end;

:: deftheorem Def2 RLVECT_2:def 2 :

:: deftheorem Def3 RLVECT_2:def 3 :

:: deftheorem Def4 defines Sum RLVECT_2:def 4 :

registration

let c₁ be non empty 1-sorted ;
cluster non empty finite Element of bool the carrier of a₁;
existence

proof end;

end;

definition

let c₁ be non empty 1-sorted ;
let c₂ be Element of c₁;
redefine func { as {c₂} -> finite Subset of a₁;
coherence

proof end;

end;

definition

let c₁ be non empty 1-sorted ;
let c₂, c₃ be Element of c₁;
redefine func { as {c₂,c₃} -> finite Subset of a₁;
coherence

proof end;

end;

definition

let c₁ be non empty 1-sorted ;
let c₂, c₃, c₄ be Element of c₁;
redefine func { as {c₂,c₃,c₄} -> finite Subset of a₁;
coherence

proof end;

end;

theorem Th10: :: RLVECT_2:10

canceled;

theorem Th11: :: RLVECT_2:11

canceled;

theorem Th12: :: RLVECT_2:12

canceled;

theorem Th13: :: RLVECT_2:13

canceled;

theorem Th14: :: RLVECT_2:14

for b₁ being non empty Abelian add-associative right_zeroed LoopStr holds Sum ({} b₁) = 0. b₁

proof end;

theorem Th15: :: RLVECT_2:15

for b₁ being non empty Abelian add-associative right_zeroed right_complementable LoopStr
for b₂ being Element of b₁ holds Sum {b₂} = b₂

proof end;

theorem Th16: :: RLVECT_2:16

for b₁ being non empty Abelian add-associative right_zeroed right_complementable LoopStr
for b₂, b₃ being Element of b₁ st b₂ <> b₃ holds
Sum {b₂,b₃} = b₂ + b₃

proof end;

theorem Th17: :: RLVECT_2:17

for b₁ being non empty Abelian add-associative right_zeroed right_complementable LoopStr
for b₂, b₃, b₄ being Element of b₁ st b₂ <> b₃ & b₃ <> b₄ & b₂ <> b₄ holds
Sum {b₂,b₃,b₄} = (b₂ + b₃) + b₄

proof end;

theorem Th18: :: RLVECT_2:18

for b₁ being non empty Abelian add-associative right_zeroed LoopStr
for b₂, b₃ being finite Subset of b₁ st b₃ misses b₂ holds
Sum (b₃ \/ b₂) = (Sum b₃) + (Sum b₂)

proof end;

theorem Th19: :: RLVECT_2:19

for b₁ being non empty Abelian add-associative right_zeroed right_complementable LoopStr
for b₂, b₃ being finite Subset of b₁ holds Sum (b₃ \/ b₂) = ((Sum b₃) + (Sum b₂)) - (Sum (b₃ /\ b₂))

proof end;

theorem Th20: :: RLVECT_2:20

for b₁ being non empty Abelian add-associative right_zeroed right_complementable LoopStr
for b₂, b₃ being finite Subset of b₁ holds Sum (b₃ /\ b₂) = ((Sum b₃) + (Sum b₂)) - (Sum (b₃ \/ b₂))

proof end;

theorem Th21: :: RLVECT_2:21

for b₁ being non empty Abelian add-associative right_zeroed right_complementable LoopStr
for b₂, b₃ being finite Subset of b₁ holds Sum (b₃ \ b₂) = (Sum (b₃ \/ b₂)) - (Sum b₂)

proof end;

theorem Th22: :: RLVECT_2:22

for b₁ being non empty Abelian add-associative right_zeroed right_complementable LoopStr
for b₂, b₃ being finite Subset of b₁ holds Sum (b₃ \ b₂) = (Sum b₃) - (Sum (b₃ /\ b₂))

proof end;

theorem Th23: :: RLVECT_2:23

for b₁ being non empty Abelian add-associative right_zeroed right_complementable LoopStr
for b₂, b₃ being finite Subset of b₁ holds Sum (b₃ \+\ b₂) = (Sum (b₃ \/ b₂)) - (Sum (b₃ /\ b₂))

proof end;

theorem Th24: :: RLVECT_2:24

for b₁ being non empty Abelian add-associative right_zeroed LoopStr
for b₂, b₃ being finite Subset of b₁ holds Sum (b₃ \+\ b₂) = (Sum (b₃ \ b₂)) + (Sum (b₂ \ b₃))

proof end;

definition

let c₁ be non empty ZeroStr ;
mode Linear_Combination of c₁ -> Element of Funcs the carrier of a₁,REAL means :Def5: :: RLVECT_2:def 5
ex b₁ being finite Subset of a₁ st
for b₂ being Element of a₁ st not b₂ in b₁ holds
a₂ . b₂ = 0;
existence

proof end;

end;

:: deftheorem Def5 defines Linear_Combination RLVECT_2:def 5 :

definition

let c₁ be non empty LoopStr ;
let c₂ be Linear_Combination of c₁;
func Carrier c₂ -> finite Subset of a₁ equals :: RLVECT_2:def 6
{ b₁ where B is Element of a₁ : a₂ . b₁ <> 0 } ;
coherence

proof end;

end;

:: deftheorem Def6 defines Carrier RLVECT_2:def 6 :

theorem Th25: :: RLVECT_2:25

canceled;

theorem Th26: :: RLVECT_2:26

canceled;

theorem Th27: :: RLVECT_2:27

canceled;

theorem Th28: :: RLVECT_2:28

for b₁ being non empty LoopStr
for b₂ being Linear_Combination of b₁
for b₃ being Element of b₁ holds
( b₂ . b₃ = 0 iff not b₃ in Carrier b₂ )

proof end;

definition

let c₁ be non empty LoopStr ;
func ZeroLC c₁ -> Linear_Combination of a₁ means :Def7: :: RLVECT_2:def 7
Carrier a₂ = {} ;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def7 defines ZeroLC RLVECT_2:def 7 :

theorem Th29: :: RLVECT_2:29

canceled;

theorem Th30: :: RLVECT_2:30

for b₁ being non empty LoopStr
for b₂ being Element of b₁ holds (ZeroLC b₁) . b₂ = 0

proof end;

definition

let c₁ be non empty LoopStr ;
let c₂ be Subset of c₁;
mode Linear_Combination of c₂ -> Linear_Combination of a₁ means :Def8: :: RLVECT_2:def 8
Carrier a₃ c= a₂;
existence

proof end;

end;

:: deftheorem Def8 defines Linear_Combination RLVECT_2:def 8 :

theorem Th31: :: RLVECT_2:31

canceled;

theorem Th32: :: RLVECT_2:32

canceled;

theorem Th33: :: RLVECT_2:33

for b₁ being RealLinearSpace
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 Th34: :: RLVECT_2:34

for b₁ being RealLinearSpace
for b₂ being Subset of b₁ holds ZeroLC b₁ is Linear_Combination of b₂

proof end;

theorem Th35: :: RLVECT_2:35

for b₁ being RealLinearSpace
for b₂ being Linear_Combination of {} the carrier of b₁ holds b₂ = ZeroLC b₁

proof end;

definition

let c₁ be RealLinearSpace;
let c₂ be FinSequence of the carrier of c₁;
let c₃ be Function of the carrier of c₁, REAL ;
func c₃ (#) c₂ -> FinSequence of the carrier of a₁ means :Def9: :: RLVECT_2:def 9
( 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 Def9 defines (#) RLVECT_2:def 9 :

theorem Th36: :: RLVECT_2:36

canceled;

theorem Th37: :: RLVECT_2:37

canceled;

theorem Th38: :: RLVECT_2:38

canceled;

theorem Th39: :: RLVECT_2:39

canceled;

theorem Th40: :: RLVECT_2:40

for b₁ being Nat
for b₂ being RealLinearSpace
for b₃ being VECTOR of b₂
for b₄ being FinSequence of the carrier of b₂
for b₅ being Function of the carrier of b₂, REAL st b₁ in dom b₄ & b₃ = b₄ . b₁ holds
(b₅ (#) b₄) . b₁ = (b₅ . b₃) * b₃

proof end;

theorem Th41: :: RLVECT_2:41

for b₁ being RealLinearSpace
for b₂ being Function of the carrier of b₁, REAL holds b₂ (#) (<*> the carrier of b₁) = <*> the carrier of b₁

proof end;

theorem Th42: :: RLVECT_2:42

for b₁ being RealLinearSpace
for b₂ being VECTOR of b₁
for b₃ being Function of the carrier of b₁, REAL holds b₃ (#) <*b₂*> = <*((b₃ . b₂) * b₂)*>

proof end;

theorem Th43: :: RLVECT_2:43

for b₁ being RealLinearSpace
for b₂, b₃ being VECTOR of b₁
for b₄ being Function of the carrier of b₁, REAL holds b₄ (#) <*b₂,b₃*> = <*((b₄ . b₂) * b₂),((b₄ . b₃) * b₃)*>

proof end;

theorem Th44: :: RLVECT_2:44

for b₁ being RealLinearSpace
for b₂, b₃, b₄ being VECTOR of b₁
for b₅ being Function of the carrier of b₁, REAL holds b₅ (#) <*b₂,b₃,b₄*> = <*((b₅ . b₂) * b₂),((b₅ . b₃) * b₃),((b₅ . b₄) * b₄)*>

proof end;

definition

let c₁ be RealLinearSpace;
let c₂ be Linear_Combination of c₁;
func Sum c₂ -> Element of a₁ means :Def10: :: RLVECT_2:def 10
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 Def10 defines Sum RLVECT_2:def 10 :

Lemma24: for b₁ being RealLinearSpace holds Sum (ZeroLC b₁) = 0. b₁

proof end;

theorem Th45: :: RLVECT_2:45

canceled;

theorem Th46: :: RLVECT_2:46

canceled;

theorem Th47: :: RLVECT_2:47

for b₁ being RealLinearSpace
for b₂ being Subset of b₁ holds
( ( b₂ <> {} & b₂ is lineary-closed ) iff for b₃ being Linear_Combination of b₂ holds Sum b₃ in b₂ )

proof end;

theorem Th48: :: RLVECT_2:48

for b₁ being RealLinearSpace holds Sum (ZeroLC b₁) = 0. b₁ by Lemma24;

theorem Th49: :: RLVECT_2:49

for b₁ being RealLinearSpace
for b₂ being Linear_Combination of {} the carrier of b₁ holds Sum b₂ = 0. b₁

proof end;

theorem Th50: :: RLVECT_2:50

for b₁ being RealLinearSpace
for b₂ being VECTOR of b₁
for b₃ being Linear_Combination of {b₂} holds Sum b₃ = (b₃ . b₂) * b₂

proof end;

theorem Th51: :: RLVECT_2:51

for b₁ being RealLinearSpace
for b₂, b₃ being VECTOR 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 Th52: :: RLVECT_2:52

for b₁ being RealLinearSpace
for b₂ being Linear_Combination of b₁ st Carrier b₂ = {} holds
Sum b₂ = 0. b₁

proof end;

theorem Th53: :: RLVECT_2:53

for b₁ being RealLinearSpace
for b₂ being VECTOR of b₁
for b₃ being Linear_Combination of b₁ st Carrier b₃ = {b₂} holds
Sum b₃ = (b₃ . b₂) * b₂

proof end;

theorem Th54: :: RLVECT_2:54

for b₁ being RealLinearSpace
for b₂, b₃ being VECTOR 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 LoopStr ;
let c₂, c₃ be Linear_Combination of c₁;
redefine pred = as c₂ = c₃ means :: RLVECT_2:def 11
for b₁ being Element of a₁ holds a₂ . b₁ = a₃ . b₁;
compatibility by FUNCT_2:113;

end;

:: deftheorem Def11 defines = RLVECT_2:def 11 :

definition

let c₁ be non empty LoopStr ;
let c₂, c₃ be Linear_Combination of c₁;
func c₂ + c₃ -> Linear_Combination of a₁ means :Def12: :: RLVECT_2:def 12
for b₁ being Element of a₁ holds a₄ . b₁ = (a₂ . b₁) + (a₃ . b₁);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def12 defines + RLVECT_2:def 12 :

theorem Th55: :: RLVECT_2:55

canceled;

theorem Th56: :: RLVECT_2:56

canceled;

theorem Th57: :: RLVECT_2:57

canceled;

theorem Th58: :: RLVECT_2:58

for b₁ being RealLinearSpace
for b₂, b₃ being Linear_Combination of b₁ holds Carrier (b₂ + b₃) c= (Carrier b₂) \/ (Carrier b₃)

proof end;

theorem Th59: :: RLVECT_2:59

for b₁ being RealLinearSpace
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 Th60: :: RLVECT_2:60

for b₁ being non empty LoopStr
for b₂, b₃ being Linear_Combination of b₁ holds b₂ + b₃ = b₃ + b₂

proof end;

theorem Th61: :: RLVECT_2:61

for b₁ being RealLinearSpace
for b₂, b₃, b₄ being Linear_Combination of b₁ holds b₂ + (b₃ + b₄) = (b₂ + b₃) + b₄

proof end;

theorem Th62: :: RLVECT_2:62

for b₁ being RealLinearSpace
for b₂ being Linear_Combination of b₁ holds
( b₂ + (ZeroLC b₁) = b₂ & (ZeroLC b₁) + b₂ = b₂ )

proof end;

definition

let c₁ be RealLinearSpace;
let c₂ be Real;
let c₃ be Linear_Combination of c₁;
func c₂ * c₃ -> Linear_Combination of a₁ means :Def13: :: RLVECT_2:def 13
for b₁ being VECTOR of a₁ holds a₄ . b₁ = a₂ * (a₃ . b₁);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def13 defines * RLVECT_2:def 13 :

theorem Th63: :: RLVECT_2:63

canceled;

theorem Th64: :: RLVECT_2:64

canceled;

theorem Th65: :: RLVECT_2:65

for b₁ being RealLinearSpace
for b₂ being Real
for b₃ being Linear_Combination of b₁ st b₂ <> 0 holds
Carrier (b₂ * b₃) = Carrier b₃

proof end;

theorem Th66: :: RLVECT_2:66

for b₁ being RealLinearSpace
for b₂ being Linear_Combination of b₁ holds 0 * b₂ = ZeroLC b₁

proof end;

theorem Th67: :: RLVECT_2:67

for b₁ being RealLinearSpace
for b₂ being Real
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 Th68: :: RLVECT_2:68

for b₁ being RealLinearSpace
for b₂, b₃ being Real
for b₄ being Linear_Combination of b₁ holds (b₂ + b₃) * b₄ = (b₂ * b₄) + (b₃ * b₄)

proof end;

theorem Th69: :: RLVECT_2:69

for b₁ being RealLinearSpace
for b₂ being Real
for b₃, b₄ being Linear_Combination of b₁ holds b₂ * (b₃ + b₄) = (b₂ * b₃) + (b₂ * b₄)

proof end;

theorem Th70: :: RLVECT_2:70

for b₁ being RealLinearSpace
for b₂, b₃ being Real
for b₄ being Linear_Combination of b₁ holds b₂ * (b₃ * b₄) = (b₂ * b₃) * b₄

proof end;

theorem Th71: :: RLVECT_2:71

for b₁ being RealLinearSpace
for b₂ being Linear_Combination of b₁ holds 1 * b₂ = b₂

proof end;

definition

let c₁ be RealLinearSpace;
let c₂ be Linear_Combination of c₁;
func - c₂ -> Linear_Combination of a₁ equals :: RLVECT_2:def 14
(- 1) * a₂;
correctness ;

end;

:: deftheorem Def14 defines - RLVECT_2:def 14 :

theorem Th72: :: RLVECT_2:72

canceled;

theorem Th73: :: RLVECT_2:73

for b₁ being RealLinearSpace
for b₂ being VECTOR of b₁
for b₃ being Linear_Combination of b₁ holds (- b₃) . b₂ = - (b₃ . b₂)

proof end;

theorem Th74: :: RLVECT_2:74

for b₁ being RealLinearSpace
for b₂, b₃ being Linear_Combination of b₁ st b₂ + b₃ = ZeroLC b₁ holds
b₃ = - b₂

proof end;

theorem Th75: :: RLVECT_2:75

for b₁ being RealLinearSpace
for b₂ being Linear_Combination of b₁ holds Carrier (- b₂) = Carrier b₂ by Th65;

theorem Th76: :: RLVECT_2:76

for b₁ being RealLinearSpace
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 Th67;

theorem Th77: :: RLVECT_2:77

for b₁ being RealLinearSpace
for b₂ being Linear_Combination of b₁ holds - (- b₂) = b₂

proof end;

definition

let c₁ be RealLinearSpace;
let c₂, c₃ be Linear_Combination of c₁;
func c₂ - c₃ -> Linear_Combination of a₁ equals :: RLVECT_2:def 15
a₂ + (- a₃);
correctness ;

end;

:: deftheorem Def15 defines - RLVECT_2:def 15 :

theorem Th78: :: RLVECT_2:78

canceled;

theorem Th79: :: RLVECT_2:79

for b₁ being RealLinearSpace
for b₂ being VECTOR of b₁
for b₃, b₄ being Linear_Combination of b₁ holds (b₃ - b₄) . b₂ = (b₃ . b₂) - (b₄ . b₂)

proof end;

theorem Th80: :: RLVECT_2:80

for b₁ being RealLinearSpace
for b₂, b₃ being Linear_Combination of b₁ holds Carrier (b₂ - b₃) c= (Carrier b₂) \/ (Carrier b₃)

proof end;

theorem Th81: :: RLVECT_2:81

for b₁ being RealLinearSpace
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 Th82: :: RLVECT_2:82

for b₁ being RealLinearSpace
for b₂ being Linear_Combination of b₁ holds b₂ - b₂ = ZeroLC b₁

proof end;

definition

let c₁ be RealLinearSpace;
func LinComb c₁ -> set means :Def16: :: RLVECT_2:def 16
for b₁ being set holds
( b₁ in a₂ iff b₁ is Linear_Combination of a₁ );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def16 defines LinComb RLVECT_2:def 16 :

registration

let c₁ be RealLinearSpace;
cluster LinComb a₁ -> non empty ;
coherence

proof end;

end;

definition

let c₁ be RealLinearSpace;
let c₂ be Element of LinComb c₁;
func @ c₂ -> Linear_Combination of a₁ equals :: RLVECT_2:def 17
a₂;
coherence by Def16;

end;

:: deftheorem Def17 defines @ RLVECT_2:def 17 :

definition

let c₁ be RealLinearSpace;
let c₂ be Linear_Combination of c₁;
func @ c₂ -> Element of LinComb a₁ equals :: RLVECT_2:def 18
a₂;
coherence by Def16;

end;

:: deftheorem Def18 defines @ RLVECT_2:def 18 :

definition

let c₁ be RealLinearSpace;
func LCAdd c₁ -> BinOp of LinComb a₁ means :Def19: :: RLVECT_2:def 19
for b₁, b₂ being Element of LinComb a₁ holds a₂ . b₁,b₂ = (@ b₁) + (@ b₂);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def19 defines LCAdd RLVECT_2:def 19 :

definition

let c₁ be RealLinearSpace;
func LCMult c₁ -> Function of [:REAL ,(LinComb a₁):], LinComb a₁ means :Def20: :: RLVECT_2:def 20
for b₁ being Real
for b₂ being Element of LinComb a₁ holds a₂ . [b₁,b₂] = b₁ * (@ b₂);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def20 defines LCMult RLVECT_2:def 20 :

definition

let c₁ be RealLinearSpace;
func LC_RLSpace c₁ -> RealLinearSpace equals :: RLVECT_2:def 21
RLSStruct(# (LinComb a₁),(@ (ZeroLC a₁)),(LCAdd a₁),(LCMult a₁) #);
coherence

proof end;

end;

:: deftheorem Def21 defines LC_RLSpace RLVECT_2:def 21 :

registration

let c₁ be RealLinearSpace;
cluster LC_RLSpace a₁ -> strict ;
coherence ;

end;

theorem Th83: :: RLVECT_2:83

canceled;

theorem Th84: :: RLVECT_2:84

canceled;

theorem Th85: :: RLVECT_2:85

canceled;

theorem Th86: :: RLVECT_2:86

canceled;

theorem Th87: :: RLVECT_2:87

canceled;

theorem Th88: :: RLVECT_2:88

canceled;

theorem Th89: :: RLVECT_2:89

canceled;

theorem Th90: :: RLVECT_2:90

canceled;

theorem Th91: :: RLVECT_2:91

canceled;

theorem Th92: :: RLVECT_2:92

for b₁ being RealLinearSpace holds the carrier of (LC_RLSpace b₁) = LinComb b₁ ;

theorem Th93: :: RLVECT_2:93

for b₁ being RealLinearSpace holds the Zero of (LC_RLSpace b₁) = ZeroLC b₁ ;

theorem Th94: :: RLVECT_2:94

for b₁ being RealLinearSpace holds the add of (LC_RLSpace b₁) = LCAdd b₁ ;

theorem Th95: :: RLVECT_2:95

for b₁ being RealLinearSpace holds the Mult of (LC_RLSpace b₁) = LCMult b₁ ;

theorem Th96: :: RLVECT_2:96

for b₁ being RealLinearSpace
for b₂, b₃ being Linear_Combination of b₁ holds (vector (LC_RLSpace b₁),b₂) + (vector (LC_RLSpace b₁),b₃) = b₂ + b₃

proof end;

theorem Th97: :: RLVECT_2:97

for b₁ being RealLinearSpace
for b₂ being Real
for b₃ being Linear_Combination of b₁ holds b₂ * (vector (LC_RLSpace b₁),b₃) = b₂ * b₃

proof end;

theorem Th98: :: RLVECT_2:98

for b₁ being RealLinearSpace
for b₂ being Linear_Combination of b₁ holds - (vector (LC_RLSpace b₁),b₂) = - b₂

proof end;

theorem Th99: :: RLVECT_2:99

for b₁ being RealLinearSpace
for b₂, b₃ being Linear_Combination of b₁ holds (vector (LC_RLSpace b₁),b₂) - (vector (LC_RLSpace b₁),b₃) = b₂ - b₃

proof end;

definition

let c₁ be RealLinearSpace;
let c₂ be Subset of c₁;
func LC_RLSpace c₂ -> strict Subspace of LC_RLSpace a₁ means :: RLVECT_2:def 22
the carrier of a₃ = { b₁ where B is Linear_Combination of a₂ : verum } ;
existence

proof end;

uniqueness by RLSUB_1:38;

end;

:: deftheorem Def22 defines LC_RLSpace RLVECT_2:def 22 :