:: Subspaces of Real Linear Space Generated by One, Two, or Three Vectors
:: and Their Cosets
:: by Wojciech A. Trybulec
::
:: Received February 24, 1993
:: Copyright (c) 1993-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies REAL_1, RLVECT_1, RLSUB_1, XBOOLE_0, SUBSET_1, FUNCT_1, RLVECT_2,
CARD_1, STRUCT_0, NUMBERS, FUNCT_2, TARSKI, ARYTM_3, ARYTM_1, SUPINF_2,
RELAT_1, CARD_3, FINSEQ_1, VALUED_1, RLVECT_3;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, FINSEQ_1, FUNCT_1,
FUNCT_2, XCMPLX_0, XREAL_0, REAL_1, DOMAIN_1, FINSEQ_4, STRUCT_0,
RLSUB_1, RLVECT_1, RLVECT_2, RLVECT_3;
constructors DOMAIN_1, REAL_1, FINSEQ_4, RLVECT_2, RLVECT_3, RELSET_1;
registrations RELSET_1, FINSET_1, NUMBERS, STRUCT_0, ORDINAL1, XREAL_0;
requirements NUMERALS, SUBSET, BOOLE, ARITHM;
definitions RLVECT_3, TARSKI, XBOOLE_0;
equalities XBOOLE_0, RLVECT_1;
expansions 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, XCMPLX_0, XCMPLX_1,
FINSEQ_2, XREAL_0;
schemes FUNCT_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();
A5: x = A2() implies thesis by A1,A3;
A6: x = A3() implies thesis by A2,A3;
x = A1() implies thesis by A1,A2;
hence thesis by A5,A6;
end;
consider f being Function of D(),R() such that
A7: for x being Element of D() holds P[x,f.x] from FUNCT_2:sch 3(A4);
take f;
thus thesis by A7;
end;
Lm1: now let V be RealLinearSpace, v be VECTOR of V, a be Real;
thus ex l being Linear_Combination of {v} st l.v = a
proof
reconsider zz=0, a as Element of REAL by XREAL_0:def 1;
deffunc F(VECTOR of V)=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 = F(u) from FUNCT_2:
sch 6;
reconsider f as Element of Funcs(the carrier of V,REAL) by FUNCT_2:8;
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 3;
Carrier f c= {v}
proof
let x be object;
assume that
A3: x in Carrier f and
A4: not x in {v};
f.x <> 0 & x <> v by A3,A4,RLVECT_2:19,TARSKI:def 1;
hence thesis by A2,A3;
end;
then reconsider f as Linear_Combination of {v} by RLVECT_2:def 6;
take f;
thus thesis by A1;
end;
end;
Lm2: now let V be RealLinearSpace, v1, v2 be VECTOR of V, a, b be Real;
assume
A1: v1 <> v2;
thus ex l being Linear_Combination of {v1,v2} st l.v1 = a & l.v2 = b
proof
reconsider zz=0, a, b as Element of REAL by XREAL_0:def 1;
deffunc F(VECTOR of V)=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 = F(u)
from FUNCT_2:sch 7(A1);
reconsider f as Element of Funcs(the carrier of V,REAL) by FUNCT_2:8;
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 3;
Carrier f c= {v1,v2}
proof
let x be object;
assume that
A4: x in Carrier f and
A5: not x in {v1,v2};
A6: x <> v2 by A5,TARSKI:def 2;
f.x <> 0 & x <> v1 by A4,A5,RLVECT_2:19,TARSKI:def 2;
hence thesis by A3,A4,A6;
end;
then reconsider f as Linear_Combination of {v1,v2} by RLVECT_2:def 6;
take f;
thus thesis by A2;
end;
end;
Lm3: now let V be RealLinearSpace, v1, v2, v3 be VECTOR of V,
a, b, c be Real;
assume that
A1: v1 <> v2 and
A2: v1 <> v3 and
A3: v2 <> v3;
thus ex l being Linear_Combination of {v1,v2,v3} st l.v1 = a & l.v2
= b & l.v3 = c
proof
reconsider zz=0, a, b, c as Element of REAL by XREAL_0:def 1;
deffunc F(VECTOR of V)=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 = F(u) from LambdaSep3(A1,A2,A3);
reconsider f as Element of Funcs(the carrier of V,REAL) by FUNCT_2:8;
now
let u be VECTOR of V;
assume
A6: not u in {v1,v2,v3};
then
A7: u <> v3 by ENUMSET1:def 1;
u <> v1 & u <> v2 by A6,ENUMSET1:def 1;
hence f.u = 0 by A5,A7;
end;
then reconsider f as Linear_Combination of V by RLVECT_2:def 3;
Carrier f c= {v1,v2,v3}
proof
let x be object;
assume that
A8: x in Carrier f and
A9: not x in {v1,v2,v3};
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 thesis by A5,A8,A10;
end;
then reconsider f as Linear_Combination of {v1,v2,v3} by RLVECT_2:def 6;
take f;
thus thesis by A4;
end;
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:61;
thus w + v - v = w by RLSUB_2:61;
thus
A1: v - v + w = 0.V + w by RLVECT_1:15
.= w by RLVECT_1:4;
thus w - v + v = w by RLSUB_2:61;
thus thesis by A1,RLSUB_2:61,RLVECT_1:29;
end;
:: RLVECT_1:37 extended
theorem
v1 - w = v2 - w implies v1 = v2
proof
assume v1 - w = v2 - w;
then - (v1 - w) = w - v2 by RLVECT_1:33;
then w - v1 = w - v2 by RLVECT_1:33;
hence thesis by RLVECT_1:23;
end;
:: Composition of RLVECT_1:38 and RLVECT_1:39
theorem Th3:
- (a * v) = (- a) * v
proof
thus - (a * v) = a * (- v) by RLVECT_1:25
.= (- a) * v by RLVECT_1:24;
end;
theorem
W1 is Subspace of W2 implies v + W1 c= v + W2
proof
assume
A1: W1 is Subspace of W2;
let x be object;
assume x in v + W1;
then consider u such that
A2: u in W1 and
A3: x = v + u by RLSUB_1:63;
u in W2 by A1,A2,RLSUB_1:8;
hence thesis by A3,RLSUB_1:63;
end;
theorem
u in v + W implies v + W = u + W
proof
reconsider C = v + W as Coset of W by RLSUB_1:def 6;
assume u in v + W;
then C = u + W by RLSUB_1:78;
hence thesis;
end;
theorem Th6:
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 c = f.w;
set b = f.v;
set a = f.u;
A4: Carrier f c= {u,v,w} by RLVECT_2:def 6;
A5: now
let x be VECTOR of V;
assume x <> v & x <> u & x <> w;
then not x in Carrier f by A4,ENUMSET1:def 1;
hence f.x = 0 by RLVECT_2:19;
end;
now
per cases;
suppose
A6: a = 0;
now
per cases;
suppose
A7: b = 0;
now
per cases;
suppose
A8: c = 0;
now
set x = the Element of Carrier f;
assume
A9: Carrier f <> {};
then
A10: x is VECTOR of V by TARSKI:def 3;
then f.x <> 0 by A9,RLVECT_2:19;
hence contradiction by A5,A6,A7,A8,A10;
end;
then f = ZeroLC(V) by RLVECT_2:def 5;
hence Sum(f) = 0.V by RLVECT_2:30
.= f.u * u by A6,RLVECT_1:10
.= f.u * u + 0.V by RLVECT_1:4
.= f.u * u + f.v * v by A7,RLVECT_1:10
.= f.u * u + f.v * v + 0.V by RLVECT_1:4
.= f.u * u + f.v * v + f.w * w by A8,RLVECT_1:10;
end;
suppose
A11: c <> 0;
A12: Carrier f c= {w}
proof
let x be object;
assume that
A13: x in Carrier f and
A14: not x in {w};
f.x <> 0 & x <> w by A13,A14,RLVECT_2:19,TARSKI:def 1;
hence contradiction by A5,A6,A7,A13;
end;
w in Carrier f by A11,RLVECT_2:19;
then
A15: Carrier f = {w} by A12,ZFMISC_1:33;
set F = <* w *>;
A16: f (#) F = <* c * w *> by RLVECT_2:26;
rng F = {w} & F is one-to-one by FINSEQ_1:39,FINSEQ_3:93;
then Sum(f) = Sum<* c * w *> by A15,A16,RLVECT_2:def 8
.= c * w by RLVECT_1:44
.= 0.V + c * w by RLVECT_1:4
.= 0.V + 0.V + c * w by RLVECT_1:4
.= a * u + 0.V + c * w by A6,RLVECT_1:10;
hence thesis by A7,RLVECT_1:10;
end;
end;
hence thesis;
end;
suppose
A17: b <> 0;
now
per cases;
suppose
A18: c = 0;
A19: Carrier f c= {v}
proof
let x be object;
assume that
A20: x in Carrier f and
A21: not x in {v};
f.x <> 0 & x <> v by A20,A21,RLVECT_2:19,TARSKI:def 1;
hence contradiction by A5,A6,A18,A20;
end;
v in Carrier f by A17,RLVECT_2:19;
then
A22: Carrier f = {v} by A19,ZFMISC_1:33;
set F = <* v *>;
A23: f (#) F = <* b * v *> by RLVECT_2:26;
rng F = {v} & F is one-to-one by FINSEQ_1:39,FINSEQ_3:93;
then Sum(f) = Sum<* b * v *> by A22,A23,RLVECT_2:def 8
.= b * v by RLVECT_1:44
.= 0.V + b * v by RLVECT_1:4
.= 0.V + b * v + 0.V by RLVECT_1:4
.= a * u + b * v + 0.V by A6,RLVECT_1:10;
hence thesis by A18,RLVECT_1:10;
end;
suppose
c <> 0;
then
A24: w in Carrier f by RLVECT_2:19;
A25: Carrier f c= {v,w}
proof
let x be object;
assume that
A26: x in Carrier f and
A27: not x in {v,w};
A28: x <> w by A27,TARSKI:def 2;
f.x <> 0 & x <> v by A26,A27,RLVECT_2:19,TARSKI:def 2;
hence contradiction by A5,A6,A26,A28;
end;
v in Carrier f by A17,RLVECT_2:19;
then {v,w } c= Carrier f by A24,ZFMISC_1:32;
then
A29: Carrier f = {v,w} by A25;
set F = <* v,w *>;
A30: f (#) F = <* b * v,c * w *> by RLVECT_2:27;
rng F = {v,w} & F is one-to-one by A3,FINSEQ_2:127,FINSEQ_3:94;
then Sum(f) = Sum<* b * v,c * w *> by A29,A30,RLVECT_2:def 8
.= b * v + c * w by RLVECT_1:45
.= 0.V + b * v + c * w by RLVECT_1:4;
hence thesis by A6,RLVECT_1:10;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
suppose
A31: a <> 0;
now
per cases;
suppose
A32: b = 0;
now
per cases;
suppose
A33: c = 0;
A34: Carrier f c= {u}
proof
let x be object;
assume that
A35: x in Carrier f and
A36: not x in {u};
f.x <> 0 & x <> u by A35,A36,RLVECT_2:19,TARSKI:def 1;
hence contradiction by A5,A32,A33,A35;
end;
u in Carrier f by A31,RLVECT_2:19;
then
A37: Carrier f = {u} by A34,ZFMISC_1:33;
set F = <* u *>;
A38: f (#) F = <* a * u *> by RLVECT_2:26;
rng F = {u} & F is one-to-one by FINSEQ_1:39,FINSEQ_3:93;
then Sum(f) = Sum<* a * u *> by A37,A38,RLVECT_2:def 8
.= a * u by RLVECT_1:44
.= a * u + 0.V by RLVECT_1:4
.= a * u + 0.V + 0.V by RLVECT_1:4
.= a * u + b * v + 0.V by A32,RLVECT_1:10;
hence thesis by A33,RLVECT_1:10;
end;
suppose
c <> 0;
then
A39: w in Carrier f by RLVECT_2:19;
A40: Carrier f c= {u,w}
proof
let x be object;
assume that
A41: x in Carrier f and
A42: not x in {u,w};
A43: x <> u by A42,TARSKI:def 2;
f.x <> 0 & x <> w by A41,A42,RLVECT_2:19,TARSKI:def 2;
hence contradiction by A5,A32,A41,A43;
end;
u in Carrier f by A31,RLVECT_2:19;
then {u,w} c= Carrier f by A39,ZFMISC_1:32;
then
A44: Carrier f = {u,w} by A40;
set F = <* u,w *>;
A45: f (#) F = <* a * u,c * w *> by RLVECT_2:27;
rng F = {u,w} & F is one-to-one by A2,FINSEQ_2:127,FINSEQ_3:94;
then Sum(f) = Sum<* a * u,c * w *> by A44,A45,RLVECT_2:def 8
.= a * u + c * w by RLVECT_1:45
.= a * u + 0.V + c * w by RLVECT_1:4;
hence thesis by A32,RLVECT_1:10;
end;
end;
hence thesis;
end;
suppose
A46: b <> 0;
now
per cases;
suppose
A47: c = 0;
A48: Carrier f c= {u,v}
proof
let x be object;
assume that
A49: x in Carrier f and
A50: not x in {u,v};
A51: x <> u by A50,TARSKI:def 2;
f.x <> 0 & x <> v by A49,A50,RLVECT_2:19,TARSKI:def 2;
hence contradiction by A5,A47,A49,A51;
end;
v in Carrier f & u in Carrier f by A31,A46,RLVECT_2:19;
then {u,v} c= Carrier f by ZFMISC_1:32;
then
A52: Carrier f = {u,v} by A48;
set F = <* u,v *>;
A53: f (#) F = <* a * u,b * v *> by RLVECT_2:27;
rng F = {u,v} & F is one-to-one by A1,FINSEQ_2:127,FINSEQ_3:94;
then Sum(f) = Sum<* a * u,b * v *> by A52,A53,RLVECT_2:def 8
.= a * u + b * v by RLVECT_1:45
.= a * u + b * v + 0.V by RLVECT_1:4;
hence thesis by A47,RLVECT_1:10;
end;
suppose
A54: c <> 0;
{u,v,w} c= Carrier f
proof
let x be object;
assume x in {u,v,w};
then x = u or x = v or x = w by ENUMSET1:def 1;
hence thesis by A31,A46,A54,RLVECT_2:19;
end;
then
A55: Carrier f = {u,v,w} by A4;
set F = <* u,v,w *>;
A56: f (#) F = <* a * u,b * v,c * w *> by RLVECT_2:28;
rng F = {u,v,w} & F is one-to-one by A1,A2,A3,FINSEQ_2:128
,FINSEQ_3:95;
then Sum(f) = Sum <* a * u,b * v,c * w *> by A55,A56,
RLVECT_2:def 8
.= a * u + b * v + c * w by RLVECT_1:46;
hence thesis;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
reconsider zz=0 as Element of REAL by XREAL_0:def 1;
theorem Th7:
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
deffunc F(VECTOR of V)=zz;
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;
reconsider aa=a, bb=b, cc=c as Element of REAL by XREAL_0:def 1;
consider f being Function of the carrier of V, REAL such that
A5: f.u = aa & f.v = bb & f.w = cc and
A6: 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:8;
now
let x be VECTOR of V;
assume
A7: not x in {u,v,w};
then
A8: x <> w by ENUMSET1:def 1;
x <> u & x <> v by A7,ENUMSET1:def 1;
hence f.x = 0 by A6,A8;
end;
then reconsider f as Linear_Combination of V by RLVECT_2:def 3;
Carrier f c= {u,v,w}
proof
let x be object;
assume
A9: x in Carrier f;
then f.x <> 0 by RLVECT_2:19;
then x = u or x = v or x = w by A6,A9;
hence thesis by ENUMSET1:def 1;
end;
then reconsider f as Linear_Combination of {u,v,w} by RLVECT_2:def 6;
assume a * u + b * v + c * w = 0.V;
then
A10: 0.V = Sum(f) by A1,A2,A3,A5,Th6;
then
A11: not u in Carrier f by A4;
( not v in Carrier f)& not w in Carrier f by A4,A10;
hence thesis by A5,A11,RLVECT_2:19;
end;
assume
A12: for a,b,c st a * u + b * v + c * w = 0.V holds a = 0 & b = 0 & c = 0;
A13: now
assume
A14: u = v or u = w or v = w;
now
per cases by A14;
suppose
u = v;
then 1 * u + (- 1) * v + 0 * w = u + (- 1) * u + 0 * w by
RLVECT_1:def 8
.= u + - u + 0 * w by RLVECT_1:16
.= u + - u + 0.V by RLVECT_1:10
.= u + - u by RLVECT_1:4
.= 0.V by RLVECT_1:5;
hence contradiction by A12;
end;
suppose
u = w;
then 1 * u + 0 * v + (- 1) * w = u + 0 * v + (- 1) * u by
RLVECT_1:def 8
.= u + 0.V + (- 1) * u by RLVECT_1:10
.= u + 0.V + - u by RLVECT_1:16
.= u + - u by RLVECT_1:4
.= 0.V by RLVECT_1:5;
hence contradiction by A12;
end;
suppose
v = w;
then 0 * u + 1 * v + (- 1) * w = 0 * u + 1 * v + - v by RLVECT_1:16
.= 0.V + 1 * v + - v by RLVECT_1:10
.= 0.V + v + - v by RLVECT_1:def 8
.= v + - v by RLVECT_1:4
.= 0.V by RLVECT_1:5;
hence contradiction by A12;
end;
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
A15: l.u * u + l.v * v + l.w * w = 0.V by A13,Th6;
then
A16: l.w = 0 by A12;
A17: l.u = 0 & l.v = 0 by A12,A15;
thus Carrier l c= {}
proof
let x be object;
assume
A18: x in Carrier l;
Carrier l c= {u,v,w} by RLVECT_2:def 6;
then x = u or x = v or x = w by A18,ENUMSET1:def 1;
hence thesis by A17,A16,A18,RLVECT_2:19;
end;
thus thesis;
end;
theorem Th8:
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:14;
Sum(l) = l.v * v by RLVECT_2:32;
hence thesis by A1;
end;
given a such that
A2: x = a * v;
deffunc F(VECTOR of V)= zz;
reconsider aa=a as Element of REAL by XREAL_0:def 1;
consider f being Function of the carrier of V, REAL such that
A3: f.v = aa and
A4: for z being VECTOR of V st z <> v holds f.z = F(z) from FUNCT_2:sch 6;
reconsider f as Element of Funcs(the carrier of V,REAL) by FUNCT_2:8;
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 3;
Carrier f c= {v}
proof
let x be object;
assume
A5: x in Carrier f;
then f.x <> 0 by RLVECT_2:19;
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 6;
Sum(f) = x by A2,A3,RLVECT_2:32;
hence thesis by RLVECT_3:14;
end;
theorem
v in Lin{v}
proof
v in {v} by TARSKI:def 1;
hence thesis by RLVECT_3:15;
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:63;
ex a st u = a * w by A1,Th8;
hence thesis by A2;
end;
given a such that
A3: x = v + a * w;
a * w in Lin{w} by Th8;
hence thesis by A3,RLSUB_1:63;
end;
theorem Th11:
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:29;
then consider a such that
A2: x = a * w1 by A1,Th8;
x = a * w1 + 0.V by A2,RLVECT_1:4
.= a * w1 + 0 * w2 by RLVECT_1:10;
hence thesis;
end;
suppose
A3: w1 <> w2;
consider l being Linear_Combination of {w1,w2} such that
A4: x = Sum(l) by A1,RLVECT_3:14;
x = l.w1 * w1 + l.w2 * w2 by A3,A4,RLVECT_2:33;
hence thesis;
end;
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 6;
then x in Lin{w1} by Th8;
hence thesis by A6,ENUMSET1:29;
end;
suppose
A7: w1 <> w2;
deffunc F(VECTOR of V)=zz;
reconsider aa=a, bb=b as Element of REAL by XREAL_0:def 1;
consider f being Function of the carrier of V, REAL such that
A8: f.w1 = aa & f.w2 = bb and
A9: for u st u <> w1 & u <> w2 holds f.u = F(u) from FUNCT_2:sch 7(
A7);
reconsider f as Element of Funcs(the carrier of V,REAL) by FUNCT_2:8;
now
let u;
assume not u in {w1,w2};
then u <> w1 & u <> w2 by TARSKI:def 2;
hence f.u = 0 by A9;
end;
then reconsider f as Linear_Combination of V by RLVECT_2:def 3;
Carrier f c= {w1,w2}
proof
let x be object;
assume that
A10: x in Carrier f and
A11: not x in {w1,w2};
x <> w1 & x <> w2 by A11,TARSKI:def 2;
then f.x = 0 by A9,A10;
hence contradiction by A10,RLVECT_2:19;
end;
then reconsider f as Linear_Combination of {w1,w2} by RLVECT_2:def 6;
x = Sum(f) by A5,A7,A8,RLVECT_2:33;
hence thesis by RLVECT_3:14;
end;
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:15;
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:63;
consider a,b such that
A3: u = a * w1 + b * w2 by A1,Th11;
take a,b;
thus thesis by A2,A3,RLVECT_1:def 3;
end;
given a,b such that
A4: x = v + a * w1 + b * w2;
a * w1 + b * w2 in Lin{w1,w2} by Th11;
then v + (a * w1 + b * w2) in v + Lin{w1,w2} by RLSUB_1:63;
hence thesis by A4,RLVECT_1:def 3;
end;
theorem Th14:
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:14;
x = l.v1 * v1 + l.v2 * v2 + l.v3 * v3 by A2,A3,Th6;
hence thesis;
end;
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:30,59;
now
per cases by A4,ENUMSET1:30;
suppose
{v1,v2,v3} = {v1,v2};
then consider a,b such that
A5: x = a * v1 + b * v2 by A1,Th11;
x = a * v1 + b * v2 + 0.V by A5,RLVECT_1:4
.= a * v1 + b * v2 + 0 * v3 by RLVECT_1:10;
hence thesis;
end;
suppose
{v1,v2,v3} = {v1,v3};
then consider a,b such that
A6: x = a * v1 + b * v3 by A1,Th11;
x = a * v1 + 0.V + b * v3 by A6,RLVECT_1:4
.= a * v1 + 0 * v2 + b * v3 by RLVECT_1:10;
hence thesis;
end;
end;
hence thesis;
end;
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:30,RLVECT_1:def 6;
hence thesis by Th11;
end;
suppose
A9: v1 = v3;
then
A10: {v1,v2,v3} = {v1,v1,v2} by ENUMSET1:57
.= {v2,v1} by ENUMSET1:30;
x = b * v2 + (a * v1 + c * v1) by A7,A9,RLVECT_1:def 3
.= b * v2 + (a + c) * v1 by RLVECT_1:def 6;
hence thesis by A10,Th11;
end;
suppose
A11: v2 = v3;
then
A12: {v1,v2,v3} = {v2,v2,v1} by ENUMSET1:59
.= {v1,v2} by ENUMSET1:30;
x = a * v1 + (b * v2 + c * v2) by A7,A11,RLVECT_1:def 3
.= a * v1 + (b + c) * v2 by RLVECT_1:def 6;
hence thesis by A12,Th11;
end;
end;
hence thesis;
end;
suppose
A13: v1 <> v2 & v1 <> v3 & v2 <> v3;
deffunc F(VECTOR of V)=zz;
A14: v1 <> v3 by A13;
A15: v2 <> v3 by A13;
A16: v1 <> v2 by A13;
reconsider aa=a, bb=b, cc=c as Element of REAL by XREAL_0:def 1;
consider f being Function of the carrier of V,REAL such that
A17: f.v1 = aa & f.v2 = bb & f.v3 = cc and
A18: for v st v <> v1 & v <> v2 & v <> v3 holds f.v = F(v) from
LambdaSep3(A16,A14, A15);
reconsider f as Element of Funcs(the carrier of V,REAL) by FUNCT_2:8;
now
let v;
assume
A19: not v in {v1,v2,v3};
then
A20: v <> v3 by ENUMSET1:def 1;
v <> v1 & v <> v2 by A19,ENUMSET1:def 1;
hence f.v = 0 by A18,A20;
end;
then reconsider f as Linear_Combination of V by RLVECT_2:def 3;
Carrier f c= {v1,v2,v3}
proof
let x be object;
assume that
A21: x in Carrier f and
A22: not x in {v1,v2,v3};
A23: x <> v3 by A22,ENUMSET1:def 1;
x <> v1 & x <> v2 by A22,ENUMSET1:def 1;
then f.x = 0 by A18,A21,A23;
hence thesis by A21,RLVECT_2:19;
end;
then reconsider f as Linear_Combination of {v1,v2,v3} by RLVECT_2:def 6;
x = Sum(f) by A7,A13,A17,Th6;
hence thesis by RLVECT_3:14;
end;
end;
hence thesis;
end;
theorem
w1 in Lin{w1,w2,w3} & w2 in Lin{w1,w2,w3} & w3 in Lin{w1,w2,w3}
proof
A1: w3 in {w1,w2,w3} by ENUMSET1:def 1;
w1 in {w1,w2,w3} & w2 in {w1,w2,w3} by ENUMSET1:def 1;
hence thesis by A1,RLVECT_3:15;
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:63;
consider a,b,c such that
A3: u = a * w1 + b * w2 + c * w3 by A1,Th14;
take a,b,c;
x = v + (a * w1 + b * w2) + c * w3 by A2,A3,RLVECT_1:def 3;
hence thesis by RLVECT_1:def 3;
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 Th14;
then v + (a * w1 + b * w2 + c * w3) in v + Lin{w1,w2,w3} by RLSUB_1:63;
then v + (a * w1 + b * w2) + c * w3 in v + Lin{w1,w2,w3} by RLVECT_1:def 3;
hence thesis by A4,RLVECT_1:def 3;
end;
theorem
{u,v} is linearly-independent & u <> v implies {u,v - u} is
linearly-independent
proof
assume
A1: {u,v} is linearly-independent & u <> v;
now
let a,b;
assume a * u + b * (v - u) = 0.V;
then
A2: 0.V = a * u + (b * v - b * u) by RLVECT_1:34
.= a * u + b * v - b * u by RLVECT_1:def 3
.= a * u - b * u + b * v by RLVECT_1:def 3
.= (a - b) * u + b * v by RLVECT_1:35;
then a - b = 0 by A1,RLVECT_3:13;
hence a = 0 & b = 0 by A1,A2,RLVECT_3:13;
end;
hence thesis by RLVECT_3:13;
end;
theorem
{u,v} is linearly-independent & u <> v implies {u,v + u} is
linearly-independent
proof
assume
A1: {u,v} is linearly-independent & u <> v;
now
let a,b;
assume a * u + b * (v + u) = 0.V;
then
A2: 0.V = a * u + (b * u + b * v) by RLVECT_1:def 5
.= a * u + b * u + b * v by RLVECT_1:def 3
.= (a + b) * u + b * v by RLVECT_1:def 6;
then b = 0 by A1,RLVECT_3:13;
hence a = 0 & b = 0 by A1,A2,RLVECT_3:13;
end;
hence thesis by RLVECT_3:13;
end;
theorem Th19:
{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 & u <> v and
A2: a <> 0;
now
let b,c;
assume b * u + c * (a * v) = 0.V;
then
A3: 0.V = b * u + c * a * v by RLVECT_1:def 7;
then c * a = 0 by A1,RLVECT_3:13;
hence b = 0 & c = 0 by A1,A2,A3,RLVECT_3:13,XCMPLX_1:6;
end;
hence thesis by RLVECT_3:13;
end;
theorem
{u,v} is linearly-independent & u <> v implies {u,- v} is
linearly-independent
proof
A1: - v = (- 1) * v by RLVECT_1:16;
assume {u,v} is linearly-independent & u <> v;
hence thesis by A1,Th19;
end;
theorem Th21:
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:10;
hence thesis by RLVECT_3:11;
end;
suppose
A2: v <> 0.V;
A3: b * (a * v) + (- a) * (b * v) = a * b * v + (- a) * (b * v) by
RLVECT_1:def 7
.= a * b * v - a * (b * v) by Th3
.= a * b * v - a * b * v by RLVECT_1:def 7
.= 0.V by RLVECT_1:15;
A4: not (b = 0 & - a = 0) by A1;
a * v <> b * v by A1,A2,RLVECT_1:37;
hence thesis by A3,A4,RLVECT_3:13;
end;
end;
hence thesis;
end;
theorem
a <> 1 implies {v,a * v} is linearly-dependent
proof
v = 1 * v by RLVECT_1:def 8;
hence thesis by Th21;
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
A2: 0.V = a * u + b * w + (c * v - c * u) by RLVECT_1:34
.= a * u + (b * w + (c * v - c * u)) by RLVECT_1:def 3
.= a * u + (b * w + c * v - c * u) by RLVECT_1:def 3
.= a * u + (b * w - c * u + c * v) by RLVECT_1:def 3
.= a * u + (b * w - c * u) + c * v by RLVECT_1:def 3
.= a * u + b * w - c * u + c * v by RLVECT_1:def 3
.= a * u - c * u + b * w + c * v by RLVECT_1:def 3
.= (a - c) * u + b * w + c * v by RLVECT_1:35;
then a - c = 0 by A1,Th7;
hence a = 0 & b = 0 & c = 0 by A1,A2,Th7;
end;
hence thesis by Th7;
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
A2: 0.V = a * u + (b * w - b * u) + c * (v - u) by RLVECT_1:34
.= a * u + (b * w + - b * u) + (c * v - c * u) by RLVECT_1:34
.= a * u + - b * u + b * w + (- c * u + c * v) by RLVECT_1:def 3
.= a * u + - b * u + (b * w + (- c * u + c * v)) by RLVECT_1:def 3
.= a * u + - b * u + (- c * u + (b * w + c * v)) by RLVECT_1:def 3
.= a * u + - b * u + - c * u + (b * w + c * v) by RLVECT_1:def 3
.= a * u + b * (- u) + - c * u + (b * w + c * v) by RLVECT_1:25
.= a * u + (- b) * u + - c * u + (b * w + c * v) by RLVECT_1:24
.= a * u + (- b) * u + c * (- u) + (b * w + c * v) by RLVECT_1:25
.= a * u + (- b) * u + (- c) * u + (b * w + c * v) by RLVECT_1:24
.= (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 6
.= (a + (- b) + (- c)) * u + b * w + c * v by RLVECT_1:def 3;
then a + (- b) + (- c) = 0 & b = 0 by A1,Th7;
hence a = 0 & b = 0 & c = 0 by A1,A2,Th7;
end;
hence thesis by Th7;
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
A2: 0.V = a * u + b * w + (c * u + c * v) by RLVECT_1:def 5
.= a * u + (b * w + (c * u + c * v)) by RLVECT_1:def 3
.= a * u + (c * u + (b * w + c * v)) by RLVECT_1:def 3
.= a * u + c * u + (b * w + c * v) by RLVECT_1:def 3
.= (a + c) * u + (b * w + c * v) by RLVECT_1:def 6
.= (a + c) * u + b * w + c * v by RLVECT_1:def 3;
then c = 0 by A1,Th7;
hence a = 0 & b = 0 & c = 0 by A1,A2,Th7;
end;
hence thesis by Th7;
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
A2: 0.V = a * u + (b * u + b * w) + c * (v + u) by RLVECT_1:def 5
.= a * u + b * u + b * w + c * (v + u) by RLVECT_1:def 3
.= (a + b) * u + b * w + c * (v + u) by RLVECT_1:def 6
.= (a + b) * u + b * w + (c * u + c * v) by RLVECT_1:def 5
.= (a + b) * u + (b * w + (c * u + c * v)) by RLVECT_1:def 3
.= (a + b) * u + (c * u + (b * w + c * v)) by RLVECT_1:def 3
.= (a + b) * u + c * u + (b * w + c * v) by RLVECT_1:def 3
.= (a + b + c) * u + (b * w + c * v) by RLVECT_1:def 6
.= (a + b + c) * u + b * w + c * v by RLVECT_1:def 3;
then a + b + c = 0 & b = 0 by A1,Th7;
hence a = 0 & b = 0 & c = 0 by A1,A2,Th7;
end;
hence thesis by Th7;
end;
theorem Th27:
{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
A3: 0.V = b * u + c * w + d * a * v by RLVECT_1:def 7;
then d * a = 0 by A1,Th7;
hence b = 0 & c = 0 & d = 0 by A1,A2,A3,Th7,XCMPLX_1:6;
end;
hence thesis by Th7;
end;
theorem Th28:
{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
A3: 0.V = c * u + d * a * w + e * (b * v) by RLVECT_1:def 7
.= c * u + d * a * w + e * b * v by RLVECT_1:def 7;
then d * a = 0 & e * b = 0 by A1,Th7;
hence c = 0 & d = 0 & e = 0 by A1,A2,A3,Th7,XCMPLX_1:6;
end;
hence thesis by Th7;
end;
theorem
{u,w,v} is linearly-independent & u <> v & u <> w & v <> w implies {u,
w,- v} is linearly-independent
proof
- v = (- 1) * v by RLVECT_1:16;
hence thesis by Th27;
end;
theorem
{u,w,v} is linearly-independent & u <> v & u <> w & v <> w implies {u,
- w,- v} is linearly-independent
proof
- v = (- 1) * v & - w = (- 1) * w by RLVECT_1:16;
hence thesis by Th28;
end;
theorem Th31:
a <> b implies {a * v,b * v,w} is linearly-dependent
proof
assume a <> b;
then {a * v,b * v} is linearly-dependent by Th21;
hence thesis by RLVECT_3:5,SETWISEO:2;
end;
theorem
a <> 1 implies {v,a * v,w} is linearly-dependent
proof
v = 1 * v by RLVECT_1:def 8;
hence thesis by Th31;
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,Th8;
now
let u;
A4: a <> 0 by A2,A3,RLVECT_1:10;
thus u in Lin{v} implies u in Lin{w}
proof
assume u in Lin{v};
then consider b such that
A5: u = b * v by Th8;
u = b * a * w by A3,A5,RLVECT_1:def 7;
hence thesis by Th8;
end;
assume u in Lin{w};
then consider b such that
A6: u = b * w by Th8;
a" * v = a" * a * w by A3,RLVECT_1:def 7
.= 1 * w by A4,XCMPLX_0:def 7
.= w by RLVECT_1:def 8;
then u = b * a" * v by A6,RLVECT_1:def 7;
hence u in Lin{v} by Th8;
end;
hence thesis by RLSUB_1:31;
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,Th11;
consider r3,r4 such that
A6: v2 = r3 * w1 + r4 * w2 by A4,Th11;
set t = r1 * r4 - r2 * r3;
A7: now
assume r1 = 0 & r2 = 0;
then v1 = 0.V + 0 * w2 by A5,RLVECT_1:10
.= 0.V + 0.V by RLVECT_1:10
.= 0.V by RLVECT_1:4;
hence contradiction by A2,RLVECT_3:11;
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
.= r3 * w1 + r3 * (r1" * r2 * w2) by RLVECT_1:def 7
.= r3 * 1 * (w1 + r1" * r2 * w2) by RLVECT_1:def 5
.= r3 * (r1" * r1) * (w1 + r1" * r2 * w2) by A9,XCMPLX_0:def 7
.= r3 * r1" * r1 * (w1 + r1" * r2 * w2)
.= r3 * r1" * (r1 * (w1 + r1" * r2 * w2)) by RLVECT_1:def 7
.= r3 * r1" * (r1 * w1 + r1 * (r1" * r2 * w2)) by RLVECT_1:def 5
.= r3 * r1" * (r1 * w1 + r1 * (r1" * r2) * w2) by RLVECT_1:def 7
.= r3 * r1" * (r1 * w1 + r1 * r1" * r2 * w2)
.= 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:12;
end;
suppose
A10: r2 <> 0;
r2" * (r1 * r4) = r2" * (r2 * r3) by A8
.= r2" * r2 * r3
.= 1 * r3 by A10,XCMPLX_0:def 7
.= r3;
then v2 = r4 * (r2" * r1) * w1 + r4 * w2 by A6
.= r4 * (r2" * r1 * w1) + r4 * w2 by RLVECT_1:def 7
.= r4 * 1 * ((r2" * r1 * w1) + w2) by RLVECT_1:def 5
.= r4 * (r2" * r2) * ((r2" * r1 * w1) + w2) by A10,XCMPLX_0:def 7
.= r4 * r2" * r2 * ((r2" * r1 * w1) + w2)
.= r4 * r2" * (r2 * ((r2" * r1 * w1) + w2)) by RLVECT_1:def 7
.= r4 * r2" * (r2 * (r2" * r1 * w1) + r2 * w2) by RLVECT_1:def 5
.= r4 * r2" * (r2 * (r2" * r1) * w1 + r2 * w2) by RLVECT_1:def 7
.= r4 * r2" * (r2 * r2" * r1 * w1 + r2 * w2)
.= 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:12;
end;
end;
hence contradiction;
end;
then
A11: r1 * r4 - r2 * r3 <> 0;
A12: now
assume
A13: r2 <> 0;
r2" * v1 = r2" * (r1 * w1) + r2" * (r2 * w2) by A5,RLVECT_1:def 5
.= r2" * r1 * w1 + r2" * (r2 * w2) by RLVECT_1:def 7
.= r2" * r1 * w1 + r2" * r2 * w2 by RLVECT_1:def 7
.= r2" * r1 * w1 + 1 * w2 by A13,XCMPLX_0:def 7
.= r2" * r1 * w1 + w2 by RLVECT_1:def 8;
then
A14: w2 = r2" * v1 - r2" * r1 * w1 by RLSUB_2:61;
then w2 = r2" * v1 - r2" * (r1 * w1) by RLVECT_1:def 7;
then v2 = r3 * w1 + r4 * (r2" * (v1 - r1 * w1)) by A6,RLVECT_1:34
.= r3 * w1 + r4 * r2" * (v1 - r1 * w1) by RLVECT_1:def 7
.= r3 * w1 + (r4 * r2" * v1 - r4 * r2" * (r1 * w1)) by RLVECT_1:34
.= r3 * w1 + r4 * r2" * v1 - r4 * r2" * (r1 * w1) by RLVECT_1:def 3
.= r4 * r2" * v1 + r3 * w1 - (r4 * r2" * r1) * w1 by RLVECT_1:def 7
.= r4 * r2" * v1 + (r3 * w1 - (r4 * r2" * r1) * w1) by RLVECT_1:def 3
.= r4 * r2" * v1 + (r3 - (r4 * r2" * r1)) * w1 by RLVECT_1:35;
then r2 * v2 = r2 * (r4 * r2" * v1) + r2 * ((r3 - (r4 * r2" * r1)) * w1)
by RLVECT_1:def 5
.= r2 * (r4 * r2") * v1 + r2 * ((r3 - (r4 * r2" * r1)) * w1) by
RLVECT_1:def 7
.= r4 * (r2 * r2") * v1 + r2 * ((r3 - (r4 * r2" * r1)) * w1)
.= 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 7
.= r4 * v1 + (r2 * r3 - r2 * r2" * (r4 * r1)) * w1
.= r4 * v1 + (r2 * r3 - 1 * (r4 * r1)) * w1 by A13,XCMPLX_0:def 7
.= r4 * v1 + (- t) * w1
.= r4 * v1 + - t * w1 by Th3;
then - t * w1 = r2 * v2 - r4 * v1 by RLSUB_2:61;
then t * w1 = - (r2 * v2 - r4 * v1) by RLVECT_1:17
.= r4 * v1 + - r2 * v2 by RLVECT_1:33;
then t" * t * w1 = t" * (r4 * v1 + - r2 * v2) by RLVECT_1:def 7;
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 8
.= t" * (r4 * v1) + t" * (- r2 * v2) by RLVECT_1:def 5
.= t" * r4 * v1 + t" * (- r2 * v2) by RLVECT_1:def 7
.= t" * r4 * v1 + t" * ((- r2) * v2) by Th3
.= t" * r4 * v1 + t" * (- r2) * v2 by RLVECT_1:def 7
.= t" * r4 * v1 + (- t") * r2 * v2
.= t" * r4 * v1 + (- t") * (r2 * v2) by RLVECT_1:def 7
.= t" * r4 * v1 + - t" * (r2 * v2) by Th3;
hence w1 = t" * r4 * v1 + - t" * r2 * v2 by RLVECT_1:def 7;
then
A15: w2 = r2" * v1 - r2" * r1 * (t" * (r4 * v1) - t" * r2 * v2) by A14,
RLVECT_1:def 7
.= r2" * v1 - r2" * r1 * (t" * (r4 * v1) - t" * (r2 * v2)) by
RLVECT_1:def 7
.= r2" * v1 - r2" * r1 * (t" * (r4 * v1 - r2 * v2)) by RLVECT_1:34
.= r2" * v1 - r1 * r2" * t" * (r4 * v1 - r2 * v2) by RLVECT_1:def 7
.= r2" * v1 - r1 * (t" * r2") * (r4 * v1 - r2 * v2)
.= r2" * v1 - r1 * ((t" * r2") * (r4 * v1 - r2 * v2)) by RLVECT_1:def 7
.= r2" * v1 - r1 * (t" * (r2" * (r4 * v1 - r2 * v2))) by RLVECT_1:def 7
.= r2" * v1 - r1 * (t" * (r2" * (r4 * v1) - r2" * (r2 * v2))) by
RLVECT_1:34
.= r2" * v1 - r1 * (t" * (r2" * (r4 * v1) - r2" * r2 * v2)) by
RLVECT_1:def 7
.= r2" * v1 - r1 * (t" * (r2" * r4 * v1 - r2" * r2 * v2)) by
RLVECT_1:def 7
.= 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 8
.= r2" * v1 - r1 * (t" * (r2" * r4 * v1) - t" * v2) by RLVECT_1:34
.= r2" * v1 - (r1 * (t" * (r2" * r4 * v1)) - r1 * (t" * v2)) by
RLVECT_1:34
.= r2" * v1 - r1 * (t" * (r2" * r4 * v1)) + r1 * (t" * v2) by RLVECT_1:29
.= r2" * v1 - r1 * (t" * (r2" * r4 * v1)) + r1 * t" * v2 by
RLVECT_1:def 7
.= r2" * v1 - (r1 * t" * (r2" * r4 * v1)) + r1 * t" * v2 by
RLVECT_1:def 7
.= r2" * v1 - (r1 * t" * (r2" * r4)) * v1 + r1 * t" * v2 by
RLVECT_1:def 7
.= (r2" - (r1 * t" * (r2" * r4))) * v1 + t" * r1 * v2 by RLVECT_1:35;
r2" - (r1 * t" * (r2" * r4)) = r2" * (1 - (r1 * (t" * r4)))
.= r2" * (t" * t - (t" * (r1 * r4))) by A11,XCMPLX_0:def 7
.= r2" * r2 * t" * (- r3)
.= 1 * t" * (- r3) by A13,XCMPLX_0:def 7
.= - (t" * r3);
hence w2 = - t" * r3 * v1 + t" * r1 * v2 by A15,Th3;
end;
set a4 = t" * r1;
set a3 = - t" * r3;
set a2 = - t" * r2;
set a1 = t" * r4;
now
assume
A16: r1 <> 0;
A17: r1" + (t" * r2 * r1" * r3) = r1" * (1 + (t" * (r2 * r3)))
.= r1" * (t" * t + (t" * (r2 * r3))) by A11,XCMPLX_0:def 7
.= t" * (r1" * r1 * r4)
.= t" * (1 * r4) by A16,XCMPLX_0:def 7
.= t" * r4;
r1" * v1 = r1" * (r1 * w1) + r1" * (r2 * w2) by A5,RLVECT_1:def 5
.= r1" * r1 * w1 + r1" * (r2 * w2) by RLVECT_1:def 7
.= 1 * w1 + r1" * (r2 * w2) by A16,XCMPLX_0:def 7
.= w1 + r1" * (r2 * w2) by RLVECT_1:def 8
.= w1 + r2 * r1" * w2 by RLVECT_1:def 7;
then
A18: w1 = r1" * v1 - r2 * r1" * w2 by RLSUB_2:61;
then v2 = r3 * (r1" * v1) - r3 * (r2 * r1"* w2) + r4 * w2 by A6,RLVECT_1:34
.= r3 * r1" * v1 - r3 * (r1" * r2 * w2) + r4 * w2 by RLVECT_1:def 7
.= r3 * r1" * v1 - r3 * (r1" * r2) * w2 + r4 * w2 by RLVECT_1:def 7
.= r3 * r1" * v1 - r1" * (r3 * r2) * w2 + r4 * w2
.= r1" * r3 * v1 - r1" * (r3 * r2 * w2) + r4 * w2 by RLVECT_1:def 7
.= r1" * (r3 * v1) - r1" * (r3 * r2 * w2) + r4 * w2 by RLVECT_1:def 7;
then r1 * v2 = r1 * (r1" * (r3 * v1) - r1" * (r3 * r2 * w2)) + r1 * (r4 *
w2) by RLVECT_1:def 5
.= r1 * (r1" * (r3 * v1) - r1" * (r3 * r2 * w2)) + r1 * r4 * w2 by
RLVECT_1:def 7
.= r1 * (r1" * (r3 * v1)) - r1 * (r1" * (r3 * r2 * w2)) + r1 * r4 * w2
by RLVECT_1:34
.= r1 * r1" * (r3 * v1) - r1 * (r1" * (r3 * r2 * w2)) + r1 * r4 * w2
by RLVECT_1:def 7
.= r1 * r1" * (r3 * v1) - r1 * r1" * (r3 * r2 * w2) + r1 * r4 * w2 by
RLVECT_1:def 7
.= 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 8
.= r3 * v1 - r3 * r2 * w2 + r1 * r4 * w2 by RLVECT_1:def 8
.= r3 * v1 - (r3 * r2 * w2 - r1 * r4 * w2) by RLVECT_1:29
.= r3 * v1 + - (r3 * r2 - r1 * r4) * w2 by RLVECT_1:35
.= r3 * v1 + (- (r3 * r2 - r1 * r4)) * w2 by Th3
.= r3 * v1 + t * w2;
then t" * (r1 * v2) = t" * (r3 * v1) + t" * (t * w2) by RLVECT_1:def 5
.= t" * (r3 * v1) + t" * t * w2 by RLVECT_1:def 7
.= t" * (r3 * v1) + 1 * w2 by A11,XCMPLX_0:def 7
.= t" * (r3 * v1) + w2 by RLVECT_1:def 8;
hence w2 = t" * (r1 * v2) - t" * (r3 * v1) by RLSUB_2:61
.= t" * r1 * v2 - t" * (r3 * v1) by RLVECT_1:def 7
.= - t" * r3 * v1 + t" * r1 * v2 by RLVECT_1:def 7;
hence w1 = r1" * v1 - (r2 * r1" * (- t" * r3 * v1) + r2 * r1" * (t" * r1 *
v2)) by A18,RLVECT_1:def 5
.= r1" * v1 - (r2 * r1" * (- t" * r3 * v1) + r2 * r1" * (t" * r1) * v2
) by RLVECT_1:def 7
.= r1" * v1 - (r2 * r1" * (- t" * r3 * v1) + r2 * (r1" * r1 * t") * v2
)
.= 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 7
.= r1" * v1 - (r2 * r1" * ((- t") * (r3 * v1)) + r2 * t" * v2) by Th3
.= r1" * v1 - (r2 * r1" * (- t") * (r3 * v1) + r2 * t" * v2) by
RLVECT_1:def 7
.= r1" * v1 - (((- 1) * t" * r2) * r1" * (r3 * v1) + r2 * t" * v2)
.= r1" * v1 - (((- 1) * t" * r2) * (r1" * (r3 * v1)) + r2 * t" * v2)
by RLVECT_1:def 7
.= r1" * v1 - (((- 1) * t") * (r2 * (r1" * (r3 * v1))) + r2 * t" * v2)
by RLVECT_1:def 7
.= r1" * v1 - ((- 1) * (t" * (r2 * (r1" * (r3 * v1)))) + r2 * t" * v2)
by RLVECT_1:def 7
.= r1" * v1 - (- (t" * (r2 * (r1" * (r3 * v1)))) + r2 * t" * v2) by
RLVECT_1:16
.= r1" * v1 - (- (t" * r2 * (r1" * (r3 * v1))) + r2 * t" * v2) by
RLVECT_1:def 7
.= r1" * v1 - (- ((t" * r2 * r1") * (r3 * v1)) + r2 * t" * v2) by
RLVECT_1:def 7
.= r1" * v1 - (- ((t" * r2 * r1" * r3) * v1) + r2 * t" * v2) by
RLVECT_1:def 7
.= r1" * v1 - - ((t" * r2 * r1" * r3) * v1) - r2 * t" * v2 by RLVECT_1:27
.= r1" * v1 + (t" * r2 * r1" * r3) * v1 - r2 * t" * v2 by RLVECT_1:17
.= t" * r4 * v1 + - t" * r2 * v2 by A17,RLVECT_1:def 6;
end;
then
A19: w1 = t" * r4 * v1 + (- t" * r2) * v2 & w2 = (- t" * r3) * v1 + t" * r1
* v2 by A7,A12,Th3;
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 Th11;
u = r5 * (a1 * v1) + r5 * (a2 * v2) + r6 * (a3 * v1 + a4 * v2) by A19,A20
,RLVECT_1:def 5
.= r5 * (a1 * v1) + r5 * (a2 * v2) + (r6 * (a3 * v1) + r6 * (a4 * v2
)) by RLVECT_1:def 5
.= r5 * a1 * v1 + r5 * (a2 * v2) + (r6 * (a3 * v1) + r6 * (a4 * v2))
by RLVECT_1:def 7
.= r5 * a1 * v1 + r5 * a2 * v2 + (r6 * (a3 * v1) + r6 * (a4 * v2))
by RLVECT_1:def 7
.= r5 * a1 * v1 + r5 * a2 * v2 + (r6 * a3 * v1 + r6 * (a4 * v2)) by
RLVECT_1:def 7
.= r5 * a1 * v1 + r5 * a2 * v2 + (r6 * a3 * v1 + r6 * a4 * v2) by
RLVECT_1:def 7
.= r5 * a1 * v1 + (r5 * a2 * v2 + (r6 * a3 * v1 + r6 * a4 * v2)) by
RLVECT_1:def 3
.= r5 * a1 * v1 + (r6 * a3 * v1 + (r5 * a2 * v2 + r6 * a4 * v2)) by
RLVECT_1:def 3
.= r5 * a1 * v1 + r6 * a3 * v1 + (r5 * a2 * v2 + r6 * a4 * v2) by
RLVECT_1:def 3
.= (r5 * a1 + r6 * a3) * v1 + (r5 * a2 * v2 + r6 * a4 * v2) by
RLVECT_1:def 6
.= (r5 * a1 + r6 * a3) * v1 + (r5 * a2 + r6 * a4) * v2 by
RLVECT_1:def 6;
hence thesis by Th11;
end;
assume u in Lin{v1,v2};
then consider r5,r6 such that
A21: u = r5 * v1 + r6 * v2 by Th11;
u = r5 * (r1 * w1 + r2 * w2) + (r6 * (r3 * w1) + r6 * (r4 * w2)) by A5,A6
,A21,RLVECT_1:def 5
.= r5 * (r1 * w1) + r5 * (r2 * w2) + (r6 * (r3 * w1) + r6 * (r4 * w2))
by RLVECT_1:def 5
.= r5 * (r1 * w1) + r5 * (r2 * w2) + r6 * (r3 * w1) + r6 * (r4 * w2)
by RLVECT_1:def 3
.= r5 * (r1 * w1) + r6 * (r3 * w1) + r5 * (r2 * w2) + r6 * (r4 * w2)
by RLVECT_1:def 3
.= (r5 * r1) * w1 + r6 * (r3 * w1) + r5 * (r2 * w2) + r6 * (r4 * w2)
by RLVECT_1:def 7
.= (r5 * r1) * w1 + (r6 * r3) * w1 + r5 * (r2 * w2) + r6 * (r4 * w2)
by RLVECT_1:def 7
.= (r5 * r1) * w1 + (r6 * r3) * w1 + (r5 * r2) * w2 + r6 * (r4 * w2)
by RLVECT_1:def 7
.= (r5 * r1) * w1 + (r6 * r3) * w1 + (r5 * r2) * w2 + (r6 * r4) * w2
by RLVECT_1:def 7
.= ((r5 * r1) + (r6 * r3)) * w1 + (r5 * r2) * w2 + (r6 * r4) * w2 by
RLVECT_1:def 6
.= ((r5 * r1) + (r6 * r3)) * w1 + ((r5 * r2) * w2 + (r6 * r4) * w2) by
RLVECT_1:def 3
.= ((r5 * r1) + (r6 * r3)) * w1 + ((r5 * r2) + (r6 * r4)) * w2 by
RLVECT_1:def 6;
hence u in Lin{w1,w2} by Th11;
end;
hence Lin{w1,w2} = Lin{v1,v2} by RLSUB_1:31;
now
let a,b;
A22: t" <> 0 by A11,XCMPLX_1:202;
assume a * w1 + b * w2 = 0.V;
then
A23: 0.V = a * (a1 * v1) + a * (a2 * v2) + b * (a3 * v1 + a4 * v2) by A19,
RLVECT_1:def 5
.= a * (a1 * v1) + a * (a2 * v2) + (b * (a3 * v1) + b * (a4 * v2)) by
RLVECT_1:def 5
.= a * a1 * v1 + a * (a2 * v2) + (b * (a3 * v1) + b * (a4 * v2)) by
RLVECT_1:def 7
.= a * a1 * v1 + a * (a2 * v2) + (b * (a3 * v1) + b * a4 * v2) by
RLVECT_1:def 7
.= a * a1 * v1 + a * (a2 * v2) + (b * a3 * v1 + b * a4 * v2) by
RLVECT_1:def 7
.= a * a1 * v1 + a * a2 * v2 + (b * a3 * v1 + b * a4 * v2) by
RLVECT_1:def 7
.= a * a1 * v1 + (a * a2 * v2 + (b * a3 * v1 + b * a4 * v2)) by
RLVECT_1:def 3
.= a * a1 * v1 + (b * a3 * v1 + (a * a2 * v2 + b * a4 * v2)) by
RLVECT_1:def 3
.= a * a1 * v1 + b * a3 * v1 + (a * a2 * v2 + b * a4 * v2) by
RLVECT_1:def 3
.= (a * a1 + b * a3) * v1 + (a * a2 * v2 + b * a4 * v2) by RLVECT_1:def 6
.= (a * a1 + b * a3) * v1 + (a * a2 + b * a4) * v2 by RLVECT_1:def 6;
then 0 = t" * (r4 * a + (- r3) * b) by A1,A2,RLVECT_3:13;
then
A24: r4 * a - r3 * b = 0 by A22,XCMPLX_1:6;
0 = t" * ((- r2) * a + r1 * b) by A1,A2,A23,RLVECT_3:13;
then
A25: r1 * b + - r2 * a = 0 by A22,XCMPLX_1:6;
assume
A26: a <> 0 or b <> 0;
now
per cases by A26;
suppose
A27: a <> 0;
a" * (r1 * b) = a" * a * r2 by A25,XCMPLX_1:4;
then a" * (r1 * b) = 1 * r2 by A27,XCMPLX_0:def 7;
then r2 = r1 * (a" * b);
then v1 = r1 * w1 + r1 * ((a" * b) * w2) by A5,RLVECT_1:def 7;
then
A28: v1 = r1 * (w1 + a" * b * w2) by RLVECT_1:def 5;
a" * a * r4 = a" * (r3 * b) by A24,XCMPLX_1:4;
then 1 * r4 = a" * (r3 * b) by A27,XCMPLX_0:def 7;
then r4 = r3 * (a" * b);
then v2 = r3 * w1 + r3 * ((a" * b) * w2) by A6,RLVECT_1:def 7;
then v2 = r3 * (w1 + a" * b * w2) by RLVECT_1:def 5;
hence contradiction by A1,A2,A28,Th21;
end;
suppose
A29: b <> 0;
b" * b * r1 = b" * (r2 * a) by A25,XCMPLX_1:4;
then 1 * r1 = b" * (r2 * a) by A29,XCMPLX_0:def 7;
then r1 = r2 * (b" * a);
then v1 = r2 * ((b" * a) * w1) + r2 * w2 by A5,RLVECT_1:def 7;
then
A30: v1 = r2 * ((b" * a) * w1 + w2) by RLVECT_1:def 5;
b" * b * r3 = b" * (r4 * a) by A24,XCMPLX_1:4;
then 1 * r3 = b" * (r4 * a) by A29,XCMPLX_0:def 7;
then r3 = r4 * (b" * a);
then v2 = r4 * ((b" * a) * w1) + r4 * w2 by A6,RLVECT_1:def 7;
then v2 = r4 * ((b" * a) * w1 + w2) by RLVECT_1:def 5;
hence contradiction by A1,A2,A30,Th21;
end;
end;
hence contradiction;
end;
hence thesis by RLVECT_3:13;
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:13;
A5: a * v = - b * w by A3,RLVECT_1:6;
now
per cases;
suppose
A6: a <> 0;
a" * a * v = a" * (- b * w) by A5,RLVECT_1:def 7;
then 1 * v = a" * (- b * w) by A6,XCMPLX_0:def 7;
then v = a" * (- b * w) by RLVECT_1:def 8
.= a" * ((- b) * w) by Th3
.= a" * (- b) * w by RLVECT_1:def 7;
hence thesis;
end;
suppose
A7: a = 0;
then 0.V = - b * w by A5,RLVECT_1:10;
then
A8: 0.V = (- b) * w by Th3;
- b <> 0 by A4,A7;
hence thesis by A1,A8,RLVECT_1:11;
end;
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 & {v,w} is linearly-independent and
A2: {u,v,w} is linearly-dependent;
consider a,b,c such that
A3: a * u + b * v + c * w = 0.V and
A4: a <> 0 or b <> 0 or c <> 0 by A2,Th7;
now
per cases;
suppose
A5: a <> 0;
a * u + (b * v + c * w) = 0.V by A3,RLVECT_1:def 3;
then a * u = - (b * v + c * w) by RLVECT_1:6;
then a" * a * u = a" * (- (b * v + c * w)) by RLVECT_1:def 7;
then 1 * u = a" * (- (b * v + c * w)) by A5,XCMPLX_0:def 7;
then u = a" * (- (b * v + c * w)) by RLVECT_1:def 8
.= a" * ((- 1) * (b * v + c * w)) by RLVECT_1:16
.= a" * (- 1) * (b * v + c * w) by RLVECT_1:def 7
.= a" * (- 1) * (b * v) + a" * (- 1) * (c * w) by RLVECT_1:def 5
.= a" * (- 1) * b * v + a" * (- 1) * (c * w) by RLVECT_1:def 7
.= a" * (- 1) * b * v + a" * (- 1) * c * w by RLVECT_1:def 7;
hence thesis;
end;
suppose
A6: a = 0;
then 0.V = 0.V + b * v + c * w by A3,RLVECT_1:10
.= b * v + c * w by RLVECT_1:4;
hence thesis by A1,A4,A6,RLVECT_3:13;
end;
end;
hence thesis;
end;
theorem
for V be RealLinearSpace, v be VECTOR of V, a be Real
ex l being Linear_Combination of {v} st l.v = a by Lm1;
theorem
for V be RealLinearSpace, v1, v2 be VECTOR of V, a, b be Real st
v1 <> v2
ex l being Linear_Combination of {v1,v2} st l.v1 = a & l.v2 = b by Lm2;
theorem
for V be RealLinearSpace, v1, v2, v3 be VECTOR of V,
a, b, c be Real st
v1 <> v2 & v1 <> v3 & v2 <> v3
ex l being Linear_Combination of {v1,v2,v3} st l.v1 = a & l.v2 = b & l.v3 = c
by Lm3;