:: Basis of Real Linear Space
:: by Wojciech A. Trybulec
::
:: Received July 10, 1990
:: Copyright (c) 1990-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, SUBSET_1, NUMBERS, RLVECT_1, RLSUB_1, FINSET_1, RLVECT_2,
FINSEQ_1, STRUCT_0, FUNCT_1, XBOOLE_0, ORDERS_1, VALUED_1, ORDINAL4,
ARYTM_3, RELAT_1, PARTFUN1, NAT_1, CARD_3, CARD_1, SUPINF_2, FINSEQ_4,
TARSKI, FUNCT_2, ARYTM_1, ZFMISC_1, ORDINAL1, RLVECT_3, FUNCT_7;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, FINSEQ_1,
RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, ORDERS_1, DOMAIN_1, XCMPLX_0,
XREAL_0, STRUCT_0, RLVECT_1, FINSEQ_4, FINSET_1, REAL_1, RLSUB_1,
RLSUB_2, RLVECT_2, NAT_1;
constructors PARTFUN1, REAL_1, NAT_1, ORDERS_1, FINSEQ_4, REALSET1, RLSUB_2,
RLVECT_2, RELSET_1, NUMBERS;
registrations XBOOLE_0, SUBSET_1, FUNCT_1, RELSET_1, FINSET_1, NUMBERS,
STRUCT_0, RLVECT_1, RLSUB_1, ORDINAL1, XREAL_0, RLVECT_2;
requirements NUMERALS, BOOLE, SUBSET, ARITHM;
definitions XBOOLE_0, RLSUB_1, RLVECT_2, TARSKI;
equalities RLSUB_1, RLVECT_2;
expansions XBOOLE_0, TARSKI;
theorems CARD_2, FUNCT_1, FUNCT_2, FINSEQ_1, FINSEQ_2, FINSEQ_3, FINSEQ_4,
FINSET_1, RLSUB_1, RLSUB_2, RLVECT_1, RLVECT_2, TARSKI, ZFMISC_1,
RELAT_1, ORDINAL1, XBOOLE_0, XBOOLE_1, XCMPLX_0, ORDERS_1, STRUCT_0,
PARTFUN1, XREAL_0;
schemes FINSEQ_1, FUNCT_1, FUNCT_2, XFAMILY;
begin
reserve x,y for object, X,Y,Z for set;
reserve a,b for Real;
reserve k for Element of NAT;
reserve V for RealLinearSpace;
reserve W1,W2,W3 for Subspace of V;
reserve v,v1,v2,u for VECTOR of V;
reserve A,B,C for Subset of V;
reserve T for finite Subset of V;
reserve L,L1,L2 for Linear_Combination of V;
reserve l for Linear_Combination of A;
reserve F,G,H for FinSequence of the carrier of V;
reserve f,g for Function of the carrier of V, REAL;
reserve p,q,r for FinSequence;
reserve M for non empty set;
reserve CF for Choice_Function of M;
Lm1: f (#) (F ^ G) = (f (#) F) ^ (f (#) G)
proof
set H = (f (#) F) ^ (f (#) G);
set I = F ^ G;
A1: len H = len(f (#) F) + len(f (#) G) by FINSEQ_1:22
.= len F + len(f (#) G) by RLVECT_2:def 7
.= len F + len G by RLVECT_2:def 7
.= len I by FINSEQ_1:22;
A2: len F = len(f (#) F) by RLVECT_2:def 7;
A3: len G = len(f (#) G) by RLVECT_2:def 7;
now
let k be Nat;
assume
A4: k in dom H;
now
per cases by A4,FINSEQ_1:25;
suppose
A5: k in dom(f (#) F);
then
A6: k in dom F by A2,FINSEQ_3:29;
then
A7: k in dom(F ^ G) by FINSEQ_3:22;
A8: F/.k = F.k by A6,PARTFUN1:def 6
.= (F ^ G).k by A6,FINSEQ_1:def 7
.= (F ^ G)/.k by A7,PARTFUN1:def 6;
thus H.k = (f (#) F).k by A5,FINSEQ_1:def 7
.= f.(I/.k) * I/.k by A5,A8,RLVECT_2:def 7;
end;
suppose
A9: ex n be Nat st n in dom(f (#) G) & k = len(f (#) F) + n;
A10: k in dom I by A1,A4,FINSEQ_3:29;
consider n be Nat such that
A11: n in dom(f (#) G) and
A12: k = len(f (#) F) + n by A9;
A13: n in dom G by A3,A11,FINSEQ_3:29;
then
A14: G/.n = G.n by PARTFUN1:def 6
.= (F ^ G).k by A2,A12,A13,FINSEQ_1:def 7
.= (F ^ G)/.k by A10,PARTFUN1:def 6;
thus H.k = (f (#) G).n by A11,A12,FINSEQ_1:def 7
.= f.(I/.k) * I/.k by A11,A14,RLVECT_2:def 7;
end;
end;
hence H.k = f.(I/.k) * I/.k;
end;
hence thesis by A1,RLVECT_2:def 7;
end;
theorem Th1:
Sum(L1 + L2) = Sum(L1) + Sum(L2)
proof
consider F such that
A1: F is one-to-one and
A2: rng F = Carrier(L1 + L2) and
A3: Sum((L1 + L2) (#) F) = Sum(L1 + L2) by RLVECT_2:def 8;
set A = Carrier(L1 + L2) \/ Carrier(L1) \/ Carrier(L2);
set C3 = A \ Carrier(L1 + L2);
consider r such that
A4: rng r = C3 and
A5: r is one-to-one by FINSEQ_4:58;
reconsider r as FinSequence of the carrier of V by A4,FINSEQ_1:def 4;
set FF = F ^ r;
A6: A = Carrier(L1 + L2) \/ (Carrier(L1) \/ Carrier(L2)) by XBOOLE_1:4;
rng F misses rng r
proof
set x = the Element of rng F /\ rng r;
assume not thesis;
then rng F /\ rng r <> {};
then x in Carrier(L1 + L2) & x in C3 by A2,A4,XBOOLE_0:def 4;
hence thesis by XBOOLE_0:def 5;
end;
then
A7: FF is one-to-one by A1,A5,FINSEQ_3:91;
A8: len r = len((L1 + L2) (#) r) by RLVECT_2:def 7;
now
let k be Nat;
assume
A9: k in dom r;
then r/.k = r.k by PARTFUN1:def 6;
then r/.k in C3 by A4,A9,FUNCT_1:def 3;
then
A10: not r/.k in Carrier((L1 + L2)) by XBOOLE_0:def 5;
k in dom((L1 + L2) (#) r) by A8,A9,FINSEQ_3:29;
then ((L1 + L2) (#) r).k = (L1 + L2).(r/.k) * r/.k by RLVECT_2:def 7;
hence ((L1 + L2) (#) r).k = 0 * r/.k by A10;
end;
then
A11: Sum((L1 + L2) (#) r) = 0 * Sum(r) by A8,RLVECT_2:3
.= 0.V by RLVECT_1:10;
set f = (L1 + L2) (#) FF;
set C1 = A \ Carrier(L1);
consider G such that
A12: G is one-to-one and
A13: rng G = Carrier(L1) and
A14: Sum(L1 (#) G) = Sum(L1) by RLVECT_2:def 8;
consider p such that
A15: rng p = C1 and
A16: p is one-to-one by FINSEQ_4:58;
reconsider p as FinSequence of the carrier of V by A15,FINSEQ_1:def 4;
set GG = G ^ p;
A17: Sum(f) = Sum(((L1 + L2) (#) F) ^ ((L1 + L2) (#) r)) by Lm1
.= Sum((L1 + L2) (#) F) + 0.V by A11,RLVECT_1:41
.= Sum((L1 + L2) (#) F);
set C2 = A \ Carrier(L2);
consider H such that
A18: H is one-to-one and
A19: rng H = Carrier(L2) and
A20: Sum(L2 (#) H) = Sum(L2) by RLVECT_2:def 8;
consider q such that
A21: rng q = C2 and
A22: q is one-to-one by FINSEQ_4:58;
reconsider q as FinSequence of the carrier of V by A21,FINSEQ_1:def 4;
set HH = H ^ q;
rng H misses rng q
proof
set x = the Element of rng H /\ rng q;
assume not thesis;
then rng H /\ rng q <> {};
then x in Carrier(L2) & x in C2 by A19,A21,XBOOLE_0:def 4;
hence thesis by XBOOLE_0:def 5;
end;
then
A23: HH is one-to-one by A18,A22,FINSEQ_3:91;
set h = L2 (#) HH;
A24: A = Carrier(L1) \/ (Carrier(L1 + L2) \/ Carrier(L2)) by XBOOLE_1:4;
rng GG = rng G \/ rng p by FINSEQ_1:31;
then rng GG = Carrier(L1) \/ A by A13,A15,XBOOLE_1:39;
then
A25: rng GG = A by A24,XBOOLE_1:7,12;
A26: len q = len(L2 (#) q) by RLVECT_2:def 7;
now
let k be Nat;
assume
A27: k in dom q;
then q/.k = q.k by PARTFUN1:def 6;
then q/.k in C2 by A21,A27,FUNCT_1:def 3;
then
A28: not q/.k in Carrier(L2) by XBOOLE_0:def 5;
k in dom(L2 (#) q) by A26,A27,FINSEQ_3:29;
then (L2 (#) q).k = L2.(q/.k) * q/.k by RLVECT_2:def 7;
hence (L2 (#) q).k = 0 * q/.k by A28;
end;
then
A29: Sum(L2 (#) q) = 0 * Sum(q) by A26,RLVECT_2:3
.= 0.V by RLVECT_1:10;
A30: Sum(h) = Sum((L2 (#) H) ^ (L2 (#) q)) by Lm1
.= Sum(L2 (#) H) + 0.V by A29,RLVECT_1:41
.= Sum(L2 (#) H);
deffunc Q(Nat)=FF <- (GG.$1);
set g = L1 (#) GG;
consider P being FinSequence such that
A31: len P = len FF and
A32: for k be Nat st k in dom P holds P.k = Q(k) from FINSEQ_1:sch 2;
A33: dom P = Seg(len FF) by A31,FINSEQ_1:def 3;
A34: len p = len(L1 (#) p) by RLVECT_2:def 7;
now
let k be Nat;
assume
A35: k in dom p;
then p/.k = p.k by PARTFUN1:def 6;
then p/.k in C1 by A15,A35,FUNCT_1:def 3;
then
A36: not p/.k in Carrier(L1) by XBOOLE_0:def 5;
k in dom(L1 (#) p) by A34,A35,FINSEQ_3:29;
then (L1 (#) p).k = L1.(p/.k) * p/.k by RLVECT_2:def 7;
hence (L1 (#) p).k = 0 * p/.k by A36;
end;
then
A37: Sum(L1 (#) p) = 0 * Sum(p) by A34,RLVECT_2:3
.= 0.V by RLVECT_1:10;
A38: Sum(g) = Sum((L1 (#) G) ^ (L1 (#) p)) by Lm1
.= Sum(L1 (#) G) + 0.V by A37,RLVECT_1:41
.= Sum(L1 (#) G);
rng FF = rng F \/ rng r by FINSEQ_1:31;
then rng FF = Carrier(L1 + L2) \/ A by A2,A4,XBOOLE_1:39;
then
A39: rng FF = A by A6,XBOOLE_1:7,12;
rng G misses rng p
proof
set x = the Element of rng G /\ rng p;
assume not thesis;
then rng G /\ rng p <> {};
then x in Carrier(L1) & x in C1 by A13,A15,XBOOLE_0:def 4;
hence thesis by XBOOLE_0:def 5;
end;
then
A40: GG is one-to-one by A12,A16,FINSEQ_3:91;
then
A41: len GG = len FF by A7,A25,A39,FINSEQ_1:48;
A42: dom P = Seg len FF by A31,FINSEQ_1:def 3;
A43: now
let x be object;
assume
A44: x in dom GG;
then reconsider n = x as Element of NAT by FINSEQ_3:23;
GG.n in rng FF by A25,A39,A44,FUNCT_1:def 3;
then
A45: FF just_once_values GG.n by A7,FINSEQ_4:8;
n in Seg(len FF) by A41,A44,FINSEQ_1:def 3;
then FF.(P.n) = FF.(FF <- (GG.n)) by A32,A42
.= GG.n by A45,FINSEQ_4:def 3;
hence GG.x = FF.(P.x);
end;
A46: rng P c= Seg(len FF)
proof
let x be object;
assume x in rng P;
then consider y being object such that
A47: y in dom P and
A48: P.y = x by FUNCT_1:def 3;
reconsider y as Element of NAT by A47,FINSEQ_3:23;
y in Seg(len FF) by A31,A47,FINSEQ_1:def 3;
then y in dom GG by A41,FINSEQ_1:def 3;
then GG.y in rng FF by A25,A39,FUNCT_1:def 3;
then
A49: FF just_once_values GG.y by A7,FINSEQ_4:8;
P.y = FF <- (GG.y) by A32,A47;
then P.y in dom FF by A49,FINSEQ_4:def 3;
hence thesis by A48,FINSEQ_1:def 3;
end;
now
let x be object;
thus x in dom GG implies x in dom P & P.x in dom FF
proof
assume x in dom GG;
then x in Seg(len P) by A41,A31,FINSEQ_1:def 3;
hence x in dom P by FINSEQ_1:def 3;
then P.x in rng P by FUNCT_1:def 3;
then P.x in Seg(len FF) by A46;
hence thesis by FINSEQ_1:def 3;
end;
assume that
A50: x in dom P and
P.x in dom FF;
x in Seg(len P) by A50,FINSEQ_1:def 3;
hence x in dom GG by A41,A31,FINSEQ_1:def 3;
end;
then
A51: GG = FF * P by A43,FUNCT_1:10;
Seg(len FF) c= rng P
proof
set f = FF" * GG;
let x be object;
assume
A52: x in Seg(len FF);
dom(FF") = rng GG by A7,A25,A39,FUNCT_1:33;
then
A53: rng f = rng(FF") by RELAT_1:28
.= dom FF by A7,FUNCT_1:33;
A54: rng P c= dom FF by A46,FINSEQ_1:def 3;
f = FF " * FF * P by A51,RELAT_1:36
.= id(dom FF) * P by A7,FUNCT_1:39
.= P by A54,RELAT_1:53;
hence thesis by A52,A53,FINSEQ_1:def 3;
end;
then
A55: Seg(len FF) = rng P by A46;
then
A56: P is one-to-one by A33,FINSEQ_4:60;
reconsider P as Function of Seg(len FF), Seg(len FF) by A46,A33,FUNCT_2:2;
reconsider P as Permutation of Seg(len FF) by A55,A56,FUNCT_2:57;
A57: len f = len FF by RLVECT_2:def 7;
then
A58: Seg len FF = dom f by FINSEQ_1:def 3;
then reconsider Fp = f * P as FinSequence of the carrier of V by FINSEQ_2:47;
A59: len g = len GG by RLVECT_2:def 7;
deffunc Q(Nat)=HH <- (GG.$1);
consider R being FinSequence such that
A60: len R = len HH and
A61: for k be Nat st k in dom R holds R.k =Q(k) from FINSEQ_1:sch 2;
A62: dom R = Seg(len HH) by A60,FINSEQ_1:def 3;
rng HH = rng H \/ rng q by FINSEQ_1:31;
then rng HH = Carrier(L2) \/ A by A19,A21,XBOOLE_1:39;
then
A63: rng HH = A by XBOOLE_1:7,12;
then
A64: len GG = len HH by A23,A40,A25,FINSEQ_1:48;
A65: dom R = Seg len HH by A60,FINSEQ_1:def 3;
A66: now
let x be object;
assume
A67: x in dom GG;
then reconsider n = x as Element of NAT by FINSEQ_3:23;
GG.n in rng HH by A25,A63,A67,FUNCT_1:def 3;
then
A68: HH just_once_values GG.n by A23,FINSEQ_4:8;
n in Seg(len HH) by A64,A67,FINSEQ_1:def 3;
then HH.(R.n) = HH.(HH <- (GG.n)) by A61,A65
.= GG.n by A68,FINSEQ_4:def 3;
hence GG.x = HH.(R.x);
end;
A69: rng R c= Seg(len HH)
proof
let x be object;
assume x in rng R;
then consider y being object such that
A70: y in dom R and
A71: R.y = x by FUNCT_1:def 3;
reconsider y as Element of NAT by A70,FINSEQ_3:23;
y in Seg(len HH) by A60,A70,FINSEQ_1:def 3;
then y in dom GG by A64,FINSEQ_1:def 3;
then GG.y in rng HH by A25,A63,FUNCT_1:def 3;
then
A72: HH just_once_values GG.y by A23,FINSEQ_4:8;
R.y = HH <- (GG.y) by A61,A70;
then R.y in dom HH by A72,FINSEQ_4:def 3;
hence thesis by A71,FINSEQ_1:def 3;
end;
now
let x be object;
thus x in dom GG implies x in dom R & R.x in dom HH
proof
assume x in dom GG;
then x in Seg(len R) by A64,A60,FINSEQ_1:def 3;
hence x in dom R by FINSEQ_1:def 3;
then R.x in rng R by FUNCT_1:def 3;
then R.x in Seg(len HH) by A69;
hence thesis by FINSEQ_1:def 3;
end;
assume that
A73: x in dom R and
R.x in dom HH;
x in Seg(len R) by A73,FINSEQ_1:def 3;
hence x in dom GG by A64,A60,FINSEQ_1:def 3;
end;
then
A74: GG = HH * R by A66,FUNCT_1:10;
Seg(len HH) c= rng R
proof
set f = HH" * GG;
let x be object;
assume
A75: x in Seg(len HH);
dom(HH") = rng GG by A23,A25,A63,FUNCT_1:33;
then
A76: rng f = rng(HH") by RELAT_1:28
.= dom HH by A23,FUNCT_1:33;
A77: rng R c= dom HH by A69,FINSEQ_1:def 3;
f = HH " * HH * R by A74,RELAT_1:36
.= id(dom HH) * R by A23,FUNCT_1:39
.= R by A77,RELAT_1:53;
hence thesis by A75,A76,FINSEQ_1:def 3;
end;
then
A78: Seg(len HH) = rng R by A69;
then
A79: R is one-to-one by A62,FINSEQ_4:60;
reconsider R as Function of Seg(len HH), Seg(len HH) by A69,A62,FUNCT_2:2;
reconsider R as Permutation of Seg(len HH) by A78,A79,FUNCT_2:57;
A80: len h = len HH by RLVECT_2:def 7;
then
A81: Seg len HH = dom h by FINSEQ_1:def 3;
then reconsider Hp = h * R as FinSequence of the carrier of V by FINSEQ_2:47;
A82: len Hp = len GG by A64,A80,A81,FINSEQ_2:44;
deffunc Q(Nat)=g/.$1 + Hp/.$1;
consider I being FinSequence such that
A83: len I = len GG and
A84: for k be Nat st k in dom I holds I.k = Q(k) from FINSEQ_1:sch 2;
dom I = Seg len GG by A83,FINSEQ_1:def 3;
then
A85: for k be Nat st k in Seg(len GG) holds I.k = Q(k) by A84;
rng I c= the carrier of V
proof
let x be object;
assume x in rng I;
then consider y being object such that
A86: y in dom I and
A87: I.y = x by FUNCT_1:def 3;
reconsider y as Element of NAT by A86,FINSEQ_3:23;
I.y = g/.y + Hp/.y by A84,A86;
hence thesis by A87;
end;
then reconsider I as FinSequence of the carrier of V by FINSEQ_1:def 4;
A88: len Fp = len I by A41,A57,A58,A83,FINSEQ_2:44;
A89: now
let x be object;
assume
A90: x in dom I;
then reconsider k = x as Element of NAT by FINSEQ_3:23;
A91: x in dom Hp by A83,A82,A90,FINSEQ_3:29;
k in dom R by A64,A62,A83,A90,FINSEQ_1:def 3;
then
A92: R.k in dom R by A78,A62,FUNCT_1:def 3;
then reconsider j = R.k as Element of NAT by FINSEQ_3:23;
set v = GG/.k;
A93: R.k in dom HH by A60,A92,FINSEQ_3:29;
A94: x in dom GG by A83,A90,FINSEQ_3:29;
then HH.j = GG.k by A66
.= GG/.k by A94,PARTFUN1:def 6;
then
A95: h.j = L2.v * v by A93,RLVECT_2:24;
k in dom P by A41,A33,A83,A90,FINSEQ_1:def 3;
then
A96: P.k in dom P by A55,A33,FUNCT_1:def 3;
then reconsider l = P.k as Element of NAT by FINSEQ_3:23;
A97: P.k in dom FF by A31,A96,FINSEQ_3:29;
x in dom Fp by A88,A90,FINSEQ_3:29;
then
A98: Fp.k = f.(P.k) by FUNCT_1:12;
k in dom Hp by A83,A82,A90,FINSEQ_3:29;
then
A99: Hp/.k = (h * R).k by PARTFUN1:def 6
.= h.(R.k) by A91,FUNCT_1:12;
A100: x in dom g by A83,A59,A90,FINSEQ_3:29;
FF.l = GG.k by A43,A94
.= GG/.k by A94,PARTFUN1:def 6;
then
A101: f.l = (L1 + L2).v * v by A97,RLVECT_2:24
.= (L1.v + L2.v) * v by RLVECT_2:def 10
.= L1.v * v + L2.v * v by RLVECT_1:def 6;
k in dom g by A83,A59,A90,FINSEQ_3:29;
then g/.k = g.k by PARTFUN1:def 6
.= L1.v * v by A100,RLVECT_2:def 7;
hence I.x = Fp.x by A84,A90,A99,A95,A98,A101;
end;
dom h = Seg(len h) by FINSEQ_1:def 3;
then
A102: Sum(Hp) = Sum(h) by A80,RLVECT_2:7;
dom f = Seg(len f) by FINSEQ_1:def 3;
then
A103: Sum(Fp) = Sum(f) by A57,RLVECT_2:7;
dom I = Seg(len I) & dom Fp = Seg(len I) by A88,FINSEQ_1:def 3;
then
A104: I = Fp by A89,FUNCT_1:2;
Seg len GG = dom g by A59,FINSEQ_1:def 3;
hence thesis by A3,A14,A20,A38,A30,A17,A103,A102,A83,A85,A82,A59,A104,
RLVECT_2:2;
end;
theorem Th2:
Sum(a * L) = a * Sum(L)
proof
per cases;
suppose
A1: a <> 0;
set l = a * L;
consider F such that
A2: F is one-to-one and
A3: rng F = Carrier(a * L) and
A4: Sum(a * L) = Sum ((a * L) (#) F) by RLVECT_2:def 8;
set f = (a * L) (#) F;
consider G such that
A5: G is one-to-one and
A6: rng G = Carrier(L) and
A7: Sum(L) = Sum(L (#) G) by RLVECT_2:def 8;
A8: len G = len F by A1,A2,A3,A5,A6,FINSEQ_1:48,RLVECT_2:42;
deffunc Q(Nat) = F <- (G.$1);
consider P being FinSequence such that
A9: len P = len F and
A10: for k be Nat st k in dom P holds P.k = Q(k) from FINSEQ_1:sch 2;
A11: Carrier(l) = Carrier(L) by A1,RLVECT_2:42;
A12: rng P c= Seg(len F)
proof
let x be object;
assume x in rng P;
then consider y being object such that
A13: y in dom P and
A14: P.y = x by FUNCT_1:def 3;
reconsider y as Element of NAT by A13,FINSEQ_3:23;
y in Seg(len F) by A9,A13,FINSEQ_1:def 3;
then y in dom G by A8,FINSEQ_1:def 3;
then G.y in rng F by A3,A6,A11,FUNCT_1:def 3;
then
A15: F just_once_values G.y by A2,FINSEQ_4:8;
P.y = F <- (G.y) by A10,A13;
then P.y in dom F by A15,FINSEQ_4:def 3;
hence thesis by A14,FINSEQ_1:def 3;
end;
A16: now
let x be object;
thus x in dom G implies x in dom P & P.x in dom F
proof
assume x in dom G;
then x in Seg(len P) by A9,A8,FINSEQ_1:def 3;
hence x in dom P by FINSEQ_1:def 3;
then P.x in rng P by FUNCT_1:def 3;
then P.x in Seg(len F) by A12;
hence thesis by FINSEQ_1:def 3;
end;
assume that
A17: x in dom P and
P.x in dom F;
x in Seg(len P) by A17,FINSEQ_1:def 3;
hence x in dom G by A9,A8,FINSEQ_1:def 3;
end;
A18: dom P = Seg len F by A9,FINSEQ_1:def 3;
now
let x be object;
assume
A19: x in dom G;
then reconsider n = x as Element of NAT by FINSEQ_3:23;
G.n in rng F by A3,A6,A11,A19,FUNCT_1:def 3;
then
A20: F just_once_values G.n by A2,FINSEQ_4:8;
n in Seg(len F) by A8,A19,FINSEQ_1:def 3;
then F.(P.n) = F.(F <- (G.n)) by A10,A18
.= G.n by A20,FINSEQ_4:def 3;
hence G.x = F.(P.x);
end;
then
A21: G = F * P by A16,FUNCT_1:10;
Seg(len F) c= rng P
proof
set f = F" * G;
let x be object;
assume
A22: x in Seg(len F);
dom(F") = rng G by A2,A3,A6,A11,FUNCT_1:33;
then
A23: rng f = rng(F") by RELAT_1:28
.= dom F by A2,FUNCT_1:33;
A24: rng P c= dom F by A12,FINSEQ_1:def 3;
f = F " * F * P by A21,RELAT_1:36
.= id(dom F) * P by A2,FUNCT_1:39
.= P by A24,RELAT_1:53;
hence thesis by A22,A23,FINSEQ_1:def 3;
end;
then
A25: Seg(len F) = rng P by A12;
A26: dom P = Seg(len F) by A9,FINSEQ_1:def 3;
then
A27: P is one-to-one by A25,FINSEQ_4:60;
reconsider P as Function of Seg(len F), Seg(len F) by A12,A26,FUNCT_2:2;
reconsider P as Permutation of Seg(len F) by A25,A27,FUNCT_2:57;
A28: len f = len F by RLVECT_2:def 7;
then
A29: dom f = Seg(len F) by FINSEQ_1:def 3;
then reconsider Fp = f * P as FinSequence of the carrier of V by
FINSEQ_2:47;
set g = L (#) G;
dom f = Seg(len f) by FINSEQ_1:def 3;
then
A30: Sum(Fp) = Sum(f) by A28,RLVECT_2:7;
A31: len Fp = len f by A29,FINSEQ_2:44;
then
A32: len Fp = len g by A8,A28,RLVECT_2:def 7;
A33: now
let k be Nat,v;
assume that
A34: k in dom g and
A35: v = g.k;
A36: k in Seg len F by A28,A31,A32,A34,FINSEQ_1:def 3;
A37: k in dom G by A8,A28,A31,A32,A34,FINSEQ_3:29;
then G.k in rng G by FUNCT_1:def 3;
then F just_once_values G.k by A2,A3,A6,A11,FINSEQ_4:8;
then
A38: F <- (G.k) in dom F by FINSEQ_4:def 3;
then reconsider i = F <- (G.k) as Element of NAT by FINSEQ_3:23;
i in Seg(len f) by A28,A38,FINSEQ_1:def 3;
then
A39: i in dom f by FINSEQ_1:def 3;
A40: k in dom P by A9,A28,A31,A32,A34,FINSEQ_3:29;
A41: G/.k = G.k by A37,PARTFUN1:def 6
.= F.(P.k) by A21,A40,FUNCT_1:13
.= F.i by A10,A18,A36
.= F/.i by A38,PARTFUN1:def 6;
thus Fp.k = f.(P.k) by A40,FUNCT_1:13
.= f.(F <- (G.k)) by A10,A18,A36
.= l.(F/.i) * F/.i by A39,RLVECT_2:def 7
.= a * L.(F/.i) * F/.i by RLVECT_2:def 11
.= a * (L.(F/.i) * F/.i) by RLVECT_1:def 7
.= a * v by A34,A35,A41,RLVECT_2:def 7;
end;
dom Fp = dom g by A32,FINSEQ_3:29;
hence thesis by A4,A7,A30,A32,A33,RLVECT_1:39;
end;
suppose
A42: a = 0;
hence Sum(a * L) = Sum(ZeroLC(V)) by RLVECT_2:43
.= 0.V by RLVECT_2:30
.= a * Sum(L) by A42,RLVECT_1:10;
end;
end;
reconsider jj=1 as Element of REAL by XREAL_0:def 1;
theorem Th3:
Sum(- L) = - Sum(L)
proof
thus Sum(- L) = (- jj) * Sum(L) by Th2
.= - Sum(L) by RLVECT_1:16;
end;
theorem Th4:
Sum(L1 - L2) = Sum(L1) - Sum(L2)
proof
thus Sum(L1 - L2) = Sum(L1) + Sum(- L2) by Th1
.= Sum(L1) + (- Sum(L2)) by Th3
.= Sum(L1) - Sum(L2) by RLVECT_1:def 11;
end;
definition
let V;
let A;
attr A is linearly-independent means
for l st Sum(l) = 0.V holds Carrier(l) = {};
end;
notation
let V;
let A;
antonym A is linearly-dependent for A is linearly-independent;
end;
theorem
A c= B & B is linearly-independent implies A is linearly-independent
proof
assume that
A1: A c= B and
A2: B is linearly-independent;
let l be Linear_Combination of A;
reconsider L = l as Linear_Combination of B by A1,RLVECT_2:21;
assume Sum(l) = 0.V;
then Carrier(L) = {} by A2;
hence thesis;
end;
theorem Th6:
A is linearly-independent implies not 0.V in A
proof
assume that
A1: A is linearly-independent and
A2: 0.V in A;
deffunc F(Element of V) = In(0,REAL);
consider f such that
A3: f.(0.V) = jj and
A4: for v being Element of V st v <> 0.V holds f.v = F(v) from FUNCT_2:
sch 6;
reconsider f as Element of Funcs(the carrier of V, REAL) by FUNCT_2:8;
ex T st for v st not v in T holds f.v = 0
proof
take T = {0.V};
let v;
assume not v in T;
then v <> 0.V by TARSKI:def 1;
hence thesis by A4;
end;
then reconsider f as Linear_Combination of V by RLVECT_2:def 3;
A5: Carrier(f) = {0.V}
proof
thus Carrier(f) c= {0.V}
proof
let x be object;
assume x in Carrier(f);
then consider v such that
A6: v = x and
A7: f.v <> 0;
v = 0.V by A4,A7;
hence thesis by A6,TARSKI:def 1;
end;
let x be object;
assume x in {0.V};
then x = 0.V by TARSKI:def 1;
hence thesis by A3;
end;
then Carrier(f) c= A by A2,ZFMISC_1:31;
then reconsider f as Linear_Combination of A by RLVECT_2:def 6;
Sum(f) = f.(0.V) * 0.V by A5,RLVECT_2:35
.= 0.V;
hence contradiction by A1,A5;
end;
theorem Th7:
{}(the carrier of V) is linearly-independent
proof
let l be Linear_Combination of {}(the carrier of V);
Carrier(l) c= {} by RLVECT_2:def 6;
hence thesis;
end;
registration
let V;
cluster linearly-independent for Subset of V;
existence
proof
take {}(the carrier of V);
thus thesis by Th7;
end;
end;
theorem Th8:
{v} is linearly-independent iff v <> 0.V
proof
thus {v} is linearly-independent implies v <> 0.V
proof
assume {v} is linearly-independent;
then not 0.V in {v} by Th6;
hence thesis by TARSKI:def 1;
end;
assume
A1: v <> 0.V;
let l be Linear_Combination of {v};
A2: Carrier(l) c= {v} by RLVECT_2:def 6;
assume
A3: Sum(l) = 0.V;
now
per cases by A2,ZFMISC_1:33;
suppose
Carrier(l) = {};
hence thesis;
end;
suppose
A4: Carrier(l) = {v};
A5: 0.V = l.v * v by A3,RLVECT_2:32;
now
assume v in Carrier(l);
then ex u st v = u & l.u <> 0;
hence contradiction by A1,A5,RLVECT_1:11;
end;
hence thesis by A4,TARSKI:def 1;
end;
end;
hence thesis;
end;
theorem
{0.V} is linearly-dependent by Th8;
theorem Th10:
{v1,v2} is linearly-independent implies v1 <> 0.V & v2 <> 0.V
proof
A1: v1 in {v1,v2} & v2 in {v1,v2} by TARSKI:def 2;
assume {v1,v2} is linearly-independent;
hence thesis by A1,Th6;
end;
theorem
{v,0.V} is linearly-dependent & {0.V,v} is linearly-dependent by Th10;
theorem Th12:
v1 <> v2 & {v1,v2} is linearly-independent iff v2 <> 0.V & for a
holds v1 <> a * v2
proof
thus v1 <> v2 & {v1,v2} is linearly-independent implies v2 <> 0.V & for a
holds v1 <> a * v2
proof
deffunc F(Element of V)=In(0,REAL);
assume that
A1: v1 <> v2 and
A2: {v1,v2} is linearly-independent;
thus v2 <> 0.V by A2,Th10;
let a;
reconsider aa=a as Element of REAL by XREAL_0:def 1;
consider f such that
A3: f.v1 = - jj & f.v2 = aa and
A4: for v being Element of V st v <> v1 & v <> v2 holds f.v = F(v)
from FUNCT_2:sch 7(A1);
reconsider f as Element of Funcs(the carrier of V, REAL) by FUNCT_2:8;
now
let v;
assume not v in {v1,v2};
then v <> v1 & v <> v2 by TARSKI:def 2;
hence f.v = 0 by A4;
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 x in Carrier(f);
then
A5: ex u st x = u & f.u <> 0;
assume not x in {v1,v2};
then x <> v1 & x <> v2 by TARSKI:def 2;
hence thesis by A4,A5;
end;
then reconsider f as Linear_Combination of {v1,v2} by RLVECT_2:def 6;
A6: v1 in Carrier(f) by A3;
set w = a * v2;
assume v1 = a * v2;
then Sum(f) = (- jj) * w + w by A1,A3,RLVECT_2:33
.= (- w) + w by RLVECT_1:16
.= - (w - w) by RLVECT_1:33
.= - 0.V by RLVECT_1:15
.= 0.V;
hence thesis by A2,A6;
end;
assume
A7: v2 <> 0.V;
assume
A8: for a holds v1 <> a * v2;
A9: 1 * v2 = v2 by RLVECT_1:def 8;
hence v1 <> v2 by A8;
let l be Linear_Combination of {v1,v2};
assume that
A10: Sum(l) = 0.V and
A11: Carrier(l) <> {};
A12: 0.V = l.v1 * v1 + l.v2 * v2 by A8,A9,A10,RLVECT_2:33;
set x = the Element of Carrier(l);
Carrier(l) c= {v1,v2} by RLVECT_2:def 6;
then
A13: x in {v1,v2} by A11;
x in Carrier(l) by A11;
then
A14: ex u st x = u & l.u <> 0;
now
per cases by A14,A13,TARSKI:def 2;
suppose
A15: l.v1 <> 0;
0.V = (l.v1)" * (l.v1 * v1 + l.v2 * v2) by A12
.= (l.v1)" * (l.v1 * v1) + (l.v1)" * (l.v2 * v2) by RLVECT_1:def 5
.= (l.v1)" * l.v1 * v1 + (l.v1)" * (l.v2 * v2) by RLVECT_1:def 7
.= (l.v1)" * l.v1 * v1 + (l.v1)" * l.v2 * v2 by RLVECT_1:def 7
.= 1 * v1 + (l.v1)" * l.v2 * v2 by A15,XCMPLX_0:def 7
.= v1 + (l.v1)" * l.v2 * v2 by RLVECT_1:def 8;
then v1 = - ((l.v1)" * l.v2 * v2) by RLVECT_1:6
.= (- jj) * ((l.v1)" * l.v2 * v2) by RLVECT_1:16
.= ((- jj) * ((l.v1)" * l.v2)) * v2 by RLVECT_1:def 7;
hence thesis by A8;
end;
suppose
A16: l.v2 <> 0 & l.v1 = 0;
0.V = (l.v2)" * (l.v1 * v1 + l.v2 * v2) by A12
.= (l.v2)" * (l.v1 * v1) + (l.v2)" * (l.v2 * v2) by RLVECT_1:def 5
.= (l.v2)" * l.v1 * v1 + (l.v2)" * (l.v2 * v2) by RLVECT_1:def 7
.= (l.v2)" * l.v1 * v1 + (l.v2)" * l.v2 * v2 by RLVECT_1:def 7
.= (l.v2)" * l.v1 * v1 + 1 * v2 by A16,XCMPLX_0:def 7
.= 0 * v1 + v2 by A16,RLVECT_1:def 8
.= 0.V + v2 by RLVECT_1:10
.= v2;
hence thesis by A7;
end;
end;
hence thesis;
end;
theorem
v1 <> v2 & {v1,v2} is linearly-independent iff for a,b st a * v1 + b *
v2 = 0.V holds a = 0 & b = 0
proof
thus v1 <> v2 & {v1,v2} is linearly-independent implies for a,b st a * v1 +
b * v2 = 0.V holds a = 0 & b = 0
proof
assume
A1: v1 <> v2 & {v1,v2} is linearly-independent;
let a,b;
assume that
A2: a * v1 + b * v2 = 0.V and
A3: a <> 0 or b <> 0;
now
per cases by A3;
suppose
A4: a <> 0;
0.V = a" * (a * v1 + b * v2) by A2
.= a" * (a * v1) + a" * (b * v2) by RLVECT_1:def 5
.= (a" * a) * v1 + a" * (b * v2) by RLVECT_1:def 7
.= (a" * a) * v1 + (a" * b) * v2 by RLVECT_1:def 7
.= 1 * v1 + (a" * b) * v2 by A4,XCMPLX_0:def 7
.= v1 + (a" * b) * v2 by RLVECT_1:def 8;
then v1 = - ((a" * b) * v2) by RLVECT_1:6
.= (- 1) * ((a" * b) * v2) by RLVECT_1:16
.= (- 1) * (a" * b) * v2 by RLVECT_1:def 7;
hence thesis by A1,Th12;
end;
suppose
A5: b <> 0;
0.V = b" * (a * v1 + b * v2) by A2
.= b" * (a * v1) + b" * (b * v2) by RLVECT_1:def 5
.= (b" * a) * v1 + b" * (b * v2) by RLVECT_1:def 7
.= (b" * a) * v1 + (b" * b) * v2 by RLVECT_1:def 7
.= (b" * a) * v1 + 1* v2 by A5,XCMPLX_0:def 7
.= (b" * a) * v1 + v2 by RLVECT_1:def 8;
then v2 = - ((b" * a) * v1) by RLVECT_1:def 10
.= (- 1) * ((b" * a) * v1) by RLVECT_1:16
.= (- 1) * (b" * a) * v1 by RLVECT_1:def 7;
hence thesis by A1,Th12;
end;
end;
hence thesis;
end;
assume
A6: for a,b st a * v1 + b * v2 = 0.V holds a = 0 & b = 0;
A7: now
let a;
assume v1 = a * v2;
then v1 = 0.V + a * v2;
then 0.V = v1 - a * v2 by RLSUB_2:61
.= v1 + (- a * v2) by RLVECT_1:def 11
.= v1 + a * (- v2) by RLVECT_1:25
.= v1 + ((- a) * v2) by RLVECT_1:24
.= 1 * v1 + (- a) * v2 by RLVECT_1:def 8;
hence contradiction by A6;
end;
now
assume
A8: v2 = 0.V;
0.V = 0.V + 0.V
.= 0 * v1 + 0.V by RLVECT_1:10
.= 0 * v1 + 1 * v2 by A8;
hence contradiction by A6;
end;
hence thesis by A7,Th12;
end;
definition
let V;
let A;
func Lin(A) -> strict Subspace of V means
:Def2:
the carrier of it = the set of all Sum(l) ;
existence
proof
set A1 = the set of all Sum(l) ;
A1 c= the carrier of V
proof
let x be object;
assume x in A1;
then ex l 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 st v in A1 & u in A1 holds v + u in A1
proof
let v,u;
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,Th1;
hence thesis;
end;
let a be Real,v;
assume v in A1;
then consider l 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,Th2;
hence thesis;
end;
Sum(l) = 0.V by RLVECT_2:30;
then 0.V in A1;
hence thesis by A1,RLSUB_1:35;
end;
uniqueness by RLSUB_1:30;
end;
theorem Th14:
x in Lin(A) iff ex l st x = Sum(l)
proof
thus x in Lin(A) implies ex l 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) by Def2;
hence thesis;
end;
given k being Linear_Combination of A such that
A1: x = Sum(k);
x in the set of all Sum(l) by A1;
then x in the carrier of Lin(A) by Def2;
hence thesis by STRUCT_0:def 5;
end;
theorem Th15:
x in A implies x in Lin(A)
proof
deffunc F(Element of V)=In(0,REAL);
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 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 st for u st not u in T holds f.u = 0
proof
take T = {v};
let u;
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 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 Th14;
end;
Lm2:
x in (0).V iff x = 0.V
proof
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 RLSUB_1:def 3;
hence thesis by TARSKI:def 1;
end;
thus thesis by RLSUB_1:17;
end;
reserve l0 for Linear_Combination of {}(the carrier of V);
theorem
Lin({}(the carrier of V)) = (0).V
proof
set A = Lin({}(the carrier of V));
now
let 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) by Def2;
then ex l0 st v = Sum(l0) by A1;
then v = 0.V by RLVECT_2:31;
hence thesis by Lm2;
end;
assume v in (0).V;
then v = 0.V by Lm2;
hence v in A by RLSUB_1:17;
end;
hence thesis by RLSUB_1:31;
end;
theorem
Lin(A) = (0).V implies A = {} or A = {0.V}
proof
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 Th15;
then x = 0.V by A1,Lm2;
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,Th15;
hence thesis by A1,A3,Lm2;
end;
theorem Th18:
for W being strict Subspace of V holds A = the carrier of W
implies Lin(A) = W
proof
let W be strict Subspace of V;
assume
A1: A = the carrier of W;
now
let v;
thus v in Lin(A) implies v in W
proof
assume v in Lin(A);
then
A2: ex l st v = Sum(l) by Th14;
A is linearly-closed by A1,RLSUB_1:34;
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,Th15;
end;
hence thesis by RLSUB_1:31;
end;
theorem
for V being strict RealLinearSpace,A being Subset of V holds A = the
carrier of V implies Lin(A) = V
proof
let V be strict RealLinearSpace,A be Subset of V;
assume A = the carrier of V;
then A = the carrier of (Omega).V;
hence thesis by Th18;
end;
Lm3: W1 is Subspace of W3 implies W1 /\ W2 is Subspace of W3
proof
A1: W1 /\ W2 is Subspace of W1 by RLSUB_2:16;
assume W1 is Subspace of W3;
hence thesis by A1,RLSUB_1:27;
end;
Lm4: W1 is Subspace of W2 & W1 is Subspace of W3 implies W1 is Subspace of W2
/\ W3
proof
assume
A1: W1 is Subspace of W2 & W1 is Subspace of W3;
now
let v;
assume v in W1;
then v in W2 & v in W3 by A1,RLSUB_1:8;
hence v in W2 /\ W3 by RLSUB_2:3;
end;
hence thesis by RLSUB_1:29;
end;
Lm5: W1 is Subspace of W2 implies W1 is Subspace of W2 + W3
proof
A1: W2 is Subspace of W2 + W3 by RLSUB_2:7;
assume W1 is Subspace of W2;
hence thesis by A1,RLSUB_1:27;
end;
Lm6: W1 is Subspace of W3 & W2 is Subspace of W3 implies W1 + W2 is Subspace
of W3
proof
assume
A1: W1 is Subspace of W3 & W2 is Subspace of W3;
now
let v;
assume v in W1 + W2;
then consider v1,v2 such that
A2: v1 in W1 & v2 in W2 and
A3: v = v1 + v2 by RLSUB_2:1;
v1 in W3 & v2 in W3 by A1,A2,RLSUB_1:8;
hence v in W3 by A3,RLSUB_1:20;
end;
hence thesis by RLSUB_1:29;
end;
theorem Th20:
A c= B implies Lin(A) is Subspace of Lin(B)
proof
assume
A1: A c= B;
now
let v;
assume v in Lin(A);
then consider l such that
A2: v = Sum(l) by Th14;
reconsider l as Linear_Combination of B by A1,RLVECT_2:21;
Sum(l) = v by A2;
hence v in Lin(B) by Th14;
end;
hence thesis by RLSUB_1:29;
end;
theorem
for V being strict RealLinearSpace,A,B being Subset of V holds Lin(A)
= V & A c= B implies Lin(B) = V
proof
let V be strict RealLinearSpace,A,B be Subset of V;
assume Lin(A) = V & A c= B;
then V is Subspace of Lin(B) by Th20;
hence thesis by RLSUB_1:26;
end;
theorem
Lin(A \/ B) = Lin(A) + Lin(B)
proof
now
deffunc G(object)= 0;
let v;
assume v in Lin(A \/ B);
then consider l being Linear_Combination of A \/ B such that
A1: v = Sum(l) by Th14;
deffunc F(object)=l.$1;
set D = Carrier(l) \ A;
set C = Carrier(l) /\ A;
defpred P[object] means $1 in C;
defpred D[object] means $1 in D;
now
let x;
assume x in the carrier of V;
then reconsider v = x as VECTOR of V;
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 (P[x] implies F(x) in REAL) & (
not P[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 (P[x] implies f.x = F(x)) &
(not P[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 holds not u in C implies 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 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;
assume x in the carrier of V;
then reconsider v = x as VECTOR of V;
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 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 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;
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,Th1;
Sum(f) in Lin(A) & Sum(g) in Lin(B) by Th14;
hence v in Lin(A) + Lin(B) by A19,RLSUB_2:1;
end;
then
A20: Lin(A \/ B) is Subspace of Lin(A) + Lin(B) by RLSUB_1:29;
Lin(A) is Subspace of Lin(A \/ B) & Lin(B) is Subspace of Lin(A \/ B) by Th20
,XBOOLE_1:7;
then Lin(A) + Lin(B) is Subspace of Lin(A \/ B) by Lm6;
hence thesis by A20,RLSUB_1:26;
end;
theorem
Lin(A /\ B) is Subspace of Lin(A) /\ Lin(B)
proof
Lin(A /\ B) is Subspace of Lin(A) & Lin(A /\ B) is Subspace of Lin(B) by Th20
,XBOOLE_1:17;
hence thesis by Lm4;
end;
Lm7: not {} in M implies dom CF = M
proof
set x = the Element of M;
A1: x in M;
assume
A2: not {} in M;
then
A3: CF is Function of M, union M by ORDERS_1:90;
union M <> {} by A1,ORDERS_1:6,A2;
hence thesis by FUNCT_2:def 1,A3;
end;
theorem Th24:
A is linearly-independent implies ex B st A c= B & B is
linearly-independent & Lin(B) = the RLSStruct of V
proof
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 holds Z in Q iff Z in bool(the carrier of V) & P[Z] from
XFAMILY:sch 1;
A2: now
let Z;
assume that
A3: 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 such that
A6: x in X and
A7: X in Z by TARSKI:def 4;
X in bool(the carrier of V) by A1,A4,A7;
hence thesis by A6;
end;
then reconsider W as Subset of V;
A8: W is linearly-independent
proof
deffunc Q(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 = Q(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 such that
A16: x in X and
A17: X in Z by A11,A14,TARSKI:def 4;
reconsider X as Subset of V by A1,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 Lm7;
then dom F is finite by A11,FINSET_1:8;
then
A19: S is finite by FINSET_1:8;
A20: now
let X;
assume X in S;
then consider x being object such that
A21: x in dom F and
A22: F.x = X by FUNCT_1:def 3;
consider y being object such that
A23: y in dom f & f.y = x by A18,A21,FUNCT_1:def 3;
A24: x = Q(y) 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;
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
A c= B and
A27: B is linearly-independent by A1,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;
set x = the Element of Z;
x in Q by A3,A4;
then
A32: ex B being Subset of V st B = x & A c= B & B is linearly-independent
by A1;
x c= W by A3,ZFMISC_1:74;
then A c= W by A32;
hence union Z in Q by A1,A8;
end;
A33: (Omega).V = the RLSStruct of V;
assume A is linearly-independent;
then Q <> {} by A1;
then consider X such that
A34: X in Q and
A35: for Z 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 RLSStruct of V;
then consider v being VECTOR of V such that
A39: not(v in Lin(B) iff v in the RLSStruct of V) by A33,RLSUB_1:31;
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(VECTOR of V)=In(0,REAL);
deffunc L(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 = L(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,Th4;
then Sum(f) = 0.V + Sum(g) by RLSUB_2:61
.= (- l.v) * v by A50;
then
A53: (- l.v) * v in Lin(B) by Th14;
(- 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,RLSUB_1:21,RLVECT_1:1;
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,Th15,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 Th25:
Lin(A) = V implies ex B st B c= A & B is linearly-independent & Lin(B) = V
proof
assume
A1: Lin(A) = V;
defpred P[set] means (ex B st B = $1 & B c= A & B is linearly-independent);
consider Q being set such that
A2: for Z holds Z in Q iff Z in bool(the carrier of V) & P[Z] from
XFAMILY:sch 1;
A3: now
let Z;
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 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 : $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 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 : x in C & C in Z} by A16,A17;
hence contradiction by A11,A12,A14,A15;
end;
then
A18: dom F = M by Lm7;
then dom F is finite by A11,FINSET_1:8;
then
A19: S is finite by FINSET_1:8;
A20: now
let X;
assume X in S;
then consider x being object such that
A21: x in dom F and
A22: F.x = X by FUNCT_1:def 3;
consider y being object such that
A23: y in dom f & f.y = x by A18,A21,FUNCT_1:def 3;
A24: x = {C : 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 st C = X & y in C & C in Z by A24;
hence X in Z;
end;
A25: now
let X,Y;
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 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 : 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 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 such that
A32: x in X and
A33: X in Z by TARSKI:def 4;
ex B 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 Th7;
then Q <> {} by A2;
then consider X such that
A34: X in Q and
A35: for Z st Z in Q & Z <> X holds not X c= Z by A3,ORDERS_1:67;
consider B 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 st v in A holds v in Lin(B);
now
reconsider F = the carrier of Lin(B) as Subset of V by RLSUB_1:def 2;
let v;
assume v in Lin(A);
then consider l such that
A41: v = Sum(l) by Th14;
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 Th14;
hence v in Lin(B) by Th18;
end;
then Lin(A) is Subspace of Lin(B) by RLSUB_1:29;
hence contradiction by A1,A39,RLSUB_1:26;
end;
then consider 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(VECTOR of V)= In(0,REAL);
deffunc F(VECTOR of V)=l.$1;
consider f such that
A48: f.v = In(0,REAL) and
A49: for u 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;
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 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 such that
A53: g.v = - l.v and
A54: for u 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;
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 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;
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,Th4;
then Sum(f) = 0.V + Sum(g) by RLSUB_2:61
.= (- l.v) * v by A55;
then
A58: (- l.v) * v in Lin(B) by Th14;
(- 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,RLSUB_1:21;
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,Th15;
hence contradiction by A35,A36,A62,A61,XBOOLE_1:7;
end;
definition
let V be RealLinearSpace;
mode Basis of V -> Subset of V means
:Def3:
it is linearly-independent & Lin (it) = the RLSStruct of V;
existence
proof
{}(the carrier of V) is linearly-independent by Th7;
then ex B being Subset of V st {}(the carrier of V) c= B & B is
linearly-independent & Lin(B) = the RLSStruct of V by Th24;
hence thesis;
end;
end;
reserve I for Basis of V;
theorem
for V being strict RealLinearSpace,A being Subset of V holds A is
linearly-independent implies ex I being Basis of V st A c= I
proof
let V be strict RealLinearSpace,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 Th24;
reconsider B as Basis of V by A2,Def3;
take B;
thus thesis by A1;
end;
theorem
Lin(A) = V implies ex I st I c= A
proof
assume Lin(A) = V;
then consider B such that
A1: B c= A and
A2: B is linearly-independent & Lin(B) = V by Th25;
reconsider B as Basis of V by A2,Def3;
take B;
thus thesis by A1;
end;
::
:: Auxiliary theorems.
::
theorem
not {} in M implies dom CF = M by Lm7;
theorem
x in (0).V iff x = 0.V by Lm2;
theorem
W1 is Subspace of W3 implies W1 /\ W2 is Subspace of W3 by Lm3;
theorem
W1 is Subspace of W2 & W1 is Subspace of W3 implies W1 is Subspace of
W2 /\ W3 by Lm4;
theorem
W1 is Subspace of W3 & W2 is Subspace of W3 implies W1 + W2 is
Subspace of W3 by Lm6;
theorem
W1 is Subspace of W2 implies W1 is Subspace of W2 + W3 by Lm5;
theorem
f (#) (F ^ G) = (f (#) F) ^ (f (#) G) by Lm1;