:: RLVECT_4 semantic presentation

scheme :: RLVECT_4:sch 1
s1{ F₁() -> non empty set , F₂() -> non empty set , F₃() -> Element of F₁(), F₄() -> Element of F₁(), F₅() -> Element of F₁(), F₆() -> Element of F₂(), F₇() -> Element of F₂(), F₈() -> Element of F₂(), F₉( set ) -> Element of F₂() } :

ex b₁ being Function of F₁(),F₂() st
( b₁ . F₃() = F₆() & b₁ . F₄() = F₇() & b₁ . F₅() = F₈() & ( for b₂ being Element of F₁() st b₂ <> F₃() & b₂ <> F₄() & b₂ <> F₅() holds
b₁ . b₂ = F₉(b₂) ) )

provided

E1: F₃() <> F₄() and
E2: F₃() <> F₅() and
E3: F₄() <> F₅()

proof end;

scheme :: RLVECT_4:sch 2
s2{ F₁() -> RealLinearSpace, F₂() -> VECTOR of F₁(), F₃() -> Real } :

ex b₁ being Linear_Combination of {F₂()} st b₁ . F₂() = F₃()

proof end;

scheme :: RLVECT_4:sch 3
s3{ F₁() -> RealLinearSpace, F₂() -> VECTOR of F₁(), F₃() -> VECTOR of F₁(), F₄() -> Real, F₅() -> Real } :

ex b₁ being Linear_Combination of {F₂(),F₃()} st
( b₁ . F₂() = F₄() & b₁ . F₃() = F₅() )

provided

E1: F₂() <> F₃()

proof end;

scheme :: RLVECT_4:sch 4
s4{ F₁() -> RealLinearSpace, F₂() -> VECTOR of F₁(), F₃() -> VECTOR of F₁(), F₄() -> VECTOR of F₁(), F₅() -> Real, F₆() -> Real, F₇() -> Real } :

ex b₁ being Linear_Combination of {F₂(),F₃(),F₄()} st
( b₁ . F₂() = F₅() & b₁ . F₃() = F₆() & b₁ . F₄() = F₇() )

provided

E1: F₂() <> F₃() and
E2: F₂() <> F₄() and
E3: F₃() <> F₄()

proof end;

theorem Th1: :: RLVECT_4:1

for b₁ being RealLinearSpace
for b₂, b₃ being VECTOR of b₁ holds
( (b₂ + b₃) - b₂ = b₃ & (b₃ + b₂) - b₂ = b₃ & (b₂ - b₂) + b₃ = b₃ & (b₃ - b₂) + b₂ = b₃ & b₂ + (b₃ - b₂) = b₃ & b₃ + (b₂ - b₂) = b₃ & b₂ - (b₂ - b₃) = b₃ )

proof end;

theorem Th2: :: RLVECT_4:2

for b₁ being RealLinearSpace
for b₂, b₃, b₄ being VECTOR of b₁ holds (b₂ + b₃) - b₄ = (b₂ - b₄) + b₃ by RLVECT_1:def 6;

theorem Th3: :: RLVECT_4:3

canceled;

theorem Th4: :: RLVECT_4:4

for b₁ being RealLinearSpace
for b₂, b₃, b₄ being VECTOR of b₁ st b₂ - b₃ = b₄ - b₃ holds
b₂ = b₄

proof end;

theorem Th5: :: RLVECT_4:5

canceled;

theorem Th6: :: RLVECT_4:6

for b₁ being Real
for b₂ being RealLinearSpace
for b₃ being VECTOR of b₂ holds - (b₁ * b₃) = (- b₁) * b₃

proof end;

theorem Th7: :: RLVECT_4:7

for b₁ being RealLinearSpace
for b₂ being VECTOR of b₁
for b₃, b₄ being Subspace of b₁ st b₃ is Subspace of b₄ holds
b₂ + b₃ c= b₂ + b₄

proof end;

theorem Th8: :: RLVECT_4:8

for b₁ being RealLinearSpace
for b₂, b₃ being VECTOR of b₁
for b₄ being Subspace of b₁ st b₂ in b₃ + b₄ holds
b₃ + b₄ = b₂ + b₄

proof end;

theorem Th9: :: RLVECT_4:9

for b₁ being RealLinearSpace
for b₂, b₃, b₄ being VECTOR of b₁
for b₅ being Linear_Combination of {b₂,b₃,b₄} st b₂ <> b₃ & b₂ <> b₄ & b₃ <> b₄ holds
Sum b₅ = (((b₅ . b₂) * b₂) + ((b₅ . b₃) * b₃)) + ((b₅ . b₄) * b₄)

proof end;

theorem Th10: :: RLVECT_4:10

for b₁ being RealLinearSpace
for b₂, b₃, b₄ being VECTOR of b₁ holds
( ( b₂ <> b₃ & b₂ <> b₄ & b₃ <> b₄ & {b₂,b₃,b₄} is linearly-independent ) iff for b₅, b₆, b₇ being Real st ((b₅ * b₂) + (b₆ * b₃)) + (b₇ * b₄) = 0. b₁ holds
( b₅ = 0 & b₆ = 0 & b₇ = 0 ) )

proof end;

theorem Th11: :: RLVECT_4:11

for b₁ being set
for b₂ being RealLinearSpace
for b₃ being VECTOR of b₂ holds
( b₁ in Lin {b₃} iff ex b₄ being Real st b₁ = b₄ * b₃ )

proof end;

theorem Th12: :: RLVECT_4:12

for b₁ being RealLinearSpace
for b₂ being VECTOR of b₁ holds b₂ in Lin {b₂}

proof end;

theorem Th13: :: RLVECT_4:13

for b₁ being set
for b₂ being RealLinearSpace
for b₃, b₄ being VECTOR of b₂ holds
( b₁ in b₃ + (Lin {b₄}) iff ex b₅ being Real st b₁ = b₃ + (b₅ * b₄) )

proof end;

theorem Th14: :: RLVECT_4:14

for b₁ being set
for b₂ being RealLinearSpace
for b₃, b₄ being VECTOR of b₂ holds
( b₁ in Lin {b₃,b₄} iff ex b₅, b₆ being Real st b₁ = (b₅ * b₃) + (b₆ * b₄) )

proof end;

theorem Th15: :: RLVECT_4:15

for b₁ being RealLinearSpace
for b₂, b₃ being VECTOR of b₁ holds
( b₂ in Lin {b₂,b₃} & b₃ in Lin {b₂,b₃} )

proof end;

theorem Th16: :: RLVECT_4:16

for b₁ being set
for b₂ being RealLinearSpace
for b₃, b₄, b₅ being VECTOR of b₂ holds
( b₁ in b₃ + (Lin {b₄,b₅}) iff ex b₆, b₇ being Real st b₁ = (b₃ + (b₆ * b₄)) + (b₇ * b₅) )

proof end;

theorem Th17: :: RLVECT_4:17

for b₁ being set
for b₂ being RealLinearSpace
for b₃, b₄, b₅ being VECTOR of b₂ holds
( b₁ in Lin {b₃,b₄,b₅} iff ex b₆, b₇, b₈ being Real st b₁ = ((b₆ * b₃) + (b₇ * b₄)) + (b₈ * b₅) )

proof end;

theorem Th18: :: RLVECT_4:18

for b₁ being RealLinearSpace
for b₂, b₃, b₄ being VECTOR of b₁ holds
( b₂ in Lin {b₂,b₃,b₄} & b₃ in Lin {b₂,b₃,b₄} & b₄ in Lin {b₂,b₃,b₄} )

proof end;

theorem Th19: :: RLVECT_4:19

for b₁ being set
for b₂ being RealLinearSpace
for b₃, b₄, b₅, b₆ being VECTOR of b₂ holds
( b₁ in b₃ + (Lin {b₄,b₅,b₆}) iff ex b₇, b₈, b₉ being Real st b₁ = ((b₃ + (b₇ * b₄)) + (b₈ * b₅)) + (b₉ * b₆) )

proof end;

theorem Th20: :: RLVECT_4:20

for b₁ being RealLinearSpace
for b₂, b₃ being VECTOR of b₁ st {b₂,b₃} is linearly-independent & b₂ <> b₃ holds
{b₂,(b₃ - b₂)} is linearly-independent

proof end;

theorem Th21: :: RLVECT_4:21

for b₁ being RealLinearSpace
for b₂, b₃ being VECTOR of b₁ st {b₂,b₃} is linearly-independent & b₂ <> b₃ holds
{b₂,(b₃ + b₂)} is linearly-independent

proof end;

theorem Th22: :: RLVECT_4:22

for b₁ being Real
for b₂ being RealLinearSpace
for b₃, b₄ being VECTOR of b₂ st {b₃,b₄} is linearly-independent & b₃ <> b₄ & b₁ <> 0 holds
{b₃,(b₁ * b₄)} is linearly-independent

proof end;

theorem Th23: :: RLVECT_4:23

for b₁ being RealLinearSpace
for b₂, b₃ being VECTOR of b₁ st {b₂,b₃} is linearly-independent & b₂ <> b₃ holds
{b₂,(- b₃)} is linearly-independent

proof end;

theorem Th24: :: RLVECT_4:24

for b₁, b₂ being Real
for b₃ being RealLinearSpace
for b₄ being VECTOR of b₃ st b₁ <> b₂ holds
not {(b₁ * b₄),(b₂ * b₄)} is linearly-independent

proof end;

theorem Th25: :: RLVECT_4:25

for b₁ being Real
for b₂ being RealLinearSpace
for b₃ being VECTOR of b₂ st b₁ <> 1 holds
not {b₃,(b₁ * b₃)} is linearly-independent

proof end;

theorem Th26: :: RLVECT_4:26

for b₁ being RealLinearSpace
for b₂, b₃, b₄ being VECTOR of b₁ st {b₂,b₃,b₄} is linearly-independent & b₂ <> b₄ & b₂ <> b₃ & b₄ <> b₃ holds
{b₂,b₃,(b₄ - b₂)} is linearly-independent

proof end;

theorem Th27: :: RLVECT_4:27

for b₁ being RealLinearSpace
for b₂, b₃, b₄ being VECTOR of b₁ st {b₂,b₃,b₄} is linearly-independent & b₂ <> b₄ & b₂ <> b₃ & b₄ <> b₃ holds
{b₂,(b₃ - b₂),(b₄ - b₂)} is linearly-independent

proof end;

theorem Th28: :: RLVECT_4:28

for b₁ being RealLinearSpace
for b₂, b₃, b₄ being VECTOR of b₁ st {b₂,b₃,b₄} is linearly-independent & b₂ <> b₄ & b₂ <> b₃ & b₄ <> b₃ holds
{b₂,b₃,(b₄ + b₂)} is linearly-independent

proof end;

theorem Th29: :: RLVECT_4:29

for b₁ being RealLinearSpace
for b₂, b₃, b₄ being VECTOR of b₁ st {b₂,b₃,b₄} is linearly-independent & b₂ <> b₄ & b₂ <> b₃ & b₄ <> b₃ holds
{b₂,(b₃ + b₂),(b₄ + b₂)} is linearly-independent

proof end;

theorem Th30: :: RLVECT_4:30

for b₁ being Real
for b₂ being RealLinearSpace
for b₃, b₄, b₅ being VECTOR of b₂ st {b₃,b₄,b₅} is linearly-independent & b₃ <> b₅ & b₃ <> b₄ & b₅ <> b₄ & b₁ <> 0 holds
{b₃,b₄,(b₁ * b₅)} is linearly-independent

proof end;

theorem Th31: :: RLVECT_4:31

for b₁, b₂ being Real
for b₃ being RealLinearSpace
for b₄, b₅, b₆ being VECTOR of b₃ st {b₄,b₅,b₆} is linearly-independent & b₄ <> b₆ & b₄ <> b₅ & b₆ <> b₅ & b₁ <> 0 & b₂ <> 0 holds
{b₄,(b₁ * b₅),(b₂ * b₆)} is linearly-independent

proof end;

theorem Th32: :: RLVECT_4:32

for b₁ being RealLinearSpace
for b₂, b₃, b₄ being VECTOR of b₁ st {b₂,b₃,b₄} is linearly-independent & b₂ <> b₄ & b₂ <> b₃ & b₄ <> b₃ holds
{b₂,b₃,(- b₄)} is linearly-independent

proof end;

theorem Th33: :: RLVECT_4:33

for b₁ being RealLinearSpace
for b₂, b₃, b₄ being VECTOR of b₁ st {b₂,b₃,b₄} is linearly-independent & b₂ <> b₄ & b₂ <> b₃ & b₄ <> b₃ holds
{b₂,(- b₃),(- b₄)} is linearly-independent

proof end;

theorem Th34: :: RLVECT_4:34

for b₁, b₂ being Real
for b₃ being RealLinearSpace
for b₄, b₅ being VECTOR of b₃ st b₁ <> b₂ holds
not {(b₁ * b₄),(b₂ * b₄),b₅} is linearly-independent

proof end;

theorem Th35: :: RLVECT_4:35

for b₁ being Real
for b₂ being RealLinearSpace
for b₃, b₄ being VECTOR of b₂ st b₁ <> 1 holds
not {b₃,(b₁ * b₃),b₄} is linearly-independent

proof end;

theorem Th36: :: RLVECT_4:36

for b₁ being RealLinearSpace
for b₂, b₃ being VECTOR of b₁ st b₂ in Lin {b₃} & b₂ <> 0. b₁ holds
Lin {b₂} = Lin {b₃}

proof end;

theorem Th37: :: RLVECT_4:37

for b₁ being RealLinearSpace
for b₂, b₃, b₄, b₅ being VECTOR of b₁ st b₂ <> b₃ & {b₂,b₃} is linearly-independent & b₂ in Lin {b₄,b₅} & b₃ in Lin {b₄,b₅} holds
( Lin {b₄,b₅} = Lin {b₂,b₃} & {b₄,b₅} is linearly-independent & b₄ <> b₅ )

proof end;

theorem Th38: :: RLVECT_4:38

for b₁ being RealLinearSpace
for b₂, b₃ being VECTOR of b₁ st b₂ <> 0. b₁ & not {b₃,b₂} is linearly-independent holds
ex b₄ being Real st b₃ = b₄ * b₂

proof end;

theorem Th39: :: RLVECT_4:39

for b₁ being RealLinearSpace
for b₂, b₃, b₄ being VECTOR of b₁ st b₂ <> b₃ & {b₂,b₃} is linearly-independent & not {b₄,b₂,b₃} is linearly-independent holds
ex b₅, b₆ being Real st b₄ = (b₅ * b₂) + (b₆ * b₃)

proof end;