:: by Wojciech A. Trybulec

::

:: Received February 24, 1993

:: Copyright (c) 1993-2021 Association of Mizar Users

scheme :: RLVECT_4:sch 1

LambdaSep3{ F_{1}() -> non empty set , F_{2}() -> non empty set , F_{3}() -> Element of F_{1}(), F_{4}() -> Element of F_{1}(), F_{5}() -> Element of F_{1}(), F_{6}() -> Element of F_{2}(), F_{7}() -> Element of F_{2}(), F_{8}() -> Element of F_{2}(), F_{9}( set ) -> Element of F_{2}() } :

LambdaSep3{ F

ex f being Function of F_{1}(),F_{2}() st

( f . F_{3}() = F_{6}() & f . F_{4}() = F_{7}() & f . F_{5}() = F_{8}() & ( for C being Element of F_{1}() st C <> F_{3}() & C <> F_{4}() & C <> F_{5}() holds

f . C = F_{9}(C) ) )

provided
( f . F

f . C = F

proof end;

Lm1: now :: thesis: for V being RealLinearSpace

for v being VECTOR of V

for a being Real ex l being Linear_Combination of {v} st l . v = a

for v being VECTOR of V

for a being Real ex l being Linear_Combination of {v} st l . v = a

let V be RealLinearSpace; :: thesis: for v being VECTOR of V

for a being Real ex l being Linear_Combination of {v} st l . v = a

let v be VECTOR of V; :: thesis: for a being Real ex l being Linear_Combination of {v} st l . v = a

let a be Real; :: thesis: ex l being Linear_Combination of {v} st l . v = a

thus ex l being Linear_Combination of {v} st l . v = a :: thesis: verum

end;
for a being Real ex l being Linear_Combination of {v} st l . v = a

let v be VECTOR of V; :: thesis: for a being Real ex l being Linear_Combination of {v} st l . v = a

let a be Real; :: thesis: ex l being Linear_Combination of {v} st l . v = a

thus ex l being Linear_Combination of {v} st l . v = a :: thesis: verum

proof

reconsider zz = 0 , a = a as Element of REAL by XREAL_0:def 1;

deffunc H_{1}( VECTOR of V) -> Element of REAL = zz;

consider f being Function of the carrier of V,REAL such that

A1: f . v = a and

A2: for u being VECTOR of V st u <> v holds

f . u = H_{1}(u)
from FUNCT_2:sch 6();

reconsider f = f as Element of Funcs ( the carrier of V,REAL) by FUNCT_2:8;

Carrier f c= {v}

take f ; :: thesis: f . v = a

thus f . v = a by A1; :: thesis: verum

end;
deffunc H

consider f being Function of the carrier of V,REAL such that

A1: f . v = a and

A2: for u being VECTOR of V st u <> v holds

f . u = H

reconsider f = f as Element of Funcs ( the carrier of V,REAL) by FUNCT_2:8;

now :: thesis: for u being VECTOR of V st not u in {v} holds

f . u = 0

then reconsider f = f as Linear_Combination of V by RLVECT_2:def 3;f . u = 0

let u be VECTOR of V; :: thesis: ( not u in {v} implies f . u = 0 )

assume not u in {v} ; :: thesis: f . u = 0

then u <> v by TARSKI:def 1;

hence f . u = 0 by A2; :: thesis: verum

end;
assume not u in {v} ; :: thesis: f . u = 0

then u <> v by TARSKI:def 1;

hence f . u = 0 by A2; :: thesis: verum

Carrier f c= {v}

proof

then reconsider f = f as Linear_Combination of {v} by RLVECT_2:def 6;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Carrier f or x in {v} )

assume that

A3: x in Carrier f and

A4: not x in {v} ; :: thesis: contradiction

( f . x <> 0 & x <> v ) by A3, A4, RLVECT_2:19, TARSKI:def 1;

hence contradiction by A2, A3; :: thesis: verum

end;
assume that

A3: x in Carrier f and

A4: not x in {v} ; :: thesis: contradiction

( f . x <> 0 & x <> v ) by A3, A4, RLVECT_2:19, TARSKI:def 1;

hence contradiction by A2, A3; :: thesis: verum

take f ; :: thesis: f . v = a

thus f . v = a by A1; :: thesis: verum

Lm2: now :: thesis: for V being RealLinearSpace

for v1, v2 being VECTOR of V

for a, b being Real st v1 <> v2 holds

ex l being Linear_Combination of {v1,v2} st

( l . v1 = a & l . v2 = b )

for v1, v2 being VECTOR of V

for a, b being Real st v1 <> v2 holds

ex l being Linear_Combination of {v1,v2} st

( l . v1 = a & l . v2 = b )

let V be RealLinearSpace; :: thesis: for v1, v2 being VECTOR of V

for a, b being Real st v1 <> v2 holds

ex l being Linear_Combination of {v1,v2} st

( l . v1 = a & l . v2 = b )

let v1, v2 be VECTOR of V; :: thesis: for a, b being Real st v1 <> v2 holds

ex l being Linear_Combination of {v1,v2} st

( l . v1 = a & l . v2 = b )

let a, b be Real; :: thesis: ( v1 <> v2 implies ex l being Linear_Combination of {v1,v2} st

( l . v1 = a & l . v2 = b ) )

assume A1: v1 <> v2 ; :: thesis: ex l being Linear_Combination of {v1,v2} st

( l . v1 = a & l . v2 = b )

thus ex l being Linear_Combination of {v1,v2} st

( l . v1 = a & l . v2 = b ) :: thesis: verum

end;
for a, b being Real st v1 <> v2 holds

ex l being Linear_Combination of {v1,v2} st

( l . v1 = a & l . v2 = b )

let v1, v2 be VECTOR of V; :: thesis: for a, b being Real st v1 <> v2 holds

ex l being Linear_Combination of {v1,v2} st

( l . v1 = a & l . v2 = b )

let a, b be Real; :: thesis: ( v1 <> v2 implies ex l being Linear_Combination of {v1,v2} st

( l . v1 = a & l . v2 = b ) )

assume A1: v1 <> v2 ; :: thesis: ex l being Linear_Combination of {v1,v2} st

( l . v1 = a & l . v2 = b )

thus ex l being Linear_Combination of {v1,v2} st

( l . v1 = a & l . v2 = b ) :: thesis: verum

proof

reconsider zz = 0 , a = a, b = b as Element of REAL by XREAL_0:def 1;

deffunc H_{1}( VECTOR of V) -> Element of REAL = zz;

consider f being Function of the carrier of V,REAL such that

A2: ( f . v1 = a & f . v2 = b ) and

A3: for u being VECTOR of V st u <> v1 & u <> v2 holds

f . u = H_{1}(u)
from FUNCT_2:sch 7(A1);

reconsider f = f as Element of Funcs ( the carrier of V,REAL) by FUNCT_2:8;

Carrier f c= {v1,v2}

take f ; :: thesis: ( f . v1 = a & f . v2 = b )

thus ( f . v1 = a & f . v2 = b ) by A2; :: thesis: verum

end;
deffunc H

consider f being Function of the carrier of V,REAL such that

A2: ( f . v1 = a & f . v2 = b ) and

A3: for u being VECTOR of V st u <> v1 & u <> v2 holds

f . u = H

reconsider f = f as Element of Funcs ( the carrier of V,REAL) by FUNCT_2:8;

now :: thesis: for u being VECTOR of V st not u in {v1,v2} holds

f . u = 0

then reconsider f = f as Linear_Combination of V by RLVECT_2:def 3;f . u = 0

let u be VECTOR of V; :: thesis: ( not u in {v1,v2} implies f . u = 0 )

assume not u in {v1,v2} ; :: thesis: f . u = 0

then ( u <> v1 & u <> v2 ) by TARSKI:def 2;

hence f . u = 0 by A3; :: thesis: verum

end;
assume not u in {v1,v2} ; :: thesis: f . u = 0

then ( u <> v1 & u <> v2 ) by TARSKI:def 2;

hence f . u = 0 by A3; :: thesis: verum

Carrier f c= {v1,v2}

proof

then reconsider f = f as Linear_Combination of {v1,v2} by RLVECT_2:def 6;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Carrier f or x in {v1,v2} )

assume that

A4: x in Carrier f and

A5: not x in {v1,v2} ; :: thesis: contradiction

A6: x <> v2 by A5, TARSKI:def 2;

( f . x <> 0 & x <> v1 ) by A4, A5, RLVECT_2:19, TARSKI:def 2;

hence contradiction by A3, A4, A6; :: thesis: verum

end;
assume that

A4: x in Carrier f and

A5: not x in {v1,v2} ; :: thesis: contradiction

A6: x <> v2 by A5, TARSKI:def 2;

( f . x <> 0 & x <> v1 ) by A4, A5, RLVECT_2:19, TARSKI:def 2;

hence contradiction by A3, A4, A6; :: thesis: verum

take f ; :: thesis: ( f . v1 = a & f . v2 = b )

thus ( f . v1 = a & f . v2 = b ) by A2; :: thesis: verum

Lm3: now :: thesis: for V being RealLinearSpace

for v1, v2, v3 being VECTOR of V

for a, b, c being Real st v1 <> v2 & v1 <> v3 & v2 <> v3 holds

ex l being Linear_Combination of {v1,v2,v3} st

( l . v1 = a & l . v2 = b & l . v3 = c )

for v1, v2, v3 being VECTOR of V

for a, b, c being Real st v1 <> v2 & v1 <> v3 & v2 <> v3 holds

ex l being Linear_Combination of {v1,v2,v3} st

( l . v1 = a & l . v2 = b & l . v3 = c )

let V be RealLinearSpace; :: thesis: for v1, v2, v3 being VECTOR of V

for a, b, c being Real st v1 <> v2 & v1 <> v3 & v2 <> v3 holds

ex l being Linear_Combination of {v1,v2,v3} st

( l . v1 = a & l . v2 = b & l . v3 = c )

let v1, v2, v3 be VECTOR of V; :: thesis: for a, b, c being Real st v1 <> v2 & v1 <> v3 & v2 <> v3 holds

ex l being Linear_Combination of {v1,v2,v3} st

( l . v1 = a & l . v2 = b & l . v3 = c )

let a, b, c be Real; :: thesis: ( v1 <> v2 & v1 <> v3 & v2 <> v3 implies ex l being Linear_Combination of {v1,v2,v3} st

( l . v1 = a & l . v2 = b & l . v3 = c ) )

assume that

A1: v1 <> v2 and

A2: v1 <> v3 and

A3: v2 <> v3 ; :: thesis: ex l being Linear_Combination of {v1,v2,v3} st

( l . v1 = a & l . v2 = b & l . v3 = c )

thus ex l being Linear_Combination of {v1,v2,v3} st

( l . v1 = a & l . v2 = b & l . v3 = c ) :: thesis: verum

end;
for a, b, c being Real st v1 <> v2 & v1 <> v3 & v2 <> v3 holds

ex l being Linear_Combination of {v1,v2,v3} st

( l . v1 = a & l . v2 = b & l . v3 = c )

let v1, v2, v3 be VECTOR of V; :: thesis: for a, b, c being Real st v1 <> v2 & v1 <> v3 & v2 <> v3 holds

ex l being Linear_Combination of {v1,v2,v3} st

( l . v1 = a & l . v2 = b & l . v3 = c )

let a, b, c be Real; :: thesis: ( v1 <> v2 & v1 <> v3 & v2 <> v3 implies ex l being Linear_Combination of {v1,v2,v3} st

( l . v1 = a & l . v2 = b & l . v3 = c ) )

assume that

A1: v1 <> v2 and

A2: v1 <> v3 and

A3: v2 <> v3 ; :: thesis: ex l being Linear_Combination of {v1,v2,v3} st

( l . v1 = a & l . v2 = b & l . v3 = c )

thus ex l being Linear_Combination of {v1,v2,v3} st

( l . v1 = a & l . v2 = b & l . v3 = c ) :: thesis: verum

proof

reconsider zz = 0 , a = a, b = b, c = c as Element of REAL by XREAL_0:def 1;

deffunc H_{1}( VECTOR of V) -> Element of REAL = zz;

consider f being Function of the carrier of V,REAL such that

A4: ( f . v1 = a & f . v2 = b & f . v3 = c ) and

A5: for u being VECTOR of V st u <> v1 & u <> v2 & u <> v3 holds

f . u = H_{1}(u)
from RLVECT_4:sch 1(A1, A2, A3);

reconsider f = f as Element of Funcs ( the carrier of V,REAL) by FUNCT_2:8;

Carrier f c= {v1,v2,v3}

take f ; :: thesis: ( f . v1 = a & f . v2 = b & f . v3 = c )

thus ( f . v1 = a & f . v2 = b & f . v3 = c ) by A4; :: thesis: verum

end;
deffunc H

consider f being Function of the carrier of V,REAL such that

A4: ( f . v1 = a & f . v2 = b & f . v3 = c ) and

A5: for u being VECTOR of V st u <> v1 & u <> v2 & u <> v3 holds

f . u = H

reconsider f = f as Element of Funcs ( the carrier of V,REAL) by FUNCT_2:8;

now :: thesis: for u being VECTOR of V st not u in {v1,v2,v3} holds

f . u = 0

then reconsider f = f as Linear_Combination of V by RLVECT_2:def 3;f . u = 0

let u be VECTOR of V; :: thesis: ( not u in {v1,v2,v3} implies f . u = 0 )

assume A6: not u in {v1,v2,v3} ; :: thesis: f . u = 0

then A7: u <> v3 by ENUMSET1:def 1;

( u <> v1 & u <> v2 ) by A6, ENUMSET1:def 1;

hence f . u = 0 by A5, A7; :: thesis: verum

end;
assume A6: not u in {v1,v2,v3} ; :: thesis: f . u = 0

then A7: u <> v3 by ENUMSET1:def 1;

( u <> v1 & u <> v2 ) by A6, ENUMSET1:def 1;

hence f . u = 0 by A5, A7; :: thesis: verum

Carrier f c= {v1,v2,v3}

proof

then reconsider f = f as Linear_Combination of {v1,v2,v3} by RLVECT_2:def 6;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Carrier f or x in {v1,v2,v3} )

assume that

A8: x in Carrier f and

A9: not x in {v1,v2,v3} ; :: thesis: contradiction

A10: ( x <> v2 & x <> v3 ) by A9, ENUMSET1:def 1;

( f . x <> 0 & x <> v1 ) by A8, A9, ENUMSET1:def 1, RLVECT_2:19;

hence contradiction by A5, A8, A10; :: thesis: verum

end;
assume that

A8: x in Carrier f and

A9: not x in {v1,v2,v3} ; :: thesis: contradiction

A10: ( x <> v2 & x <> v3 ) by A9, ENUMSET1:def 1;

( f . x <> 0 & x <> v1 ) by A8, A9, ENUMSET1:def 1, RLVECT_2:19;

hence contradiction by A5, A8, A10; :: thesis: verum

take f ; :: thesis: ( f . v1 = a & f . v2 = b & f . v3 = c )

thus ( f . v1 = a & f . v2 = b & f . v3 = c ) by A4; :: thesis: verum

theorem :: RLVECT_4:1

for V being RealLinearSpace

for v, w being VECTOR of V holds

( (v + w) - v = w & (w + v) - v = w & (v - v) + w = w & (w - v) + v = w & v + (w - v) = w & w + (v - v) = w & v - (v - w) = w )

for v, w being VECTOR of V holds

( (v + w) - v = w & (w + v) - v = w & (v - v) + w = w & (w - v) + v = w & v + (w - v) = w & w + (v - v) = w & v - (v - w) = w )

proof end;

:: RLVECT_1:37 extended

:: Composition of RLVECT_1:38 and RLVECT_1:39

theorem :: RLVECT_4:4

for V being RealLinearSpace

for v being VECTOR of V

for W1, W2 being Subspace of V st W1 is Subspace of W2 holds

v + W1 c= v + W2

for v being VECTOR of V

for W1, W2 being Subspace of V st W1 is Subspace of W2 holds

v + W1 c= v + W2

proof end;

theorem :: RLVECT_4:5

for V being RealLinearSpace

for u, v being VECTOR of V

for W being Subspace of V st u in v + W holds

v + W = u + W

for u, v being VECTOR of V

for W being Subspace of V st u in v + W holds

v + W = u + W

proof end;

theorem Th6: :: RLVECT_4:6

for V being RealLinearSpace

for u, v, w being VECTOR of V

for l being Linear_Combination of {u,v,w} st u <> v & u <> w & v <> w holds

Sum l = (((l . u) * u) + ((l . v) * v)) + ((l . w) * w)

for u, v, w being VECTOR of V

for l being Linear_Combination of {u,v,w} st u <> v & u <> w & v <> w holds

Sum l = (((l . u) * u) + ((l . v) * v)) + ((l . w) * w)

proof end;

reconsider zz = 0 as Element of REAL by XREAL_0:def 1;

theorem Th7: :: RLVECT_4:7

for V being RealLinearSpace

for u, v, w being VECTOR of V holds

( ( u <> v & u <> w & v <> w & {u,v,w} is linearly-independent ) iff for a, b, c being Real st ((a * u) + (b * v)) + (c * w) = 0. V holds

( a = 0 & b = 0 & c = 0 ) )

for u, v, w being VECTOR of V holds

( ( u <> v & u <> w & v <> w & {u,v,w} is linearly-independent ) iff for a, b, c being Real st ((a * u) + (b * v)) + (c * w) = 0. V holds

( a = 0 & b = 0 & c = 0 ) )

proof end;

theorem Th8: :: RLVECT_4:8

for x being set

for V being RealLinearSpace

for v being VECTOR of V holds

( x in Lin {v} iff ex a being Real st x = a * v )

for V being RealLinearSpace

for v being VECTOR of V holds

( x in Lin {v} iff ex a being Real st x = a * v )

proof end;

theorem :: RLVECT_4:10

for x being set

for V being RealLinearSpace

for v, w being VECTOR of V holds

( x in v + (Lin {w}) iff ex a being Real st x = v + (a * w) )

for V being RealLinearSpace

for v, w being VECTOR of V holds

( x in v + (Lin {w}) iff ex a being Real st x = v + (a * w) )

proof end;

theorem Th11: :: RLVECT_4:11

for x being set

for V being RealLinearSpace

for w1, w2 being VECTOR of V holds

( x in Lin {w1,w2} iff ex a, b being Real st x = (a * w1) + (b * w2) )

for V being RealLinearSpace

for w1, w2 being VECTOR of V holds

( x in Lin {w1,w2} iff ex a, b being Real st x = (a * w1) + (b * w2) )

proof end;

theorem :: RLVECT_4:12

for V being RealLinearSpace

for w1, w2 being VECTOR of V holds

( w1 in Lin {w1,w2} & w2 in Lin {w1,w2} )

for w1, w2 being VECTOR of V holds

( w1 in Lin {w1,w2} & w2 in Lin {w1,w2} )

proof end;

theorem :: RLVECT_4:13

for x being set

for V being RealLinearSpace

for v, w1, w2 being VECTOR of V holds

( x in v + (Lin {w1,w2}) iff ex a, b being Real st x = (v + (a * w1)) + (b * w2) )

for V being RealLinearSpace

for v, w1, w2 being VECTOR of V holds

( x in v + (Lin {w1,w2}) iff ex a, b being Real st x = (v + (a * w1)) + (b * w2) )

proof end;

theorem Th14: :: RLVECT_4:14

for x being set

for V being RealLinearSpace

for v1, v2, v3 being VECTOR of V holds

( x in Lin {v1,v2,v3} iff ex a, b, c being Real st x = ((a * v1) + (b * v2)) + (c * v3) )

for V being RealLinearSpace

for v1, v2, v3 being VECTOR of V holds

( x in Lin {v1,v2,v3} iff ex a, b, c being Real st x = ((a * v1) + (b * v2)) + (c * v3) )

proof end;

theorem :: RLVECT_4:15

for V being RealLinearSpace

for w1, w2, w3 being VECTOR of V holds

( w1 in Lin {w1,w2,w3} & w2 in Lin {w1,w2,w3} & w3 in Lin {w1,w2,w3} )

for w1, w2, w3 being VECTOR of V holds

( w1 in Lin {w1,w2,w3} & w2 in Lin {w1,w2,w3} & w3 in Lin {w1,w2,w3} )

proof end;

theorem :: RLVECT_4:16

for x being set

for V being RealLinearSpace

for v, w1, w2, w3 being VECTOR of V holds

( x in v + (Lin {w1,w2,w3}) iff ex a, b, c being Real st x = ((v + (a * w1)) + (b * w2)) + (c * w3) )

for V being RealLinearSpace

for v, w1, w2, w3 being VECTOR of V holds

( x in v + (Lin {w1,w2,w3}) iff ex a, b, c being Real st x = ((v + (a * w1)) + (b * w2)) + (c * w3) )

proof end;

theorem :: RLVECT_4:17

for V being RealLinearSpace

for u, v being VECTOR of V st {u,v} is linearly-independent & u <> v holds

{u,(v - u)} is linearly-independent

for u, v being VECTOR of V st {u,v} is linearly-independent & u <> v holds

{u,(v - u)} is linearly-independent

proof end;

theorem :: RLVECT_4:18

for V being RealLinearSpace

for u, v being VECTOR of V st {u,v} is linearly-independent & u <> v holds

{u,(v + u)} is linearly-independent

for u, v being VECTOR of V st {u,v} is linearly-independent & u <> v holds

{u,(v + u)} is linearly-independent

proof end;

theorem Th19: :: RLVECT_4:19

for a being Real

for V being RealLinearSpace

for u, v being VECTOR of V st {u,v} is linearly-independent & u <> v & a <> 0 holds

{u,(a * v)} is linearly-independent

for V being RealLinearSpace

for u, v being VECTOR of V st {u,v} is linearly-independent & u <> v & a <> 0 holds

{u,(a * v)} is linearly-independent

proof end;

theorem :: RLVECT_4:20

for V being RealLinearSpace

for u, v being VECTOR of V st {u,v} is linearly-independent & u <> v holds

{u,(- v)} is linearly-independent

for u, v being VECTOR of V st {u,v} is linearly-independent & u <> v holds

{u,(- v)} is linearly-independent

proof end;

theorem Th21: :: RLVECT_4:21

for a, b being Real

for V being RealLinearSpace

for v being VECTOR of V st a <> b holds

{(a * v),(b * v)} is linearly-dependent

for V being RealLinearSpace

for v being VECTOR of V st a <> b holds

{(a * v),(b * v)} is linearly-dependent

proof end;

theorem :: RLVECT_4:22

for a being Real

for V being RealLinearSpace

for v being VECTOR of V st a <> 1 holds

{v,(a * v)} is linearly-dependent

for V being RealLinearSpace

for v being VECTOR of V st a <> 1 holds

{v,(a * v)} is linearly-dependent

proof end;

theorem :: RLVECT_4:23

for V being RealLinearSpace

for u, v, w being VECTOR of V st {u,w,v} is linearly-independent & u <> v & u <> w & v <> w holds

{u,w,(v - u)} is linearly-independent

for u, v, w being VECTOR of V st {u,w,v} is linearly-independent & u <> v & u <> w & v <> w holds

{u,w,(v - u)} is linearly-independent

proof end;

theorem :: RLVECT_4:24

for V being RealLinearSpace

for u, v, w being VECTOR of V st {u,w,v} is linearly-independent & u <> v & u <> w & v <> w holds

{u,(w - u),(v - u)} is linearly-independent

for u, v, w being VECTOR of V st {u,w,v} is linearly-independent & u <> v & u <> w & v <> w holds

{u,(w - u),(v - u)} is linearly-independent

proof end;

theorem :: RLVECT_4:25

for V being RealLinearSpace

for u, v, w being VECTOR of V st {u,w,v} is linearly-independent & u <> v & u <> w & v <> w holds

{u,w,(v + u)} is linearly-independent

for u, v, w being VECTOR of V st {u,w,v} is linearly-independent & u <> v & u <> w & v <> w holds

{u,w,(v + u)} is linearly-independent

proof end;

theorem :: RLVECT_4:26

for V being RealLinearSpace

for u, v, w being VECTOR of V st {u,w,v} is linearly-independent & u <> v & u <> w & v <> w holds

{u,(w + u),(v + u)} is linearly-independent

for u, v, w being VECTOR of V st {u,w,v} is linearly-independent & u <> v & u <> w & v <> w holds

{u,(w + u),(v + u)} is linearly-independent

proof end;

theorem Th27: :: RLVECT_4:27

for a being Real

for V being RealLinearSpace

for u, v, w being VECTOR of V st {u,w,v} is linearly-independent & u <> v & u <> w & v <> w & a <> 0 holds

{u,w,(a * v)} is linearly-independent

for V being RealLinearSpace

for u, v, w being VECTOR of V st {u,w,v} is linearly-independent & u <> v & u <> w & v <> w & a <> 0 holds

{u,w,(a * v)} is linearly-independent

proof end;

theorem Th28: :: RLVECT_4:28

for a, b being Real

for V being RealLinearSpace

for u, v, w being VECTOR of V st {u,w,v} is linearly-independent & u <> v & u <> w & v <> w & a <> 0 & b <> 0 holds

{u,(a * w),(b * v)} is linearly-independent

for V being RealLinearSpace

for u, v, w being VECTOR of V st {u,w,v} is linearly-independent & u <> v & u <> w & v <> w & a <> 0 & b <> 0 holds

{u,(a * w),(b * v)} is linearly-independent

proof end;

theorem :: RLVECT_4:29

for V being RealLinearSpace

for u, v, w being VECTOR of V st {u,w,v} is linearly-independent & u <> v & u <> w & v <> w holds

{u,w,(- v)} is linearly-independent

for u, v, w being VECTOR of V st {u,w,v} is linearly-independent & u <> v & u <> w & v <> w holds

{u,w,(- v)} is linearly-independent

proof end;

theorem :: RLVECT_4:30

for V being RealLinearSpace

for u, v, w being VECTOR of V st {u,w,v} is linearly-independent & u <> v & u <> w & v <> w holds

{u,(- w),(- v)} is linearly-independent

for u, v, w being VECTOR of V st {u,w,v} is linearly-independent & u <> v & u <> w & v <> w holds

{u,(- w),(- v)} is linearly-independent

proof end;

theorem Th31: :: RLVECT_4:31

for a, b being Real

for V being RealLinearSpace

for v, w being VECTOR of V st a <> b holds

{(a * v),(b * v),w} is linearly-dependent

for V being RealLinearSpace

for v, w being VECTOR of V st a <> b holds

{(a * v),(b * v),w} is linearly-dependent

proof end;

theorem :: RLVECT_4:32

for a being Real

for V being RealLinearSpace

for v, w being VECTOR of V st a <> 1 holds

{v,(a * v),w} is linearly-dependent

for V being RealLinearSpace

for v, w being VECTOR of V st a <> 1 holds

{v,(a * v),w} is linearly-dependent

proof end;

theorem :: RLVECT_4:33

for V being RealLinearSpace

for v, w being VECTOR of V st v in Lin {w} & v <> 0. V holds

Lin {v} = Lin {w}

for v, w being VECTOR of V st v in Lin {w} & v <> 0. V holds

Lin {v} = Lin {w}

proof end;

theorem :: RLVECT_4:34

for V being RealLinearSpace

for v1, v2, w1, w2 being VECTOR of V st v1 <> v2 & {v1,v2} is linearly-independent & v1 in Lin {w1,w2} & v2 in Lin {w1,w2} holds

( Lin {w1,w2} = Lin {v1,v2} & {w1,w2} is linearly-independent & w1 <> w2 )

for v1, v2, w1, w2 being VECTOR of V st v1 <> v2 & {v1,v2} is linearly-independent & v1 in Lin {w1,w2} & v2 in Lin {w1,w2} holds

( Lin {w1,w2} = Lin {v1,v2} & {w1,w2} is linearly-independent & w1 <> w2 )

proof end;

theorem :: RLVECT_4:35

for V being RealLinearSpace

for v, w being VECTOR of V st w <> 0. V & {v,w} is linearly-dependent holds

ex a being Real st v = a * w

for v, w being VECTOR of V st w <> 0. V & {v,w} is linearly-dependent holds

ex a being Real st v = a * w

proof end;

theorem :: RLVECT_4:36

for V being RealLinearSpace

for u, v, w being VECTOR of V st v <> w & {v,w} is linearly-independent & {u,v,w} is linearly-dependent holds

ex a, b being Real st u = (a * v) + (b * w)

for u, v, w being VECTOR of V st v <> w & {v,w} is linearly-independent & {u,v,w} is linearly-dependent holds

ex a, b being Real st u = (a * v) + (b * w)

proof end;

theorem :: RLVECT_4:37

for V being RealLinearSpace

for v being VECTOR of V

for a being Real ex l being Linear_Combination of {v} st l . v = a by Lm1;

for v being VECTOR of V

for a being Real ex l being Linear_Combination of {v} st l . v = a by Lm1;

theorem :: RLVECT_4:38

theorem :: RLVECT_4:39