:: Dimension of 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 NUMBERS, BHSP_1, FINSET_1, SUBSET_1, RLVECT_1, RLVECT_3,
XBOOLE_0, RLVECT_2, CARD_3, TARSKI, FUNCT_1, CARD_1, FINSEQ_1, STRUCT_0,
RELAT_1, VALUED_1, FINSEQ_4, ORDINAL4, ARYTM_1, ARYTM_3, XXREAL_0,
RLSUB_1, RLVECT_5, NAT_1, SUPINF_2, FUNCT_2, RLSUB_2, REAL_1, ALGSTR_0,
RUSUB_4;
notations TARSKI, XBOOLE_0, ENUMSET1, SUBSET_1, CARD_1, ORDINAL1, NUMBERS,
XCMPLX_0, XREAL_0, REAL_1, NAT_1, FINSEQ_1, FUNCT_1, FUNCT_2, DOMAIN_1,
STRUCT_0, ALGSTR_0, RLVECT_1, FINSEQ_3, FINSEQ_4, FINSET_1, RLSUB_1,
RLVECT_2, BHSP_1, RLVECT_3, RUSUB_1, RUSUB_2, RUSUB_3, XXREAL_0;
constructors XXREAL_0, REAL_1, NAT_1, PARTFUN1, FINSEQ_3, FINSEQ_4, REALSET1,
RLVECT_2, RLVECT_3, RUSUB_2, RUSUB_3, RELSET_1;
registrations SUBSET_1, RELSET_1, FINSET_1, XREAL_0, NAT_1, FINSEQ_1,
STRUCT_0, RLVECT_1, RLSUB_1, RLVECT_3, ORDINAL1, CARD_1, RLVECT_2;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
definitions TARSKI;
equalities XBOOLE_0, STRUCT_0;
expansions XBOOLE_0, TARSKI, STRUCT_0;
theorems FUNCT_1, FINSEQ_1, FINSEQ_2, FINSEQ_3, FINSEQ_4, FINSET_1, RLSUB_2,
RLVECT_1, RLVECT_2, TARSKI, XBOOLE_0, XBOOLE_1, RUSUB_1, RUSUB_2,
RLVECT_3, ENUMSET1, RLVECT_5, NAT_1, SUBSET_1, RUSUB_3, RLSUB_1, CARD_1,
CARD_2, XCMPLX_0, XCMPLX_1, XREAL_1, XXREAL_0, STRUCT_0, ZFMISC_1;
schemes NAT_1, XBOOLE_0, FINSEQ_1, DOMAIN_1;
begin :: Finite-dimensional real unitary space
theorem Th1:
for V being RealUnitarySpace, A,B being finite Subset of V, v
being VECTOR of V st v in Lin(A \/ B) & not v in Lin(B) holds ex w being VECTOR
of V st w in A & w in Lin(A \/ B \ {w} \/ {v})
proof
let V be RealUnitarySpace;
let A, B be finite Subset of V;
let v be VECTOR of V such that
A1: v in Lin(A \/ B) and
A2: not v in Lin(B);
consider L being Linear_Combination of (A \/ B) such that
A3: v = Sum(L) by A1,RUSUB_3:1;
v in {v} by TARSKI:def 1;
then v in Lin({v}) by RUSUB_3:2;
then consider Lv being Linear_Combination of {v} such that
A4: v = Sum(Lv) by RUSUB_3:1;
A5: Carrier(L) c= A \/ B by RLVECT_2:def 6;
now
assume
A6: for w being VECTOR of V st w in A holds L.w = 0;
now
let x be object;
assume that
A7: x in Carrier(L) and
A8: x in A;
ex u being VECTOR of V st x = u & L.u <> 0 by A7,RLVECT_5:3;
hence contradiction by A6,A8;
end;
then Carrier(L) misses A by XBOOLE_0:3;
then Carrier(L) c= B by A5,XBOOLE_1:73;
then L is Linear_Combination of B by RLVECT_2:def 6;
hence contradiction by A2,A3,RUSUB_3:1;
end;
then consider w being VECTOR of V such that
A9: w in A and
A10: L.w <> 0;
consider F being FinSequence of the carrier of V such that
A11: F is one-to-one and
A12: rng F = Carrier(L) and
A13: Sum(L) = Sum(L (#) F) by RLVECT_2:def 8;
A14: w in rng F by A10,A12,RLVECT_5:3;
then reconsider Fw1 = (F -| w) as FinSequence of the carrier of V by
FINSEQ_4:41;
reconsider Fw2 = (F |-- w) as FinSequence of the carrier of V by A14,
FINSEQ_4:50;
A15: rng Fw1 misses rng Fw2 by A11,A14,FINSEQ_4:57;
set Fw = Fw1 ^ Fw2;
consider K being Linear_Combination of V such that
A16: Carrier(K) = rng Fw /\ Carrier(L) and
A17: L (#) Fw = K (#) Fw by RLVECT_5:7;
F just_once_values w by A11,A14,FINSEQ_4:8;
then Fw = F - {w} by FINSEQ_4:54;
then
A18: rng Fw = Carrier(L) \ {w} by A12,FINSEQ_3:65;
then
A19: Carrier(K) = rng Fw by A16,XBOOLE_1:28,36;
then
A20: Carrier(K) c= A \/ B \ {w} by A5,A18,XBOOLE_1:33;
take w;
set a = L.w;
A21: a" <> 0 by A10,XCMPLX_1:202;
F = (F -| w) ^ <* w *> ^ (F |-- w) by A14,FINSEQ_4:51;
then F = Fw1 ^ (<* w *> ^ Fw2) by FINSEQ_1:32;
then L (#) F = (L (#) Fw1) ^ (L (#) (<* w *> ^ Fw2)) by RLVECT_3:34
.= (L (#) Fw1) ^ ((L (#) <* w *>) ^ (L (#) Fw2)) by RLVECT_3:34
.= (L (#) Fw1) ^ (L (#) <* w *>) ^ (L (#) Fw2) by FINSEQ_1:32
.= (L (#) Fw1) ^ <* a*w *> ^ (L (#) Fw2) by RLVECT_2:26;
then
A22: Sum(L (#) F) = Sum((L (#) Fw1) ^ (<* a*w *> ^ (L (#) Fw2))) by FINSEQ_1:32
.= Sum(L (#) Fw1) + Sum(<* a*w *> ^ (L (#) Fw2)) by RLVECT_1:41
.= Sum(L (#) Fw1) + (Sum(<* a*w *>) + Sum(L (#) Fw2)) by RLVECT_1:41
.= Sum(L (#) Fw1) + (Sum(L (#) Fw2) + a*w) by RLVECT_1:44
.= (Sum(L (#) Fw1) + Sum(L (#) Fw2)) + a*w by RLVECT_1:def 3
.= Sum((L (#) Fw1) ^ (L (#) Fw2)) + a*w by RLVECT_1:41
.= Sum(L (#) (Fw1 ^ Fw2)) + a*w by RLVECT_3:34;
reconsider K as Linear_Combination of (A \/ B \ {w}) by A20,RLVECT_2:def 6;
Carrier (-K + Lv) c= Carrier(-K) \/ Carrier(Lv) by RLVECT_2:37;
then
A23: Carrier (-K + Lv) c= Carrier(K) \/ Carrier(Lv) by RLVECT_2:51;
set LC = a"*(-K + Lv);
Carrier(Lv) c= {v} by RLVECT_2:def 6;
then Carrier(K) \/ Carrier(Lv) c= A \/ B \ {w} \/ {v} by A20,XBOOLE_1:13;
then Carrier (-K + Lv) c= A \/ B \ {w} \/ {v} by A23;
then Carrier (LC) c= A \/ B \ {w} \/ {v} by A21,RLVECT_2:42;
then
A24: LC is Linear_Combination of (A \/ B \ {w} \/ {v}) by RLVECT_2:def 6;
Fw1 is one-to-one & Fw2 is one-to-one by A11,A14,FINSEQ_4:52,53;
then Fw is one-to-one by A15,FINSEQ_3:91;
then Sum(K (#) Fw) = Sum(K) by A19,RLVECT_2:def 8;
then a"*v = a"*Sum(K) + a"*(a*w) by A3,A13,A22,A17,RLVECT_1:def 5
.= a"*Sum(K) + (a"*a)*w by RLVECT_1:def 7
.= a"*Sum(K) +1*w by A10,XCMPLX_0:def 7
.= a"*Sum(K) + w by RLVECT_1:def 8;
then w = a"*v - a"*Sum(K) by RLSUB_2:61
.= a"*(v - Sum(K)) by RLVECT_1:34
.= a"*(-Sum(K) + v) by RLVECT_1:def 11;
then w = a"*(Sum(-K) + Sum(Lv)) by A4,RLVECT_3:3
.= a"*Sum(-K + Lv) by RLVECT_3:1
.= Sum(a"*(-K + Lv)) by RLVECT_3:2;
hence thesis by A9,A24,RUSUB_3:1;
end;
Lm1: for X being set, x be set st x in X holds X \ {x} \/ {x} = X
proof
let X be set;
let x be set;
assume x in X;
then
A1: {x} is Subset of X by SUBSET_1:41;
{x} \/ (X \ {x}) = {x} \/ X by XBOOLE_1:39
.= X by A1,XBOOLE_1:12;
hence thesis;
end;
theorem Th2:
for V being RealUnitarySpace, A,B being finite Subset of V st the
UNITSTR of V = Lin(A) & B is linearly-independent holds card B <= card A & ex C
being finite Subset of V st C c= A & card C = card A - card B & the UNITSTR of
V = Lin(B \/ C)
proof
let V be RealUnitarySpace;
defpred P[Nat] means for n being Element of NAT for A, B being
finite Subset of V st card(A) = n & card(B) = $1 & the UNITSTR of V = Lin(A) &
B is linearly-independent holds $1 <= n & ex C being finite Subset of V st C c=
A & card(C) = n - $1 & the UNITSTR of V = Lin(B \/ C);
A1: for m being Nat st P[m] holds P[m + 1]
proof
let m be Nat such that
A2: P[m];
let n be Element of NAT;
let A, B be finite Subset of V such that
A3: card(A) = n and
A4: card(B) = m + 1 and
A5: the UNITSTR of V = Lin(A) and
A6: B is linearly-independent;
consider v being object such that
A7: v in B by A4,CARD_1:27,XBOOLE_0:def 1;
reconsider v as VECTOR of V by A7;
set Bv = B \ {v};
A8: Bv is linearly-independent by A6,RLVECT_3:5,XBOOLE_1:36;
{v} is Subset of B by A7,SUBSET_1:41;
then
A9: card(B \ {v}) = card(B) - card({v}) by CARD_2:44
.= m + 1 - 1 by A4,CARD_1:30
.= m;
then consider C being finite Subset of V such that
A10: C c= A and
A11: card(C) = n - m and
A12: the UNITSTR of V = Lin(Bv \/ C) by A2,A3,A5,A8;
A13: not v in Lin(Bv) by A6,A7,RUSUB_3:25;
A14: now
assume m = n;
then consider C being finite Subset of V such that
C c= A and
A15: card(C) = m - m and
A16: the UNITSTR of V = Lin(Bv \/ C) by A2,A3,A5,A9,A8;
C = {} by A15;
then Bv is Basis of V by A8,A16,RUSUB_3:def 2;
hence contradiction by A13,RUSUB_3:21;
end;
v in Lin(Bv \/ C) by A12;
then consider w being VECTOR of V such that
A17: w in C and
A18: w in Lin(C \/ Bv \ {w} \/ {v}) by A13,Th1;
set Cw = C \ {w};
(Bv \ {w}) \/ {v} c= Bv \/ {v} by XBOOLE_1:9,36;
then Cw \/ ((Bv \ {w}) \/ {v}) c= Cw \/ (Bv \/ {v}) by XBOOLE_1:9;
then
A19: Cw \/ ((Bv \ {w}) \/ {v}) c= B \/ Cw by A7,Lm1;
{w} is Subset of C by A17,SUBSET_1:41;
then
A20: card(Cw) = card(C) - card({w}) by CARD_2:44
.= n - m - 1 by A11,CARD_1:30
.= n - (m + 1);
Cw c= C by XBOOLE_1:36;
then
A21: Cw c= A by A10;
C \/ Bv \ {w} \/ {v} = (Cw \/ (Bv \ {w})) \/ {v} by XBOOLE_1:42
.= Cw \/ ((Bv \ {w}) \/ {v}) by XBOOLE_1:4;
then Lin(C \/ Bv \ {w} \/ {v}) is Subspace of Lin(B \/ Cw) by A19,RUSUB_3:7
;
then
A22: w in Lin(B \/ Cw) by A18,RUSUB_1:1;
A23: Bv c= B & C = Cw \/ {w} by A17,Lm1,XBOOLE_1:36;
now
let x be object;
assume x in Bv \/ C;
then x in Bv or x in C by XBOOLE_0:def 3;
then x in B or x in Cw or x in {w} by A23,XBOOLE_0:def 3;
then x in B \/ Cw or x in {w} by XBOOLE_0:def 3;
then x in Lin(B \/ Cw) or x = w by RUSUB_3:2,TARSKI:def 1;
hence x in the carrier of Lin(B \/ Cw) by A22;
end;
then Bv \/ C c= the carrier of Lin(B \/ Cw);
then Lin(Bv \/ C) is Subspace of Lin(B \/ Cw) by RUSUB_3:27;
then
A24: the carrier of Lin(Bv \/ C) c= the carrier of Lin(B \/ Cw) by
RUSUB_1:def 1;
the carrier of Lin(B \/ Cw) c= the carrier of V by RUSUB_1:def 1;
then the carrier of Lin(B \/ Cw) = the carrier of V by A12,A24;
then
A25: the UNITSTR of V = Lin(B \/ Cw) by A12,RUSUB_1:24;
m <= n by A2,A3,A5,A9,A8;
then m < n by A14,XXREAL_0:1;
hence thesis by A21,A20,A25,NAT_1:13;
end;
A26: P[0]
proof
let n be Element of NAT;
let A, B be finite Subset of V such that
A27: card(A) = n and
A28: card(B) = 0 and
A29: the UNITSTR of V = Lin(A) and
B is linearly-independent;
B = {} by A28;
then A = B \/ A;
hence thesis by A27,A29;
end;
A30: for m being Nat holds P[m] from NAT_1:sch 2(A26, A1);
let A, B be finite Subset of V;
assume the UNITSTR of V = Lin(A) & B is linearly-independent;
hence thesis by A30;
end;
definition
let V be RealUnitarySpace;
attr V is finite-dimensional means
:Def1:
ex A being finite Subset of V st A is Basis of V;
end;
registration
cluster strict finite-dimensional for RealUnitarySpace;
existence
proof
set V = the RealUnitarySpace;
take (0).V;
thus (0).V is strict;
take A = {}( the carrier of (0).V );
Lin(A) = (0).(0).V by RUSUB_3:3;
then A is linearly-independent & Lin(A) = the UNITSTR of (0).V by
RLVECT_3:7,RUSUB_1:30;
hence thesis by RUSUB_3:def 2;
end;
end;
theorem Th3:
for V being RealUnitarySpace st V is finite-dimensional holds for
I being Basis of V holds I is finite
proof
let V be RealUnitarySpace;
assume V is finite-dimensional;
then consider A being finite Subset of V such that
A1: A is Basis of V;
let B be Basis of V;
consider p being FinSequence such that
A2: rng p = A by FINSEQ_1:52;
reconsider p as FinSequence of the carrier of V by A2,FINSEQ_1:def 4;
set Car = {Carrier(L) where L is Linear_Combination of B: ex i being Element
of NAT st i in dom p & Sum(L) = p.i};
set C = union Car;
A3: C c= B
proof
let x be object;
assume x in C;
then consider R being set such that
A4: x in R and
A5: R in Car by TARSKI:def 4;
ex L being Linear_Combination of B st R = Carrier(L) & ex i being
Element of NAT st i in dom p & Sum(L) = p.i by A5;
then R c= B by RLVECT_2:def 6;
hence thesis by A4;
end;
then reconsider C as Subset of V by XBOOLE_1:1;
for v being VECTOR of V holds v in (Omega).V iff v in Lin(C)
proof
let v be VECTOR of V;
hereby
assume v in (Omega).V;
v in the UNITSTR of V;
then v in Lin(A) by A1,RUSUB_3:def 2;
then consider LA being Linear_Combination of A such that
A6: v = Sum(LA) by RUSUB_3:1;
Carrier(LA) c= the carrier of Lin(C)
proof
let w be object;
assume
A7: w in Carrier(LA);
then reconsider w9= w as VECTOR of V;
w9 in Lin(B) by RUSUB_3:21;
then consider LB being Linear_Combination of B such that
A8: w = Sum(LB) by RUSUB_3:1;
Carrier(LA) c= A by RLVECT_2:def 6;
then ex i being object st i in dom p & w = p.i by A2,A7,FUNCT_1:def 3;
then
A9: Carrier(LB) in Car by A8;
Carrier(LB) c= C
by A9,TARSKI:def 4;
then LB is Linear_Combination of C by RLVECT_2:def 6;
then w in Lin(C) by A8,RUSUB_3:1;
hence thesis;
end;
then ex LC being Linear_Combination of C st Sum(LA) = Sum(LC) by
RUSUB_3:17;
hence v in Lin(C) by A6,RUSUB_3:1;
end;
assume v in Lin(C);
v in the carrier of the UNITSTR of V;
then v in the carrier of (Omega).V by RUSUB_1:def 3;
hence thesis;
end;
then (Omega).V = Lin(C) by RUSUB_1:25;
then
A10: the UNITSTR of V = Lin(C) by RUSUB_1:def 3;
A11: B is linearly-independent by RUSUB_3:def 2;
then C is linearly-independent by A3,RLVECT_3:5;
then
A12: C is Basis of V by A10,RUSUB_3:def 2;
B c= C
proof
set D = B \ C;
assume not B c= C;
then ex v being object st v in B & not v in C;
then reconsider D as non empty Subset of V by XBOOLE_0:def 5;
reconsider B as Subset of V;
C \/ (B \ C) = C \/ B by XBOOLE_1:39
.= B by A3,XBOOLE_1:12;
then B = C \/ D;
hence contradiction by A11,A12,RUSUB_3:26,XBOOLE_1:79;
end;
then
A13: B = C by A3;
defpred P[set, object] means
ex L being Linear_Combination of B st $2 = Carrier
(L) & Sum(L) = p.$1;
A14: for i being Nat st i in Seg len p ex x being object st P[i, x]
proof
let i be Nat;
assume i in Seg len p;
then i in dom p by FINSEQ_1:def 3;
then p.i in the carrier of V by FINSEQ_2:11;
then p.i in Lin(B) by RUSUB_3:21;
then consider L being Linear_Combination of B such that
A15: p.i = Sum(L) by RUSUB_3:1;
P[i, Carrier(L)] by A15;
hence thesis;
end;
ex q being FinSequence st dom q = Seg len p & for i being Nat st i in
Seg len p holds P[i, q.i] from FINSEQ_1:sch 1(A14);
then consider q being FinSequence such that
A16: dom q = Seg len p and
A17: for i being Nat st i in Seg len p holds P[i, q.i];
A18: dom p = dom q by A16,FINSEQ_1:def 3;
A19: for i being Nat, y1,y2 being set st i in Seg len p & P[i, y1] & P[i, y2
] holds y1 = y2
proof
let i be Nat;
let y1,y2 be set;
assume that
i in Seg len p and
A20: P[i, y1] and
A21: P[i, y2];
consider L1 being Linear_Combination of B such that
A22: y1 = Carrier(L1) & Sum(L1) = p.i by A20;
consider L2 being Linear_Combination of B such that
A23: y2 = Carrier(L2) & Sum(L2) = p.i by A21;
Carrier(L1) c= B & Carrier(L2) c= B by RLVECT_2:def 6;
hence thesis by A11,A22,A23,RLVECT_5:1;
end;
now
let x be object;
assume x in Car;
then consider L being Linear_Combination of B such that
A24: x = Carrier(L) and
A25: ex i being Element of NAT st i in dom p & Sum(L) = p.i;
consider i being Element of NAT such that
A26: i in dom p and
A27: Sum(L) = p.i by A25;
P[i, q.i] by A16,A17,A18,A26;
then x = q.i by A19,A16,A18,A24,A26,A27;
hence x in rng q by A18,A26,FUNCT_1:def 3;
end;
then
A28: Car c= rng q;
for R being set st R in Car holds R is finite
proof
let R be set;
assume R in Car;
then ex L being Linear_Combination of B st R = Carrier(L) & ex i being
Element of NAT st i in dom p & Sum(L) = p.i;
hence thesis;
end;
hence thesis by A13,A28,FINSET_1:7;
end;
theorem
for V being RealUnitarySpace, A being Subset of V st V is
finite-dimensional & A is linearly-independent holds A is finite
proof
let V be RealUnitarySpace;
let A be Subset of V;
assume that
A1: V is finite-dimensional and
A2: A is linearly-independent;
consider B being Basis of V such that
A3: A c= B by A2,RUSUB_3:15;
B is finite by A1,Th3;
hence thesis by A3;
end;
theorem Th5:
for V being RealUnitarySpace, A,B being Basis of V st V is
finite-dimensional holds card A = card B
proof
let V be RealUnitarySpace;
let A, B be Basis of V;
assume V is finite-dimensional;
then reconsider A9= A, B9= B as finite Subset of V by Th3;
the UNITSTR of V = Lin(B) & A9 is linearly-independent by RUSUB_3:def 2;
then
A1: card A9 <= card B9 by Th2;
the UNITSTR of V = Lin(A) & B9 is linearly-independent by RUSUB_3:def 2;
then card B9 <= card A9 by Th2;
hence thesis by A1,XXREAL_0:1;
end;
theorem Th6:
for V being RealUnitarySpace holds (0).V is finite-dimensional
proof
let V be RealUnitarySpace;
reconsider V9= (0).V as strict RealUnitarySpace;
reconsider I = {}(the carrier of V9) as finite Subset of V9;
the carrier of V9 = {0.V} by RUSUB_1:def 2
.= {0.V9} by RUSUB_1:4
.= the carrier of (0).V9 by RUSUB_1:def 2;
then
A1: V9 = (0).V9 by RUSUB_1:26;
I is linearly-independent & Lin(I) = (0).V9 by RLVECT_3:7,RUSUB_3:3;
then I is Basis of V9 by A1,RUSUB_3:def 2;
hence thesis;
end;
theorem Th7:
for V being RealUnitarySpace, W being Subspace of V st V is
finite-dimensional holds W is finite-dimensional
proof
let V be RealUnitarySpace;
let W be Subspace of V;
set A = the Basis of W;
consider I being Basis of V such that
A1: A c= I by RUSUB_3:24;
assume V is finite-dimensional;
then I is finite by Th3;
hence thesis by A1;
end;
registration
let V be RealUnitarySpace;
cluster finite-dimensional strict for Subspace of V;
existence
proof
take (0).V;
thus thesis by Th6;
end;
end;
registration
let V be finite-dimensional RealUnitarySpace;
cluster -> finite-dimensional for Subspace of V;
correctness by Th7;
end;
registration
let V be finite-dimensional RealUnitarySpace;
cluster strict for Subspace of V;
existence
proof
(0).V is strict finite-dimensional Subspace of V;
hence thesis;
end;
end;
begin :: Dimension of real unitary space
definition
let V be RealUnitarySpace;
assume
A1: V is finite-dimensional;
func dim V -> Element of NAT means
:Def2:
for I being Basis of V holds it = card I;
existence
proof
consider A being finite Subset of V such that
A2: A is Basis of V by A1;
consider n being Element of NAT such that
A3: n = card A;
for I being Basis of V holds card I = n by A1,A2,A3,Th5;
hence thesis;
end;
uniqueness
proof
let n, m be Element of NAT;
assume that
A4: for I being Basis of V holds card I = n and
A5: for I being Basis of V holds card I = m;
consider A being finite Subset of V such that
A6: A is Basis of V by A1;
card A = n by A4,A6;
hence thesis by A5,A6;
end;
end;
theorem Th8:
for V being finite-dimensional RealUnitarySpace, W being Subspace
of V holds dim W <= dim V
proof
let V be finite-dimensional RealUnitarySpace;
let W be Subspace of V;
set A = the Basis of W;
reconsider A as Subset of W;
A is linearly-independent by RUSUB_3:def 2;
then reconsider B=A as linearly-independent Subset of V by RUSUB_3:22;
reconsider A9= B as finite Subset of V by Th3;
reconsider V9= V as RealUnitarySpace;
set I = the Basis of V9;
A1: Lin(I) = the UNITSTR of V9 by RUSUB_3:def 2;
reconsider I as finite Subset of V by Th3;
A2: dim V = card I by Def2;
card A9 <= card I by A1,Th2;
hence thesis by A2,Def2;
end;
theorem Th9:
for V being finite-dimensional RealUnitarySpace, A being Subset
of V st A is linearly-independent holds card A = dim Lin(A)
proof
let V be finite-dimensional RealUnitarySpace;
let A be Subset of V such that
A1: A is linearly-independent;
set W = Lin(A);
for x being object st x in A holds x in the carrier of W
by STRUCT_0:def 5,RUSUB_3:2;
then reconsider B = A as linearly-independent Subset of W by A1,RUSUB_3:23
,TARSKI:def 3;
W = Lin(B) by RUSUB_3:28;
then reconsider B as Basis of W by RUSUB_3:def 2;
card B = dim W by Def2;
hence thesis;
end;
theorem Th10:
for V being finite-dimensional RealUnitarySpace holds dim V = dim (Omega).V
proof
let V be finite-dimensional RealUnitarySpace;
consider I being finite Subset of V such that
A1: I is Basis of V by Def1;
A2: (Omega).V = the UNITSTR of V by RUSUB_1:def 3
.= Lin(I) by A1,RUSUB_3:def 2;
card I = dim V & I is linearly-independent by A1,Def2,RUSUB_3:def 2;
hence thesis by A2,Th9;
end;
theorem
for V being finite-dimensional RealUnitarySpace, W being Subspace of V
holds dim V = dim W iff (Omega).V = (Omega).W
proof
let V be finite-dimensional RealUnitarySpace;
let W be Subspace of V;
consider A being finite Subset of V such that
A1: A is Basis of V by Def1;
hereby
set A = the Basis of W;
consider B being Basis of V such that
A2: A c= B by RUSUB_3:24;
the carrier of W c= the carrier of V by RUSUB_1:def 1;
then reconsider A9= A as finite Subset of V by Th3,XBOOLE_1:1;
reconsider B9= B as finite Subset of V by Th3;
assume dim V = dim W;
then
A3: card A = dim V by Def2
.= card B by Def2;
A4: now
assume A <> B;
then A c< B by A2;
then card A9 < card B9 by CARD_2:48;
hence contradiction by A3;
end;
reconsider B as Subset of V;
reconsider A as Subset of W;
(Omega).V = the UNITSTR of V by RUSUB_1:def 3
.= Lin(B) by RUSUB_3:def 2
.= Lin(A) by A4,RUSUB_3:28
.= the UNITSTR of W by RUSUB_3:def 2
.= (Omega).W by RUSUB_1:def 3;
hence (Omega).V = (Omega).W;
end;
consider B being finite Subset of W such that
A5: B is Basis of W by Def1;
A6: A is linearly-independent by A1,RUSUB_3:def 2;
assume (Omega).V = (Omega).W;
then the UNITSTR of V = (Omega).W by RUSUB_1:def 3
.= the UNITSTR of W by RUSUB_1:def 3;
then
A7: Lin(A) = the UNITSTR of W by A1,RUSUB_3:def 2
.= Lin(B) by A5,RUSUB_3:def 2;
A8: B is linearly-independent by A5,RUSUB_3:def 2;
reconsider B as Subset of W;
reconsider A as Subset of V;
dim V = card A by A1,Def2
.= dim Lin(B) by A6,A7,Th9
.= card B by A8,Th9
.= dim W by A5,Def2;
hence thesis;
end;
theorem Th12:
for V being finite-dimensional RealUnitarySpace holds dim V = 0
iff (Omega).V = (0).V
proof
let V be finite-dimensional RealUnitarySpace;
consider I being finite Subset of V such that
A1: I is Basis of V by Def1;
hereby
consider I being finite Subset of V such that
A2: I is Basis of V by Def1;
assume dim V = 0;
then card I = 0 by A2,Def2;
then
A3: I = {}(the carrier of V);
(Omega).V = the UNITSTR of V by RUSUB_1:def 3
.= Lin(I) by A2,RUSUB_3:def 2
.= (0).V by A3,RUSUB_3:3;
hence (Omega).V = (0).V;
end;
A4: I <> {0.V} by A1,RUSUB_3:def 2,RLVECT_3:8;
assume (Omega).V = (0).V;
then the UNITSTR of V = (0).V by RUSUB_1:def 3;
then Lin(I) = (0).V by A1,RUSUB_3:def 2;
then I = {} or I = {0.V} by RUSUB_3:4;
hence thesis by A1,A4,Def2,CARD_1:27;
end;
theorem
for V being finite-dimensional RealUnitarySpace holds dim V = 1 iff ex
v being VECTOR of V st v <> 0.V & (Omega).V = Lin{v}
proof
let V be finite-dimensional RealUnitarySpace;
hereby
consider I being finite Subset of V such that
A1: I is Basis of V by Def1;
assume dim V = 1;
then card I = 1 by A1,Def2;
then consider v being object such that
A2: I = {v} by CARD_2:42;
v in I by A2,TARSKI:def 1;
then reconsider v as VECTOR of V;
{v} is linearly-independent by A1,A2,RUSUB_3:def 2;
then
A3: v <> 0.V by RLVECT_3:8;
Lin{v} = the UNITSTR of V by A1,A2,RUSUB_3:def 2;
hence ex v being VECTOR of V st v <> 0.V & (Omega).V = Lin{v} by A3,
RUSUB_1:def 3;
end;
given v being VECTOR of V such that
A4: v <> 0.V & (Omega).V = Lin{v};
{v} is linearly-independent & Lin{v} = the UNITSTR of V by A4,RLVECT_3:8
,RUSUB_1:def 3;
then
A5: {v} is Basis of V by RUSUB_3:def 2;
card {v} = 1 by CARD_1:30;
hence thesis by A5,Def2;
end;
theorem
for V being finite-dimensional RealUnitarySpace holds dim V = 2 iff ex
u,v being VECTOR of V st u <> v & {u, v} is linearly-independent & (Omega).V =
Lin{u, v}
proof
let V be finite-dimensional RealUnitarySpace;
hereby
consider I being finite Subset of V such that
A1: I is Basis of V by Def1;
assume dim V = 2;
then
A2: card I = 2 by A1,Def2;
then consider u being object such that
A3: u in I by CARD_1:27,XBOOLE_0:def 1;
reconsider u as VECTOR of V by A3;
now
assume I c= {u};
then card I <= card {u} by NAT_1:43;
then 2 <= 1 by A2,CARD_1:30;
hence contradiction;
end;
then consider v being object such that
A4: v in I and
A5: not v in {u};
reconsider v as VECTOR of V by A4;
A6: v <> u by A5,TARSKI:def 1;
A7: now
assume not I c= {u, v};
then consider w being object such that
A8: w in I and
A9: not w in {u, v};
for x being object st x in {u,v,w} holds x in I
by A3,A4,A8,ENUMSET1:def 1;
then {u, v, w} c= I;
then
A10: card {u, v, w} <= card I by NAT_1:43;
w <> u & w <> v by A9,TARSKI:def 2;
then 3 <= 2 by A2,A6,A10,CARD_2:58;
hence contradiction;
end;
for x being object st x in {u,v} holds x in I by A3,A4,TARSKI:def 2;
then {u, v} c= I;
then
A11: I = {u, v} by A7;
then
A12: {u, v} is linearly-independent by A1,RUSUB_3:def 2;
Lin{u, v} = the UNITSTR of V by A1,A11,RUSUB_3:def 2
.= (Omega).V by RUSUB_1:def 3;
hence ex u,v being VECTOR of V st u <> v & {u,v} is linearly-independent &
(Omega).V = Lin{u, v} by A6,A12;
end;
given u,v being VECTOR of V such that
A13: u <> v and
A14: {u, v} is linearly-independent and
A15: (Omega).V = Lin{u, v};
Lin{u, v} = the UNITSTR of V by A15,RUSUB_1:def 3;
then
A16: {u, v} is Basis of V by A14,RUSUB_3:def 2;
card {u, v} = 2 by A13,CARD_2:57;
hence thesis by A16,Def2;
end;
theorem Th15:
for V being finite-dimensional RealUnitarySpace, W1,W2 being
Subspace of V holds dim(W1 + W2) + dim(W1 /\ W2) = dim W1 + dim W2
proof
let V be finite-dimensional RealUnitarySpace;
let W1,W2 be Subspace of V;
reconsider V as RealUnitarySpace;
reconsider W1, W2 as Subspace of V;
consider I being finite Subset of W1 /\ W2 such that
A1: I is Basis of W1 /\ W2 by Def1;
W1 /\ W2 is Subspace of W2 by RUSUB_2:16;
then consider I2 being Basis of W2 such that
A2: I c= I2 by A1,RUSUB_3:24;
W1 /\ W2 is Subspace of W1 by RUSUB_2:16;
then consider I1 being Basis of W1 such that
A3: I c= I1 by A1,RUSUB_3:24;
reconsider I2 as finite Subset of W2 by Th3;
reconsider I1 as finite Subset of W1 by Th3;
A4: now
I1 is linearly-independent by RUSUB_3:def 2;
then reconsider I19 = I1 as linearly-independent Subset of V by RUSUB_3:22;
the carrier of W1 /\ W2 c= the carrier of V by RUSUB_1:def 1;
then reconsider I9= I as Subset of V by XBOOLE_1:1;
assume not I1 /\ I2 c= I;
then consider x being object such that
A5: x in I1 /\ I2 and
A6: not x in I;
x in I1 by A5,XBOOLE_0:def 4;
then x in Lin(I1) by RUSUB_3:2;
then x in the UNITSTR of W1 by RUSUB_3:def 2;
then
A7: x in the carrier of W1;
A8: the carrier of W1 c= the carrier of V by RUSUB_1:def 1;
then reconsider x9= x as VECTOR of V by A7;
now
let y be object;
the carrier of W1 /\ W2 c= the carrier of V by RUSUB_1:def 1;
then
A9: I c= the carrier of V;
assume y in I \/ {x};
then y in I or y in {x} by XBOOLE_0:def 3;
then y in the carrier of V or y = x by A9,TARSKI:def 1;
hence y in the carrier of V by A7,A8;
end;
then reconsider Ix = I \/ {x} as Subset of V by TARSKI:def 3;
now
let y be object;
assume y in I \/ {x};
then y in I or y in {x} by XBOOLE_0:def 3;
then y in I1 or y = x by A3,TARSKI:def 1;
hence y in I19 by A5,XBOOLE_0:def 4;
end;
then
A10: Ix c= I19;
x in {x} by TARSKI:def 1;
then
A11: x9 in Ix by XBOOLE_0:def 3;
x in I2 by A5,XBOOLE_0:def 4;
then x in Lin(I2) by RUSUB_3:2;
then x in the UNITSTR of W2 by RUSUB_3:def 2;
then x in the carrier of W2;
then x in (the carrier of W1) /\ (the carrier of W2) by A7,XBOOLE_0:def 4;
then x in the carrier of W1 /\ W2 by RUSUB_2:def 2;
then x in the UNITSTR of W1 /\ W2;
then
A12: x in Lin(I) by A1,RUSUB_3:def 2;
Ix \ {x} = I \ {x} by XBOOLE_1:40
.= I by A6,ZFMISC_1:57;
then not x9 in Lin(I9) by A10,A11,RLVECT_3:5,RUSUB_3:25;
hence contradiction by A12,RUSUB_3:28;
end;
set A = I1 \/ I2;
now
let v be object;
A13: the carrier of W1 c= the carrier of V & the carrier of W2 c= the
carrier of V by RUSUB_1:def 1;
assume v in A;
then
A14: v in I1 or v in I2 by XBOOLE_0:def 3;
then v in the carrier of W1 or v in the carrier of W2;
then reconsider v9= v as VECTOR of V by A13;
v9 in W1 or v9 in W2 by A14;
then v9 in W1 + W2 by RUSUB_2:2;
hence v in the carrier of W1 + W2;
end;
then reconsider A as finite Subset of W1 + W2 by TARSKI:def 3;
I c= I1 /\ I2 by A3,A2,XBOOLE_1:19;
then I = I1 /\ I2 by A4;
then
A15: card A = card I1 + card I2 - card I by CARD_2:45;
for L being Linear_Combination of A st Sum(L) = 0.(W1 + W2) holds
Carrier(L) = {}
proof
W1 is Subspace of W1 + W2 & I1 is linearly-independent by RUSUB_2:7
,RUSUB_3:def 2;
then reconsider I19 = I1 as linearly-independent Subset of W1 + W2 by
RUSUB_3:22;
reconsider W29= W2 as Subspace of W1 + W2 by RUSUB_2:7;
reconsider W19= W1 as Subspace of W1 + W2 by RUSUB_2:7;
let L be Linear_Combination of A;
assume
A16: Sum(L) = 0.(W1 + W2);
A17: I1 misses (Carrier(L) \ I1) by XBOOLE_1:79;
set B = Carrier(L) /\ I1;
consider F being FinSequence of the carrier of W1 + W2 such that
A18: F is one-to-one and
A19: rng F = Carrier(L) and
A20: Sum(L) = Sum(L (#) F) by RLVECT_2:def 8;
reconsider B as Subset of rng F by A19,XBOOLE_1:17;
reconsider F1 = F - B`, F2 = F - B as FinSequence of the carrier of W1 +
W2 by FINSEQ_3:86;
consider L1 being Linear_Combination of W1 + W2 such that
A21: Carrier(L1) = rng F1 /\ Carrier(L) and
A22: L1 (#) F1 = L (#) F1 by RLVECT_5:7;
F1 is one-to-one by A18,FINSEQ_3:87;
then
A23: Sum(L (#) F1) = Sum(L1) by A21,A22,RLVECT_5:6,XBOOLE_1:17;
rng F c= rng F;
then reconsider X = rng F as Subset of rng F;
consider L2 being Linear_Combination of W1 + W2 such that
A24: Carrier(L2) = rng F2 /\ Carrier(L) and
A25: L2 (#) F2 = L (#) F2 by RLVECT_5:7;
F2 is one-to-one by A18,FINSEQ_3:87;
then
A26: Sum(L (#) F2) = Sum(L2) by A24,A25,RLVECT_5:6,XBOOLE_1:17;
X \ B` = X /\ B`` by SUBSET_1:13
.= B by XBOOLE_1:28;
then rng F1 = B by FINSEQ_3:65;
then
A27: Carrier(L1) = I1 /\ (Carrier(L) /\ Carrier(L)) by A21,XBOOLE_1:16
.= Carrier(L) /\ I1;
then consider K1 being Linear_Combination of W19 such that
Carrier(K1) = Carrier(L1) and
A28: Sum(K1) = Sum(L1) by RUSUB_3:20;
rng F2 = Carrier(L) \ (Carrier(L) /\ I1) by A19,FINSEQ_3:65
.= Carrier(L) \ I1 by XBOOLE_1:47;
then
A29: Carrier(L2) = Carrier(L) \ I1 by A24,XBOOLE_1:28,36;
then Carrier(L1) /\ Carrier(L2) = Carrier(L) /\ (I1 /\ (Carrier(L) \ I1))
by A27,XBOOLE_1:16
.= Carrier(L) /\ {} by A17
.= {};
then
A30: Carrier(L1) misses Carrier(L2);
A31: Carrier(L) c= I1 \/ I2 by RLVECT_2:def 6;
then
A32: Carrier(L2) c= I2 by A29,XBOOLE_1:43;
Carrier(L2) c= I2 by A31,A29,XBOOLE_1:43;
then consider K2 being Linear_Combination of W29 such that
Carrier(K2) = Carrier(L2) and
A33: Sum(K2) = Sum(L2) by RUSUB_3:20,XBOOLE_1:1;
A34: Sum(K1) in W1;
ex P being Permutation of dom F st (F - B`) ^ (F - B) = F* P by
FINSEQ_3:115;
then
A35: 0.(W1 + W2) = Sum(L (#) (F1^F2)) by A16,A20,RLVECT_5:4
.= Sum((L (#) F1) ^ (L (#) F2)) by RLVECT_3:34
.= Sum(L1) + Sum(L2) by A23,A26,RLVECT_1:41;
then Sum(L1) = - Sum(L2) by RLVECT_1:def 10
.= - Sum(K2) by A33,RUSUB_1:9;
then Sum(K1) in W2 by A28;
then Sum(K1) in W1 /\ W2 by A34,RUSUB_2:3;
then Sum(K1) in Lin(I) by A1,RUSUB_3:def 2;
then consider KI being Linear_Combination of I such that
A36: Sum(K1) = Sum(KI) by RUSUB_3:1;
A37: Carrier(L) = Carrier(L1) \/ Carrier(L2) by A27,A29,XBOOLE_1:51;
A38: now
assume not Carrier(L) c= Carrier(L1 + L2);
then consider x being object such that
A39: x in Carrier(L) and
A40: not x in Carrier(L1 + L2);
reconsider x as VECTOR of W1 + W2 by A39;
A41: 0 = (L1 + L2).x by A40,RLVECT_2:19
.= L1.x + L2.x by RLVECT_2:def 10;
per cases by A37,A39,XBOOLE_0:def 3;
suppose
A42: x in Carrier(L1);
then not x in Carrier(L2) by A30,XBOOLE_0:3;
then
A43: L2.x = 0 by RLVECT_2:19;
ex v being VECTOR of W1 + W2 st x = v & L1.v <> 0 by A42,RLVECT_5:3;
hence contradiction by A41,A43;
end;
suppose
A44: x in Carrier(L2);
then not x in Carrier(L1) by A30,XBOOLE_0:3;
then
A45: L1.x = 0 by RLVECT_2:19;
ex v being VECTOR of W1 + W2 st x = v & L2.v <> 0 by A44,RLVECT_5:3;
hence contradiction by A41,A45;
end;
end;
A46: I \/ I2 = I2 by A2,XBOOLE_1:12;
A47: I2 is linearly-independent by RUSUB_3:def 2;
A48: Carrier(L1) c= I1 by A27,XBOOLE_1:17;
W1 /\ W2 is Subspace of W1 + W2 by RUSUB_2:22;
then consider LI being Linear_Combination of W1 + W2 such that
A49: Carrier(LI) = Carrier(KI) and
A50: Sum(LI) = Sum(KI) by RUSUB_3:19;
Carrier(LI) c= I by A49,RLVECT_2:def 6;
then Carrier(LI) c= I19 by A3;
then
A51: LI = L1 by A48,A28,A36,A50,RLVECT_5:1;
Carrier(LI) c= I by A49,RLVECT_2:def 6;
then Carrier(LI + L2) c= Carrier(LI) \/ Carrier(L2) & Carrier(LI) \/
Carrier(L2) c= I2 by A46,A32,RLVECT_2:37,XBOOLE_1:13;
then
A52: Carrier(LI + L2) c= I2;
W2 is Subspace of W1 + W2 by RUSUB_2:7;
then consider K being Linear_Combination of W2 such that
A53: Carrier(K) = Carrier(LI + L2) and
A54: Sum(K) = Sum(LI + L2) by A52,RUSUB_3:20,XBOOLE_1:1;
reconsider K as Linear_Combination of I2 by A52,A53,RLVECT_2:def 6;
0.W2 = Sum(LI) + Sum(L2) by A28,A35,A36,A50,RUSUB_1:5
.= Sum(K) by A54,RLVECT_3:1;
then {} = Carrier(L1 + L2) by A53,A51,A47,RLVECT_3:def 1;
hence thesis by A38;
end;
then
A55: A is linearly-independent by RLVECT_3:def 1;
the carrier of W1 + W2 c= the carrier of V by RUSUB_1:def 1;
then reconsider A9= A as Subset of V by XBOOLE_1:1;
A56: card I2 = dim W2 by Def2;
now
let x be object;
assume x in the carrier of W1 + W2;
then x in W1 + W2;
then consider w1, w2 being VECTOR of V such that
A57: w1 in W1 and
A58: w2 in W2 and
A59: x = w1 + w2 by RUSUB_2:1;
reconsider w1 as VECTOR of W1 by A57;
w1 in Lin(I1) by RUSUB_3:21;
then consider K1 being Linear_Combination of I1 such that
A60: w1 = Sum(K1) by RUSUB_3:1;
reconsider w2 as VECTOR of W2 by A58;
w2 in Lin(I2) by RUSUB_3:21;
then consider K2 being Linear_Combination of I2 such that
A61: w2 = Sum(K2) by RUSUB_3:1;
consider L2 being Linear_Combination of V such that
A62: Carrier(L2) = Carrier(K2) and
A63: Sum(L2) = Sum(K2) by RUSUB_3:19;
A64: Carrier(L2) c= I2 by A62,RLVECT_2:def 6;
consider L1 being Linear_Combination of V such that
A65: Carrier(L1) = Carrier(K1) and
A66: Sum(L1) = Sum(K1) by RUSUB_3:19;
set L = L1 + L2;
Carrier(L1) c= I1 by A65,RLVECT_2:def 6;
then
Carrier(L) c= Carrier(L1) \/ Carrier(L2) & Carrier(L1) \/ Carrier(L2)
c= I1 \/ I2 by A64,RLVECT_2:37,XBOOLE_1:13;
then Carrier(L) c= I1 \/ I2;
then reconsider L as Linear_Combination of A9 by RLVECT_2:def 6;
x = Sum(L) by A59,A60,A66,A61,A63,RLVECT_3:1;
then x in Lin(A9) by RUSUB_3:1;
hence x in the carrier of Lin(A9);
end;
then the carrier of W1 + W2 c= the carrier of Lin(A9);
then Lin(A9) = Lin(A) & W1 + W2 is Subspace of Lin(A9) by RUSUB_1:22
,RUSUB_3:28;
then Lin(A) = W1 + W2 by RUSUB_1:20;
then
A67: A is Basis of W1 + W2 by A55,RUSUB_3:def 2;
card I = dim(W1 /\ W2) by A1,Def2;
then dim(W1 + W2) + dim(W1 /\ W2) = card I1 + card I2 + - card I + card I
by A15,A67,Def2
.= dim W1 + dim W2 by A56,Def2;
hence thesis;
end;
theorem
for V being finite-dimensional RealUnitarySpace, W1,W2 being Subspace
of V holds dim(W1 /\ W2) >= dim W1 + dim W2 - dim V
proof
let V be finite-dimensional RealUnitarySpace;
let W1,W2 be Subspace of V;
A1: dim(W1 + W2) <= dim V & dim V + (dim(W1 /\ W2) - dim V) = dim(W1 /\ W2)
by Th8;
dim W1 + dim W2 - dim V = dim(W1 + W2) + dim(W1 /\ W2) - dim V by Th15
.= dim(W1 + W2) + (dim(W1 /\ W2) - dim V);
hence thesis by A1,XREAL_1:6;
end;
theorem
for V being finite-dimensional RealUnitarySpace, W1,W2 being Subspace
of V st V is_the_direct_sum_of W1, W2 holds dim V = dim W1 + dim W2
proof
let V be finite-dimensional RealUnitarySpace;
let W1,W2 be Subspace of V;
assume
A1: V is_the_direct_sum_of W1, W2;
then
A2: the UNITSTR of V = W1 + W2 by RUSUB_2:def 4;
W1 /\ W2 = (0).V by A1,RUSUB_2:def 4;
then (Omega).(W1 /\ W2) = (0).V by RUSUB_1:def 3
.= (0).(W1 /\ W2) by RUSUB_1:30;
then dim(W1 /\ W2) = 0 by Th12;
then dim W1 + dim W2 = dim(W1 + W2) + 0 by Th15
.= dim (Omega).V by A2,RUSUB_1:def 3
.= dim V by Th10;
hence thesis;
end;
begin :: Fixed-dimensional subspace family
Lm2: for V being finite-dimensional RealUnitarySpace, n being Element of NAT
st n <= dim V holds ex W being strict Subspace of V st dim W = n
proof
let V be finite-dimensional RealUnitarySpace;
let n be Element of NAT;
consider I being finite Subset of V such that
A1: I is Basis of V by Def1;
assume n <= dim V;
then n <= card I by A1,Def2;
then consider A being finite Subset of I such that
A2: card A = n by FINSEQ_4:72;
reconsider A as Subset of V by XBOOLE_1:1;
reconsider W = Lin(A) as strict finite-dimensional Subspace of V;
I is linearly-independent by A1,RUSUB_3:def 2;
then dim W = n by A2,Th9,RLVECT_3:5;
hence thesis;
end;
theorem
for V being finite-dimensional RealUnitarySpace, W being Subspace of V
, n being Element of NAT holds n <= dim V iff ex W being strict Subspace of V
st dim W = n by Lm2,Th8;
definition
let V be finite-dimensional RealUnitarySpace, n be Element of NAT;
func n Subspaces_of V -> set means
:Def3:
for x being object holds x in it iff
ex W being strict Subspace of V st W = x & dim W = n;
existence
proof
set S = {Lin(A) where A is Subset of V: A is linearly-independent & card A
= n};
take S;
for x being object holds x in S iff ex W being strict Subspace of V st W
= x & dim W = n
proof
let x be object;
hereby
assume x in S;
then
A1: ex A being Subset of V st x = Lin(A) & A is linearly-independent &
card A = n;
then reconsider W = x as strict Subspace of V;
dim W = n by A1,Th9;
hence ex W being strict Subspace of V st W = x & dim W = n;
end;
given W being strict Subspace of V such that
A2: W = x and
A3: dim W = n;
consider A being finite Subset of W such that
A4: A is Basis of W by Def1;
reconsider A as Subset of W;
A is linearly-independent by A4,RUSUB_3:def 2;
then reconsider B=A as linearly-independent Subset of V by RUSUB_3:22;
A5: x = Lin(A) by A2,A4,RUSUB_3:def 2
.= Lin(B) by RUSUB_3:28;
then card B = n by A2,A3,Th9;
hence thesis by A5;
end;
hence thesis;
end;
uniqueness
proof
defpred P[object] means
ex W being strict Subspace of V st W = $1 & dim W = n;
for X1,X2 being set st (for x being object holds x in X1 iff P[x]) &
(for x being object holds x in X2 iff P[x]) holds X1 = X2 from XBOOLE_0:sch 3;
hence thesis;
end;
end;
theorem
for V being finite-dimensional RealUnitarySpace, n being Element of
NAT st n <= dim V holds n Subspaces_of V is non empty
proof
let V be finite-dimensional RealUnitarySpace;
let n be Element of NAT;
assume n <= dim V;
then ex W being strict Subspace of V st dim W = n by Lm2;
hence thesis by Def3;
end;
theorem
for V being finite-dimensional RealUnitarySpace, n being Element of
NAT st dim V < n holds n Subspaces_of V = {}
proof
let V be finite-dimensional RealUnitarySpace;
let n be Element of NAT;
assume that
A1: dim V < n and
A2: n Subspaces_of V <> {};
consider x being object such that
A3: x in n Subspaces_of V by A2,XBOOLE_0:def 1;
ex W being strict Subspace of V st W = x & dim W = n by A3,Def3;
hence contradiction by A1,Th8;
end;
theorem
for V being finite-dimensional RealUnitarySpace, W being Subspace of V
, n being Element of NAT holds n Subspaces_of W c= n Subspaces_of V
proof
let V be finite-dimensional RealUnitarySpace;
let W be Subspace of V;
let n be Element of NAT;
let x be object;
assume x in n Subspaces_of W;
then consider W1 being strict Subspace of W such that
A1: W1 = x and
A2: dim W1 = n by Def3;
reconsider W1 as strict Subspace of V by RUSUB_1:21;
W1 in n Subspaces_of V by A2,Def3;
hence thesis by A1;
end;
begin :: Affine set
definition
let V be non empty RLSStruct, S be Subset of V;
attr S is Affine means
:Def4:
for x,y being VECTOR of V, a being Real st x
in S & y in S holds (1 - a) * x + a * y in S;
end;
theorem
for V being non empty RLSStruct holds [#]V is Affine & {}V is Affine;
theorem
for V being vector-distributive scalar-distributive scalar-associative
scalar-unital non empty RLSStruct, v being VECTOR
of V holds {v} is Affine
proof
let V be vector-distributive scalar-distributive scalar-associative
scalar-unital non empty RLSStruct;
let v be VECTOR of V;
for x,y being VECTOR of V, a being Real
st x in {v} & y in {v} holds (1-a)*x + a*y in {v}
proof
let x,y being VECTOR of V;
let a be Real;
assume x in {v} & y in {v};
then x = v & y = v by TARSKI:def 1;
then (1-a)*x + a*y = ((1-a)+a)*v by RLVECT_1:def 6
.= v by RLVECT_1:def 8;
hence thesis by TARSKI:def 1;
end;
hence thesis;
end;
registration
let V be non empty RLSStruct;
cluster non empty Affine for Subset of V;
existence
proof
take [#]V;
thus thesis;
end;
cluster empty Affine for Subset of V;
existence
proof
take {}V;
thus thesis;
end;
end;
definition
let V be RealLinearSpace, W be Subspace of V;
func Up(W) -> non empty Subset of V equals
the carrier of W;
coherence by RLSUB_1:def 2;
end;
definition
let V be RealUnitarySpace, W be Subspace of V;
func Up(W) -> non empty Subset of V equals
the carrier of W;
coherence by RUSUB_1:def 1;
end;
theorem
for V being RealLinearSpace, W being Subspace of V holds Up(W) is
Affine & 0.V in the carrier of W
proof
let V be RealLinearSpace;
let W be Subspace of V;
for x,y being VECTOR of V, a being Real st x in Up(W) & y in Up(W)
holds (1 - a) * x + a * y in Up(W)
proof
let x,y be VECTOR of V;
let a be Real;
assume that
A1: x in Up(W) and
A2: y in Up(W);
reconsider aa=a as Real;
y in W by A2;
then
A3: aa * y in W by RLSUB_1:21;
x in W by A1;
then (1 - aa) * x in W by RLSUB_1:21;
then (1 - a) * x + a * y in W by A3,RLSUB_1:20;
hence thesis;
end;
hence Up(W) is Affine;
0.V in W by RLSUB_1:17;
hence thesis;
end;
theorem Th25:
for V being RealLinearSpace, A being Affine Subset of V st 0.V in A
for x being VECTOR of V, a being Real st x in A holds a * x in A
proof
let V be RealLinearSpace;
let A be Affine Subset of V;
assume
A1: 0.V in A;
for x being VECTOR of V, a being Real st x in A holds a * x in A
proof
let x be VECTOR of V;
let a be Real;
assume x in A;
then (1-a) * 0.V + a * x in A by A1,Def4;
then 0.V + a * x in A;
hence thesis;
end;
hence thesis;
end;
definition
let V be non empty RLSStruct, S be non empty Subset of V;
attr S is Subspace-like means
0.V in S & for x,y being Element of V,
a being Real st x in S & y in S holds x + y in S & a * x in S;
end;
theorem Th26:
for V being RealLinearSpace, A being non empty Affine Subset of
V st 0.V in A holds A is Subspace-like & A = the carrier of Lin(A)
proof
let V be RealLinearSpace;
let A be non empty Affine Subset of V;
assume
A1: 0.V in A;
A2: for x,y being Element of V, a being Real
st x in A & y in A holds x + y in A & a * x in A
proof
let x,y be Element of V;
let a be Real;
assume that
A3: x in A and
A4: y in A;
reconsider x,y as VECTOR of V;
A5: 2 * ( (1-1/2) * x + (1/2) * y ) = 2*( (1-1/2) * x) + 2*((1/2) * y) by
RLVECT_1:def 5
.= ( 2*(1-1/2) ) * x + 2*((1/2) * y) by RLVECT_1:def 7
.= ( 2 - 1 ) * x + ( 2*(1/2) ) * y by RLVECT_1:def 7
.= x + 1 * y by RLVECT_1:def 8
.= x + y by RLVECT_1:def 8;
(1 - 1/2) * x + (1/2) * y in A by A3,A4,Def4;
hence thesis by A1,A3,A5,Th25;
end;
hence A is Subspace-like by A1;
for x being object st x in the carrier of Lin(A) holds x in A
proof
let x be object;
assume x in the carrier of Lin(A);
then x in Lin(A);
then
A6: ex l being Linear_Combination of A st x = Sum(l) by RLVECT_3:14;
( for v,u being VECTOR of V st v in A & u in A holds v + u in A)& for
a being Real, v being VECTOR of V st v in A holds a * v in A by A2;
then A is linearly-closed by RLSUB_1:def 1;
hence thesis by A6,RLVECT_2:29;
end;
then
A7: the carrier of Lin(A) c= A;
for x being object st x in A holds x in the carrier of Lin(A)
by RLVECT_3:15,STRUCT_0:def 5;
then A c= the carrier of Lin(A);
hence thesis by A7;
end;
theorem
for V being RealLinearSpace, W being Subspace of V holds Up(W) is
Subspace-like
proof
let V be RealLinearSpace;
let W be Subspace of V;
0.V in W by RLSUB_1:17;
hence 0.V in Up(W);
thus for x,y being Element of V, a being Real
st x in Up(W) & y in Up(W)
holds x + y in Up(W) & a * x in Up(W)
proof
let x,y be Element of V;
let a be Real;
assume that
A1: x in Up(W) and
A2: y in Up(W);
reconsider x,y as Element of V;
reconsider aa=a as Real;
A3: x in W by A1;
then
A4: aa * x in W by RLSUB_1:21;
y in W by A2;
then x + y in W by A3,RLSUB_1:20;
hence thesis by A4;
end;
end;
theorem
for V being RealUnitarySpace, A being non empty Affine Subset of V st
0.V in A holds A = the carrier of Lin(A)
proof
let V be RealUnitarySpace;
let A be non empty Affine Subset of V;
assume 0.V in A;
then
A1: A is Subspace-like by Th26;
for x being object st x in the carrier of Lin(A) holds x in A
proof
let x be object;
assume x in the carrier of Lin(A);
then x in Lin(A);
then
A2: ex l being Linear_Combination of A st x = Sum(l) by RUSUB_3:1;
( for v,u being VECTOR of V st v in A & u in A holds v + u in A)& for
a being Real, v being VECTOR of V
st v in A holds a * v in A by A1;
then A is linearly-closed by RLSUB_1:def 1;
hence thesis by A2,RLVECT_2:29;
end;
then
A3: the carrier of Lin(A) c= A;
for x being object st x in A holds x in the carrier of Lin(A)
by RUSUB_3:2,STRUCT_0:def 5;
then A c= the carrier of Lin(A);
hence thesis by A3;
end;
theorem
for V being RealUnitarySpace, W being Subspace of V holds Up(W) is
Subspace-like
proof
let V be RealUnitarySpace;
let W be Subspace of V;
0.V in W by RUSUB_1:11;
hence 0.V in Up(W);
thus for x,y being Element of V, a being Real
st x in Up(W) & y in Up(W)
holds x + y in Up(W) & a * x in Up(W)
proof
let x,y be Element of V;
let a be Real;
assume that
A1: x in Up(W) and
A2: y in Up(W);
reconsider x,y as Element of V;
A3: x in W by A1;
then
A4: a * x in W by RUSUB_1:15;
y in W by A2;
then x + y in W by A3,RUSUB_1:14;
hence thesis by A4;
end;
end;
definition
let V be non empty addLoopStr, M be Subset of V, v be Element of V;
func v + M -> Subset of V equals
{v + u where u is Element of V: u in M};
coherence
proof
set Y = {v + u where u is Element of V: u in M};
defpred P[object] means ex u being Element of V st $1 = v + u & u in M;
consider X being set such that
A1: for x being object holds x in X iff x in the carrier of V & P[x] from
XBOOLE_0:sch 1;
X c= the carrier of V
by A1;
then reconsider X as Subset of V;
reconsider X as Subset of V;
A2: Y c= X
proof
let x be object;
assume x in Y;
then ex u being Element of V st x = v + u & u in M;
hence thesis by A1;
end;
X c= Y
proof
let x be object;
assume x in X;
then ex u being Element of V st x = v + u & u in M by A1;
hence thesis;
end;
hence thesis by A2,XBOOLE_0:def 10;
end;
end;
theorem
for V being RealLinearSpace, W being strict Subspace of V, M being
Subset of V, v being VECTOR of V st Up(W) = M holds v + W = v + M
proof
let V be RealLinearSpace;
let W be strict Subspace of V;
let M be Subset of V;
let v be VECTOR of V;
assume
A1: Up(W) = M;
for x being object st x in v + M holds x in v + W
proof
let x be object;
assume x in v + M;
then consider u being Element of V such that
A2: x = v + u and
A3: u in M;
u in W by A1,A3;
then x in {v + u9 where u9 is VECTOR of V : u9 in W} by A2;
hence thesis by RLSUB_1:def 5;
end;
then
A4: v + M c= v + W;
for x being object st x in v + W holds x in v + M
proof
let x be object;
assume x in v + W;
then x in {v + u where u is VECTOR of V : u in W} by RLSUB_1:def 5;
then consider u being VECTOR of V such that
A5: x = v + u and
A6: u in W;
u in M by A1,A6;
hence thesis by A5;
end;
then v + W c= v + M;
hence thesis by A4;
end;
theorem Th31:
for V being Abelian add-associative vector-distributive scalar-distributive
scalar-associative scalar-unital non
empty RLSStruct, M being Affine Subset of V, v being VECTOR of V holds v + M
is Affine
proof
let V be Abelian add-associative vector-distributive scalar-distributive
scalar-associative scalar-unital non empty RLSStruct;
let M be Affine Subset of V;
let v be VECTOR of V;
for x,y being VECTOR of V, a being Real
st x in v + M & y in v + M holds (1-a)*x + a*y in v + M
proof
let x,y be VECTOR of V;
let a be Real;
assume that
A1: x in v + M and
A2: y in v + M;
consider x9 being Element of V such that
A3: x = v + x9 and
A4: x9 in M by A1;
consider y9 being Element of V such that
A5: y = v + y9 and
A6: y9 in M by A2;
A7: (1 - a) * x + a * y = (1-a)*v + (1-a)*x9 + a * (v + y9) by A3,A5,
RLVECT_1:def 5
.= (1-a)*v + (1-a)*x9 + (a*v + a*y9) by RLVECT_1:def 5
.= (1-a)*v + (1-a)*x9 + a*v + a*y9 by RLVECT_1:def 3
.= (1-a)*x9 + ((1-a)*v + a*v) + a*y9 by RLVECT_1:def 3
.= (1-a)*x9 + (1-a+a)*v + a*y9 by RLVECT_1:def 6
.= (1-a)*x9 + v + a*y9 by RLVECT_1:def 8
.= v + ((1-a)*x9 + a*y9) by RLVECT_1:def 3;
(1 - a) * x9 + a * y9 in M by A4,A6,Def4;
hence thesis by A7;
end;
hence thesis;
end;
theorem
for V being RealUnitarySpace, W being strict Subspace of V, M being
Subset of V, v being VECTOR of V st Up(W) = M holds v + W = v + M
proof
let V be RealUnitarySpace;
let W be strict Subspace of V;
let M be Subset of V;
let v be VECTOR of V;
assume
A1: Up(W) = M;
for x being object st x in v + M holds x in v + W
proof
let x be object;
assume x in v + M;
then consider u being Element of V such that
A2: x = v + u and
A3: u in M;
u in W by A1,A3;
then x in {v + u9 where u9 is VECTOR of V : u9 in W} by A2;
hence thesis by RUSUB_1:def 4;
end;
then
A4: v + M c= v + W;
for x being object st x in v + W holds x in v + M
proof
let x be object;
assume x in v + W;
then x in {v + u where u is VECTOR of V : u in W} by RUSUB_1:def 4;
then consider u being VECTOR of V such that
A5: x = v + u and
A6: u in W;
u in M by A1,A6;
hence thesis by A5;
end;
then v + W c= v + M;
hence thesis by A4;
end;
definition
let V be non empty addLoopStr, M,N be Subset of V;
func M + N -> Subset of V equals
{u + v where u,v is Element of V: u in M &
v in N};
coherence
proof
defpred P[set,set] means $1 in M & $2 in N;
deffunc F(Element of V,Element of V) = $1+$2;
{F(u,v) where u,v is Element of V : P[u,v]} is Subset of V from
DOMAIN_1:sch 9;
hence thesis;
end;
end;
definition
let V be Abelian non empty addLoopStr, M,N be Subset of V;
redefine func M + N; :: redefines + (RUSUB_4, definition)
commutativity
proof
let M,N be Subset of V;
for x being object st x in M + N holds x in N + M
proof
let x be object;
assume x in M + N;
then ex u1,v1 being Element of V st x = u1 + v1 & u1 in M & v1 in N;
hence thesis;
end;
then
A1: M + N c= N + M;
for x being object st x in N + M holds x in M + N
proof
let x be object;
assume x in N + M;
then ex u1,v1 being Element of V st x = u1 + v1 & u1 in N & v1 in M;
hence thesis;
end;
then N + M c= M + N;
hence thesis by A1;
end;
end;
theorem Th33:
for V being non empty addLoopStr, M being Subset of V, v being
Element of V holds {v} + M = v + M
proof
let V be non empty addLoopStr;
let M be Subset of V;
let v be Element of V;
for x being object st x in v + M holds x in {v} + M
proof
let x be object;
assume x in v + M;
then
A1: ex u being Element of V st x = v + u & u in M;
v in {v} by TARSKI:def 1;
hence thesis by A1;
end;
then
A2: v + M c= {v} + M;
for x being object st x in {v} + M holds x in v + M
proof
let x be object;
assume x in {v} + M;
then consider v1,u1 being Element of V such that
A3: x = v1 + u1 and
A4: v1 in {v} and
A5: u1 in M;
v1 = v by A4,TARSKI:def 1;
hence thesis by A3,A5;
end;
then {v} + M c= v + M;
hence thesis by A2;
end;
theorem
for V being Abelian add-associative vector-distributive scalar-distributive
scalar-associative scalar-unital non empty
RLSStruct, M being Affine Subset of V, v being VECTOR of V holds {v} + M is
Affine
proof
let V be Abelian add-associative vector-distributive scalar-distributive
scalar-associative scalar-unital non empty RLSStruct;
let M be Affine Subset of V;
let v be VECTOR of V;
{v} + M = v + M by Th33;
hence thesis by Th31;
end;
theorem
for V being non empty RLSStruct, M,N being Affine Subset of V holds M
/\ N is Affine
proof
let V be non empty RLSStruct;
let M,N be Affine Subset of V;
for x,y being VECTOR of V, a being Real
st x in M /\ N & y in M /\ N
holds (1 - a) * x + a * y in M /\ N
proof
let x,y be VECTOR of V;
let a be Real;
assume
A1: x in M /\ N & y in M /\ N;
then x in N & y in N by XBOOLE_0:def 4;
then
A2: (1 - a) * x + a * y in N by Def4;
x in M & y in M by A1,XBOOLE_0:def 4;
then (1 - a) * x + a * y in M by Def4;
hence thesis by A2,XBOOLE_0:def 4;
end;
hence thesis;
end;
theorem
for V being Abelian add-associative vector-distributive scalar-distributive
scalar-associative scalar-unital non empty
RLSStruct, M,N being Affine Subset of V holds M + N is Affine
proof
let V be Abelian add-associative vector-distributive scalar-distributive
scalar-associative scalar-unital non empty RLSStruct;
let M,N be Affine Subset of V;
for x,y being VECTOR of V, a being Real
st x in M + N & y in M + N holds
(1 - a) * x + a * y in M + N
proof
let x,y be VECTOR of V;
let a be Real;
assume that
A1: x in M + N and
A2: y in M + N;
consider u1,v1 being Element of V such that
A3: x = u1 + v1 and
A4: u1 in M & v1 in N by A1;
consider u2,v2 being Element of V such that
A5: y = u2 + v2 and
A6: u2 in M & v2 in N by A2;
A7: (1 - a) * x + a * y = (1 - a) * u1 + (1 - a) * v1 + a * (u2 + v2) by A3,A5,
RLVECT_1:def 5
.= (1 - a) * u1 + (1 - a) * v1 + ( a * u2 + a * v2 ) by RLVECT_1:def 5
.= (1 - a) * u1 + (1 - a) * v1 + a * u2 + a * v2 by RLVECT_1:def 3
.= (1 - a) * v1 + ((1 - a) * u1 + a * u2) + a * v2 by RLVECT_1:def 3
.= ((1 - a) * u1 + a * u2) + ((1 - a) * v1 + a * v2) by RLVECT_1:def 3;
(1 - a) * u1 + a * u2 in M & (1 - a) * v1 + a * v2 in N by A4,A6,Def4;
hence thesis by A7;
end;
hence thesis;
end;