:: Linear Combinations in Real Unitary Space
:: by Noboru Endou , Takashi Mitsuishi and Yasunari Shidama
::
:: Received October 9, 2002
:: Copyright (c) 2002-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 BHSP_1, SUBSET_1, RLVECT_3, STRUCT_0, RLSUB_1, CARD_3, RLVECT_2,
TARSKI, RLVECT_1, ARYTM_3, REAL_1, RELAT_1, SUPINF_2, CARD_1, FUNCT_1,
NUMBERS, FUNCT_2, FINSET_1, XBOOLE_0, ZFMISC_1, ORDINAL1, ORDERS_1,
ARYTM_1, FINSEQ_1, VALUED_1, NAT_1, ORDINAL4, CLASSES1, XXREAL_0,
PARTFUN1, FUNCT_7;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, CARD_1, ORDINAL1, NUMBERS,
XCMPLX_0, XREAL_0, REAL_1, FINSEQ_1, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2,
NAT_1, ORDERS_1, DOMAIN_1, STRUCT_0, RLVECT_1, FINSET_1, RLSUB_1,
RLVECT_2, BHSP_1, RLVECT_3, RUSUB_1, RUSUB_2, CLASSES1, XXREAL_0;
constructors PARTFUN1, XXREAL_0, REAL_1, NAT_1, ORDERS_1, REALSET1, RFINSEQ,
RLVECT_2, RLVECT_3, CLASSES1, RUSUB_2, RELSET_1, NUMBERS;
registrations SUBSET_1, ORDINAL1, RELSET_1, FUNCT_2, FINSET_1, NUMBERS,
FINSEQ_1, STRUCT_0, RLVECT_3, BHSP_1, RUSUB_1, CARD_1, RLVECT_2, XREAL_0;
requirements NUMERALS, BOOLE, SUBSET, ARITHM;
definitions XBOOLE_0, RLVECT_2, TARSKI, RLVECT_3, RLSUB_1;
equalities XBOOLE_0, RLVECT_2, RLVECT_1;
expansions XBOOLE_0, TARSKI, RLVECT_3;
theorems FUNCT_1, FUNCT_2, FINSEQ_1, FINSEQ_2, FINSEQ_3, FINSET_1, ORDERS_1,
RLSUB_2, RLVECT_1, RLVECT_2, TARSKI, ZFMISC_1, RELAT_1, ORDINAL1,
XBOOLE_0, XBOOLE_1, RUSUB_1, RUSUB_2, RLVECT_3, ENUMSET1, RLVECT_4,
RFINSEQ, NAT_1, SUBSET_1, XCMPLX_0, XCMPLX_1, CARD_2, STRUCT_0, PARTFUN1,
XREAL_0;
schemes FUNCT_1, FUNCT_2, NAT_1, RLVECT_4, XFAMILY;
begin :: Definition and fundamental properties of linear combination
definition
let V be RealUnitarySpace;
let A be Subset of V;
func Lin(A) -> strict Subspace of V means
:Def1:
the carrier of it = the set of all Sum(l)
where l is Linear_Combination of A;
existence
proof
set A1 = the set of all Sum(l) where l is Linear_Combination of A;
A1 c= the carrier of V
proof
let x be object;
assume x in A1;
then ex l being Linear_Combination of A st x = Sum(l);
hence thesis;
end;
then reconsider A1 as Subset of V;
reconsider l = ZeroLC(V) as Linear_Combination of A by RLVECT_2:22;
A1: A1 is linearly-closed
proof
thus for v,u being VECTOR of V st v in A1 & u in A1 holds v + u in A1
proof
let v,u be VECTOR of V;
assume that
A2: v in A1 and
A3: u in A1;
consider l1 being Linear_Combination of A such that
A4: v = Sum(l1) by A2;
consider l2 being Linear_Combination of A such that
A5: u = Sum(l2) by A3;
reconsider f = l1 + l2 as Linear_Combination of A by RLVECT_2:38;
v + u = Sum(f) by A4,A5,RLVECT_3:1;
hence thesis;
end;
let a be Real;
let v be VECTOR of V;
assume v in A1;
then consider l being Linear_Combination of A such that
A6: v = Sum(l);
reconsider f = a * l as Linear_Combination of A by RLVECT_2:44;
a * v = Sum(f) by A6,RLVECT_3:2;
hence thesis;
end;
Sum(l) = 0.V by RLVECT_2:30;
then 0.V in A1;
hence thesis by A1,RUSUB_1:29;
end;
uniqueness by RUSUB_1:24;
end;
theorem Th1:
for V being RealUnitarySpace, A being Subset of V, x be object holds
x in Lin(A) iff ex l being Linear_Combination of A st x = Sum(l)
proof
let V be RealUnitarySpace;
let A be Subset of V;
let x be object;
thus x in Lin(A) implies ex l being Linear_Combination of A st x = Sum(l)
proof
assume x in Lin(A);
then x in the carrier of Lin(A) by STRUCT_0:def 5;
then x in the set of all Sum(l) where l is Linear_Combination of A
by Def1;
hence thesis;
end;
given k being Linear_Combination of A such that
A1: x = Sum(k);
x in the set of all Sum(l) where l is Linear_Combination of A by A1;
then x in the carrier of Lin(A) by Def1;
hence thesis by STRUCT_0:def 5;
end;
reconsider jj=1, zz=In(0,REAL) as Element of REAL by XREAL_0:def 1;
theorem Th2:
for V being RealUnitarySpace, A being Subset of V, x being set st
x in A holds x in Lin(A)
proof
deffunc F(set) = zz;
let V be RealUnitarySpace;
let A be Subset of V;
let x be set;
assume
A1: x in A;
then reconsider v = x as VECTOR of V;
consider f being Function of the carrier of V, REAL such that
A2: f.v = jj and
A3: 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;
ex T being finite Subset of V st for u being VECTOR of V st not u in T
holds f.u = 0
proof
take T = {v};
let u be VECTOR of V;
assume not u in T;
then u <> v by TARSKI:def 1;
hence thesis by A3;
end;
then reconsider f as Linear_Combination of V by RLVECT_2:def 3;
A4: Carrier(f) c= {v}
proof
let x be object;
assume x in Carrier(f);
then consider u being VECTOR of V such that
A5: x = u and
A6: f.u <> 0;
u = v by A3,A6;
hence thesis by A5,TARSKI:def 1;
end;
then reconsider f as Linear_Combination of {v} by RLVECT_2:def 6;
A7: Sum(f) = 1 * v by A2,RLVECT_2:32
.= v by RLVECT_1:def 8;
{v} c= A by A1,ZFMISC_1:31;
then Carrier(f) c= A by A4;
then reconsider f as Linear_Combination of A by RLVECT_2:def 6;
Sum(f) = v by A7;
hence thesis by Th1;
end;
Lm1: for V being RealUnitarySpace, x being object
holds x in (0).V iff x = 0.V
proof
let V be RealUnitarySpace;
let x be object;
thus x in (0).V implies x = 0.V
proof
assume x in (0).V;
then x in the carrier of (0).V by STRUCT_0:def 5;
then x in {0.V} by RUSUB_1:def 2;
hence thesis by TARSKI:def 1;
end;
thus thesis by RUSUB_1:11;
end;
theorem
for V being RealUnitarySpace holds Lin({}(the carrier of V)) = (0).V
proof
let V be RealUnitarySpace;
set A = Lin({}(the carrier of V));
now
let v be VECTOR of V;
thus v in A implies v in (0).V
proof
assume v in A;
then
A1: v in the carrier of A by STRUCT_0:def 5;
the carrier of A = the set of all
Sum(l0) where l0 is Linear_Combination of {}(the
carrier of V) by Def1;
then
ex l0 being Linear_Combination of {}(the carrier of V) st v = Sum(l0
) by A1;
then v = 0.V by RLVECT_2:31;
hence thesis by Lm1;
end;
assume v in (0).V;
then v = 0.V by Lm1;
hence v in A by RUSUB_1:11;
end;
hence thesis by RUSUB_1:25;
end;
theorem
for V being RealUnitarySpace, A being Subset of V st Lin(A) = (0).V
holds A = {} or A = {0.V}
proof
let V be RealUnitarySpace;
let A be Subset of V;
assume that
A1: Lin(A) = (0).V and
A2: A <> {};
thus A c= {0.V}
proof
let x be object;
assume x in A;
then x in Lin(A) by Th2;
then x = 0.V by A1,Lm1;
hence thesis by TARSKI:def 1;
end;
set y = the Element of A;
let x be object;
assume x in {0.V};
then
A3: x = 0.V by TARSKI:def 1;
y in A & y in Lin(A) by A2,Th2;
hence thesis by A1,A3,Lm1;
end;
theorem Th5:
for V being RealUnitarySpace, W being strict Subspace of V, A
being Subset of V st A = the carrier of W holds Lin(A) = W
proof
let V be RealUnitarySpace;
let W be strict Subspace of V;
let A be Subset of V;
assume
A1: A = the carrier of W;
now
let v be VECTOR of V;
thus v in Lin(A) implies v in W
proof
assume v in Lin(A);
then
A2: ex l being Linear_Combination of A st v = Sum(l) by Th1;
A is linearly-closed by A1,RUSUB_1:28;
then v in the carrier of W by A1,A2,RLVECT_2:29;
hence thesis by STRUCT_0:def 5;
end;
v in W iff v in the carrier of W by STRUCT_0:def 5;
hence v in W implies v in Lin(A) by A1,Th2;
end;
hence thesis by RUSUB_1:25;
end;
theorem
for V being strict RealUnitarySpace,A being Subset of V holds A = the
carrier of V implies Lin(A) = V
proof
let V be strict RealUnitarySpace, A be Subset of V;
assume A = the carrier of V;
then A = the carrier of (Omega).V by RUSUB_1:def 3;
hence Lin(A) = (Omega).V by Th5
.= V by RUSUB_1:def 3;
end;
Lm2: for V being RealUnitarySpace, W1,W2,W3 being Subspace of V st W1 is
Subspace of W3 holds W1 /\ W2 is Subspace of W3
proof
let V be RealUnitarySpace;
let W1,W2,W3 be Subspace of V;
A1: W1 /\ W2 is Subspace of W1 by RUSUB_2:16;
assume W1 is Subspace of W3;
hence thesis by A1,RUSUB_1:21;
end;
Lm3: for V being RealUnitarySpace, W1,W2,W3 being Subspace of V st W1 is
Subspace of W2 & W1 is Subspace of W3 holds W1 is Subspace of W2 /\ W3
proof
let V be RealUnitarySpace;
let W1,W2,W3 be Subspace of V;
assume
A1: W1 is Subspace of W2 & W1 is Subspace of W3;
now
let v be VECTOR of V;
assume v in W1;
then v in W2 & v in W3 by A1,RUSUB_1:1;
hence v in W2 /\ W3 by RUSUB_2:3;
end;
hence thesis by RUSUB_1:23;
end;
Lm4: for V being RealUnitarySpace, W1,W2,W3 being Subspace of V st W1 is
Subspace of W2 holds W1 is Subspace of W2 + W3
proof
let V be RealUnitarySpace;
let W1,W2,W3 be Subspace of V;
A1: W2 is Subspace of W2 + W3 by RUSUB_2:7;
assume W1 is Subspace of W2;
hence thesis by A1,RUSUB_1:21;
end;
Lm5: for V being RealUnitarySpace, W1,W2,W3 being Subspace of V st W1 is
Subspace of W3 & W2 is Subspace of W3 holds W1 + W2 is Subspace of W3
proof
let V be RealUnitarySpace;
let W1,W2,W3 be Subspace of V;
assume
A1: W1 is Subspace of W3 & W2 is Subspace of W3;
now
let v be VECTOR of V;
assume v in W1 + W2;
then consider v1,v2 being VECTOR of V such that
A2: v1 in W1 & v2 in W2 and
A3: v = v1 + v2 by RUSUB_2:1;
v1 in W3 & v2 in W3 by A1,A2,RUSUB_1:1;
hence v in W3 by A3,RUSUB_1:14;
end;
hence thesis by RUSUB_1:23;
end;
theorem Th7:
for V being RealUnitarySpace, A,B being Subset of V st A c= B
holds Lin(A) is Subspace of Lin(B)
proof
let V be RealUnitarySpace;
let A,B be Subset of V;
assume
A1: A c= B;
now
let v be VECTOR of V;
assume v in Lin(A);
then consider l being Linear_Combination of A such that
A2: v = Sum(l) by Th1;
reconsider l as Linear_Combination of B by A1,RLVECT_2:21;
Sum(l) = v by A2;
hence v in Lin(B) by Th1;
end;
hence thesis by RUSUB_1:23;
end;
theorem
for V being strict RealUnitarySpace, A,B being Subset of V st Lin(A) =
V & A c= B holds Lin(B) = V
proof
let V be strict RealUnitarySpace, A,B be Subset of V;
assume Lin(A) = V & A c= B;
then V is Subspace of Lin(B) by Th7;
hence thesis by RUSUB_1:20;
end;
theorem
for V being RealUnitarySpace, A,B being Subset of V holds Lin(A \/ B)
= Lin(A) + Lin(B)
proof
let V be RealUnitarySpace;
let A,B be Subset of V;
now
deffunc G(object) = 0;
let v be VECTOR of V;
assume v in Lin(A \/ B);
then consider l being Linear_Combination of A \/ B such that
A1: v = Sum(l) by Th1;
deffunc F(object) = l.$1;
set D = Carrier(l) \ A;
set C = Carrier(l) /\ A;
defpred C[object] means $1 in C;
defpred D[object] means $1 in D;
now
let x be set;
assume x in the carrier of V;
then reconsider v = x as VECTOR of V;
for f being Function of the carrier of V, REAL holds f.v in REAL;
hence x in C implies l.x in REAL;
assume not x in C;
thus 0 in REAL by XREAL_0:def 1;
end;
then
A2: for x being object st x in the carrier of V holds (C[x] implies F(x) in
REAL) & (not C[x] implies G(x) in REAL);
consider f being Function of the carrier of V, REAL such that
A3: for x being object st x in the carrier of V holds (C[x] implies f.x
= F(x)) & (not C[x] implies f.x = G(x)) from FUNCT_2:sch 5(A2);
reconsider C as finite Subset of V;
reconsider f as Element of Funcs(the carrier of V, REAL) by FUNCT_2:8;
for u being VECTOR of V st not u in C holds f.u = 0 by A3;
then reconsider f as Linear_Combination of V by RLVECT_2:def 3;
A4: Carrier(f) c= C
proof
let x be object;
assume x in Carrier(f);
then
A5: ex u being VECTOR of V st x = u & f.u <> 0;
assume not x in C;
hence thesis by A3,A5;
end;
C c= A by XBOOLE_1:17;
then Carrier(f) c= A by A4;
then reconsider f as Linear_Combination of A by RLVECT_2:def 6;
now
let x be set;
assume x in the carrier of V;
then reconsider v = x as VECTOR of V;
for g being Function of the carrier of V, REAL holds g.v in REAL;
hence x in D implies l.x in REAL;
assume not x in D;
thus 0 in REAL by XREAL_0:def 1;
end;
then
A6: for x being object st x in the carrier of V holds (D[x] implies F(x) in
REAL) & (not D[x] implies G(x) in REAL);
consider g being Function of the carrier of V, REAL such that
A7: for x being object st x in the carrier of V holds (D[x] implies g.x
= F(x)) & (not D[x] implies g.x = G(x)) from FUNCT_2:sch 5(A6);
reconsider D as finite Subset of V;
reconsider g as Element of Funcs(the carrier of V, REAL) by FUNCT_2:8;
for u being VECTOR of V holds not u in D implies g.u = 0 by A7;
then reconsider g as Linear_Combination of V by RLVECT_2:def 3;
A8: D c= B
proof
let x be object;
assume x in D;
then
A9: x in Carrier(l) & not x in A by XBOOLE_0:def 5;
Carrier(l) c= A \/ B by RLVECT_2:def 6;
hence thesis by A9,XBOOLE_0:def 3;
end;
Carrier(g) c= D
proof
let x be object;
assume x in Carrier(g);
then
A10: ex u being VECTOR of V st x = u & g.u <> 0;
assume not x in D;
hence thesis by A7,A10;
end;
then Carrier(g) c= B by A8;
then reconsider g as Linear_Combination of B by RLVECT_2:def 6;
l = f + g
proof
let v be VECTOR of V;
now
per cases;
suppose
A11: v in C;
A12: now
assume v in D;
then not v in A by XBOOLE_0:def 5;
hence contradiction by A11,XBOOLE_0:def 4;
end;
thus (f + g).v = f.v + g.v by RLVECT_2:def 10
.= l.v + g.v by A3,A11
.= l.v + 0 by A7,A12
.= l.v;
end;
suppose
A13: not v in C;
now
per cases;
suppose
A14: v in Carrier(l);
A15: now
assume not v in D;
then not v in Carrier(l) or v in A by XBOOLE_0:def 5;
hence contradiction by A13,A14,XBOOLE_0:def 4;
end;
thus (f + g). v = f.v + g.v by RLVECT_2:def 10
.= 0 + g.v by A3,A13
.= l.v by A7,A15;
end;
suppose
A16: not v in Carrier(l);
then
A17: not v in D by XBOOLE_0:def 5;
A18: not v in C by A16,XBOOLE_0:def 4;
thus (f + g).v = f.v + g.v by RLVECT_2:def 10
.= 0 + g.v by A3,A18
.= 0 + 0 by A7,A17
.= l.v by A16;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
then
A19: v = Sum(f) + Sum(g) by A1,RLVECT_3:1;
Sum(f) in Lin(A) & Sum(g) in Lin(B) by Th1;
hence v in Lin(A) + Lin(B) by A19,RUSUB_2:1;
end;
then
A20: Lin(A \/ B) is Subspace of Lin(A) + Lin(B) by RUSUB_1:23;
Lin(A) is Subspace of Lin(A \/ B) & Lin(B) is Subspace of Lin(A \/ B) by Th7,
XBOOLE_1:7;
then Lin(A) + Lin(B) is Subspace of Lin(A \/ B) by Lm5;
hence thesis by A20,RUSUB_1:20;
end;
theorem
for V being RealUnitarySpace, A,B being Subset of V holds Lin(A /\ B)
is Subspace of Lin(A) /\ Lin(B)
proof
let V be RealUnitarySpace;
let A,B be Subset of V;
Lin(A /\ B) is Subspace of Lin(A) & Lin(A /\ B) is Subspace of Lin(B) by Th7,
XBOOLE_1:17;
hence thesis by Lm3;
end;
theorem Th11:
for V being RealUnitarySpace, A being Subset of V st A is
linearly-independent holds ex B being Subset of V st A c= B & B is
linearly-independent & Lin(B) = the UNITSTR of V
proof
let V be RealUnitarySpace;
let A be Subset of V;
defpred P[set] means (ex B being Subset of V st B = $1 & A c= B & B is
linearly-independent);
consider Q being set such that
A1: for Z being set holds Z in Q iff Z in bool(the carrier of V) & P[Z]
from XFAMILY:sch 1;
A2: now
let Z be set;
assume that
A3: Z <> {} and
A4: Z c= Q and
A5: Z is c=-linear;
set x = the Element of Z;
x in Q by A3,A4;
then
A6: ex B being Subset of V st B = x & A c= B & B is linearly-independent by A1;
set W = union Z;
W c= the carrier of V
proof
let x be object;
assume x in W;
then consider X being set such that
A7: x in X and
A8: X in Z by TARSKI:def 4;
X in bool(the carrier of V) by A1,A4,A8;
hence thesis by A7;
end;
then reconsider W as Subset of V;
A9: W is linearly-independent
proof
deffunc F(object) = {C where C is Subset of V: $1 in C & C in Z};
let l be Linear_Combination of W;
assume that
A10: Sum(l) = 0.V and
A11: Carrier(l) <> {};
consider f being Function such that
A12: dom f = Carrier(l) and
A13: for x being object st x in Carrier(l) holds f.x = F(x) from
FUNCT_1:sch 3;
reconsider M = rng f as non empty set by A11,A12,RELAT_1:42;
set F = the Choice_Function of M;
set S = rng F;
A14: now
assume {} in M;
then consider x being object such that
A15: x in dom f and
A16: f.x = {} by FUNCT_1:def 3;
Carrier(l) c= W by RLVECT_2:def 6;
then consider X being set such that
A17: x in X and
A18: X in Z by A12,A15,TARSKI:def 4;
reconsider X as Subset of V by A1,A4,A18;
X in {C where C is Subset of V: x in C & C in Z} by A17,A18;
hence contradiction by A12,A13,A15,A16;
end;
then
A19: dom F = M by RLVECT_3:28;
then dom F is finite by A12,FINSET_1:8;
then
A20: S is finite by FINSET_1:8;
A21: now
let X be set;
assume X in S;
then consider x being object such that
A22: x in dom F and
A23: F.x = X by FUNCT_1:def 3;
consider y being object such that
A24: y in dom f & f.y = x by A19,A22,FUNCT_1:def 3;
A25: x = {C where C is Subset of V: y in C & C in Z} by A12,A13,A24;
reconsider x as set by TARSKI:1;
X in x by A14,A19,A22,A23,ORDERS_1:89;
then ex C being Subset of V st C = X & y in C & C in Z by A25;
hence X in Z;
end;
A26: now
let X,Y be set;
assume X in S & Y in S;
then X in Z & Y in Z by A21;
then X,Y are_c=-comparable by A5,ORDINAL1:def 8;
hence X c= Y or Y c= X;
end;
S <> {} by A19,RELAT_1:42;
then union S in S by A26,A20,CARD_2:62;
then union S in Z by A21;
then consider B being Subset of V such that
A27: B = union S and
A c= B and
A28: B is linearly-independent by A1,A4;
Carrier(l) c= union S
proof
let x be object;
set X = f.x;
assume
A29: x in Carrier(l);
then
A30: f.x = {C where C is Subset of V: x in C & C in Z} by A13;
A31: f.x in M by A12,A29,FUNCT_1:def 3;
then F.X in X by A14,ORDERS_1:89;
then
A32: ex C being Subset of V st F.X = C & x in C & C in Z by A30;
F.X in S by A19,A31,FUNCT_1:def 3;
hence thesis by A32,TARSKI:def 4;
end;
then l is Linear_Combination of B by A27,RLVECT_2:def 6;
hence thesis by A10,A11,A28;
end;
x c= W by A3,ZFMISC_1:74;
then A c= W by A6;
hence union Z in Q by A1,A9;
end;
A33: (Omega).V = the UNITSTR of V by RUSUB_1:def 3;
assume A is linearly-independent;
then Q <> {} by A1;
then consider X being set such that
A34: X in Q and
A35: for Z being set st Z in Q & Z <> X holds not X c= Z by A2,ORDERS_1:67;
consider B being Subset of V such that
A36: B = X and
A37: A c= B and
A38: B is linearly-independent by A1,A34;
take B;
thus A c= B & B is linearly-independent by A37,A38;
assume Lin(B) <> the UNITSTR of V;
then consider v being VECTOR of V such that
A39: not(v in Lin(B) iff v in the UNITSTR of V) by A33,RUSUB_1:25;
A40: B \/ {v} is linearly-independent
proof
let l be Linear_Combination of B \/ {v};
assume
A41: Sum(l) = 0.V;
now
per cases;
suppose
v in Carrier(l);
then
A42: - l.v <> 0 by RLVECT_2:19;
deffunc G(set) = zz;
deffunc F(VECTOR of V) = l.$1;
consider f being Function of the carrier of V, REAL such that
A43: f.v = In(0,REAL) and
A44: 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 Carrier(l) \ {v};
then not u in Carrier(l) or u in {v} by XBOOLE_0:def 5;
then l.u = 0 & u <> v or u = v by TARSKI:def 1;
hence f.u = 0 by A43,A44;
end;
then reconsider f as Linear_Combination of V by RLVECT_2:def 3;
Carrier(f) c= B
proof
let x be object;
A45: Carrier(l) c= B \/ {v} by RLVECT_2:def 6;
assume x in Carrier(f);
then consider u being VECTOR of V such that
A46: u = x and
A47: f.u <> 0;
f.u = l.u by A43,A44,A47;
then u in Carrier(l) by A47;
then u in B or u in {v} by A45,XBOOLE_0:def 3;
hence thesis by A43,A46,A47,TARSKI:def 1;
end;
then reconsider f as Linear_Combination of B by RLVECT_2:def 6;
consider g being Function of the carrier of V, REAL such that
A48: g.v = - l.v and
A49: for u being VECTOR of V st u <> v holds g.u = G(u) from
FUNCT_2:sch 6;
reconsider g 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 g.u = 0 by A49;
end;
then reconsider g as Linear_Combination of V by RLVECT_2:def 3;
Carrier(g) c= {v}
proof
let x be object;
assume x in Carrier(g);
then ex u being VECTOR of V st x = u & g.u <> 0;
then x = v by A49;
hence thesis by TARSKI:def 1;
end;
then reconsider g as Linear_Combination of {v} by RLVECT_2:def 6;
A50: Sum(g) = (- l.v) * v by A48,RLVECT_2:32;
f - g = l
proof
let u be VECTOR of V;
now
per cases;
suppose
A51: v = u;
thus (f - g).u = f.u - g.u by RLVECT_2:54
.= l.u by A43,A48,A51;
end;
suppose
A52: v <> u;
thus (f - g).u = f.u - g.u by RLVECT_2:54
.= l.u - g.u by A44,A52
.= l.u - 0 by A49,A52
.= l.u;
end;
end;
hence thesis;
end;
then 0.V = Sum(f) - Sum(g) by A41,RLVECT_3:4;
then Sum(f) = 0.V + Sum(g) by RLSUB_2:61
.= (- l.v) * v by A50,RLVECT_1:4;
then
A53: (- l.v) * v in Lin(B) by Th1;
(- l.v)" * ((- l.v) * v) = (- l.v)" * (- l.v) * v by RLVECT_1:def 7
.= 1 * v by A42,XCMPLX_0:def 7
.= v by RLVECT_1:def 8;
hence thesis by A39,A53,RLVECT_1:1,RUSUB_1:15;
end;
suppose
A54: not v in Carrier(l);
Carrier(l) c= B
proof
let x be object;
assume
A55: x in Carrier(l);
Carrier(l) c= B \/ {v} by RLVECT_2:def 6;
then x in B or x in {v} by A55,XBOOLE_0:def 3;
hence thesis by A54,A55,TARSKI:def 1;
end;
then l is Linear_Combination of B by RLVECT_2:def 6;
hence thesis by A38,A41;
end;
end;
hence thesis;
end;
v in {v} by TARSKI:def 1;
then
A56: v in B \/ {v} by XBOOLE_0:def 3;
A57: not v in B by A39,Th2,RLVECT_1:1;
B c= B \/ {v} by XBOOLE_1:7;
then A c= B \/ {v} by A37;
then B \/ {v} in Q by A1,A40;
hence contradiction by A35,A36,A56,A57,XBOOLE_1:7;
end;
theorem Th12:
for V being RealUnitarySpace, A being Subset of V st Lin(A) = V
holds ex B being Subset of V st B c= A & B is linearly-independent & Lin(B) = V
proof
let V be RealUnitarySpace;
let A be Subset of V;
assume
A1: Lin(A) = V;
defpred P[set] means (ex B being Subset of V st B = $1 & B c= A & B is
linearly-independent);
consider Q being set such that
A2: for Z being set holds Z in Q iff Z in bool(the carrier of V) & P[Z]
from XFAMILY:sch 1;
A3: now
let Z be set;
assume that
Z <> {} and
A4: Z c= Q and
A5: Z is c=-linear;
set W = union Z;
W c= the carrier of V
proof
let x be object;
assume x in W;
then consider X being set such that
A6: x in X and
A7: X in Z by TARSKI:def 4;
X in bool(the carrier of V) by A2,A4,A7;
hence thesis by A6;
end;
then reconsider W as Subset of V;
A8: W is linearly-independent
proof
deffunc F(object) = {C where C is Subset of V: $1 in C & C in Z};
let l be Linear_Combination of W;
assume that
A9: Sum(l) = 0.V and
A10: Carrier(l) <> {};
consider f being Function such that
A11: dom f = Carrier(l) and
A12: for x being object st x in Carrier(l) holds f.x = F(x) from
FUNCT_1:sch 3;
reconsider M = rng f as non empty set by A10,A11,RELAT_1:42;
set F = the Choice_Function of M;
set S = rng F;
A13: now
assume {} in M;
then consider x being object such that
A14: x in dom f and
A15: f.x = {} by FUNCT_1:def 3;
Carrier(l) c= W by RLVECT_2:def 6;
then consider X being set such that
A16: x in X and
A17: X in Z by A11,A14,TARSKI:def 4;
reconsider X as Subset of V by A2,A4,A17;
X in {C where C is Subset of V : x in C & C in Z} by A16,A17;
hence contradiction by A11,A12,A14,A15;
end;
then
A18: dom F = M by RLVECT_3:28;
then dom F is finite by A11,FINSET_1:8;
then
A19: S is finite by FINSET_1:8;
A20: now
let X be set;
assume X in S;
then consider x be object such that
A21: x in dom F and
A22: F.x = X by FUNCT_1:def 3;
consider y be object such that
A23: y in dom f & f.y = x by A18,A21,FUNCT_1:def 3;
A24: x = {C where C is Subset of V : y in C & C in Z} by A11,A12,A23;
reconsider x as set by TARSKI:1;
X in x by A13,A18,A21,A22,ORDERS_1:89;
then ex C being Subset of V st C = X & y in C & C in Z by A24;
hence X in Z;
end;
A25: now
let X,Y be set;
assume X in S & Y in S;
then X in Z & Y in Z by A20;
then X,Y are_c=-comparable by A5,ORDINAL1:def 8;
hence X c= Y or Y c= X;
end;
S <> {} by A18,RELAT_1:42;
then union S in S by A25,A19,CARD_2:62;
then union S in Z by A20;
then consider B being Subset of V such that
A26: B = union S and
B c= A and
A27: B is linearly-independent by A2,A4;
Carrier(l) c= union S
proof
let x be object;
set X = f.x;
assume
A28: x in Carrier(l);
then
A29: f.x = {C where C is Subset of V : x in C & C in Z} by A12;
A30: f.x in M by A11,A28,FUNCT_1:def 3;
then F.X in X by A13,ORDERS_1:89;
then
A31: ex C being Subset of V st F.X = C & x in C & C in Z by A29;
F.X in S by A18,A30,FUNCT_1:def 3;
hence thesis by A31,TARSKI:def 4;
end;
then l is Linear_Combination of B by A26,RLVECT_2:def 6;
hence thesis by A9,A10,A27;
end;
W c= A
proof
let x be object;
assume x in W;
then consider X being set such that
A32: x in X and
A33: X in Z by TARSKI:def 4;
ex B being Subset of V st B = X & B c= A & B is
linearly-independent by A2,A4,A33;
hence thesis by A32;
end;
hence union Z in Q by A2,A8;
end;
{}(the carrier of V) c= A & {}(the carrier of V) is linearly-independent
by RLVECT_3:7;
then Q <> {} by A2;
then consider X being set such that
A34: X in Q and
A35: for Z being set st Z in Q & Z <> X holds not X c= Z by A3,ORDERS_1:67;
consider B being Subset of V such that
A36: B = X and
A37: B c= A and
A38: B is linearly-independent by A2,A34;
take B;
thus B c= A & B is linearly-independent by A37,A38;
assume
A39: Lin(B) <> V;
now
assume
A40: for v being VECTOR of V st v in A holds v in Lin(B);
now
reconsider F = the carrier of Lin(B) as Subset of V by RUSUB_1:def 1;
let v be VECTOR of V;
assume v in Lin(A);
then consider l being Linear_Combination of A such that
A41: v = Sum(l) by Th1;
Carrier(l) c= the carrier of Lin(B)
proof
let x be object;
assume
A42: x in Carrier(l);
then reconsider a = x as VECTOR of V;
Carrier(l) c= A by RLVECT_2:def 6;
then a in Lin(B) by A40,A42;
hence thesis by STRUCT_0:def 5;
end;
then reconsider l as Linear_Combination of F by RLVECT_2:def 6;
Sum(l) = v by A41;
then v in Lin(F) by Th1;
hence v in Lin(B) by Th5;
end;
then Lin(A) is Subspace of Lin(B) by RUSUB_1:23;
hence contradiction by A1,A39,RUSUB_1:20;
end;
then consider v being VECTOR of V such that
A43: v in A and
A44: not v in Lin(B);
A45: B \/ {v} is linearly-independent
proof
let l be Linear_Combination of B \/ {v};
assume
A46: Sum(l) = 0.V;
now
per cases;
suppose
v in Carrier(l);
then
A47: - l.v <> 0 by RLVECT_2:19;
deffunc G(set) = In(0,REAL);
deffunc F(VECTOR of V) = l.$1;
consider f being Function of the carrier of V, REAL such that
A48: f.v = In(0,REAL) and
A49: 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 Carrier(l) \ {v};
then not u in Carrier(l) or u in {v} by XBOOLE_0:def 5;
then l.u = 0 & u <> v or u = v by TARSKI:def 1;
hence f.u = 0 by A48,A49;
end;
then reconsider f as Linear_Combination of V by RLVECT_2:def 3;
Carrier(f) c= B
proof
let x be object;
A50: Carrier(l) c= B \/ {v} by RLVECT_2:def 6;
assume x in Carrier(f);
then consider u being VECTOR of V such that
A51: u = x and
A52: f.u <> 0;
f.u = l.u by A48,A49,A52;
then u in Carrier(l) by A52;
then u in B or u in {v} by A50,XBOOLE_0:def 3;
hence thesis by A48,A51,A52,TARSKI:def 1;
end;
then reconsider f as Linear_Combination of B by RLVECT_2:def 6;
consider g being Function of the carrier of V, REAL such that
A53: g.v = - l.v and
A54: for u being VECTOR of V st u <> v holds g.u = G(u) from
FUNCT_2:sch 6;
reconsider g 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 g.u = 0 by A54;
end;
then reconsider g as Linear_Combination of V by RLVECT_2:def 3;
Carrier(g) c= {v}
proof
let x be object;
assume x in Carrier(g);
then ex u being VECTOR of V st x = u & g.u <> 0;
then x = v by A54;
hence thesis by TARSKI:def 1;
end;
then reconsider g as Linear_Combination of {v} by RLVECT_2:def 6;
A55: Sum(g) = (- l.v) * v by A53,RLVECT_2:32;
f - g = l
proof
let u be VECTOR of V;
now
per cases;
suppose
A56: v = u;
thus (f - g).u = f.u - g.u by RLVECT_2:54
.= l.u by A48,A53,A56;
end;
suppose
A57: v <> u;
thus (f - g).u = f.u - g.u by RLVECT_2:54
.= l.u - g.u by A49,A57
.= l.u - 0 by A54,A57
.= l.u;
end;
end;
hence thesis;
end;
then 0.V = Sum(f) - Sum(g) by A46,RLVECT_3:4;
then Sum(f) = 0.V + Sum(g) by RLSUB_2:61
.= (- l.v) * v by A55,RLVECT_1:4;
then
A58: (- l.v) * v in Lin(B) by Th1;
(- l.v)" * ((- l.v) * v) = (- l.v)" * (- l.v) * v by RLVECT_1:def 7
.= 1 * v by A47,XCMPLX_0:def 7
.= v by RLVECT_1:def 8;
hence thesis by A44,A58,RUSUB_1:15;
end;
suppose
A59: not v in Carrier(l);
Carrier(l) c= B
proof
let x be object;
assume
A60: x in Carrier(l);
Carrier(l) c= B \/ {v} by RLVECT_2:def 6;
then x in B or x in {v} by A60,XBOOLE_0:def 3;
hence thesis by A59,A60,TARSKI:def 1;
end;
then l is Linear_Combination of B by RLVECT_2:def 6;
hence thesis by A38,A46;
end;
end;
hence thesis;
end;
{v} c= A by A43,ZFMISC_1:31;
then B \/ {v} c= A by A37,XBOOLE_1:8;
then
A61: B \/ {v} in Q by A2,A45;
v in {v} by TARSKI:def 1;
then
A62: v in B \/ {v} by XBOOLE_0:def 3;
not v in B by A44,Th2;
hence contradiction by A35,A36,A62,A61,XBOOLE_1:7;
end;
begin :: Definition of the basis of real unitay space
definition
let V be RealUnitarySpace;
mode Basis of V -> Subset of V means
:Def2:
it is linearly-independent & Lin (it) = the UNITSTR of V;
existence
proof
{}(the carrier of V) is linearly-independent by RLVECT_3:7;
then ex B being Subset of V st {}(the carrier of V) c= B & B is
linearly-independent & Lin(B) = the UNITSTR of V by Th11;
hence thesis;
end;
end;
theorem
for V being strict RealUnitarySpace, A being Subset of V st A is
linearly-independent holds ex I being Basis of V st A c= I
proof
let V be strict RealUnitarySpace, A be Subset of V;
assume A is linearly-independent;
then consider B being Subset of V such that
A1: A c= B and
A2: B is linearly-independent & Lin(B) = V by Th11;
reconsider B as Basis of V by A2,Def2;
take B;
thus thesis by A1;
end;
theorem
for V being RealUnitarySpace, A being Subset of V st Lin(A) = V holds
ex I being Basis of V st I c= A
proof
let V be RealUnitarySpace;
let A be Subset of V;
assume Lin(A) = V;
then consider B being Subset of V such that
A1: B c= A and
A2: B is linearly-independent & Lin(B) = V by Th12;
reconsider B as Basis of V by A2,Def2;
take B;
thus thesis by A1;
end;
theorem Th15:
for V being RealUnitarySpace, A being Subset of V st A is
linearly-independent holds ex I being Basis of V st A c= I
proof
let V be RealUnitarySpace, A be Subset of V;
assume A is linearly-independent;
then consider B being Subset of V such that
A1: A c= B and
A2: B is linearly-independent & Lin(B) = the UNITSTR of V by Th11;
reconsider B as Basis of V by A2,Def2;
take B;
thus thesis by A1;
end;
begin :: Some theorems of Lin, Sum, Carrier
theorem Th16:
for V being RealUnitarySpace, L being Linear_Combination of V, A
being Subset of V, F being FinSequence of V st rng F c= the carrier of Lin(A)
holds ex K being Linear_Combination of A st Sum(L (#) F) = Sum(K)
proof
let V be RealUnitarySpace;
let L be Linear_Combination of V;
let A be Subset of V;
defpred P[Nat] means
for F being FinSequence of V st rng F c= the
carrier of Lin(A) & len F = $1 holds ex K being Linear_Combination of A st Sum(
L (#) F) = Sum(K);
let F be FinSequence of V;
assume
A1: rng F c= the carrier of Lin(A);
A2: len F is Nat;
A3: for n being Nat st P[n] holds P[n + 1]
proof
let n be Nat;
assume
A4: P[n];
let F be FinSequence of V such that
A5: rng F c= the carrier of Lin(A) and
A6: len F = n + 1;
consider G being FinSequence, x being object such that
A7: F = G^<*x*> by A6,FINSEQ_2:18;
reconsider G, x9= <*x*> as FinSequence of V by A7,FINSEQ_1:36;
A8: rng(G^<*x*>) = rng G \/ rng <*x*> by FINSEQ_1:31
.= rng G \/ {x} by FINSEQ_1:38;
then
A9: rng G c= rng F by A7,XBOOLE_1:7;
{x} c= rng F by A7,A8,XBOOLE_1:7;
then {x} c= the carrier of Lin(A) by A5;
then x in {x} implies x in the carrier of Lin(A);
then
A10: x in Lin(A) by STRUCT_0:def 5,TARSKI:def 1;
then
A11: x in V by RUSUB_1:2;
consider LA1 being Linear_Combination of A such that
A12: x = Sum(LA1) by A10,Th1;
reconsider x as VECTOR of V by A11,STRUCT_0:def 5;
len(G^<*x*>) = len G + len <*x*> by FINSEQ_1:22
.= len G + 1 by FINSEQ_1:39;
then consider LA2 being Linear_Combination of A such that
A13: Sum(L (#) G) = Sum(LA2) by A4,A5,A6,A7,A9,XBOOLE_1:1;
L.x * LA1 is Linear_Combination of A by RLVECT_2:44;
then
A14: LA2 + L.x * LA1 is Linear_Combination of A by RLVECT_2:38;
Sum(L (#) F) = Sum((L (#) G) ^ (L (#) x9)) by A7,RLVECT_3:34
.= Sum(LA2) + Sum(L (#) x9) by A13,RLVECT_1:41
.= Sum(LA2) + Sum(<*L.x * x*>) by RLVECT_2:26
.= Sum(LA2) + L.x * Sum(LA1) by A12,RLVECT_1:44
.= Sum(LA2) + Sum(L.x * LA1) by RLVECT_3:2
.= Sum(LA2 + L.x * LA1) by RLVECT_3:1;
hence thesis by A14;
end;
A15: P[0]
proof
let F be FinSequence of V;
assume that
rng F c= the carrier of Lin(A) and
A16: len F = 0;
F = <*>(the carrier of V) by A16;
then L (#) F = <*>(the carrier of V) by RLVECT_2:25;
then
A17: Sum(L (#) F) = 0.V by RLVECT_1:43
.= Sum(ZeroLC(V)) by RLVECT_2:30;
ZeroLC(V) is Linear_Combination of A by RLVECT_2:22;
hence thesis by A17;
end;
for n being Nat holds P[n] from NAT_1:sch 2(A15, A3);
hence thesis by A1,A2;
end;
theorem
for V being RealUnitarySpace, L being Linear_Combination of V, A being
Subset of V st Carrier(L) c= the carrier of Lin(A) holds ex K being
Linear_Combination of A st Sum(L) = Sum(K)
proof
let V be RealUnitarySpace;
let L be Linear_Combination of V, A be Subset of V;
consider F being FinSequence of V such that
F is one-to-one and
A1: rng F = Carrier(L) and
A2: Sum(L) = Sum(L (#) F) by RLVECT_2:def 8;
assume Carrier(L) c= the carrier of Lin(A);
then consider K being Linear_Combination of A such that
A3: Sum(L (#) F) = Sum(K) by A1,Th16;
take K;
thus thesis by A2,A3;
end;
theorem Th18:
for V being RealUnitarySpace, W being Subspace of V, L being
Linear_Combination of V st Carrier(L) c= the carrier of W for K being
Linear_Combination of W st K = L|the carrier of W holds Carrier(L) = Carrier(K)
& Sum(L) = Sum(K)
proof
let V be RealUnitarySpace;
let W be Subspace of V;
let L be Linear_Combination of V such that
A1: Carrier(L) c= the carrier of W;
let K be Linear_Combination of W such that
A2: K = L|the carrier of W;
A3: dom K = the carrier of W by FUNCT_2:def 1;
now
let x be object;
assume x in Carrier(K);
then consider w being VECTOR of W such that
A4: x = w and
A5: K.w <> 0;
A6: w is VECTOR of V by RUSUB_1:3;
L.w <> 0 by A2,A3,A5,FUNCT_1:47;
hence x in Carrier(L) by A4,A6;
end;
then
A7: Carrier(K) c= Carrier(L);
consider G being FinSequence of W such that
A8: G is one-to-one & rng G = Carrier(K) and
A9: Sum(K) = Sum(K (#) G) by RLVECT_2:def 8;
consider F being FinSequence of V such that
A10: F is one-to-one and
A11: rng F = Carrier(L) and
A12: Sum(L) = Sum(L (#) F) by RLVECT_2:def 8;
now
let x be object;
assume
A13: x in Carrier(L);
then consider v being VECTOR of V such that
A14: x = v and
A15: L.v <> 0;
K.v <> 0 by A1,A2,A3,A13,A14,A15,FUNCT_1:47;
hence x in Carrier(K) by A1,A13,A14;
end;
then
A16: Carrier(L) c= Carrier(K);
then
A17: Carrier(K) = Carrier(L) by A7;
then F,G are_fiberwise_equipotent by A10,A11,A8,RFINSEQ:26;
then consider P being Permutation of dom G such that
A18: F = G*P by RFINSEQ:4;
len(K (#) G) = len G by RLVECT_2:def 7;
then
A19: dom(K (#) G) = dom G by FINSEQ_3:29;
then reconsider q = (K (#) G)*P as FinSequence of W by FINSEQ_2:47;
A20: len q = len (K (#) G) by A19,FINSEQ_2:44;
then len q = len G by RLVECT_2:def 7;
then
A21: dom q = dom G by FINSEQ_3:29;
set p = L (#) F;
A22: the carrier of W c= the carrier of V by RUSUB_1:def 1;
rng q c= the carrier of W by FINSEQ_1:def 4;
then rng q c= the carrier of V by A22;
then reconsider q9= q as FinSequence of V by FINSEQ_1:def 4;
consider f being sequence of the carrier of W such that
A23: Sum(q) = f.(len q) and
A24: f.0 = 0.W and
A25: for i being Nat, w being VECTOR of W st i < len q & w =
q.(i + 1) holds f.(i + 1) = f.i + w by RLVECT_1:def 12;
dom f = NAT & rng f c= the carrier of W by FUNCT_2:def 1,RELAT_1:def 19;
then reconsider f9= f as sequence of the carrier of V by A22,FUNCT_2:2
,XBOOLE_1:1;
A26: for i being Nat, v being VECTOR of V st i < len q9 & v = q9.
(i + 1) holds f9.(i + 1) = f9.i + v
proof
let i be Nat, v be VECTOR of V;
assume that
A27: i < len q9 and
A28: v = q9.(i + 1);
1 <= i + 1 & i + 1 <= len q by A27,NAT_1:11,13;
then i + 1 in dom q by FINSEQ_3:25;
then reconsider v9= v as VECTOR of W by A28,FINSEQ_2:11;
f.(i + 1) = f.i + v9 by A25,A27,A28;
hence thesis by RUSUB_1:6;
end;
A29: len G = len F by A18,FINSEQ_2:44;
then
A30: dom G = dom F by FINSEQ_3:29;
len G = len (L (#) F) by A29,RLVECT_2:def 7;
then
A31: dom p = dom G by FINSEQ_3:29;
A32: dom q = dom(K (#) G) by A20,FINSEQ_3:29;
now
let i be Nat;
set v = F/.i;
set j = P.i;
assume
A33: i in dom p;
then
A34: F/.i = F.i by A31,A30,PARTFUN1:def 6;
then v in rng F by A31,A30,A33,FUNCT_1:def 3;
then reconsider w = v as VECTOR of W by A17,A11;
dom P = dom G & rng P = dom G by FUNCT_2:52,def 3;
then
A35: j in dom G by A31,A33,FUNCT_1:def 3;
then j in Seg card G by FINSEQ_1:def 3;
then reconsider j as Element of NAT;
A36: G/.j = G.(P.i) by A35,PARTFUN1:def 6
.= v by A18,A31,A30,A33,A34,FUNCT_1:12;
q.i = (K (#) G).j by A31,A21,A33,FUNCT_1:12
.= K.w * w by A32,A21,A35,A36,RLVECT_2:def 7
.= L.v * w by A2,A3,FUNCT_1:47
.= L.v * v by RUSUB_1:7;
hence p.i = q.i by A33,RLVECT_2:def 7;
end;
then
A37: L (#) F = (K (#) G)*P by A31,A21,FINSEQ_1:13;
len G = len (K (#) G) by RLVECT_2:def 7;
then dom G = dom (K (#) G) by FINSEQ_3:29;
then reconsider P as Permutation of dom (K (#) G);
q = (K (#) G)*P;
then
A38: Sum(K (#) G) = Sum(q) by RLVECT_2:7;
A39: f9.len q9 is Element of V;
f9.0 = 0.V by A24,RUSUB_1:4;
hence thesis by A7,A16,A12,A9,A37,A38,A23,A26,A39,RLVECT_1:def 12;
end;
theorem Th19:
for V being RealUnitarySpace, W being Subspace of V, K being
Linear_Combination of W holds ex L being Linear_Combination of V st Carrier(K)
= Carrier(L) & Sum(K) = Sum(L)
proof
let V be RealUnitarySpace;
let W be Subspace of V;
let K be Linear_Combination of W;
defpred P[object, object] means
($1 in W & $2 = K.$1) or (not $1 in W & $2 = 0);
reconsider K9= K as Function of the carrier of W, REAL;
A1: the carrier of W c= the carrier of V by RUSUB_1:def 1;
then reconsider C = Carrier(K) as finite Subset of V by XBOOLE_1:1;
A2: for x being object st x in the carrier of V
ex y being object st y in REAL & P[x, y]
proof
let x be object;
assume x in the carrier of V;
then reconsider x as VECTOR of V;
per cases;
suppose
A3: x in W;
then reconsider x as VECTOR of W by STRUCT_0:def 5;
P[x, K.x] by A3;
hence thesis;
end;
suppose
A4: not x in W;
0 in REAL by XREAL_0:def 1;
hence thesis by A4;
end;
end;
ex L being Function of the carrier of V, REAL st
for x being object st x in
the carrier of V holds P[x, L.x] from FUNCT_2:sch 1(A2);
then consider L being Function of the carrier of V, REAL such that
A5: for x being object st x in the carrier of V holds P[x, L.x];
A6: now
let v be VECTOR of V;
assume not v in C;
then P[v, K.v] & not v in C & v in the carrier of W or P[v, 0] by
STRUCT_0:def 5;
then P[v, K.v] & K.v = 0 or P[v, 0];
hence L.v = 0 by A5;
end;
L is Element of Funcs(the carrier of V, REAL) by FUNCT_2:8;
then reconsider L as Linear_Combination of V by A6,RLVECT_2:def 3;
reconsider L9= L|the carrier of W as Function of the carrier of W, REAL by A1
,FUNCT_2:32;
take L;
now
let x be object;
assume x in Carrier(L) & not x in the carrier of W;
then (ex v being VECTOR of V st x = v & L.v <> 0 )& not x in W by
STRUCT_0:def 5;
hence contradiction by A5;
end;
then
A7: Carrier(L) c= the carrier of W;
now
let x be object;
assume
A8: x in the carrier of W;
then P[x, L.x] by A5,A1;
hence K9.x = L9.x by A8,FUNCT_1:49,STRUCT_0:def 5;
end;
then K9 = L9 by FUNCT_2:12;
hence thesis by A7,Th18;
end;
theorem Th20:
for V being RealUnitarySpace, W being Subspace of V, L being
Linear_Combination of V st Carrier(L) c= the carrier of W holds ex K being
Linear_Combination of W st Carrier(K) = Carrier(L) & Sum(K) = Sum (L)
proof
let V being RealUnitarySpace;
let W being Subspace of V;
let L be Linear_Combination of V;
assume
A1: Carrier(L) c= the carrier of W;
then reconsider C = Carrier(L) as finite Subset of W;
the carrier of W c= the carrier of V by RUSUB_1:def 1;
then reconsider
K = L|the carrier of W as Function of the carrier of W, REAL by FUNCT_2:32;
A2: K is Element of Funcs(the carrier of W, REAL) by FUNCT_2:8;
A3: dom K = the carrier of W by FUNCT_2:def 1;
now
let w be VECTOR of W;
A4: w is VECTOR of V by RUSUB_1:3;
assume not w in C;
then L.w = 0 by A4;
hence K.w = 0 by A3,FUNCT_1:47;
end;
then reconsider K as Linear_Combination of W by A2,RLVECT_2:def 3;
take K;
thus thesis by A1,Th18;
end;
theorem Th21:
for V being RealUnitarySpace, I being Basis of V, v being VECTOR
of V holds v in Lin(I)
proof
let V be RealUnitarySpace;
let I be Basis of V;
let v be VECTOR of V;
v in the UNITSTR of V by STRUCT_0:def 5;
hence thesis by Def2;
end;
theorem Th22:
for V being RealUnitarySpace, W being Subspace of V, A being
Subset of W st A is linearly-independent holds A is linearly-independent Subset
of V
proof
let V be RealUnitarySpace;
let W be Subspace of V;
let A be Subset of W;
the carrier of W c= the carrier of V by RUSUB_1:def 1;
then reconsider A9= A as Subset of V by XBOOLE_1:1;
assume
A1: A is linearly-independent;
now
assume A9 is linearly-dependent;
then consider L being Linear_Combination of A9 such that
A2: Sum(L) = 0.V and
A3: Carrier(L) <> {};
Carrier(L) c= A by RLVECT_2:def 6;
then consider LW being Linear_Combination of W such that
A4: Carrier(LW) = Carrier(L) and
A5: Sum(LW) = Sum(L) by Th20,XBOOLE_1:1;
reconsider LW as Linear_Combination of A by A4,RLVECT_2:def 6;
Sum(LW) = 0.W by A2,A5,RUSUB_1:4;
hence contradiction by A1,A3,A4;
end;
hence thesis;
end;
theorem
for V being RealUnitarySpace, W being Subspace of V, A being Subset of
V st A is linearly-independent & A c= the carrier of W holds A is
linearly-independent Subset of W
proof
let V be RealUnitarySpace;
let W be Subspace of V;
let A be Subset of V such that
A1: A is linearly-independent and
A2: A c= the carrier of W;
reconsider A9= A as Subset of W by A2;
now
assume A9 is linearly-dependent;
then consider K being Linear_Combination of A9 such that
A3: Sum(K) = 0.W and
A4: Carrier(K) <> {};
consider L being Linear_Combination of V such that
A5: Carrier(L) = Carrier(K) and
A6: Sum(L) = Sum(K) by Th19;
reconsider L as Linear_Combination of A by A5,RLVECT_2:def 6;
Sum(L) = 0.V by A3,A6,RUSUB_1:4;
hence contradiction by A1,A4,A5;
end;
hence thesis;
end;
theorem
for V being RealUnitarySpace, W being Subspace of V, A being Basis of
W ex B being Basis of V st A c= B
proof
let V be RealUnitarySpace;
let W be Subspace of V;
let A be Basis of W;
A is linearly-independent by Def2;
then reconsider B = A as linearly-independent Subset of V by Th22;
consider I being Basis of V such that
A1: B c= I by Th15;
take I;
thus thesis by A1;
end;
theorem Th25:
for V being RealUnitarySpace, A being Subset of V st A is
linearly-independent for v being VECTOR of V st v in A for B being Subset of V
st B = A \ {v} holds not v in Lin(B)
proof
let V be RealUnitarySpace;
let A be Subset of V such that
A1: A is linearly-independent;
let v be VECTOR of V;
assume v in A;
then
A2: {v} is Subset of A by SUBSET_1:41;
let B be Subset of V such that
A3: B = A \ {v};
B c= A by A3,XBOOLE_1:36;
then
A4: B \/ {v} c= A \/ A by A2,XBOOLE_1:13;
assume v in Lin(B);
then consider L being Linear_Combination of B such that
A5: v = Sum(L) by Th1;
{v} is linearly-independent by A1,A2,RLVECT_3:5;
then v <> 0.V by RLVECT_3:8;
then Carrier(L) is non empty by A5,RLVECT_2:34;
then
A6: ex w being object st w in Carrier(L);
v in {v} by TARSKI:def 1;
then v in Lin({v}) by Th2;
then consider K being Linear_Combination of {v} such that
A7: v = Sum(K) by Th1;
A8: Carrier(L) c= B & Carrier(K) c= {v} by RLVECT_2:def 6;
then Carrier(L) \/ Carrier(K) c= B \/ {v} by XBOOLE_1:13;
then Carrier(L - K) c= Carrier(L) \/ Carrier(K) & Carrier(L) \/ Carrier(K)
c= A by A4,RLVECT_2:55;
then Carrier(L - K) c= A;
then
A9: L - K is Linear_Combination of A by RLVECT_2:def 6;
A10: for x being VECTOR of V holds x in Carrier(L) implies K.x = 0
proof
let x be VECTOR of V;
assume x in Carrier(L);
then not x in Carrier(K) by A3,A8,XBOOLE_0:def 5;
hence thesis;
end;
now
let x be object such that
A11: x in Carrier(L) and
A12: not x in Carrier(L - K);
reconsider x as VECTOR of V by A11;
A13: L.x <> 0 by A11,RLVECT_2:19;
(L - K).x = L.x - K.x by RLVECT_2:54
.= L.x - 0 by A10,A11
.= L.x;
hence contradiction by A12,A13;
end;
then
A14: Carrier(L) c= Carrier(L - K);
0.V = Sum(L) + (- Sum(K)) by A5,A7,RLVECT_1:5
.= Sum(L) + Sum(-K) by RLVECT_3:3
.= Sum(L - K) by RLVECT_3:1;
hence contradiction by A1,A6,A9,A14;
end;
Lm6: for X being set, x being set st not x in X holds X \ {x} = X
proof
let X be set, x be set such that
A1: not x in X;
now
assume X meets {x};
then consider y being object such that
A2: y in X /\ {x} by XBOOLE_0:4;
y in X & y in {x} by A2,XBOOLE_0:def 4;
hence contradiction by A1,TARSKI:def 1;
end;
hence thesis by XBOOLE_1:83;
end;
theorem
for V being RealUnitarySpace, I being Basis of V, A being non empty
Subset of V st A misses I for B being Subset of V st B = I \/ A holds B is
linearly-dependent
proof
let V be RealUnitarySpace;
let I be Basis of V;
let A be non empty Subset of V such that
A1: A misses I;
consider v being object such that
A2: v in A by XBOOLE_0:def 1;
let B be Subset of V such that
A3: B = I \/ A;
A4: A c= B by A3,XBOOLE_1:7;
reconsider v as VECTOR of V by A2;
reconsider Bv = B \ {v} as Subset of V;
A5: I \ {v} c= B \ {v} by A3,XBOOLE_1:7,33;
not v in I by A1,A2,XBOOLE_0:3;
then I c= Bv by A5,Lm6;
then
A6: Lin(I) is Subspace of Lin(Bv) by Th7;
assume
A7: B is linearly-independent;
v in Lin(I) by Th21;
hence contradiction by A7,A2,A4,A6,Th25,RUSUB_1:1;
end;
theorem
for V being RealUnitarySpace, W being Subspace of V, A being Subset of
V st A c= the carrier of W holds Lin(A) is Subspace of W
proof
let V be RealUnitarySpace;
let W be Subspace of V;
let A be Subset of V;
assume
A1: A c= the carrier of W;
now
let w be object;
assume w in the carrier of Lin(A);
then w in Lin(A) by STRUCT_0:def 5;
then consider L being Linear_Combination of A such that
A2: w = Sum(L) by Th1;
Carrier(L) c= A by RLVECT_2:def 6;
then
ex K being Linear_Combination of W st Carrier(K) = Carrier(L) & Sum(L)
= Sum(K) by A1,Th20,XBOOLE_1:1;
hence w in the carrier of W by A2;
end;
then the carrier of Lin(A) c= the carrier of W;
hence thesis by RUSUB_1:22;
end;
theorem
for V being RealUnitarySpace, W being Subspace of V, A being Subset of
V, B being Subset of W st A = B holds Lin(A) = Lin(B)
proof
let V be RealUnitarySpace;
let W be Subspace of V;
let A be Subset of V, B be Subset of W;
reconsider B9= Lin(B), V9= V as RealUnitarySpace;
A1: B9 is Subspace of V9 by RUSUB_1:21;
assume
A2: A = B;
now
let x be object;
assume x in the carrier of Lin(A);
then x in Lin(A) by STRUCT_0:def 5;
then consider L being Linear_Combination of A such that
A3: x = Sum(L) by Th1;
Carrier(L) c= A by RLVECT_2:def 6;
then consider K being Linear_Combination of W such that
A4: Carrier(K) = Carrier(L) and
A5: Sum(K) = Sum(L) by A2,Th20,XBOOLE_1:1;
reconsider K as Linear_Combination of B by A2,A4,RLVECT_2:def 6;
x = Sum(K) by A3,A5;
then x in Lin(B) by Th1;
hence x in the carrier of Lin(B) by STRUCT_0:def 5;
end;
then
A6: the carrier of Lin(A) c= the carrier of Lin(B);
now
let x be object;
assume x in the carrier of Lin(B);
then x in Lin(B) by STRUCT_0:def 5;
then consider K being Linear_Combination of B such that
A7: x = Sum(K) by Th1;
consider L being Linear_Combination of V such that
A8: Carrier(L) = Carrier(K) and
A9: Sum(L) = Sum(K) by Th19;
reconsider L as Linear_Combination of A by A2,A8,RLVECT_2:def 6;
x = Sum(L) by A7,A9;
then x in Lin(A) by Th1;
hence x in the carrier of Lin(A) by STRUCT_0:def 5;
end;
then the carrier of Lin(B) c= the carrier of Lin(A);
then the carrier of Lin(A) = the carrier of Lin(B) by A6;
hence thesis by A1,RUSUB_1:24;
end;
begin ::Subspaces of real unitary space generated by one, two, or three vectors
theorem Th29:
for V being RealUnitarySpace, v being VECTOR of V, x being set
holds x in Lin{v} iff ex a being Real st x = a * v
proof
deffunc F(set) = In(0,REAL);
let V be RealUnitarySpace;
let v be VECTOR of V;
let x be set;
thus x in Lin{v} implies ex a being Real 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 Th1;
Sum(l) = l.v * v by RLVECT_2:32;
hence thesis by A1;
end;
given a be Real such that
A2: x = a * v;
reconsider 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 = a 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 Th1;
end;
theorem
for V being RealUnitarySpace, v being VECTOR of V holds v in Lin{v}
proof
let V be RealUnitarySpace;
let v be VECTOR of V;
v in {v} by TARSKI:def 1;
hence thesis by Th2;
end;
theorem
for V being RealUnitarySpace, v,w being VECTOR of V, x being set holds
x in v + Lin{w} iff ex a being Real st x = v + a * w
proof
let V be RealUnitarySpace;
let v,w be VECTOR of V;
let x be set;
thus x in v + Lin{w} implies ex a being Real 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 RUSUB_2:63;
ex a being Real st u = a * w by A1,Th29;
hence thesis by A2;
end;
given a be Real such that
A3: x = v + a * w;
a * w in Lin{w} by Th29;
hence thesis by A3,RUSUB_2:63;
end;
theorem Th32:
for V being RealUnitarySpace, w1,w2 being VECTOR of V, x being
set holds x in Lin{w1,w2} iff ex a,b being Real st x = a * w1 + b * w2
proof
let V be RealUnitarySpace;
let w1,w2 be VECTOR of V;
let x be set;
thus x in Lin{w1,w2} implies ex a,b being Real 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 being Real such that
A2: x = a * w1 by A1,Th29;
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,Th1;
x = l.w1 * w1 + l.w2 * w2 by A3,A4,RLVECT_2:33;
hence thesis;
end;
end;
hence thesis;
end;
given a,b be Real 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 Th29;
hence thesis by A6,ENUMSET1:29;
end;
suppose
A7: w1 <> w2;
deffunc F(set) = In(0,REAL);
reconsider a,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 = a & f.w2 = b and
A9: for u being VECTOR of V 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 be VECTOR of V;
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 Th1;
end;
end;
hence thesis;
end;
theorem
for V being RealUnitarySpace, w1,w2 being VECTOR of V holds w1 in Lin{
w1,w2} & w2 in Lin{w1,w2}
proof
let V be RealUnitarySpace;
let w1,w2 be VECTOR of V;
w1 in {w1,w2} & w2 in {w1,w2} by TARSKI:def 2;
hence thesis by Th2;
end;
theorem
for V being RealUnitarySpace, v,w1,w2 being VECTOR of V, x being set
holds x in v + Lin{w1,w2} iff ex a,b being Real st x = v + a * w1 + b * w2
proof
let V be RealUnitarySpace;
let v,w1,w2 be VECTOR of V;
let x be set;
thus x in v + Lin{w1,w2} implies ex a,b being Real st x = v + a * w1 + b * w2
proof
assume x in v + Lin{w1,w2};
then consider u being VECTOR of V such that
A1: u in Lin{w1,w2} and
A2: x = v + u by RUSUB_2:63;
consider a,b being Real such that
A3: u = a * w1 + b * w2 by A1,Th32;
take a,b;
thus thesis by A2,A3,RLVECT_1:def 3;
end;
given a,b be Real such that
A4: x = v + a * w1 + b * w2;
a * w1 + b * w2 in Lin{w1,w2} by Th32;
then v + (a * w1 + b * w2) in v + Lin{w1,w2} by RUSUB_2:63;
hence thesis by A4,RLVECT_1:def 3;
end;
theorem Th35:
for V being RealUnitarySpace, v1,v2,v3 being VECTOR of V, x
being set holds x in Lin{v1,v2,v3} iff ex a,b,c being Real st x = a * v1 + b *
v2 + c * v3
proof
let V be RealUnitarySpace;
let v1,v2,v3 be VECTOR of V;
let x be set;
thus x in Lin{v1,v2,v3} implies ex a,b,c being Real 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,Th1;
x = l.v1 * v1 + l.v2 * v2 + l.v3 * v3 by A2,A3,RLVECT_4:6;
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 being Real such that
A5: x = a * v1 + b * v2 by A1,Th32;
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 being Real such that
A6: x = a * v1 + b * v3 by A1,Th32;
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 be Real 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 Th32;
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,Th32;
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,Th32;
end;
end;
hence thesis;
end;
suppose
A13: v1 <> v2 & v1 <> v3 & v2 <> v3;
deffunc F(set)=In(0,REAL);
A14: v1 <> v3 by A13;
A15: v2 <> v3 by A13;
A16: v1 <> v2 by A13;
reconsider a,b,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 = a & f.v2 = b & f.v3 = c and
A18: for v being VECTOR of V st v <> v1 & v <> v2 & v <> v3 holds f.
v = F(v) from RLVECT_4:sch 1 (A16,A14,A15);
reconsider f as Element of Funcs(the carrier of V,REAL) by FUNCT_2:8;
now
let v be VECTOR of 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,RLVECT_4:6;
hence thesis by Th1;
end;
end;
hence thesis;
end;
theorem
for V being RealUnitarySpace, w1,w2,w3 being VECTOR of V holds w1 in
Lin{w1,w2,w3} & w2 in Lin{w1,w2,w3} & w3 in Lin{w1,w2,w3}
proof
let V be RealUnitarySpace;
let w1,w2,w3 be VECTOR of V;
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,Th2;
end;
theorem
for V being RealUnitarySpace, v,w1,w2,w3 being VECTOR of V, x being
set holds x in v + Lin{w1,w2,w3} iff ex a,b,c being Real st x = v + a * w1 + b
* w2 + c * w3
proof
let V be RealUnitarySpace;
let v,w1,w2,w3 be VECTOR of V;
let x be set;
thus x in v + Lin{w1,w2,w3} implies ex a,b,c being Real st x = v + a * w1 +
b * w2 + c * w3
proof
assume x in v + Lin{w1,w2,w3};
then consider u being VECTOR of V such that
A1: u in Lin{w1,w2,w3} and
A2: x = v + u by RUSUB_2:63;
consider a,b,c being Real such that
A3: u = a * w1 + b * w2 + c * w3 by A1,Th35;
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 be Real such that
A4: x = v + a * w1 + b * w2 + c * w3;
a * w1 + b * w2 + c * w3 in Lin{w1,w2,w3} by Th35;
then v + (a * w1 + b * w2 + c * w3) in v + Lin{w1,w2,w3} by RUSUB_2: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
for V being RealUnitarySpace, v,w being VECTOR of V st v in Lin{w} & v
<> 0.V holds Lin{v} = Lin{w}
proof
let V be RealUnitarySpace;
let v,w be VECTOR of V;
assume that
A1: v in Lin{w} and
A2: v <> 0.V;
consider a be Real such that
A3: v = a * w by A1,Th29;
now
let u be VECTOR of V;
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 being Real such that
A5: u = b * v by Th29;
u = b * a * w by A3,A5,RLVECT_1:def 7;
hence thesis by Th29;
end;
assume u in Lin{w};
then consider b being Real such that
A6: u = b * w by Th29;
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 Th29;
end;
hence thesis by RUSUB_1:25;
end;
theorem
for V being RealUnitarySpace, v1,v2,w1,w2 being VECTOR of V st v1 <>
v2 & {v1,v2} is linearly-independent & v1 in Lin{w1,w2} & v2 in Lin{w1,w2}
holds Lin{w1,w2} = Lin{v1,v2} & {w1,w2} is linearly-independent & w1 <> w2
proof
let V be RealUnitarySpace;
let v1,v2,w1,w2 be VECTOR of V;
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 being Real such that
A5: v1 = r1 * w1 + r2 * w2 by A3,Th32;
consider r3,r4 being Real such that
A6: v2 = r3 * w1 + r4 * w2 by A4,Th32;
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 RLVECT_4:3;
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 RLVECT_4:3
.= 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 RLVECT_4:3;
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,RLVECT_4:3;
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 RLVECT_4:3
.= 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
RLVECT_4:3
.= r1" * v1 - (r2 * r1" * (- t") * (r3 * v1) + r2 * t" * v2) by
RLVECT_1:def 7
.= r1" * v1 - (((- jj) * t" * r2) * r1" * (r3 * v1) + r2 * t" * v2)
.= r1" * v1 - (((- jj) * t" * r2) * (r1" * (r3 * v1)) + r2 * t" * v2)
by RLVECT_1:def 7
.= r1" * v1 - (((- jj) * t") * (r2 * (r1" * (r3 * v1))) + r2 * t" * v2)
by RLVECT_1:def 7
.= r1" * v1 - ((- jj) * (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,RLVECT_4:3;
now
let u being VECTOR of V;
thus u in Lin{w1,w2} implies u in Lin{v1,v2}
proof
assume u in Lin{w1,w2};
then consider r5,r6 being Real such that
A20: u = r5 * w1 + r6 * w2 by Th32;
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 Th32;
end;
assume u in Lin{v1,v2};
then consider r5,r6 being Real such that
A21: u = r5 * v1 + r6 * v2 by Th32;
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 Th32;
end;
hence Lin{w1,w2} = Lin{v1,v2} by RUSUB_1:25;
now
let a,b be Real;
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,RLVECT_4:21;
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,RLVECT_4:21;
end;
end;
hence contradiction;
end;
hence thesis by RLVECT_3:13;
end;
begin :: Auxiliary theorems
theorem
for V being RealUnitarySpace, x being set holds x in (0).V iff x = 0.V
by Lm1;
theorem
for V being RealUnitarySpace, W1,W2,W3 being Subspace of V st W1 is
Subspace of W3 holds W1 /\ W2 is Subspace of W3 by Lm2;
theorem
for V being RealUnitarySpace, W1,W2,W3 being Subspace of V st W1 is
Subspace of W2 & W1 is Subspace of W3 holds W1 is Subspace of W2 /\ W3 by Lm3;
theorem
for V being RealUnitarySpace, W1,W2,W3 being Subspace of V st W1 is
Subspace of W3 & W2 is Subspace of W3 holds W1 + W2 is Subspace of W3 by Lm5;
theorem
for V being RealUnitarySpace, W1,W2,W3 being Subspace of V st W1 is
Subspace of W2 holds W1 is Subspace of W2 + W3 by Lm4;
theorem
for V being RealUnitarySpace, W1,W2 being Subspace of V, v being
VECTOR of V st W1 is Subspace of W2 holds v + W1 c= v + W2
proof
let V be RealUnitarySpace;
let W1,W2 being Subspace of V;
let v being VECTOR of V;
assume
A1: W1 is Subspace of W2;
let x be object;
assume x in v + W1;
then consider u being VECTOR of V such that
A2: u in W1 and
A3: x = v + u by RUSUB_2:63;
u in W2 by A1,A2,RUSUB_1:1;
hence thesis by A3,RUSUB_2:63;
end;