Copyright (c) 1993 Association of Mizar Users
environ
vocabulary RLVECT_1, RLSUB_1, FUNCT_1, RLVECT_2, FUNCT_2, ARYTM_1, BOOLE,
FINSEQ_1, RELAT_1, SEQ_1, RLVECT_3;
notation TARSKI, XBOOLE_0, SUBSET_1, NUMBERS, FINSEQ_1, FUNCT_1, FUNCT_2,
REAL_1, STRUCT_0, RLSUB_1, RLVECT_1, RLVECT_2, RLVECT_3, FRAENKEL;
constructors REAL_1, RLVECT_2, RLVECT_3, FINSEQ_4, MEMBERED, XBOOLE_0;
clusters STRUCT_0, RELSET_1, MEMBERED, ZFMISC_1, XBOOLE_0;
requirements NUMERALS, SUBSET, BOOLE, ARITHM;
definitions RLVECT_3, TARSKI, XBOOLE_0;
theorems ENUMSET1, FINSEQ_1, FINSEQ_3, RLSUB_1, RLSUB_2, RLVECT_1, RLVECT_2,
RLVECT_3, SETWISEO, TARSKI, ZFMISC_1, FUNCT_2, XBOOLE_0, XBOOLE_1,
VECTSP_1, XCMPLX_0, XCMPLX_1, FINSEQ_2;
schemes FUNCT_2, RLVECT_2;
begin
reserve x for set;
reserve a,b,c,d,e,r1,r2,r3,r4,r5,r6 for Real;
reserve V for RealLinearSpace;
reserve u,v,v1,v2,v3,w,w1,w2,w3 for VECTOR of V;
reserve W,W1,W2 for Subspace of V;
scheme LambdaSep3{D, R() -> non empty set,
A1, A2, A3() -> Element of D(),
B1, B2, B3() -> Element of R(),
F(set) -> Element of R()}:
ex f being Function of D(),R() st
f.A1() = B1() & f.A2() = B2() & f.A3() = B3() &
for C being Element of D() st C <> A1() & C <> A2() & C <> A3() holds
f.C = F(C) provided
A1: A1() <> A2() and
A2: A1() <> A3() and
A3: A2() <> A3()
proof defpred P[Element of D(),set] means ($1 = A1() implies $2 = B1()) &
($1 = A2() implies $2 = B2()) & ($1 = A3() implies $2 = B3()) &
($1 <> A1() & $1 <> A2() & $1 <> A3() implies $2 = F($1));
A4: for x being Element of D() ex y being Element of R() st P[x,y]
proof let x be Element of D();
(x = A1() implies thesis) & (x = A2() implies thesis) &
(x = A3() implies thesis) &
(x <> A1() & x <> A2() & x <> A3() implies thesis) by A1,A2,A3;
hence thesis;
end;
consider f being Function of D(),R() such that
A5: for x being Element of D() holds P[x,f.x] from FuncExD(A4);
take f;
thus thesis by A5;
end;
scheme LinCEx1{V() -> RealLinearSpace, v() -> VECTOR of V(), a() -> Real}:
ex l being Linear_Combination of {v()} st l.v() = a()
proof
deffunc F(VECTOR of V())=0;
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 = F(u)
from LambdaSep1;
reconsider f as Element of Funcs(the carrier of V(),REAL) by FUNCT_2:11;
now let u be VECTOR of V();
assume not u in {v()};
then u <> v() by TARSKI:def 1;
hence f.u = 0 by A2;
end;
then reconsider f as Linear_Combination of V() by RLVECT_2:def 5;
Carrier f c= {v()}
proof let x;
assume that A3: x in Carrier f and A4: not x in {v()};
f.x <> 0 & x <> v() by A3,A4,RLVECT_2:28,TARSKI:def 1;
hence thesis by A2,A3;
end;
then reconsider f as Linear_Combination of {v()} by RLVECT_2:def 8;
take f;
thus thesis by A1;
end;
scheme LinCEx2{V() -> RealLinearSpace, v1, v2() -> VECTOR of V(),
a, b() -> Real}:
ex l being Linear_Combination of {v1(),v2()} st l.v1() = a() & l.v2() = b()
provided
A1: v1() <> v2()
proof
deffunc F(VECTOR of V())=0;
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 = F(u) from LambdaSep2(A1);
reconsider f as Element of Funcs(the carrier of V(),REAL) by FUNCT_2:11;
now let u be VECTOR of V();
assume not u in {v1(),v2()};
then u <> v1() & u <> v2() by TARSKI:def 2;
hence f.u = 0 by A3;
end;
then reconsider f as Linear_Combination of V() by RLVECT_2:def 5;
Carrier f c= {v1(),v2()}
proof let x;
assume that A4: x in Carrier f and A5: not x in {v1(),v2()};
f.x <> 0 & x <> v1() & x <> v2() by A4,A5,RLVECT_2:28,TARSKI:def 2;
hence thesis by A3,A4;
end;
then reconsider f as Linear_Combination of {v1(),v2()} by RLVECT_2:def 8;
take f;
thus thesis by A2;
end;
scheme LinCEx3{V() -> RealLinearSpace, v1, v2, v3() -> VECTOR of V(),
a, b, c() -> Real}:
ex l being Linear_Combination of {v1(),v2(),v3()} st
l.v1() = a() & l.v2() = b() & l.v3() = c() provided
A1: v1() <> v2() and
A2: v1() <> v3() and
A3: v2() <> v3()
proof
deffunc F(VECTOR of V())=0;
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 = F(u) from LambdaSep3(A1,A2,A3);
reconsider f as Element of Funcs(the carrier of V(),REAL) by FUNCT_2:11;
now let u be VECTOR of V();
assume not u in {v1(),v2(),v3()};
then u <> v1() & u <> v2() & u <> v3() by ENUMSET1:14;
hence f.u = 0 by A5;
end;
then reconsider f as Linear_Combination of V() by RLVECT_2:def 5;
Carrier f c= {v1(),v2(),v3()}
proof let x;
assume that A6: x in Carrier f and A7: not x in {v1(),v2(),v3()};
f.x <> 0 & x <> v1() & x <> v2() & x <> v3()
by A6,A7,ENUMSET1:14,RLVECT_2:28;
hence thesis by A5,A6;
end;
then reconsider f as Linear_Combination of {v1(),v2(),v3()} by RLVECT_2:def
8;
take f;
thus thesis by A4;
end;
theorem
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
thus v + w - v = w by RLSUB_2:78;
thus w + v - v = w by RLSUB_2:78;
thus A1: v - v + w = 0.V + w by RLVECT_1:28
.= w by RLVECT_1:10;
thus w - v + v = w by RLSUB_2:78;
thus thesis by A1,RLSUB_2:78,RLVECT_1:43;
end;
theorem Th2:
v + u - w = v - w + u
proof
thus v + u - w = v + u + - w by RLVECT_1:def 11
.= v + - w + u by RLVECT_1:def 6
.= v - w + u by RLVECT_1:def 11;
end;
:: RLVECT_1:37 extended
canceled;
theorem
v1 - w = v2 - w implies v1 = v2
proof assume v1 - w = v2 - w;
then - (v1 - w) = w - v2 by VECTSP_1:81;
then w - v1 = w - v2 by VECTSP_1:81;
hence thesis by RLVECT_1:37;
end;
:: Composition of RLVECT_1:38 and RLVECT_1:39
canceled;
theorem Th6:
- (a * v) = (- a) * v
proof
thus - (a * v) = a * (- v) by RLVECT_1:39
.= (- a) * v by RLVECT_1:38;
end;
theorem
W1 is Subspace of W2 implies v + W1 c= v + W2
proof assume A1: W1 is Subspace of W2;
let x;
assume x in v + W1;
then consider u such that A2: u in W1 and A3: x = v + u by RLSUB_1:79;
u in W2 by A1,A2,RLSUB_1:16;
hence thesis by A3,RLSUB_1:79;
end;
theorem
u in v + W implies v + W = u + W
proof assume A1: u in v + W;
reconsider C = v + W as Coset of W by RLSUB_1:def 6;
C = u + W by A1,RLSUB_1:94;
hence thesis;
end;
theorem Th9:
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 let f be Linear_Combination of {u,v,w};
assume that A1: u <> v and A2: u <> w and A3: v <> w;
set a = f.u; set b = f.v; set c = f.w;
A4: Carrier f c= {u,v,w} by RLVECT_2:def 8;
A5: now let x be VECTOR of V;
assume x <> v & x <> u & x <> w;
then not x in Carrier f by A4,ENUMSET1:13;
hence f.x = 0 by RLVECT_2:28;
end;
now per cases;
suppose A6: a = 0;
now per cases;
suppose A7: b = 0;
now per cases;
suppose A8: c = 0;
now assume
A9: Carrier f <> {};
consider x being Element of Carrier f;
A10: x is VECTOR of V by A9,TARSKI:def 3;
then f.x <> 0 by A9,RLVECT_2:28;
hence contradiction by A5,A6,A7,A8,A10;
end;
then f = ZeroLC(V) by RLVECT_2:def 7;
hence Sum(f) = 0.V by RLVECT_2:48
.= f.u * u by A6,RLVECT_1:23
.= f.u * u + 0.V by RLVECT_1:10
.= f.u * u + f.v * v by A7,RLVECT_1:23
.= f.u * u + f.v * v + 0.V by RLVECT_1:10
.= f.u * u + f.v * v + f.w * w by A8,RLVECT_1:23;
suppose A11: c <> 0;
A12: Carrier f = {w}
proof
thus Carrier f c= {w}
proof let x;
assume that A13: x in Carrier f and A14: not x in {w};
A15: f.x <> 0 by A13,RLVECT_2:28;
x <> u & x <> v & x <> w
by A6,A7,A13,A14,RLVECT_2:28,TARSKI:def
1;
hence contradiction by A5,A13,A15;
end;
w in Carrier f by A11,RLVECT_2:28;
hence thesis by ZFMISC_1:37;
end;
set F = <* w *>;
A16: rng F = {w} by FINSEQ_1:56;
A17: F is one-to-one by FINSEQ_3:102;
f (#) F = <* c * w *> by RLVECT_2:42;
then Sum(f) = Sum<* c * w *> by A12,A16,A17,RLVECT_2:def 10
.= c * w by RLVECT_1:61
.= 0.V + c * w by RLVECT_1:10
.= 0.V + 0.V + c * w by RLVECT_1:10
.= a * u + 0.V + c * w by A6,RLVECT_1:23;
hence thesis by A7,RLVECT_1:23;
end;
hence thesis;
suppose A18: b <> 0;
now per cases;
suppose A19: c = 0;
A20: Carrier f = {v}
proof
thus Carrier f c= {v}
proof let x;
assume that A21: x in Carrier f and A22: not x in {v};
A23: f.x <> 0 by A21,RLVECT_2:28;
x <> u & x <> v & x <> w
by A6,A19,A21,A22,RLVECT_2:28,TARSKI:def
1;
hence contradiction by A5,A21,A23;
end;
v in Carrier f by A18,RLVECT_2:28;
hence thesis by ZFMISC_1:37;
end;
set F = <* v *>;
A24: rng F = {v} by FINSEQ_1:56;
A25: F is one-to-one by FINSEQ_3:102;
f (#) F = <* b * v *> by RLVECT_2:42;
then Sum(f) = Sum<* b * v *> by A20,A24,A25,RLVECT_2:def 10
.= b * v by RLVECT_1:61
.= 0.V + b * v by RLVECT_1:10
.= 0.V + b * v + 0.V by RLVECT_1:10
.= a * u + b * v + 0.V by A6,RLVECT_1:23;
hence thesis by A19,RLVECT_1:23;
suppose A26: c <> 0;
A27: Carrier f = {v,w}
proof
thus Carrier f c= {v,w}
proof let x;
assume that A28: x in Carrier f and A29: not x in {v,w};
A30: f.x <> 0 by A28,RLVECT_2:28;
x <> v & x <> w & x <> u by A6,A28,A29,RLVECT_2:28,TARSKI:
def 2;
hence contradiction by A5,A28,A30;
end;
v in Carrier f & w in Carrier f by A18,A26,RLVECT_2:28;
hence {v,w} c= Carrier f by ZFMISC_1:38;
end;
set F = <* v,w *>;
A31: rng F = {v,w} by FINSEQ_2:147;
A32: F is one-to-one by A3,FINSEQ_3:103;
f (#) F = <* b * v,c * w *> by RLVECT_2:43;
then Sum(f) = Sum<* b * v,c * w *> by A27,A31,A32,RLVECT_2:def 10
.= b * v + c * w by RLVECT_1:62
.= 0.V + b * v + c * w by RLVECT_1:10;
hence thesis by A6,RLVECT_1:23;
end;
hence thesis;
end;
hence thesis;
suppose A33: a <> 0;
now per cases;
suppose A34: b = 0;
now per cases;
suppose A35: c = 0;
A36: Carrier f = {u}
proof
thus Carrier f c= {u}
proof let x;
assume that A37: x in Carrier f and A38: not x in {u};
A39: f.x <> 0 by A37,RLVECT_2:28;
x <> u & x <> v & x <> w
by A34,A35,A37,A38,RLVECT_2:28,TARSKI:
def 1;
hence contradiction by A5,A37,A39;
end;
u in Carrier f by A33,RLVECT_2:28;
hence thesis by ZFMISC_1:37;
end;
set F = <* u *>;
A40: rng F = {u} by FINSEQ_1:56;
A41: F is one-to-one by FINSEQ_3:102;
f (#) F = <* a * u *> by RLVECT_2:42;
then Sum(f) = Sum<* a * u *> by A36,A40,A41,RLVECT_2:def 10
.= a * u by RLVECT_1:61
.= a * u + 0.V by RLVECT_1:10
.= a * u + 0.V + 0.V by RLVECT_1:10
.= a * u + b * v + 0.V by A34,RLVECT_1:23;
hence thesis by A35,RLVECT_1:23;
suppose A42: c <> 0;
A43: Carrier f = {u,w}
proof
thus Carrier f c= {u,w}
proof let x;
assume that A44: x in Carrier f and A45: not x in {u,w};
A46: f.x <> 0 by A44,RLVECT_2:28;
x <> v & x <> w & x <> u by A34,A44,A45,RLVECT_2:28,TARSKI:
def 2;
hence contradiction by A5,A44,A46;
end;
u in Carrier f & w in Carrier f by A33,A42,RLVECT_2:28;
hence {u,w} c= Carrier f by ZFMISC_1:38;
end;
set F = <* u,w *>;
A47: rng F = {u,w} by FINSEQ_2:147;
A48: F is one-to-one by A2,FINSEQ_3:103;
f (#) F = <* a * u,c * w *> by RLVECT_2:43;
then Sum(f) = Sum<* a * u,c * w *> by A43,A47,A48,RLVECT_2:def 10
.= a * u + c * w by RLVECT_1:62
.= a * u + 0.V + c * w by RLVECT_1:10;
hence thesis by A34,RLVECT_1:23;
end;
hence thesis;
suppose A49: b <> 0;
now per cases;
suppose A50: c = 0;
A51: Carrier f = {u,v}
proof
thus Carrier f c= {u,v}
proof let x;
assume that A52: x in Carrier f and A53: not x in {u,v};
A54: f.x <> 0 by A52,RLVECT_2:28;
x <> v & x <> w & x <> u by A50,A52,A53,RLVECT_2:28,TARSKI:
def 2;
hence contradiction by A5,A52,A54;
end;
v in Carrier f & u in Carrier f by A33,A49,RLVECT_2:28;
hence {u,v} c= Carrier f by ZFMISC_1:38;
end;
set F = <* u,v *>;
A55: rng F = {u,v} by FINSEQ_2:147;
A56: F is one-to-one by A1,FINSEQ_3:103;
f (#) F = <* a * u,b * v *> by RLVECT_2:43;
then Sum(f) = Sum<* a * u,b * v *> by A51,A55,A56,RLVECT_2:def 10
.= a * u + b * v by RLVECT_1:62
.= a * u + b * v + 0.V by RLVECT_1:10;
hence thesis by A50,RLVECT_1:23;
suppose A57: c <> 0;
{u,v,w} c= Carrier f
proof let x;
assume x in {u,v,w};
then x = u or x = v or x = w by ENUMSET1:13;
hence x in Carrier f by A33,A49,A57,RLVECT_2:28;
end;
then A58: Carrier f = {u,v,w} by A4,XBOOLE_0:def 10;
set F = <* u,v,w *>;
A59: rng F = {u,v,w} by FINSEQ_2:148;
A60: F is one-to-one by A1,A2,A3,FINSEQ_3:104;
f (#) F = <* a * u,b * v,c * w *> by RLVECT_2:44;
then Sum(f) = Sum
<* a * u,b * v,c * w *> by A58,A59,A60,RLVECT_2:def 10
.= a * u + b * v + c * w by RLVECT_1:63;
hence thesis;
end;
hence thesis;
end;
hence thesis;
end;
hence thesis;
end;
theorem Th10:
u <> v & u <> w & v <> w & {u,v,w} is linearly-independent iff
for a,b,c st a * u + b * v + c * w = 0.V holds a = 0 & b = 0 & c = 0
proof
thus u <> v & u <> w & v <> w & {u,v,w} is linearly-independent implies
for a,b,c st a * u + b * v + c * w = 0.V holds a = 0 & b = 0 & c = 0
proof assume that A1: u <> v and A2: u <> w and A3: v <> w and
A4: {u,v,w} is linearly-independent;
let a,b,c;
assume A5: a * u + b * v + c * w = 0.V;
deffunc F(VECTOR of V)=0;
consider f being Function of the carrier of V, REAL such that
A6: f.u = a and A7: f.v = b and A8: f.w = c and
A9: for x being VECTOR of V st x <> u & x <> v & x <> w holds f.x = F(x)
from LambdaSep3(A1,A2,A3
);
reconsider f as Element of Funcs(the carrier of V,REAL) by FUNCT_2:11;
now let x be VECTOR of V;
assume not x in {u,v,w};
then x <> u & x <> v & x <> w by ENUMSET1:14;
hence f.x = 0 by A9;
end;
then reconsider f as Linear_Combination of V by RLVECT_2:def 5;
Carrier f c= {u,v,w}
proof let x;
assume A10: x in Carrier f;
then f.x <> 0 by RLVECT_2:28;
then x = u or x = v or x = w by A9,A10;
hence thesis by ENUMSET1:14;
end;
then reconsider f as Linear_Combination of {u,v,w} by RLVECT_2:def 8;
0.V = Sum(f) by A1,A2,A3,A5,A6,A7,A8,Th9;
then not v in Carrier f & not w in Carrier f & not u in Carrier f by A4,
RLVECT_3:def 1;
hence thesis by A6,A7,A8,RLVECT_2:28;
end;
assume A11: for a,b,c st a * u + b * v + c * w = 0.V holds
a = 0 & b = 0 & c = 0;
A12: now assume A13: u = v or u = w or v = w;
now per cases by A13;
suppose u = v;
then 1 * u + (- 1) * v + 0 * w = u + (- 1) * u + 0 * w by RLVECT_1:def
9
.= u + - u + 0 * w by RLVECT_1:29
.= u + - u + 0.V by RLVECT_1:23
.= u + - u by RLVECT_1:10
.= 0.V by RLVECT_1:16;
hence contradiction by A11;
suppose u = w;
then 1 * u + 0 * v + (- 1) * w = u + 0 * v + (- 1) * u by RLVECT_1:def
9
.= u + 0.V + (- 1) * u by RLVECT_1:23
.= u + 0.V + - u by RLVECT_1:29
.= u + - u by RLVECT_1:10
.= 0.V by RLVECT_1:16;
hence contradiction by A11;
suppose v = w;
then 0 * u + 1 * v + (- 1) * w = 0 * u + 1 * v + - v by RLVECT_1:29
.= 0.V + 1 * v + - v by RLVECT_1:23
.= 0.V + v + - v by RLVECT_1:def 9
.= v + - v by RLVECT_1:10
.= 0.V by RLVECT_1:16;
hence contradiction by A11;
end;
hence contradiction;
end;
hence u <> v & u <> w & v <> w;
let l be Linear_Combination of {u,v,w};
assume Sum(l) = 0.V;
then l.u * u + l.v * v + l.w * w = 0.V by A12,Th9;
then A14: l.u = 0 & l.v = 0 & l.w = 0 by A11;
thus Carrier l c= {}
proof let x;
assume A15: x in Carrier l;
Carrier l c= {u,v,w} by RLVECT_2:def 8;
then x = u or x = v or x = w by A15,ENUMSET1:13;
hence thesis by A14,A15,RLVECT_2:28;
end;
thus {} c= Carrier l by XBOOLE_1:2;
end;
theorem Th11:
x in Lin{v} iff ex a st x = a * v
proof
thus x in Lin{v} implies ex a st x = a * v
proof assume x in Lin{v};
then consider l being Linear_Combination of {v} such that A1: x = Sum(l)
by RLVECT_3:17;
Sum(l) = l.v * v by RLVECT_2:50;
hence thesis by A1;
end;
given a such that A2: x = a * v;
deffunc F(VECTOR of V)= 0;
consider f being Function of the carrier of V, REAL such that
A3: f.v = a and A4: for z being VECTOR of V st z <> v holds f.z = F(z)
from LambdaSep1;
reconsider f as Element of Funcs(the carrier of V,REAL) by FUNCT_2:11;
now let z be VECTOR of V;
assume not z in {v};
then z <> v by TARSKI:def 1;
hence f.z = 0 by A4;
end;
then reconsider f as Linear_Combination of V by RLVECT_2:def 5;
Carrier f c= {v}
proof let x;
assume A5: x in Carrier f;
then f.x <> 0 by RLVECT_2:28;
then x = v by A4,A5;
hence thesis by TARSKI:def 1;
end;
then reconsider f as Linear_Combination of {v} by RLVECT_2:def 8;
Sum(f) = x by A2,A3,RLVECT_2:50;
hence thesis by RLVECT_3:17;
end;
theorem
v in Lin{v}
proof v in {v} by TARSKI:def 1;
hence thesis by RLVECT_3:18;
end;
theorem
x in v + Lin{w} iff ex a st x = v + a * w
proof
thus x in v + Lin{w} implies ex a st x = v + a * w
proof assume x in v + Lin{w};
then consider u being VECTOR of V such that
A1: u in Lin{w} and A2: x = v + u by RLSUB_1:79;
consider a such that A3: u = a * w by A1,Th11;
thus thesis by A2,A3;
end;
given a such that A4: x = v + a * w;
a * w in Lin{w} by Th11;
hence thesis by A4,RLSUB_1:79;
end;
theorem Th14:
x in Lin{w1,w2} iff ex a,b st x = a * w1 + b * w2
proof
thus x in Lin{w1,w2} implies ex a,b st x = a * w1 + b * w2
proof assume A1: x in Lin{w1,w2};
now per cases;
suppose w1 = w2;
then {w1,w2} = {w1} by ENUMSET1:69;
then consider a such that A2: x = a * w1 by A1,Th11;
x = a * w1 + 0.V by A2,RLVECT_1:10
.= a * w1 + 0 * w2 by RLVECT_1:23;
hence thesis;
suppose A3: w1 <> w2;
consider l being Linear_Combination of {w1,w2} such that
A4: x = Sum(l) by A1,RLVECT_3:17;
x = l.w1 * w1 + l.w2 * w2 by A3,A4,RLVECT_2:51;
hence thesis;
end;
hence thesis;
end;
given a,b such that A5: x = a * w1 + b * w2;
now per cases;
suppose A6: w1 = w2;
then x = (a + b) * w1 by A5,RLVECT_1:def 9;
then x in Lin{w1} by Th11;
hence thesis by A6,ENUMSET1:69;
suppose A7: w1 <> w2;
deffunc F(VECTOR of V)=0;
consider f being Function of the carrier of V, REAL such that
A8: f.w1 = a and A9: f.w2 = b and
A10: for u st u <> w1 & u <> w2 holds f.u = F(u) from LambdaSep2(A7);
reconsider f as Element of Funcs(the carrier of V,REAL) by FUNCT_2:11;
now let u;
assume not u in {w1,w2};
then u <> w1 & u <> w2 by TARSKI:def 2;
hence f.u = 0 by A10;
end;
then reconsider f as Linear_Combination of V by RLVECT_2:def 5;
Carrier f c= {w1,w2}
proof let x;
assume that A11: x in Carrier f and A12: not x in {w1,w2};
x <> w1 & x <> w2 by A12,TARSKI:def 2;
then f.x = 0 by A10,A11;
hence contradiction by A11,RLVECT_2:28;
end;
then reconsider f as Linear_Combination of {w1,w2} by RLVECT_2:def 8;
x = Sum(f) by A5,A7,A8,A9,RLVECT_2:51;
hence thesis by RLVECT_3:17;
end;
hence thesis;
end;
theorem
w1 in Lin{w1,w2} & w2 in Lin{w1,w2}
proof w1 in {w1,w2} & w2 in {w1,w2} by TARSKI:def 2;
hence thesis by RLVECT_3:18;
end;
theorem
x in v + Lin{w1,w2} iff ex a,b st x = v + a * w1 + b * w2
proof
thus x in v + Lin{w1,w2} implies ex a,b st x = v + a * w1 + b * w2
proof assume x in v + Lin{w1,w2};
then consider u such that A1: u in Lin{w1,w2} and A2: x = v + u
by RLSUB_1:79;
consider a,b such that A3: u = a * w1 + b * w2 by A1,Th14;
take a,b;
thus thesis by A2,A3,RLVECT_1:def 6;
end;
given a,b such that A4: x = v + a * w1 + b * w2;
a * w1 + b * w2 in Lin{w1,w2} by Th14;
then v + (a * w1 + b * w2) in v + Lin{w1,w2} by RLSUB_1:79;
hence thesis by A4,RLVECT_1:def 6;
end;
theorem Th17:
x in Lin{v1,v2,v3} iff ex a,b,c st x = a * v1 + b * v2 + c * v3
proof
thus x in Lin{v1,v2,v3} implies ex a,b,c st x = a * v1 + b * v2 + c * v3
proof assume A1: x in Lin{v1,v2,v3};
now per cases;
suppose A2: v1 <> v2 & v1 <> v3 & v2 <> v3;
consider l being Linear_Combination of {v1,v2,v3} such that
A3: x = Sum(l) by A1,RLVECT_3:17;
x = l.v1 * v1 + l.v2 * v2 + l.v3 * v3 by A2,A3,Th9;
hence thesis;
suppose v1 = v2 or v1 = v3 or v2 = v3;
then A4: {v1,v2,v3} = {v1,v3} or {v1,v2,v3} = {v1,v1,v2} or
{v1,v2,v3} = {v3,v3,v1} by ENUMSET1:70,100;
now per cases by A4,ENUMSET1:70;
suppose {v1,v2,v3} = {v1,v2};
then consider a,b such that A5: x = a * v1 + b * v2 by A1,Th14;
x = a * v1 + b * v2 + 0.V by A5,RLVECT_1:10
.= a * v1 + b * v2 + 0 * v3 by RLVECT_1:23;
hence thesis;
suppose {v1,v2,v3} = {v1,v3};
then consider a,b such that A6: x = a * v1 + b * v3 by A1,Th14;
x = a * v1 + 0.V + b * v3 by A6,RLVECT_1:10
.= a * v1 + 0 * v2 + b * v3 by RLVECT_1:23;
hence thesis;
end;
hence thesis;
end;
hence thesis;
end;
given a,b,c such that A7: x = a * v1 + b * v2 + c * v3;
now per cases;
suppose A8: v1 = v2 or v1 = v3 or v2 = v3;
now per cases by A8;
suppose v1 = v2;
then {v1,v2,v3} = {v1,v3} & x = (a + b) * v1 + c * v3
by A7,ENUMSET1:70,RLVECT_1:def 9;
hence thesis by Th14;
suppose A9: v1 = v3;
then A10: {v1,v2,v3} = {v1,v1,v2} by ENUMSET1:98
.= {v2,v1} by ENUMSET1:70;
x = b * v2 + (a * v1 + c * v1) by A7,A9,RLVECT_1:def 6
.= b * v2 + (a + c) * v1 by RLVECT_1:def 9;
hence thesis by A10,Th14;
suppose A11: v2 = v3;
then A12: x = a * v1 + (b * v2 + c * v2) by A7,RLVECT_1:def 6
.= a * v1 + (b + c) * v2 by RLVECT_1:def 9;
{v1,v2,v3} = {v2,v2,v1} by A11,ENUMSET1:100
.= {v1,v2} by ENUMSET1:70;
hence thesis by A12,Th14;
end;
hence thesis;
suppose A13: v1 <> v2 & v1 <> v3 & v2 <> v3;
then A14: v1 <> v2;
A15: v1 <> v3 by A13;
A16: v2 <> v3 by A13;
deffunc F(VECTOR of V)=0;
consider f being Function of the carrier of V,REAL such that
A17: f.v1 = a and A18: f.v2 = b and A19: f.v3 = c and
A20: for v st v <> v1 & v <> v2 & v <> v3 holds f.v = F(v)
from LambdaSep3(A14,A15,
A16);
reconsider f as Element of Funcs(the carrier of V,REAL) by FUNCT_2:11;
now let v;
assume not v in {v1,v2,v3};
then v <> v1 & v <> v2 & v <> v3 by ENUMSET1:14;
hence f.v = 0 by A20;
end;
then reconsider f as Linear_Combination of V by RLVECT_2:def 5;
Carrier f c= {v1,v2,v3}
proof let x;
assume that A21: x in Carrier f and A22: not x in {v1,v2,v3};
x <> v1 & x <> v2 & x <> v3 by A22,ENUMSET1:14;
then f.x = 0 by A20,A21;
hence thesis by A21,RLVECT_2:28;
end;
then reconsider f as Linear_Combination of {v1,v2,v3} by RLVECT_2:def 8
;
x = Sum(f) by A7,A13,A17,A18,A19,Th9;
hence thesis by RLVECT_3:17;
end;
hence thesis;
end;
theorem
w1 in Lin{w1,w2,w3} & w2 in Lin{w1,w2,w3} & w3 in Lin{w1,w2,w3}
proof w1 in {w1,w2,w3} & w2 in {w1,w2,w3} & w3 in {w1,w2,w3} by ENUMSET1:14;
hence thesis by RLVECT_3:18;
end;
theorem
x in v + Lin{w1,w2,w3} iff ex a,b,c st x = v + a * w1 + b * w2 + c * w3
proof
thus x in v + Lin{w1,w2,w3} implies
ex a,b,c st x = v + a * w1 + b * w2 + c * w3
proof assume x in v + Lin{w1,w2,w3};
then consider u such that A1: u in Lin{w1,w2,w3} and A2: x = v + u
by RLSUB_1:79;
consider a,b,c such that A3: u = a * w1 + b * w2 + c * w3 by A1,Th17;
take a,b,c;
x = v + (a * w1 + b * w2) + c * w3 by A2,A3,RLVECT_1:def 6;
hence thesis by RLVECT_1:def 6;
end;
given a,b,c such that A4: x = v + a * w1 + b * w2 + c * w3;
a * w1 + b * w2 + c * w3 in Lin{w1,w2,w3} by Th17;
then v + (a * w1 + b * w2 + c * w3) in v + Lin{w1,w2,w3} by RLSUB_1:79;
then v + (a * w1 + b * w2) + c * w3 in
v + Lin{w1,w2,w3} by RLVECT_1:def 6;
hence thesis by A4,RLVECT_1:def 6;
end;
theorem
{u,v} is linearly-independent & u <> v implies
{u,v - u} is linearly-independent
proof assume that A1: {u,v} is linearly-independent and A2: u <> v;
now let a,b;
assume a * u + b * (v - u) = 0.V;
then 0.V = a * u + (b * v - b * u) by RLVECT_1:48
.= a * u + b * v - b * u by RLVECT_1:42
.= a * u - b * u + b * v by Th2
.= (a - b) * u + b * v by RLVECT_1:49;
then a - b = 0 & b = 0 by A1,A2,RLVECT_3:14;
hence a = 0 & b = 0;
end;
hence thesis by RLVECT_3:14;
end;
theorem
{u,v} is linearly-independent & u <> v implies
{u,v + u} is linearly-independent
proof assume that A1: {u,v} is linearly-independent and A2: u <> v;
now let a,b;
assume a * u + b * (v + u) = 0.V;
then 0.V = a * u + (b * u + b * v) by RLVECT_1:def 9
.= a * u + b * u + b * v by RLVECT_1:def 6
.= (a + b) * u + b * v by RLVECT_1:def 9;
then a + b = 0 & b = 0 by A1,A2,RLVECT_3:14;
hence a = 0 & b = 0;
end;
hence thesis by RLVECT_3:14;
end;
theorem Th22:
{u,v} is linearly-independent & u <> v & a <> 0 implies
{u,a * v} is linearly-independent
proof assume that A1: {u,v} is linearly-independent and
A2: u <> v and A3: a <> 0;
now let b,c;
assume b * u + c * (a * v) = 0.V;
then 0.V = b * u + c * a * v by RLVECT_1:def 9;
then b = 0 & c * a = 0 by A1,A2,RLVECT_3:14;
hence b = 0 & c = 0 by A3,XCMPLX_1:6;
end;
hence thesis by RLVECT_3:14;
end;
theorem
{u,v} is linearly-independent & u <> v implies
{u,- v} is linearly-independent
proof assume A1: {u,v} is linearly-independent & u <> v;
- 1 <> 0 & - v = (- 1) * v by RLVECT_1:29;
hence thesis by A1,Th22;
end;
theorem Th24:
a <> b implies {a * v,b * v} is linearly-dependent
proof assume A1: a <> b;
now per cases;
suppose v = 0.V;
then a * v = 0.V by RLVECT_1:23;
hence thesis by RLVECT_3:12;
suppose v <> 0.V;
then A2: a * v <> b * v by A1,RLVECT_1:51;
A3: b * (a * v) + (- a) * (b * v)
= a * b * v + (- a) * (b * v) by RLVECT_1:def 9
.= a * b * v + - a * (b * v) by Th6
.= a * b * v - a * (b * v) by RLVECT_1:def 11
.= a * b * v - a * b * v by RLVECT_1:def 9
.= 0.V by RLVECT_1:28;
not (b = 0 & - a = 0) by A1,XCMPLX_1:135;
hence thesis by A2,A3,RLVECT_3:14;
end;
hence thesis;
end;
theorem
a <> 1 implies {v,a * v} is linearly-dependent
proof v = 1 * v by RLVECT_1:def 9;
hence thesis by Th24;
end;
theorem
{u,w,v} is linearly-independent & u <> v & u <> w & v <> w implies
{u,w,v - u} is linearly-independent
proof assume A1: {u,w,v} is linearly-independent & u <> v & u <> w & v <> w;
now let a,b,c;
assume a * u + b * w + c * (v - u) = 0.V;
then 0.V = a * u + b * w + (c * v - c * u) by RLVECT_1:48
.= a * u + (b * w + (c * v - c * u)) by RLVECT_1:def 6
.= a * u + (b * w + c * v - c * u) by RLVECT_1:42
.= a * u + (b * w - c * u + c * v) by Th2
.= a * u + (b * w - c * u) + c * v by RLVECT_1:def 6
.= a * u + b * w - c * u + c * v by RLVECT_1:42
.= a * u - c * u + b * w + c * v by Th2
.= (a - c) * u + b * w + c * v by RLVECT_1:49;
then a - c = 0 & b = 0 & c = 0 by A1,Th10;
hence a = 0 & b = 0 & c = 0;
end;
hence thesis by Th10;
end;
theorem
{u,w,v} is linearly-independent & u <> v & u <> w & v <> w implies
{u,w - u,v - u} is linearly-independent
proof assume that A1: {u,w,v} is linearly-independent &
u <> v & u <> w & v <> w;
now let a,b,c;
assume a * u + b * (w - u) + c * (v - u) = 0.V;
then 0.V = a * u + (b * w - b * u) + c * (v - u) by RLVECT_1:48
.= a * u + (b * w - b * u) + (c * v - c * u) by RLVECT_1:48
.= a * u + (b * w + - b * u) + (c * v - c * u) by RLVECT_1:def 11
.= a * u + (- b * u + b * w) + (c * v + - c * u) by RLVECT_1:def 11
.= a * u + - b * u + b * w + (- c * u + c * v) by RLVECT_1:def 6
.= a * u + - b * u + (b * w + (- c * u + c * v)) by RLVECT_1:def 6
.= a * u + - b * u + (- c * u + (b * w + c * v)) by RLVECT_1:def 6
.= a * u + - b * u + - c * u + (b * w + c * v) by RLVECT_1:def 6
.= a * u + b * (- u) + - c * u + (b * w + c * v) by RLVECT_1:39
.= a * u + (- b) * u + - c * u + (b * w + c * v) by RLVECT_1:38
.= a * u + (- b) * u + c * (- u) + (b * w + c * v) by RLVECT_1:39
.= a * u + (- b) * u + (- c) * u + (b * w + c * v) by RLVECT_1:38
.= (a + (- b)) * u + (- c) * u + (b * w + c * v) by RLVECT_1:def 9
.= (a + (- b) + (- c)) * u + (b * w + c * v) by RLVECT_1:def 9
.= (a + (- b) + (- c)) * u + b * w + c * v by RLVECT_1:def 6;
then a + (- b) + (- c) = 0 & b = 0 & c = 0 by A1,Th10;
hence a = 0 & b = 0 & c = 0;
end;
hence thesis by Th10;
end;
theorem
{u,w,v} is linearly-independent & u <> v & u <> w & v <> w implies
{u,w,v + u} is linearly-independent
proof assume A1: {u,w,v} is linearly-independent & u <> v & u <> w & v <> w;
now let a,b,c;
assume a * u + b * w + c * (v + u) = 0.V;
then 0.V = a * u + b * w + (c * u + c * v) by RLVECT_1:def 9
.= a * u + (b * w + (c * u + c * v)) by RLVECT_1:def 6
.= a * u + (c * u + (b * w + c * v)) by RLVECT_1:def 6
.= a * u + c * u + (b * w + c * v) by RLVECT_1:def 6
.= (a + c) * u + (b * w + c * v) by RLVECT_1:def 9
.= (a + c) * u + b * w + c * v by RLVECT_1:def 6;
then a + c = 0 & b = 0 & c = 0 by A1,Th10;
hence a = 0 & b = 0 & c = 0;
end;
hence thesis by Th10;
end;
theorem
{u,w,v} is linearly-independent & u <> v & u <> w & v <> w implies
{u,w + u,v + u} is linearly-independent
proof assume A1: {u,w,v} is linearly-independent & u <> v & u <> w & v <> w;
now let a,b,c;
assume a * u + b * (w + u) + c * (v + u) = 0.V;
then 0.V = a * u + (b * u + b * w) + c * (v + u) by RLVECT_1:def 9
.= a * u + b * u + b * w + c * (v + u) by RLVECT_1:def 6
.= (a + b) * u + b * w + c * (v + u) by RLVECT_1:def 9
.= (a + b) * u + b * w + (c * u + c * v) by RLVECT_1:def 9
.= (a + b) * u + (b * w + (c * u + c * v)) by RLVECT_1:def 6
.= (a + b) * u + (c * u + (b * w + c * v)) by RLVECT_1:def 6
.= (a + b) * u + c * u + (b * w + c * v) by RLVECT_1:def 6
.= (a + b + c) * u + (b * w + c * v) by RLVECT_1:def 9
.= (a + b + c) * u + b * w + c * v by RLVECT_1:def 6;
then a + b + c = 0 & b = 0 & c = 0 by A1,Th10;
hence a = 0 & b = 0 & c = 0;
end;
hence thesis by Th10;
end;
theorem Th30:
{u,w,v} is linearly-independent & u <> v & u <> w & v <> w & a <> 0 implies
{u,w,a * v} is linearly-independent
proof assume that A1: {u,w,v} is linearly-independent &
u <> v & u <> w & v <> w and A2: a <> 0;
now let b,c,d;
assume b * u + c * w + d * (a * v) = 0.V;
then 0.V = b * u + c * w + d * a * v by RLVECT_1:def 9;
then b = 0 & c = 0 & d * a = 0 by A1,Th10;
hence b = 0 & c = 0 & d = 0 by A2,XCMPLX_1:6;
end;
hence thesis by Th10;
end;
theorem Th31:
{u,w,v} is linearly-independent &
u <> v & u <> w & v <> w & a <> 0 & b <> 0 implies
{u,a * w,b * v} is linearly-independent
proof assume that A1: {u,w,v} is linearly-independent &
u <> v & u <> w & v <> w and A2: a <> 0 & b <> 0;
now let c,d,e;
assume c * u + d * (a * w) + e * (b * v) = 0.V;
then 0.V = c * u + d * a * w + e * (b * v) by RLVECT_1:def 9
.= c * u + d * a * w + e * b * v by RLVECT_1:def 9;
then c = 0 & d * a = 0 & e * b = 0 by A1,Th10;
hence c = 0 & d = 0 & e = 0 by A2,XCMPLX_1:6;
end;
hence thesis by Th10;
end;
theorem
{u,w,v} is linearly-independent & u <> v & u <> w & v <> w implies
{u,w,- v} is linearly-independent
proof - 1 <> 0 & - v = (- 1) * v by RLVECT_1:29;
hence thesis by Th30;
end;
theorem
{u,w,v} is linearly-independent & u <> v & u <> w & v <> w implies
{u,- w,- v} is linearly-independent
proof 0 <> - 1 & - v = (- 1) * v & - w = (- 1) * w
by RLVECT_1:29;
hence thesis by Th31;
end;
theorem Th34:
a <> b implies {a * v,b * v,w} is linearly-dependent
proof assume a <> b;
then {a * v,b * v} is linearly-dependent & {a * v,b * v} c= {a * v,b * v,w
}
by Th24,SETWISEO:4;
hence thesis by RLVECT_3:6;
end;
theorem
a <> 1 implies {v,a * v,w} is linearly-dependent
proof v = 1 * v by RLVECT_1:def 9;
hence thesis by Th34;
end;
theorem
v in Lin{w} & v <> 0.V implies Lin{v} = Lin{w}
proof assume that A1: v in Lin{w} and A2: v <> 0.V;
consider a such that A3: v = a * w by A1,Th11;
now let u;
thus u in Lin{v} implies u in Lin{w}
proof assume u in Lin{v};
then consider b such that A4: u = b * v by Th11;
u = b * a * w by A3,A4,RLVECT_1:def 9;
hence thesis by Th11;
end;
assume u in Lin{w};
then consider b such that A5: u = b * w by Th11;
A6: a <> 0 by A2,A3,RLVECT_1:23;
a" * v = a" * a * w by A3,RLVECT_1:def 9
.= 1 * w by A6,XCMPLX_0:def 7
.= w by RLVECT_1:def 9;
then u = b * a" * v by A5,RLVECT_1:def 9;
hence u in Lin{v} by Th11;
end;
hence thesis by RLSUB_1:39;
end;
theorem
v1 <> v2 & {v1,v2} is linearly-independent &
v1 in Lin{w1,w2} & v2 in Lin{w1,w2} implies
Lin{w1,w2} = Lin{v1,v2} & {w1,w2} is linearly-independent & w1 <> w2
proof assume that A1: v1 <> v2 and
A2: {v1,v2} is linearly-independent and
A3: v1 in Lin{w1,w2} and A4: v2 in Lin{w1,w2};
consider r1,r2 such that A5: v1 = r1 * w1 + r2 * w2 by A3,Th14;
consider r3,r4 such that A6: v2 = r3 * w1 + r4 * w2 by A4,Th14;
A7: now assume r1 = 0 & r2 = 0;
then v1 = 0.V + 0 * w2 by A5,RLVECT_1:23
.= 0.V + 0.V by RLVECT_1:23
.= 0.V by RLVECT_1:10;
hence contradiction by A2,RLVECT_3:12;
end;
now assume A8: r1 * r4 = r2 * r3;
now per cases by A7;
suppose A9: r1 <> 0;
r1" * r1 * r4 = r1" * (r2 * r3) by A8,XCMPLX_1:4;
then 1 * r4 = r1" * (r2 * r3) by A9,XCMPLX_0:def 7;
then v2 = r3 * w1 + r3 * (r1" * r2) * w2 by A6,XCMPLX_1:4
.= r3 * w1 + r3 * (r1" * r2 * w2) by RLVECT_1:def 9
.= r3 * 1 * (w1 + r1" * r2 * w2) by RLVECT_1:def 9
.= r3 * (r1" * r1) * (w1 + r1" * r2 * w2) by A9,XCMPLX_0:def 7
.= r3 * r1" * r1 * (w1 + r1" * r2 * w2) by XCMPLX_1:4
.= r3 * r1" * (r1 * (w1 + r1" * r2 * w2)) by RLVECT_1:def 9
.= r3 * r1" * (r1 * w1 + r1 * (r1" * r2 * w2)) by RLVECT_1:def
9
.= r3 * r1" * (r1 * w1 + r1 * (r1" * r2) * w2) by RLVECT_1:def
9
.= r3 * r1" * (r1 * w1 + r1 * r1" * r2 * w2) by XCMPLX_1:4
.= r3 * r1" * (r1 * w1 + 1 * r2 * w2) by A9,XCMPLX_0:def 7
.= r3 * r1" * (r1 * w1 + r2 * w2);
hence contradiction by A1,A2,A5,RLVECT_3:13;
suppose A10: r2 <> 0;
r2" * (r1 * r4) = r2" * r2 * r3 by A8,XCMPLX_1:4
.= 1 * r3 by A10,XCMPLX_0:def 7
.= r3;
then v2 = r4 * (r2" * r1) * w1 + r4 * w2 by A6,XCMPLX_1:4
.= r4 * (r2" * r1 * w1) + r4 * w2 by RLVECT_1:def 9
.= r4 * 1 * ((r2" * r1 * w1) + w2) by RLVECT_1:def 9
.= r4 * (r2" * r2) * ((r2" * r1 * w1) + w2) by A10,XCMPLX_0:def
7
.= r4 * r2" * r2 * ((r2" * r1 * w1) + w2) by XCMPLX_1:4
.= r4 * r2" * (r2 * ((r2" * r1 * w1) + w2)) by RLVECT_1:def 9
.= r4 * r2" * (r2 * (r2" * r1 * w1) + r2 * w2) by RLVECT_1:def
9
.= r4 * r2" * (r2 * (r2" * r1) * w1 + r2 * w2) by RLVECT_1:def
9
.= r4 * r2" * (r2 * r2" * r1 * w1 + r2 * w2) by XCMPLX_1:4
.= r4 * r2" * (1 * r1 * w1 + r2 * w2) by A10,XCMPLX_0:def 7
.= r4 * r2" * (r1 * w1 + r2 * w2);
hence contradiction by A1,A2,A5,RLVECT_3:13;
end;
hence contradiction;
end;
then A11: r1 * r4 - r2 * r3 <> 0 by XCMPLX_1:15;
set t = r1 * r4 - r2 * r3;
A12: now assume A13: r2 <> 0;
r2" * v1 = r2" * (r1 * w1) + r2" * (r2 * w2) by A5,RLVECT_1:def 9
.= r2" * r1 * w1 + r2" * (r2 * w2) by RLVECT_1:def 9
.= r2" * r1 * w1 + r2" * r2 * w2 by RLVECT_1:def 9
.= r2" * r1 * w1 + 1 * w2 by A13,XCMPLX_0:def 7
.= r2" * r1 * w1 + w2 by RLVECT_1:def 9;
then A14: w2 = r2" * v1 - r2" * r1 * w1 by RLSUB_2:78;
then w2 = r2" * v1 - r2" * (r1 * w1) by RLVECT_1:def 9;
then v2 = r3 * w1 + r4 * (r2" * (v1 - r1 * w1)) by A6,RLVECT_1:48
.= r3 * w1 + r4 * r2" * (v1 - r1 * w1) by RLVECT_1:def 9
.= r3 * w1 + (r4 * r2" * v1 - r4 * r2" * (r1 * w1)) by RLVECT_1:48
.= r3 * w1 + r4 * r2" * v1 - r4 * r2" * (r1 * w1) by RLVECT_1:42
.= r4 * r2" * v1 + r3 * w1 - (r4 * r2" * r1) * w1 by RLVECT_1:def
9
.= r4 * r2" * v1 + (r3 * w1 - (r4 * r2" * r1) * w1) by RLVECT_1:42
.= r4 * r2" * v1 + (r3 - (r4 * r2" * r1)) * w1 by RLVECT_1:49;
then r2 * v2 =
r2 * (r4 * r2" * v1) + r2 * ((r3 - (r4 * r2" * r1)) * w1)
by RLVECT_1:def 9
.= r2 * (r4 * r2") * v1 + r2 * ((r3 - (r4 * r2" * r1)) * w1)
by RLVECT_1:def 9
.= r4 * (r2 * r2") * v1 + r2 * ((r3 - (r4 * r2" * r1)) * w1)
by XCMPLX_1:4
.= r4 * 1 * v1 + r2 * ((r3 - (r4 * r2" * r1)) * w1) by A13,XCMPLX_0:def
7
.= r4 * v1 + r2 * (r3 - (r4 * r2" * r1)) * w1 by RLVECT_1:def 9
.= r4 * v1 + (r2 * r3 - r2 * (r2" * r4 * r1)) * w1 by XCMPLX_1:40
.= r4 * v1 + (r2 * r3 - r2 * (r2" * (r4 * r1))) * w1 by XCMPLX_1:4
.= r4 * v1 + (r2 * r3 - r2 * r2" * (r4 * r1)) * w1 by XCMPLX_1:4
.= r4 * v1 + (r2 * r3 - 1 * (r4 * r1)) * w1 by A13,XCMPLX_0:def 7
.= r4 * v1 + (- t) * w1 by XCMPLX_1:143
.= r4 * v1 + - t * w1 by Th6;
then - t * w1 = r2 * v2 - r4 * v1 by RLSUB_2:78;
then t * w1 = - (r2 * v2 - r4 * v1) by RLVECT_1:30
.= r4 * v1 + - r2 * v2 by RLVECT_1:47;
then t" * t * w1 = t" * (r4 * v1 + - r2 * v2) by RLVECT_1:def 9;
then 1 * w1 = t" * (r4 * v1 + - r2 * v2) by A11,XCMPLX_0:def 7;
then w1 = t" * (r4 * v1 + - r2 * v2) by RLVECT_1:def 9
.= t" * (r4 * v1) + t" * (- r2 * v2) by RLVECT_1:def 9
.= t" * r4 * v1 + t" * (- r2 * v2) by RLVECT_1:def 9
.= t" * r4 * v1 + t" * ((- r2) * v2) by Th6
.= t" * r4 * v1 + t" * (- r2) * v2 by RLVECT_1:def 9
.= t" * r4 * v1 + (- t") * r2 * v2 by XCMPLX_1:176
.= t" * r4 * v1 + (- t") * (r2 * v2) by RLVECT_1:def 9
.= t" * r4 * v1 + - t" * (r2 * v2) by Th6;
hence w1 = t" * r4 * v1 + - t" * r2 * v2 by RLVECT_1:def 9;
then A15: w2 =
r2" * v1 - r2" * r1 * (t" * r4 * v1 - t" * r2 * v2) by A14,RLVECT_1:
def 11
.= r2" * v1 - r2" * r1 * (t" * (r4 * v1) - t" * r2 * v2) by RLVECT_1:def
9
.= r2" * v1 - r2" * r1 * (t" * (r4 * v1) - t" * (r2 * v2)) by RLVECT_1:
def 9
.= r2" * v1 - r2" * r1 * (t" * (r4 * v1 - r2 * v2)) by RLVECT_1:48
.= r2" * v1 - r1 * r2" * t" * (r4 * v1 - r2 * v2) by RLVECT_1:def 9
.= r2" * v1 - r1 * (t" * r2") * (r4 * v1 - r2 * v2) by XCMPLX_1:4
.= r2" * v1 - r1 * ((t" * r2") * (r4 * v1 - r2 * v2)) by RLVECT_1:def 9
.= r2" * v1 - r1 * (t" * (r2" * (r4 * v1 - r2 * v2))) by RLVECT_1:def 9
.= r2" * v1 - r1 * (t" * (r2" * (r4 * v1) - r2" * (r2 * v2)))
by RLVECT_1:48
.= r2" * v1 - r1 * (t" * (r2" * (r4 * v1) - r2" * r2 * v2))
by RLVECT_1:def 9
.= r2" * v1 - r1 * (t" * (r2" * r4 * v1 - r2" * r2 * v2))
by RLVECT_1:def 9
.= r2" * v1 - r1 * (t" * (r2" * r4 * v1 - 1 * v2)) by A13,XCMPLX_0:def 7
.= r2" * v1 - r1 * (t" * (r2" * r4 * v1 - v2)) by RLVECT_1:def 9
.= r2" * v1 - r1 * (t" * (r2" * r4 * v1) - t" * v2) by RLVECT_1:48
.= r2" * v1 - (r1 * (t" * (r2" * r4 * v1)) - r1 * (t" * v2))
by RLVECT_1:48
.= r2" * v1 - r1 * (t" * (r2" * r4 * v1)) + r1 * (t" * v2) by RLVECT_1:43
.= r2" * v1 - r1 * (t" * (r2" * r4 * v1)) + r1 * t" * v2 by RLVECT_1:def
9
.= r2" * v1 - (r1 * t" * (r2" * r4 * v1)) + r1 * t" * v2 by RLVECT_1:def
9
.= r2" * v1 - (r1 * t" * (r2" * r4)) * v1 + r1 * t" * v2 by RLVECT_1:def
9
.= (r2" - (r1 * t" * (r2" * r4))) * v1 + t" * r1 * v2 by RLVECT_1:49;
r2" - (r1 * t" * (r2" * r4)) =
r2" - (r1 * (t" * (r2" * r4))) by XCMPLX_1:4
.= r2" - (r1 * (r2" * (t" * r4))) by XCMPLX_1:4
.= r2" * 1 - (r2" * (r1 * (t" * r4))) by XCMPLX_1:4
.= r2" * (1 - (r1 * (t" * r4))) by XCMPLX_1:40
.= r2" * (t" * t - (r1 * (t" * r4))) by A11,XCMPLX_0:def 7
.= r2" * (t" * t - (t" * (r1 * r4))) by XCMPLX_1:4
.= r2" * (t" * (r1 * r4 - r2 * r3 - r1 * r4)) by XCMPLX_1:40
.= r2" * (t" * (r1 * r4 + - r2 * r3 - r1 * r4)) by XCMPLX_0:def 8
.= r2" * t" * (r1 * r4 + - r2 * r3 - r1 * r4) by XCMPLX_1:4
.= r2" * t" * (- r2 * r3) by XCMPLX_1:26
.= r2" * t" * (r2 * (- r3)) by XCMPLX_1:175
.= r2" * (t" * (r2 * (- r3))) by XCMPLX_1:4
.= r2" * (t" * r2 * (- r3)) by XCMPLX_1:4
.= r2" * (r2 * t") * (- r3) by XCMPLX_1:4
.= r2" * r2 * t" * (- r3) by XCMPLX_1:4
.= 1 * t" * (- r3) by A13,XCMPLX_0:def 7
.= - (t" * r3) by XCMPLX_1:175;
hence w2 = - t" * r3 * v1 + t" * r1 * v2 by A15,Th6;
end;
now assume A16: r1 <> 0;
A17: r1" + (t" * r2 * r1" * r3) = r1" + (r1" * t" * r2 * r3) by XCMPLX_1:
4
.= r1" + (r1" * t" * (r2 * r3)) by XCMPLX_1:4
.= r1" * 1 + (r1" * (t" * (r2 * r3))) by XCMPLX_1:4
.= r1" * (1 + (t" * (r2 * r3))) by XCMPLX_1:8
.= r1" * (t" * t + (t" * (r2 * r3))) by A11,XCMPLX_0:def 7
.= r1" * (t" * (t + r2 * r3)) by XCMPLX_1:8
.= r1" * t" * (r1 * r4 - r2 * r3 + r2 * r3) by XCMPLX_1:4
.= t" * r1" * (r1 * r4) by XCMPLX_1:27
.= t" * (r1" * (r1 * r4)) by XCMPLX_1:4
.= t" * (r1" * r1 * r4) by XCMPLX_1:4
.= t" * (1 * r4) by A16,XCMPLX_0:def 7
.= t" * r4;
r1" * v1 = r1" * (r1 * w1) + r1" * (r2 * w2) by A5,RLVECT_1:def 9
.= r1" * r1 * w1 + r1" * (r2 * w2) by RLVECT_1:def 9
.= 1 * w1 + r1" * (r2 * w2) by A16,XCMPLX_0:def 7
.= w1 + r1" * (r2 * w2) by RLVECT_1:def 9
.= w1 + r2 * r1" * w2 by RLVECT_1:def 9;
then A18: w1 = r1" * v1 - r2 * r1" * w2 by RLSUB_2:78;
then v2 = r3 * (r1" * v1) - r3 * (r2 * r1"* w2) + r4 * w2
by A6,RLVECT_1:48
.= r3 * r1" * v1 - r3 * (r1" * r2 * w2) + r4 * w2 by RLVECT_1:def 9
.= r3 * r1" * v1 - r3 * (r1" * r2) * w2 + r4 * w2 by RLVECT_1:def 9
.= r3 * r1" * v1 - r1" * (r3 * r2) * w2 + r4 * w2 by XCMPLX_1:4
.= r1" * r3 * v1 - r1" * (r3 * r2 * w2) + r4 * w2 by RLVECT_1:def 9
.= r1" * (r3 * v1) - r1" * (r3 * r2 * w2) + r4 * w2 by RLVECT_1:def
9;
then r1 * v2 = r1 * (r1" * (r3 * v1) - r1" * (r3 * r2 * w2)) +
r1 * (r4 * w2) by RLVECT_1:def 9
.= r1 * (r1" * (r3 * v1) - r1" * (r3 * r2 * w2)) + r1 * r4 * w2
by RLVECT_1:def 9
.= r1 * (r1" * (r3 * v1)) - r1 * (r1" * (r3 * r2 * w2)) + r1 * r4 * w2
by RLVECT_1:48
.= r1 * r1" * (r3 * v1) - r1 * (r1" * (r3 * r2 * w2)) + r1 * r4 * w2
by RLVECT_1:def 9
.= r1 * r1" * (r3 * v1) - r1 * r1" * (r3 * r2 * w2) + r1 * r4 * w2
by RLVECT_1:def 9
.= 1 * (r3 * v1) - r1 * r1" * (r3 * r2 * w2) + r1 * r4 * w2
by A16,XCMPLX_0:
def 7
.= 1 * (r3 * v1) - 1 * (r3 * r2 * w2) + r1 * r4 * w2 by A16,XCMPLX_0:
def 7
.= r3 * v1 - 1 * (r3 * r2 * w2) + r1 * r4 * w2 by RLVECT_1:def 9
.= r3 * v1 - r3 * r2 * w2 + r1 * r4 * w2 by RLVECT_1:def 9
.= r3 * v1 - (r3 * r2 * w2 - r1 * r4 * w2) by RLVECT_1:43
.= r3 * v1 - (r3 * r2 - r1 * r4) * w2 by RLVECT_1:49
.= r3 * v1 + - (r3 * r2 - r1 * r4) * w2 by RLVECT_1:def 11
.= r3 * v1 + (- (r3 * r2 - r1 * r4)) * w2 by Th6
.= r3 * v1 + t * w2 by XCMPLX_1:143;
then t" * (r1 * v2) = t" * (r3 * v1) + t" * (t * w2) by RLVECT_1:def 9
.= t" * (r3 * v1) + t" * t * w2 by RLVECT_1:def 9
.= t" * (r3 * v1) + 1 * w2 by A11,XCMPLX_0:def 7
.= t" * (r3 * v1) + w2 by RLVECT_1:def 9;
hence w2 = t" * (r1 * v2) - t" * (r3 * v1) by RLSUB_2:78
.= t" * r1 * v2 - t" * (r3 * v1) by RLVECT_1:def 9
.= t" * r1 * v2 - t" * r3 * v1 by RLVECT_1:def 9
.= - t" * r3 * v1 + t" * r1 * v2 by RLVECT_1:def 11;
hence w1 = r1" * v1 - (r2 * r1" * (- t" * r3 * v1) +
r2 * r1" * (t" * r1 * v2)) by A18,RLVECT_1:def 9
.= r1" * v1 - (r2 * r1" * (- t" * r3 * v1) +
r2 * r1" * (t" * r1) * v2) by RLVECT_1:def 9
.= r1" * v1 - (r2 * r1" * (- t" * r3 * v1) +
r2 * (r1" * (r1 * t")) * v2) by XCMPLX_1:4
.= r1" * v1 - (r2 * r1" * (- t" * r3 * v1) +
r2 * (r1" * r1 * t") * v2) by XCMPLX_1:4
.= r1" * v1 - (r2 * r1" * (- t" * r3 * v1) +
r2 * (1 * t") * v2) by A16,XCMPLX_0:def 7
.= r1" * v1 - (r2 * r1" * (- t" * (r3 * v1)) +
r2 * t" * v2) by RLVECT_1:def 9
.= r1" * v1 - (r2 * r1" * ((- t") * (r3 * v1)) + r2 * t" * v2)
by Th6
.= r1" * v1 - (r2 * r1" * (- t") * (r3 * v1) + r2 * t" * v2)
by RLVECT_1:def 9
.= r1" * v1 - (r2 * r1" * (- t") * r3 * v1 + r2 * t" * v2)
by RLVECT_1:def 9
.= r1" * v1 - ((- t") * r2 * r1" * r3 * v1 + r2 * t" * v2) by
XCMPLX_1:4
.= r1" * v1 - (((- 1) * t" * r2) * r1" * r3 * v1 + r2 * t" * v2)
by XCMPLX_1:180
.= r1" * v1 - (((- 1) * t" * r2) * r1" * (r3 * v1) + r2 * t" * v2)
by RLVECT_1:def 9
.= r1" * v1 - (((- 1) * t" * r2) * (r1" * (r3 * v1))
+ r2 * t" * v2) by RLVECT_1:def 9
.= r1" * v1 - (((- 1) * t") * (r2 * (r1" * (r3 * v1)))
+ r2 * t" * v2) by RLVECT_1:def 9
.= r1" * v1 - ((- 1) * (t" * (r2 * (r1" * (r3 * v1))))
+ r2 * t" * v2) by RLVECT_1:def 9
.= r1" * v1 - (- (t" * (r2 * (r1" * (r3 * v1))))
+ r2 * t" * v2) by RLVECT_1:29
.= r1" * v1 - (- (t" * r2 * (r1" * (r3 * v1)))
+ r2 * t" * v2) by RLVECT_1:def 9
.= r1" * v1 - (- ((t" * r2 * r1") * (r3 * v1))
+ r2 * t" * v2) by RLVECT_1:def 9
.= r1" * v1 - (- ((t" * r2 * r1" * r3) * v1) + r2 * t" * v2)
by RLVECT_1:def 9
.= r1" * v1 - - ((t" * r2 * r1" * r3) * v1) - r2 * t" * v2
by RLVECT_1:41
.= r1" * v1 + (- - (t" * r2 * r1" * r3 * v1)) - r2 * t" * v2
by RLVECT_1:def 11
.= r1" * v1 + (t" * r2 * r1" * r3) * v1 - r2 * t" * v2
by RLVECT_1:30
.= t" * r4 * v1 - t" * r2 * v2 by A17,RLVECT_1:def 9
.= t" * r4 * v1 + - t" * r2 * v2 by RLVECT_1:def 11;
end;
then A19: w1 = t" * r4 * v1 + (- t" * r2) * v2 &
w2 = (- t" * r3) * v1 + t" * r1 * v2 by A7,A12,Th6;
set a1 = t" * r4; set a2 = - t" * r2; set a3 = - t" * r3; set a4 = t" * r1;
now let u;
thus u in Lin{w1,w2} implies u in Lin{v1,v2}
proof assume u in Lin{w1,w2};
then consider r5,r6 such that A20: u = r5 * w1 + r6 * w2 by Th14;
u = r5 * (a1 * v1) + r5 * (a2 * v2) + r6 * (a3 * v1 + a4 * v2)
by A19,A20,RLVECT_1:
def 9
.= r5 * (a1 * v1) + r5 * (a2 * v2) + (r6 * (a3 * v1) +
r6 * (a4 * v2)) by RLVECT_1:def 9
.= r5 * a1 * v1 + r5 * (a2 * v2) + (r6 * (a3 * v1) +
r6 * (a4 * v2)) by RLVECT_1:def 9
.= r5 * a1 * v1 + r5 * a2 * v2 + (r6 * (a3 * v1) +
r6 * (a4 * v2)) by RLVECT_1:def 9
.= r5 * a1 * v1 + r5 * a2 * v2 + (r6 * a3 * v1 +
r6 * (a4 * v2)) by RLVECT_1:def 9
.= r5 * a1 * v1 + r5 * a2 * v2 + (r6 * a3 * v1 +
r6 * a4 * v2) by RLVECT_1:def 9
.= r5 * a1 * v1 + (r5 * a2 * v2 + (r6 * a3 * v1 +
r6 * a4 * v2)) by RLVECT_1:def 6
.= r5 * a1 * v1 + (r6 * a3 * v1 + (r5 * a2 * v2 +
r6 * a4 * v2)) by RLVECT_1:def 6
.= r5 * a1 * v1 + r6 * a3 * v1 + (r5 * a2 * v2 +
r6 * a4 * v2) by RLVECT_1:def 6
.= (r5 * a1 + r6 * a3) * v1 + (r5 * a2 * v2 +
r6 * a4 * v2) by RLVECT_1:def 9
.= (r5 * a1 + r6 * a3) * v1 + (r5 * a2 + r6 * a4) * v2
by RLVECT_1:def 9;
hence u in Lin{v1,v2} by Th14;
end;
assume u in Lin{v1,v2};
then consider r5,r6 such that A21: u = r5 * v1 + r6 * v2 by Th14;
u = r5 * (r1 * w1 + r2 * w2) + (r6 * (r3 * w1) + r6 * (r4 * w2))
by A5,A6,A21,RLVECT_1:def 9
.= r5 * (r1 * w1) + r5 * (r2 * w2) + (r6 * (r3 * w1) + r6 * (r4 * w2))
by RLVECT_1:def 9
.= r5 * (r1 * w1) + r5 * (r2 * w2) + r6 * (r3 * w1) + r6 * (r4 * w2)
by RLVECT_1:def 6
.= r5 * (r1 * w1) + r6 * (r3 * w1) + r5 * (r2 * w2) + r6 * (r4 * w2)
by RLVECT_1:def 6
.= (r5 * r1) * w1 + r6 * (r3 * w1) + r5 * (r2 * w2) + r6 * (r4 * w2)
by RLVECT_1:def 9
.= (r5 * r1) * w1 + (r6 * r3) * w1 + r5 * (r2 * w2) + r6 * (r4 * w2)
by RLVECT_1:def 9
.= (r5 * r1) * w1 + (r6 * r3) * w1 + (r5 * r2) * w2 + r6 * (r4 * w2)
by RLVECT_1:def 9
.= (r5 * r1) * w1 + (r6 * r3) * w1 + (r5 * r2) * w2 + (r6 * r4) * w2
by RLVECT_1:def 9
.= ((r5 * r1) + (r6 * r3)) * w1 + (r5 * r2) * w2 + (r6 * r4) * w2
by RLVECT_1:def 9
.= ((r5 * r1) + (r6 * r3)) * w1 + ((r5 * r2) * w2 + (r6 * r4) * w2)
by RLVECT_1:def 6
.= ((r5 * r1) + (r6 * r3)) * w1 + ((r5 * r2) + (r6 * r4)) * w2
by RLVECT_1:def 9;
hence u in Lin{w1,w2} by Th14;
end;
hence Lin{w1,w2} = Lin{v1,v2} by RLSUB_1:39;
now let a,b;
assume a * w1 + b * w2 = 0.V;
then 0.V = a * (a1 * v1) + a * (a2 * v2) + b * (a3 * v1 + a4 * v2)
by A19,RLVECT_1:def 9
.= a * (a1 * v1) + a * (a2 * v2) + (b * (a3 * v1) + b * (a4 * v2))
by RLVECT_1:def 9
.= a * a1 * v1 + a * (a2 * v2) + (b * (a3 * v1) + b * (a4 * v2))
by RLVECT_1:def 9
.= a * a1 * v1 + a * (a2 * v2) + (b * (a3 * v1) + b * a4 * v2)
by RLVECT_1:def 9
.= a * a1 * v1 + a * (a2 * v2) + (b * a3 * v1 + b * a4 * v2)
by RLVECT_1:def 9
.= a * a1 * v1 + a * a2 * v2 + (b * a3 * v1 + b * a4 * v2)
by RLVECT_1:def 9
.= a * a1 * v1 + (a * a2 * v2 + (b * a3 * v1 + b * a4 * v2))
by RLVECT_1:def 6
.= a * a1 * v1 + (b * a3 * v1 + (a * a2 * v2 + b * a4 * v2))
by RLVECT_1:def 6
.= a * a1 * v1 + b * a3 * v1 + (a * a2 * v2 + b * a4 * v2)
by RLVECT_1:def 6
.= (a * a1 + b * a3) * v1 + (a * a2 * v2 + b * a4 * v2) by RLVECT_1:def
9
.= (a * a1 + b * a3) * v1 + (a * a2 + b * a4) * v2 by RLVECT_1:def 9;
then A22: a * a1 + b * a3 = 0 & a * a2 + b * a4 = 0 by A1,A2,RLVECT_3:14
;
a * a1 = t" * r4 * a & b * a3 = t" * (- r3) * b &
a * a2 = t" * (- r2) * a & b * a4 = t" * r1 * b by XCMPLX_1:175;
then a * a1 = t" * (r4 * a) & b * a3 = t" * ((- r3) * b) &
a * a2 = t" * ((- r2) * a) & b * a4 = t" * (r1 * b) by XCMPLX_1:4;
then 0 = t" * (r4 * a + (- r3) * b) &
0 = t" * ((- r2) * a + r1 * b) & t" <> 0 by A11,A22,XCMPLX_1:8,203;
then r4 * a + (- r3) * b = 0 & (- r2) * a + r1 * b = 0 by XCMPLX_1:6;
then r4 * a + - r3 * b = 0 & r1 * b + (- r2) * a = 0
by XCMPLX_1:175;
then r4 * a - r3 * b = 0 & r1 * b + - r2 * a = 0
by XCMPLX_0:def 8,XCMPLX_1:175
;
then A23: a * r4 = r3 * b & r1 * b = a * r2 &
r4 * a = b * r3 & b * r1 = r2 * a by XCMPLX_1:15,136;
assume A24: a <> 0 or b <> 0;
now per cases by A24;
suppose A25: a <> 0;
a" * a * r4 = a" * (r3 * b) & a" * (r1 * b) = a" * a * r2
by A23,XCMPLX_1:4;
then 1 * r4 = a" * (r3 * b) & a" * (r1 * b) = 1 * r2 by A25,XCMPLX_0:
def 7;
then r4 = r3 * (a" * b) & r2 = r1 * (a" * b) by XCMPLX_1:4;
then v1 = r1 * w1 + r1 * ((a" * b) * w2) &
v2 = r3 * w1 + r3 * ((a" * b) * w2) by A5,A6,RLVECT_1:def 9;
then v1 = r1 * (w1 + a" * b * w2) &
v2 = r3 * (w1 + a" * b * w2) by RLVECT_1:def 9;
hence contradiction by A1,A2,Th24;
suppose A26: b <> 0;
b" * b * r3 = b" * (r4 * a) & b" * b * r1 = b" * (r2 * a)
by A23,XCMPLX_1:4;
then 1 * r3 = b" * (r4 * a) & 1 * r1 = b" * (r2 * a) by A26,XCMPLX_0:
def 7;
then r3 = r4 * (b" * a) & r1 = r2 * (b" * a) by XCMPLX_1:4;
then v1 = r2 * ((b" * a) * w1) + r2 * w2 &
v2 = r4 * ((b" * a) * w1) + r4 * w2 by A5,A6,RLVECT_1:def 9;
then v1 = r2 * ((b" * a) * w1 + w2) &
v2 = r4 * ((b" * a) * w1 + w2) by RLVECT_1:def 9;
hence contradiction by A1,A2,Th24;
end;
hence contradiction;
end;
hence thesis by RLVECT_3:14;
end;
theorem
w <> 0.V & {v,w} is linearly-dependent implies ex a st v = a * w
proof assume that A1: w <> 0.V and A2: {v,w} is linearly-dependent;
consider a,b such that A3: a * v + b * w = 0.V and A4: a <> 0 or b <> 0
by A2,RLVECT_3:14;
A5: a * v = - b * w by A3,RLVECT_1:19;
now per cases;
suppose A6: a <> 0;
a" * a * v = a" * (- b * w) by A5,RLVECT_1:def 9;
then 1 * v = a" * (- b * w) by A6,XCMPLX_0:def 7;
then v = a" * (- b * w) by RLVECT_1:def 9
.= a" * ((- b) * w) by Th6
.= a" * (- b) * w by RLVECT_1:def 9;
hence thesis;
suppose a = 0;
then 0.V = - b * w & b <> 0 by A4,A5,RLVECT_1:23;
then 0.V = (- b) * w & - b <> 0 by Th6,XCMPLX_1:135;
hence thesis by A1,RLVECT_1:24;
end;
hence thesis;
end;
theorem
v <> w & {v,w} is linearly-independent & {u,v,w} is linearly-dependent
implies
ex a,b st u = a * v + b * w
proof assume that A1: v <> w and
A2: {v,w} is linearly-independent and
A3: {u,v,w} is linearly-dependent;
consider a,b,c such that A4: a * u + b * v + c * w = 0.V and
A5: a <> 0 or b <> 0 or c <> 0 by A3,Th10;
now per cases;
suppose A6: a <> 0;
a * u + (b * v + c * w) = 0.V by A4,RLVECT_1:def 6;
then a * u = - (b * v + c * w) by RLVECT_1:19;
then a" * a * u = a" * (- (b * v + c * w)) by RLVECT_1:def 9;
then 1 * u = a" * (- (b * v + c * w)) by A6,XCMPLX_0:def 7;
then u = a" * (- (b * v + c * w)) by RLVECT_1:def 9
.= a" * ((- 1) * (b * v + c * w)) by RLVECT_1:29
.= a" * (- 1) * (b * v + c * w) by RLVECT_1:def 9
.= a" * (- 1) * (b * v) + a" * (- 1) * (c * w) by RLVECT_1:def 9
.= a" * (- 1) * b * v + a" * (- 1) * (c * w) by RLVECT_1:def 9
.= a" * (- 1) * b * v + a" * (- 1) * c * w by RLVECT_1:def 9;
hence thesis;
suppose A7: a = 0;
then 0.V = 0.V + b * v + c * w by A4,RLVECT_1:23
.= b * v + c * w by RLVECT_1:10;
hence thesis by A1,A2,A5,A7,RLVECT_3:14;
end;
hence thesis;
end;