:: RLVECT_4 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

scheme :: RLVECT_4:sch 1
LambdaSep3{ F1() -> non empty set , F2() -> non empty set , F3() -> Element of F1(), F4() -> Element of F1(), F5() -> Element of F1(), F6() -> Element of F2(), F7() -> Element of F2(), F8() -> Element of F2(), F9( set ) -> Element of F2() } :
ex f being Function of F1(),F2() st
( f . F3() = F6() & f . F4() = F7() & f . F5() = F8() & ( for C being Element of F1() st C <> F3() & C <> F4() & C <> F5() holds
f . C = F9(C) ) )
provided
A1: F3() <> F4() and
A2: F3() <> F5() and
A3: F4() <> F5()
proof end;

scheme :: RLVECT_4:sch 2
LinCEx1{ F1() -> RealLinearSpace, F2() -> VECTOR of F1(), F3() -> Real } :
ex l being Linear_Combination of {F2()} st l . F2() = F3()
proof end;

scheme :: RLVECT_4:sch 3
LinCEx2{ F1() -> RealLinearSpace, F2() -> VECTOR of F1(), F3() -> VECTOR of F1(), F4() -> Real, F5() -> Real } :
ex l being Linear_Combination of {F2(),F3()} st
( l . F2() = F4() & l . F3() = F5() )
provided
A1: F2() <> F3()
proof end;

scheme :: RLVECT_4:sch 4
LinCEx3{ F1() -> RealLinearSpace, F2() -> VECTOR of F1(), F3() -> VECTOR of F1(), F4() -> VECTOR of F1(), F5() -> Real, F6() -> Real, F7() -> Real } :
ex l being Linear_Combination of {F2(),F3(),F4()} st
( l . F2() = F5() & l . F3() = F6() & l . F4() = F7() )
provided
A1: F2() <> F3() and
A2: F2() <> F4() and
A3: F3() <> F4()
proof end;

theorem :: RLVECT_4:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 )
proof end;

theorem Th2: :: RLVECT_4:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace
for v, u, w being VECTOR of V holds (v + u) - w = (v - w) + u by RLVECT_1:def 6;

theorem :: RLVECT_4:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: RLVECT_4:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace
for v1, w, v2 being VECTOR of V st v1 - w = v2 - w holds
v1 = v2
proof end;

theorem :: RLVECT_4:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th6: :: RLVECT_4:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being Real
for V being RealLinearSpace
for v being VECTOR of V holds - (a * v) = (- a) * v
proof end;

theorem :: RLVECT_4:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: RLVECT_4:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th9: :: RLVECT_4:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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)
proof end;

theorem Th10: :: RLVECT_4:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 ) )
proof end;

theorem Th11: :: RLVECT_4:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 )
proof end;

theorem :: RLVECT_4:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace
for v being VECTOR of V holds v in Lin {v}
proof end;

theorem :: RLVECT_4:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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) )
proof end;

theorem Th14: :: RLVECT_4:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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) )
proof end;

theorem :: RLVECT_4:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace
for w1, w2 being VECTOR of V holds
( w1 in Lin {w1,w2} & w2 in Lin {w1,w2} )
proof end;

theorem :: RLVECT_4:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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) )
proof end;

theorem Th17: :: RLVECT_4:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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) )
proof end;

theorem :: RLVECT_4:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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} )
proof end;

theorem :: RLVECT_4:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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) )
proof end;

theorem :: RLVECT_4:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: RLVECT_4:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th22: :: RLVECT_4:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: RLVECT_4:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th24: :: RLVECT_4:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b being Real
for V being RealLinearSpace
for v being VECTOR of V st a <> b holds
not {(a * v),(b * v)} is linearly-independent
proof end;

theorem :: RLVECT_4:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being Real
for V being RealLinearSpace
for v being VECTOR of V st a <> 1 holds
not {v,(a * v)} is linearly-independent
proof end;

theorem :: RLVECT_4:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace
for u, w, v 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:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace
for u, w, v 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:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace
for u, w, v 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:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace
for u, w, v 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 Th30: :: RLVECT_4:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being Real
for V being RealLinearSpace
for u, w, v 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 Th31: :: RLVECT_4:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b being Real
for V being RealLinearSpace
for u, w, v 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:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace
for u, w, v 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:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace
for u, w, v 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 Th34: :: RLVECT_4:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b being Real
for V being RealLinearSpace
for v, w being VECTOR of V st a <> b holds
not {(a * v),(b * v),w} is linearly-independent
proof end;

theorem :: RLVECT_4:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being Real
for V being RealLinearSpace
for v, w being VECTOR of V st a <> 1 holds
not {v,(a * v),w} is linearly-independent
proof end;

theorem :: RLVECT_4:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace
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:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 )
proof end;

theorem :: RLVECT_4:38  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace
for w, v being VECTOR of V st w <> 0. V & not {v,w} is linearly-independent holds
ex a being Real st v = a * w
proof end;

theorem :: RLVECT_4:39  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace
for v, w, u being VECTOR of V st v <> w & {v,w} is linearly-independent & not {u,v,w} is linearly-independent holds
ex a, b being Real st u = (a * v) + (b * w)
proof end;