:: Steinitz Theorem and Dimension of a Vector Space
:: by Mariusz \.Zynel
::
:: Received October 6, 1995
:: Copyright (c) 1995-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, VECTSP_1, RLSUB_1, NAT_1, XBOOLE_0, STRUCT_0, SUBSET_1,
RLVECT_2, FINSEQ_1, FUNCT_2, RELAT_1, CARD_3, VALUED_1, FUNCT_1,
PARTFUN1, SUPINF_2, ORDINAL4, TARSKI, ARYTM_3, ARYTM_1, CLASSES1,
FINSET_1, RLVECT_3, CARD_1, XXREAL_0, FINSEQ_4, RLVECT_5, RLSUB_2;
notations TARSKI, XBOOLE_0, ENUMSET1, SUBSET_1, CARD_1, ORDINAL1, NUMBERS,
XCMPLX_0, RELAT_1, DOMAIN_1, STRUCT_0, FUNCT_1, PARTFUN1, FUNCT_2, NAT_1,
FINSET_1, FINSEQ_1, FINSEQ_3, FINSEQ_4, CLASSES1, RLVECT_1, VECTSP_1,
VECTSP_4, VECTSP_6, VECTSP_5, VECTSP_7, MATRLIN, XXREAL_0;
constructors FINSEQ_4, XXREAL_0, NAT_1, REALSET1, RFINSEQ, VECTSP_5, VECTSP_6,
VECTSP_7, CLASSES1, MATRLIN, RELSET_1;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, FUNCT_2,
FINSET_1, XREAL_0, NAT_1, FINSEQ_1, STRUCT_0, VECTSP_1, VECTSP_7,
MATRLIN, CARD_1, RELSET_1;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
definitions TARSKI;
expansions TARSKI;
theorems TARSKI, ENUMSET1, SUBSET_1, NAT_1, CARD_1, CARD_2, FUNCT_1, FUNCT_2,
FINSEQ_1, FINSEQ_2, FINSEQ_3, FINSEQ_4, FINSET_1, RFINSEQ, RLVECT_1,
VECTSP_1, VECTSP_4, VECTSP_5, VECTSP_6, VECTSP_7, MATRLIN, XBOOLE_0,
XBOOLE_1, RLVECT_2, VECTSP_2, ZFMISC_1, XREAL_1, XXREAL_0, STRUCT_0,
PARTFUN1, RELAT_1;
schemes NAT_1, FINSEQ_1, FUNCT_2;
begin
reserve GF for Field,
V for VectSp of GF,
W for Subspace of V,
x, y, y1, y2 for set,
i, n, m for Nat;
::
:: Preliminaries
::
registration
let S be non empty 1-sorted;
cluster non empty for Subset of S;
existence
proof
set A = the non empty Subset of S;
A is Subset of S;
hence thesis;
end;
end;
Lm1: for X, x being set st x in X holds X \ {x} \/ {x} = X
proof
let X, 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;
:: More On Linear Combinations
theorem Th1:
for L being Linear_Combination of V for F, G being FinSequence of
the carrier of V for P being Permutation of dom F st G = F*P holds Sum(L (#) F)
= Sum(L (#) G)
proof
let L be Linear_Combination of V;
let F, G be FinSequence of the carrier of V;
set p = L (#) F, q = L (#) G;
let P be Permutation of dom F such that
A1: G = F*P;
A2: len G = len F by A1,FINSEQ_2:44;
len F = len(L (#) F) by VECTSP_6:def 5;
then
A3: dom F = dom(L (#) F) by FINSEQ_3:29;
then reconsider r = (L (#) F)*P as FinSequence of the carrier of V by
FINSEQ_2:47;
len r = len(L (#) F) by A3,FINSEQ_2:44;
then
A4: dom r = dom(L (#) F) by FINSEQ_3:29;
A5: len p = len F by VECTSP_6:def 5;
then
A6: dom F = dom p by FINSEQ_3:29;
len q = len G by VECTSP_6:def 5;
then
A7: dom p = dom q by A5,A2,FINSEQ_3:29;
A8: dom F = dom G by A2,FINSEQ_3:29;
now
let k be Nat;
assume
A9: k in dom q;
set l = P.k;
dom P = dom F & rng P = dom F by FUNCT_2:52,def 3;
then
A10: l in dom F by A7,A6,A9,FUNCT_1:def 3;
then reconsider l as Element of NAT;
G/.k = G.k by A7,A8,A6,A9,PARTFUN1:def 6
.= F.(P.k) by A1,A7,A8,A6,A9,FUNCT_1:12
.= F/.l by A10,PARTFUN1:def 6;
then q.k = L.(F/.l) * (F/.l) by A9,VECTSP_6:def 5
.= (L (#) F).(P.k) by A6,A10,VECTSP_6:def 5
.= r.k by A7,A4,A9,FUNCT_1:12;
hence q.k = r.k;
end;
hence thesis by A3,A7,A4,FINSEQ_1:13,RLVECT_2:7;
end;
theorem Th2:
for L being Linear_Combination of V for F being FinSequence of
the carrier of V st Carrier(L) misses rng F holds Sum(L (#) F) = 0.V
proof
let L be Linear_Combination of V;
defpred P[FinSequence] means for G being FinSequence of the carrier of V st
G = $1 holds Carrier(L) misses rng G implies Sum(L (#) G) = 0.V;
A1: for p being FinSequence, x being object st P[p] holds P[p^<*x*>]
proof
let p be FinSequence, x be object such that
A2: P[p];
let G be FinSequence of the carrier of V;
assume
A3: G = p^<*x*>;
then reconsider p, x9= <*x*> as FinSequence of the carrier of V by
FINSEQ_1:36;
x in {x} by TARSKI:def 1;
then
A4: x in rng x9 by FINSEQ_1:38;
rng x9 c= the carrier of V by FINSEQ_1:def 4;
then reconsider x as Vector of V by A4;
assume Carrier(L) misses rng G;
then
A5: {} = Carrier(L) /\ rng G by XBOOLE_0:def 7
.= Carrier(L) /\ (rng p \/ rng<*x*>) by A3,FINSEQ_1:31
.= Carrier(L) /\ (rng p \/ {x}) by FINSEQ_1:38
.= Carrier(L) /\ rng p \/ Carrier(L) /\ {x} by XBOOLE_1:23;
then Carrier(L) /\ rng p = {};
then Carrier(L) misses rng p by XBOOLE_0:def 7;
then
A6: Sum(L (#) p) = 0.V by A2;
now
A7: x in {x} by TARSKI:def 1;
assume x in Carrier(L);
then x in Carrier(L) /\ {x} by A7,XBOOLE_0:def 4;
hence contradiction by A5;
end;
then
A8: L.x = 0.GF by VECTSP_6:2;
Sum(L (#) G) = Sum((L (#) p) ^ (L (#) x9)) by A3,VECTSP_6:13
.= Sum(L (#) p) + Sum(L (#) x9) by RLVECT_1:41
.= 0.V + Sum(<* L.x * x *>) by A6,VECTSP_6:10
.= Sum(<* L.x * x *>) by RLVECT_1:4
.= 0.GF * x by A8,RLVECT_1:44
.= 0.V by VECTSP_1:15;
hence thesis;
end;
A9: P[{}]
proof
let G be FinSequence of the carrier of V;
assume G = {};
then
A10: L (#) G = <*>(the carrier of V) by VECTSP_6:9;
assume Carrier(L) misses rng G;
thus thesis by A10,RLVECT_1:43;
end;
A11: for p being FinSequence holds P[p] from FINSEQ_1:sch 3(A9, A1);
let F be FinSequence of the carrier of V;
assume Carrier(L) misses rng F;
hence thesis by A11;
end;
theorem Th3:
for F being FinSequence of the carrier of V st F is one-to-one
for L being Linear_Combination of V st Carrier(L) c= rng F holds Sum(L (#) F) =
Sum(L)
proof
let F be FinSequence of the carrier of V such that
A1: F is one-to-one;
rng F c= rng F;
then reconsider X = rng F as Subset of rng F;
let L be Linear_Combination of V such that
A2: Carrier(L) c= rng F;
consider G being FinSequence of the carrier of V such that
A3: G is one-to-one and
A4: rng G = Carrier(L) and
A5: Sum(L) = Sum(L (#) G) by VECTSP_6:def 6;
reconsider A = rng G as Subset of rng F by A2,A4;
set F1 = F - A`;
X \ A` = X /\ A`` by SUBSET_1:13
.= A by XBOOLE_1:28;
then
A6: rng F1 = rng G by FINSEQ_3:65;
F1 is one-to-one by A1,FINSEQ_3:87;
then F1, G are_fiberwise_equipotent by A3,A6,RFINSEQ:26;
then
A7: ex Q being Permutation of dom G st F1 = G*Q by RFINSEQ:4;
reconsider F1, F2 = F - A as FinSequence of the carrier of V by FINSEQ_3:86;
rng F2 = rng F \ rng G by FINSEQ_3:65;
then
A8: rng F2 misses rng G by XBOOLE_1:79;
ex P being Permutation of dom F st (F - A`) ^ (F - A) = F* P by FINSEQ_3:115;
then Sum(L (#) F) = Sum(L (#) (F1^F2)) by Th1
.= Sum((L (#) F1) ^ (L (#) F2)) by VECTSP_6:13
.= Sum(L (#) F1) + Sum(L (#) F2) by RLVECT_1:41
.= Sum(L (#) F1) + 0.V by A4,A8,Th2
.= Sum(L (#) G) + 0.V by A7,Th1
.= Sum(L) by A5,RLVECT_1:4;
hence thesis;
end;
theorem Th4:
for L being Linear_Combination of V for F being FinSequence of
the carrier of V holds ex K being Linear_Combination of V st Carrier(K) = rng F
/\ Carrier(L) & L (#) F = K (#) F
proof
let L be Linear_Combination of V, F be FinSequence of the carrier of V;
defpred P[object, object] means
$1 is Vector of V implies ($1 in rng F & $2 = L.$1
) or (not $1 in rng F & $2 = 0.GF);
reconsider R = rng F as finite Subset of V by FINSEQ_1:def 4;
A1: for x being object st x in the carrier of V
ex y being object st y in the carrier of GF & P[x, y]
proof
let x be object;
assume x in the carrier of V;
then reconsider x9= x as Vector of V;
per cases;
suppose
x in rng F;
then P[x, L.x9];
hence thesis;
end;
suppose
not x in rng F;
hence thesis;
end;
end;
ex K being Function of the carrier of V, the carrier of GF st
for x being object st x
in the carrier of V holds P[x, K.x] from FUNCT_2:sch 1(A1);
then consider
K being Function of the carrier of V, the carrier of GF such that
A2: for x being object st x in the carrier of V holds P[x, K.x];
A3: now
let v be Vector of V;
assume
A4: not v in R /\ Carrier(L);
per cases by A4,XBOOLE_0:def 4;
suppose
not v in R;
hence K.v = 0.GF by A2;
end;
suppose
A5: not v in Carrier(L);
P[v, K.v] & P[v, L.v] or P[v, K.v] & P[v, 0.GF] by A2;
hence K.v = 0.GF by A5,VECTSP_6:2;
end;
end;
reconsider K as Element of Funcs(the carrier of V, the carrier of GF) by
FUNCT_2:8;
reconsider K as Linear_Combination of V by A3,VECTSP_6:def 1;
now
let v be object;
assume
A6: v in rng F /\ Carrier(L);
then reconsider v9= v as Vector of V;
v in Carrier(L) by A6,XBOOLE_0:def 4;
then
A7: L.v9 <> 0.GF by VECTSP_6:2;
v in R by A6,XBOOLE_0:def 4;
then K.v9 = L.v9 by A2;
hence v in Carrier(K) by A7,VECTSP_6:1;
end;
then
A8: rng F /\ Carrier(L) c= Carrier(K);
take K;
A9: L (#) F = K (#) F
proof
set p = L (#) F, q = K (#) F;
A10: len p = len F by VECTSP_6:def 5;
len q = len F by VECTSP_6:def 5;
then
A11: dom p = dom q by A10,FINSEQ_3:29;
A12: dom p = dom F by A10,FINSEQ_3:29;
now
let k be Nat;
set u = F/.k;
A13: P[u, K.u] by A2;
assume
A14: k in dom p;
then F/.k = F.k & p.k = L.u * u by A12,PARTFUN1:def 6,VECTSP_6:def 5;
hence p.k = q.k by A11,A12,A14,A13,FUNCT_1:def 3,VECTSP_6:def 5;
end;
hence thesis by A11,FINSEQ_1:13;
end;
now
let v be object;
assume v in Carrier(K);
then ex v9 being Vector of V st v9= v & K.v9 <> 0.GF by VECTSP_6:1;
hence v in rng F /\ Carrier(L) by A3;
end;
then Carrier(K) c= rng F /\ Carrier(L);
hence thesis by A8,A9,XBOOLE_0:def 10;
end;
theorem Th5:
for L being Linear_Combination of V for A being Subset of V for F
being FinSequence of the carrier of V st rng F c= the carrier of Lin(A) holds
ex K being Linear_Combination of A st Sum(L (#) F) = Sum(K)
proof
let L be Linear_Combination of V;
let A be Subset of V;
defpred P[Nat] means for F being FinSequence of the carrier of V st rng F c=
the carrier of Lin(A) & len F = $1 holds ex K being Linear_Combination of A st
Sum(L (#) F) = Sum(K);
A1: for n being Nat st P[n] holds P[n + 1]
proof
let n be Nat;
assume
A2: P[n];
let F be FinSequence of the carrier of V such that
A3: rng F c= the carrier of Lin(A) and
A4: len F = n + 1;
consider G being FinSequence, x being object such that
A5: F = G^<*x*> by A4,FINSEQ_2:18;
reconsider G, x9= <*x*> as FinSequence of the carrier of V by A5,
FINSEQ_1:36;
A6: rng(G^<*x*>) = rng G \/ rng <*x*> by FINSEQ_1:31
.= rng G \/ {x} by FINSEQ_1:38;
then
A7: rng G c= rng F by A5,XBOOLE_1:7;
{x} c= rng F by A5,A6,XBOOLE_1:7;
then {x} c= the carrier of Lin(A) by A3;
then x in {x} implies x in the carrier of Lin(A);
then
A8: x in Lin(A) by STRUCT_0:def 5,TARSKI:def 1;
then consider LA1 being Linear_Combination of A such that
A9: x = Sum(LA1) by VECTSP_7:7;
x in V by A8,VECTSP_4:9;
then reconsider x as Vector of V by STRUCT_0:def 5;
len(G^<*x*>) = len G + len <*x*> by FINSEQ_1:22
.= len G + 1 by FINSEQ_1:39;
then consider LA2 being Linear_Combination of A such that
A10: Sum(L (#) G) = Sum(LA2) by A2,A3,A4,A5,A7,XBOOLE_1:1;
L.x * LA1 is Linear_Combination of A by VECTSP_6:31;
then
A11: LA2 + L.x * LA1 is Linear_Combination of A by VECTSP_6:24;
Sum(L (#) F) = Sum((L (#) G) ^ (L (#) x9)) by A5,VECTSP_6:13
.= Sum(LA2) + Sum(L (#) x9) by A10,RLVECT_1:41
.= Sum(LA2) + Sum(<*L.x * x*>) by VECTSP_6:10
.= Sum(LA2) + L.x * Sum(LA1) by A9,RLVECT_1:44
.= Sum(LA2) + Sum(L.x * LA1) by VECTSP_6:45
.= Sum(LA2 + L.x * LA1) by VECTSP_6:44;
hence thesis by A11;
end;
let F be FinSequence of the carrier of V;
assume
A12: rng F c= the carrier of Lin(A);
A13: len F is Nat;
A14: P[0]
proof
let F be FinSequence of the carrier of V;
assume that
rng F c= the carrier of Lin(A) and
A15: len F = 0;
F = <*>(the carrier of V) by A15;
then L (#) F = <*>(the carrier of V) by VECTSP_6:9;
then
A16: Sum(L (#) F) = 0.V by RLVECT_1:43
.= Sum(ZeroLC(V)) by VECTSP_6:15;
ZeroLC(V) is Linear_Combination of A by VECTSP_6:5;
hence thesis by A16;
end;
for n being Nat holds P[n] from NAT_1:sch 2(A14, A1);
hence thesis by A12,A13;
end;
theorem Th6:
for L being Linear_Combination of V for A being Subset of V st
Carrier(L) c= the carrier of Lin(A) holds ex K being Linear_Combination of A st
Sum(L) = Sum(K)
proof
let L be Linear_Combination of V, A be Subset of V;
consider F being FinSequence of the carrier of V such that
F is one-to-one and
A1: rng F = Carrier(L) and
A2: Sum(L) = Sum(L (#) F) by VECTSP_6:def 6;
assume Carrier(L) c= the carrier of Lin(A);
then consider K being Linear_Combination of A such that
A3: Sum(L (#) F) = Sum(K) by A1,Th5;
take K;
thus thesis by A2,A3;
end;
theorem Th7:
for L being Linear_Combination of V st Carrier(L) c= the carrier
of W for K being Linear_Combination of W st K = L|the carrier of W holds
Carrier(L) = Carrier(K) & Sum(L) = Sum(K)
proof
let L be Linear_Combination of V such that
A1: Carrier(L) c= the carrier of W;
let K be Linear_Combination of W such that
A2: K = L|the carrier of W;
A3: dom K = the carrier of W by FUNCT_2:def 1;
now
let x be object;
assume x in Carrier(K);
then consider w being Vector of W such that
A4: x = w and
A5: K.w <> 0.GF by VECTSP_6:1;
A6: w is Vector of V by VECTSP_4:10;
L.w <> 0.GF by A2,A3,A5,FUNCT_1:47;
hence x in Carrier(L) by A4,A6,VECTSP_6:1;
end;
then
A7: Carrier(K) c= Carrier(L);
consider G being FinSequence of the carrier of W such that
A8: G is one-to-one & rng G = Carrier(K) and
A9: Sum(K) = Sum(K (#) G) by VECTSP_6:def 6;
consider F being FinSequence of the carrier of V such that
A10: F is one-to-one and
A11: rng F = Carrier(L) and
A12: Sum(L) = Sum(L (#) F) by VECTSP_6:def 6;
now
let x be object;
assume
A13: x in Carrier(L);
then consider v being Vector of V such that
A14: x = v and
A15: L.v <> 0.GF by VECTSP_6:1;
K.v <> 0.GF by A1,A2,A3,A13,A14,A15,FUNCT_1:47;
hence x in Carrier(K) by A1,A13,A14,VECTSP_6:1;
end;
then
A16: Carrier(L) c= Carrier(K);
then
A17: Carrier(K) = Carrier(L) by A7,XBOOLE_0:def 10;
then F, G are_fiberwise_equipotent by A10,A11,A8,RFINSEQ:26;
then consider P being Permutation of dom G such that
A18: F = G*P by RFINSEQ:4;
len(K (#) G) = len G by VECTSP_6:def 5;
then
A19: dom(K (#) G) = dom G by FINSEQ_3:29;
then reconsider q = (K (#) G)*P as FinSequence of the carrier of W by
FINSEQ_2:47;
A20: len q = len (K (#) G) by A19,FINSEQ_2:44;
then len q = len G by VECTSP_6:def 5;
then
A21: dom q = dom G by FINSEQ_3:29;
set p = L (#) F;
A22: the carrier of W c= the carrier of V by VECTSP_4:def 2;
rng q c= the carrier of W by FINSEQ_1:def 4;
then rng q c= the carrier of V by A22;
then reconsider q9= q as FinSequence of the carrier of V by FINSEQ_1:def 4;
consider f being sequence of the carrier of W such that
A23: Sum(q) = f.(len q) and
A24: f.0 = 0.W and
A25: for i being Nat, w being Vector of W st i < len q & w =
q.(i + 1) holds f.(i + 1) = f.i + w by RLVECT_1:def 12;
dom f = NAT & rng f c= the carrier of W by FUNCT_2:def 1,RELAT_1:def 19;
then reconsider f9= f as sequence of the carrier of V by A22,FUNCT_2:2
,XBOOLE_1:1;
A26: for i being Nat, v being Vector of V st i < len q9 & v = q9.
(i + 1) holds f9.(i + 1) = f9.i + v
proof
let i be Nat, v be Vector of V;
assume that
A27: i < len q9 and
A28: v = q9.(i + 1);
1 <= i + 1 & i + 1 <= len q by A27,NAT_1:11,13;
then i + 1 in dom q by FINSEQ_3:25;
then reconsider v9= v as Vector of W by A28,FINSEQ_2:11;
f.(i + 1) = f.i + v9 by A25,A27,A28;
hence thesis by VECTSP_4:13;
end;
A29: len G = len F by A18,FINSEQ_2:44;
then
A30: dom G = dom F by FINSEQ_3:29;
len G = len (L (#) F) by A29,VECTSP_6:def 5;
then
A31: dom p = dom G by FINSEQ_3:29;
A32: dom q = dom(K (#) G) by A20,FINSEQ_3:29;
now
let i be Nat;
set v = F/.i;
set j = P.i;
assume
A33: i in dom p;
then
A34: F/.i = F.i by A31,A30,PARTFUN1:def 6;
then v in rng F by A31,A30,A33,FUNCT_1:def 3;
then reconsider w = v as Vector of W by A17,A11;
dom P = dom G & rng P = dom G by FUNCT_2:52,def 3;
then
A35: j in dom G by A31,A33,FUNCT_1:def 3;
then reconsider j as Element of NAT;
A36: G/.j = G.(P.i) by A35,PARTFUN1:def 6
.= v by A18,A31,A30,A33,A34,FUNCT_1:12;
q.i = (K (#) G).j by A31,A21,A33,FUNCT_1:12
.= K.w * w by A32,A21,A35,A36,VECTSP_6:def 5
.= L.v * w by A2,A3,FUNCT_1:47
.= L.v * v by VECTSP_4:14;
hence p.i = q.i by A33,VECTSP_6:def 5;
end;
then
A37: L (#) F = (K (#) G)*P by A31,A21,FINSEQ_1:13;
len G = len (K (#) G) by VECTSP_6:def 5;
then dom G = dom (K (#) G) by FINSEQ_3:29;
then reconsider P as Permutation of dom (K (#) G);
q = (K (#) G)*P;
then
A38: Sum(K (#) G) = Sum(q) by RLVECT_2:7;
A39: f9.len q9 is Element of V;
f9.0 = 0.V by A24,VECTSP_4:11;
hence thesis by A7,A16,A12,A9,A37,A38,A23,A26,A39,RLVECT_1:def 12
,XBOOLE_0:def 10;
end;
theorem Th8:
for K being Linear_Combination of W ex L being
Linear_Combination of V st Carrier(K) = Carrier(L) & Sum(K) = Sum (L)
proof
let K be Linear_Combination of W;
defpred P[object,object] means
($1 in W & $2 = K.$1) or (not $1 in W & $2 = 0.GF);
reconsider K9= K as Function of the carrier of W, the carrier of GF;
A1: the carrier of W c= the carrier of V by VECTSP_4:def 2;
then reconsider C = Carrier(K) as finite Subset of V by XBOOLE_1:1;
A2: for x being object st x in the carrier of V
ex y being object st y in the carrier of GF & P[x, y]
proof
let x be object;
assume x in the carrier of V;
then reconsider x as Vector of V;
per cases;
suppose
A3: x in W;
then reconsider x as Vector of W by STRUCT_0:def 5;
P[x, K.x] by A3;
hence thesis;
end;
suppose
not x in W;
hence thesis;
end;
end;
ex L being Function of the carrier of V, the carrier of GF st
for x being object st x
in the carrier of V holds P[x, L.x] from FUNCT_2:sch 1(A2);
then consider
L being Function of the carrier of V, the carrier of GF such that
A4: for x being object st x in the carrier of V holds P[x, L.x];
A5: now
let v be Vector of V;
assume not v in C;
then P[v, K.v] & not v in C & v in the carrier of W or P[v, 0.GF] by
STRUCT_0:def 5;
then P[v, K.v] & K.v = 0.GF or P[v, 0.GF] by VECTSP_6:2;
hence L.v = 0.GF by A4;
end;
L is Element of Funcs(the carrier of V, the carrier of GF) by FUNCT_2:8;
then reconsider L as Linear_Combination of V by A5,VECTSP_6:def 1;
reconsider L9= L|the carrier of W as Function of the carrier of W, the
carrier of GF by A1,FUNCT_2:32;
take L;
now
let x be object;
assume that
A6: x in Carrier(L) and
A7: not x in the carrier of W;
consider v being Vector of V such that
A8: x = v and
A9: L.v <> 0.GF by A6,VECTSP_6:1;
P[v, 0.GF] by A7,A8,STRUCT_0:def 5;
hence contradiction by A4,A9;
end;
then
A10: Carrier(L) c= the carrier of W;
now
let x be object;
assume
A11: x in the carrier of W;
then P[x, L.x] by A4,A1;
hence K9.x = L9.x by A11,FUNCT_1:49,STRUCT_0:def 5;
end;
then K9 = L9 by FUNCT_2:12;
hence thesis by A10,Th7;
end;
theorem Th9:
for L being Linear_Combination of V st Carrier(L) c= the carrier
of W holds ex K being Linear_Combination of W st Carrier(K) = Carrier(L) & Sum(
K) = Sum (L)
proof
let L be Linear_Combination of V;
assume
A1: Carrier(L) c= the carrier of W;
then reconsider C = Carrier(L) as finite Subset of W;
the carrier of W c= the carrier of V by VECTSP_4:def 2;
then reconsider K = L|the carrier of W as Function of the carrier of W, the
carrier of GF by FUNCT_2:32;
A2: K is Element of Funcs(the carrier of W, the carrier of GF) by FUNCT_2:8;
A3: dom K = the carrier of W by FUNCT_2:def 1;
now
let w be Vector of W;
A4: w is Vector of V by VECTSP_4:10;
assume not w in C;
then L.w = 0.GF by A4,VECTSP_6:2;
hence K.w = 0.GF by A3,FUNCT_1:47;
end;
then reconsider K as Linear_Combination of W by A2,VECTSP_6:def 1;
take K;
thus thesis by A1,Th7;
end;
:: More On Linear Independence & Basis
theorem Th10:
for I being Basis of V, v being Vector of V holds v in Lin(I)
proof
let I be Basis of V, v be Vector of V;
v in the ModuleStr of V by STRUCT_0:def 5;
hence thesis by VECTSP_7:def 3;
end;
registration
let GF, V;
cluster linearly-independent for Subset of V;
existence
proof
take {}V;
thus thesis;
end;
end;
theorem Th11:
for A being Subset of W st A is linearly-independent holds A is
linearly-independent Subset of V
proof
let A be Subset of W;
the carrier of W c= the carrier of V by VECTSP_4:def 2;
then reconsider A9= A as Subset of V by XBOOLE_1:1;
assume
A1: A is linearly-independent;
now
assume A9 is linearly-dependent;
then consider L being Linear_Combination of A9 such that
A2: Sum(L) = 0.V and
A3: Carrier(L) <> {} by VECTSP_7:def 1;
Carrier(L) c= A9 by VECTSP_6:def 4;
then consider LW being Linear_Combination of W such that
A4: Carrier(LW) = Carrier(L) and
A5: Sum(LW) = Sum(L) by Th9,XBOOLE_1:1;
reconsider LW as Linear_Combination of A by A4,VECTSP_6:def 4;
Sum(LW) = 0.W by A2,A5,VECTSP_4:11;
hence contradiction by A1,A3,A4,VECTSP_7:def 1;
end;
hence thesis;
end;
theorem Th12:
for A being Subset of V st A is linearly-independent & A c= the
carrier of W holds A is linearly-independent Subset of W
proof
let A be Subset of V such that
A1: A is linearly-independent and
A2: A c= the carrier of W;
reconsider A9= A as Subset of W by A2;
now
assume A9 is linearly-dependent;
then consider K being Linear_Combination of A9 such that
A3: Sum(K) = 0.W and
A4: Carrier(K) <> {} by VECTSP_7:def 1;
consider L being Linear_Combination of V such that
A5: Carrier(L) = Carrier(K) and
A6: Sum(L) = Sum(K) by Th8;
reconsider L as Linear_Combination of A by A5,VECTSP_6:def 4;
Sum(L) = 0.V by A3,A6,VECTSP_4:11;
hence contradiction by A1,A4,A5,VECTSP_7:def 1;
end;
hence thesis;
end;
theorem Th13:
for A being Basis of W ex B being Basis of V st A c= B
proof
let A be Basis of W;
A is linearly-independent by VECTSP_7:def 3;
then reconsider B = A as linearly-independent Subset of V by Th11;
consider I being Basis of V such that
A1: B c= I by VECTSP_7:19;
take I;
thus thesis by A1;
end;
theorem Th14:
for A being Subset of V st A is linearly-independent for v being
Vector of V st v in A for B being Subset of V st B = A \ {v} holds not v in Lin
(B)
proof
let A be Subset of V such that
A1: A is linearly-independent;
let v be Vector of V;
assume v in A;
then
A2: {v} is Subset of A by SUBSET_1:41;
v in {v} by TARSKI:def 1;
then v in Lin({v}) by VECTSP_7:8;
then consider K being Linear_Combination of {v} such that
A3: v = Sum(K) by VECTSP_7:7;
let B be Subset of V such that
A4: B = A \ {v};
B c= A by A4,XBOOLE_1:36;
then
A5: B \/ {v} c= A \/ A by A2,XBOOLE_1:13;
assume v in Lin(B);
then consider L being Linear_Combination of B such that
A6: v = Sum(L) by VECTSP_7:7;
A7: Carrier(L) c= B & Carrier(K) c= {v} by VECTSP_6:def 4;
then Carrier(L) \/ Carrier(K) c= B \/ {v} by XBOOLE_1:13;
then Carrier(L - K) c= Carrier(L) \/ Carrier(K) & Carrier(L) \/ Carrier(K)
c= A by A5,VECTSP_6:41;
then Carrier(L - K) c= A;
then
A8: L - K is Linear_Combination of A by VECTSP_6:def 4;
A9: for x being Vector of V holds x in Carrier(L) implies K.x = 0.GF
proof
let x be Vector of V;
assume x in Carrier(L);
then not x in Carrier(K) by A4,A7,XBOOLE_0:def 5;
hence thesis by VECTSP_6:2;
end;
A10: now
let x be set such that
A11: x in Carrier(L) and
A12: not x in Carrier(L - K);
reconsider x as Vector of V by A11;
A13: L.x <> 0.GF by A11,VECTSP_6:2;
(L - K).x = L.x - K.x by VECTSP_6:40
.= L.x - 0.GF by A9,A11
.= L.x + (-0.GF) by RLVECT_1:def 11
.= L.x + 0.GF by RLVECT_1:12
.= L.x by RLVECT_1:4;
hence contradiction by A12,A13,VECTSP_6:2;
end;
{v} is linearly-independent by A1,A2,VECTSP_7:1;
then v <> 0.V by VECTSP_7:3;
then Carrier(L) <> {} by A6,VECTSP_6:19;
then ex w being object st w in Carrier(L) by XBOOLE_0:def 1;
then
A14: Carrier(L - K) is non empty by A10;
0.V = Sum(L) + (- Sum(K)) by A6,A3,RLVECT_1:def 10
.= Sum(L) + Sum(-K) by VECTSP_6:46
.= Sum(L + (- K)) by VECTSP_6:44
.= Sum(L - K) by VECTSP_6:def 11;
hence contradiction by A1,A8,A14,VECTSP_7:def 1;
end;
theorem Th15:
for I being Basis of V for A being non empty Subset of V st A
misses I for B being Subset of V st B = I \/ A holds B is linearly-dependent
proof
let I be Basis of V;
let A be non empty Subset of V such that
A1: A misses I;
consider v being object such that
A2: v in A by XBOOLE_0:def 1;
let B be Subset of V such that
A3: B = I \/ A;
A4: A c= B by A3,XBOOLE_1:7;
reconsider v as Vector of V by A2;
reconsider Bv = B \ {v} as Subset of V;
A5: I \ {v} c= B \ {v} by A3,XBOOLE_1:7,33;
not v in I by A1,A2,XBOOLE_0:3;
then I c= Bv by A5,ZFMISC_1:57;
then
A6: Lin(I) is Subspace of Lin(Bv) by VECTSP_7:13;
assume
A7: B is linearly-independent;
v in Lin(I) by Th10;
hence contradiction by A7,A2,A4,A6,Th14,VECTSP_4:8;
end;
theorem Th16:
for A being Subset of V st A c= the carrier of W holds Lin(A) is
Subspace of W
proof
let A be Subset of V;
assume
A1: A c= the carrier of W;
now
let w be object;
assume w in the carrier of Lin(A);
then w in Lin(A) by STRUCT_0:def 5;
then consider L being Linear_Combination of A such that
A2: w = Sum(L) by VECTSP_7:7;
Carrier(L) c= A by VECTSP_6:def 4;
then
ex K being Linear_Combination of W st Carrier(K) = Carrier (L) & Sum(L)
= Sum(K) by A1,Th9,XBOOLE_1:1;
hence w in the carrier of W by A2;
end;
then the carrier of Lin(A) c= the carrier of W;
hence thesis by VECTSP_4:27;
end;
theorem Th17:
for A being Subset of V, B being Subset of W st A = B holds Lin( A) = Lin(B)
proof
let A be Subset of V, B be Subset of W;
reconsider B9= Lin(B), V9= V as VectSp of GF;
A1: B9 is Subspace of V9 by VECTSP_4:26;
assume
A2: A = B;
now
let x be object;
assume x in the carrier of Lin(A);
then x in Lin(A) by STRUCT_0:def 5;
then consider L being Linear_Combination of A such that
A3: x = Sum(L) by VECTSP_7:7;
Carrier(L) c= A by VECTSP_6:def 4;
then consider K being Linear_Combination of W such that
A4: Carrier(K) = Carrier(L) and
A5: Sum(K) = Sum(L) by A2,Th9,XBOOLE_1:1;
reconsider K as Linear_Combination of B by A2,A4,VECTSP_6:def 4;
x = Sum(K) by A3,A5;
then x in Lin(B) by VECTSP_7:7;
hence x in the carrier of Lin(B) by STRUCT_0:def 5;
end;
then
A6: the carrier of Lin(A) c= the carrier of Lin(B);
now
let x be object;
assume x in the carrier of Lin(B);
then x in Lin(B) by STRUCT_0:def 5;
then consider K being Linear_Combination of B such that
A7: x = Sum(K) by VECTSP_7:7;
consider L being Linear_Combination of V such that
A8: Carrier(L) = Carrier(K) and
A9: Sum(L) = Sum(K) by Th8;
reconsider L as Linear_Combination of A by A2,A8,VECTSP_6:def 4;
x = Sum(L) by A7,A9;
then x in Lin(A) by VECTSP_7:7;
hence x in the carrier of Lin(A) by STRUCT_0:def 5;
end;
then the carrier of Lin(B) c= the carrier of Lin(A);
then the carrier of Lin(A) = the carrier of Lin(B) by A6,XBOOLE_0:def 10;
hence thesis by A1,VECTSP_4:29;
end;
begin
::
:: Steinitz Theorem
::
:: Exchange Lemma
theorem Th18:
for A, B being finite Subset of V
for 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 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,VECTSP_7:7;
v in {v} by TARSKI:def 1;
then v in Lin({v}) by VECTSP_7:8;
then consider Lv being Linear_Combination of {v} such that
A4: v = Sum(Lv) by VECTSP_7:7;
A5: Carrier(L) c= A \/ B by VECTSP_6:def 4;
now
assume
A6: for w being Vector of V st w in A holds L.w = 0.GF;
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.GF by A7,VECTSP_6:1;
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 VECTSP_6:def 4;
hence contradiction by A2,A3,VECTSP_7:7;
end;
then consider w being Vector of V such that
A9: w in A and
A10: L.w <> 0.GF;
set a = L.w;
take w;
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 VECTSP_6:def 6;
A14: w in Carrier(L) by A10,VECTSP_6:1;
then reconsider Fw1 = F -| w as FinSequence of the carrier of V by A12,
FINSEQ_4:41;
reconsider Fw2 = F |-- w as FinSequence of the carrier of V by A12,A14,
FINSEQ_4:50;
A15: rng Fw1 misses rng Fw2 by A11,A12,A14,FINSEQ_4:57;
set Fw = Fw1 ^ Fw2;
F just_once_values w by A11,A12,A14,FINSEQ_4:8;
then
A16: Fw = F - {w} by FINSEQ_4:54;
then
A17: rng Fw = Carrier(L) \ {w} by A12,FINSEQ_3:65;
F = (F -| w) ^ <* w *> ^ (F |-- w) by A12,A14,FINSEQ_4:51;
then F = Fw1 ^ (<* w *> ^ Fw2) by FINSEQ_1:32;
then L (#) F = (L (#) Fw1) ^ (L (#) (<* w *> ^ Fw2)) by VECTSP_6:13
.= (L (#) Fw1) ^ ((L (#) <* w *>) ^ (L (#) Fw2)) by VECTSP_6:13
.= (L (#) Fw1) ^ (L (#) <* w *>) ^ (L (#) Fw2) by FINSEQ_1:32
.= (L (#) Fw1) ^ <* a*w *> ^ (L (#) Fw2) by VECTSP_6:10;
then
A18: 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 VECTSP_6:13;
consider K being Linear_Combination of V such that
A19: Carrier(K) = rng Fw /\ Carrier(L) and
A20: L (#) Fw = K (#) Fw by Th4;
rng Fw = rng F \ {w} by A16,FINSEQ_3:65;
then
A21: Carrier(K) = rng Fw by A12,A19,XBOOLE_1:28;
A22: Carrier(L) \ {w} c= A \/ B \ {w} by A5,XBOOLE_1:33;
then reconsider K as Linear_Combination of (A \/ B \ {w}) by A17,A21,
VECTSP_6:def 4;
set LC = a"*(-K + Lv);
Carrier (-K + Lv) c= Carrier(-K) \/ Carrier(Lv) by VECTSP_6:23;
then
A23: Carrier (-K + Lv) c= Carrier(K) \/ Carrier(Lv) by VECTSP_6:38;
Carrier(Lv) c= {v} by VECTSP_6:def 4;
then Carrier(K) \/ Carrier(Lv) c= A \/ B \ {w} \/ {v} by A17,A21,A22,
XBOOLE_1:13;
then Carrier (a"*(-K + Lv)) c= Carrier(-K + Lv) & Carrier (-K + Lv) c= A \/
B \ { w} \/ {v} by A23,VECTSP_6:28;
then Carrier (LC) c= A \/ B \ {w} \/ {v};
then
A24: LC is Linear_Combination of (A \/ B \ {w} \/ {v}) by VECTSP_6:def 4;
Fw1 is one-to-one & Fw2 is one-to-one by A11,A12,A14,FINSEQ_4:52,53;
then Fw is one-to-one by A15,FINSEQ_3:91;
then Sum(K (#) Fw) = Sum(K) by A21,VECTSP_6:def 6;
then a"*v = a"*Sum(K) + a"*(a*w) by A3,A13,A18,A20,VECTSP_1:def 14
.= a"*Sum(K) + w by A10,VECTSP_1:20;
then w = a"*v - a"*Sum(K) by VECTSP_2:2
.= a"*(v - Sum(K)) by VECTSP_1:23
.= a"*(-Sum(K) + v) by RLVECT_1:def 11;
then w = a"*(Sum(-K) + Sum(Lv)) by A4,VECTSP_6:46
.= a"*Sum(-K + Lv) by VECTSP_6:44
.= Sum(a"*(-K + Lv)) by VECTSP_6:45;
hence thesis by A9,A24,VECTSP_7:7;
end;
::$N Steinitz Theorem
theorem Th19:
for A, B being finite Subset of V st the ModuleStr 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 ModuleStr of V = Lin(B \/ C)
proof
defpred P[Nat] means for n being Nat for A, B being finite Subset of V st
card(A) = n & card(B) = $1 & the ModuleStr 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 ModuleStr 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 Nat;
let A, B be finite Subset of V such that
A3: card(A) = n and
A4: card(B) = m + 1 and
A5: the ModuleStr 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,VECTSP_7:1,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 ModuleStr of V = Lin(Bv \/ C) by A2,A3,A5,A8;
A13: not v in Lin(Bv) by A6,A7,Th14;
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 ModuleStr of V = Lin(Bv \/ C) by A2,A3,A5,A9,A8;
C = {} by A15;
then Bv is Basis of V by A8,A16,VECTSP_7:def 3;
hence contradiction by A13,Th10;
end;
v in Lin(Bv \/ C) by A12,STRUCT_0:def 5;
then consider w being Vector of V such that
A17: w in C and
A18: w in Lin(C \/ Bv \ {w} \/ {v}) by A13,Th18;
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,
VECTSP_7:13;
then
A22: w in Lin(B \/ Cw) by A18,VECTSP_4:8;
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 TARSKI:def 1,VECTSP_7:8;
hence x in the carrier of Lin(B \/ Cw) by A22,STRUCT_0:def 5;
end;
then Bv \/ C c= the carrier of Lin(B \/ Cw);
then Lin(Bv \/ C) is Subspace of Lin(B \/ Cw) by Th16;
then
A24: the carrier of Lin(Bv \/ C) c= the carrier of Lin(B \/ Cw) by
VECTSP_4:def 2;
the carrier of Lin(B \/ Cw) c= the carrier of V by VECTSP_4:def 2;
then the carrier of Lin(B \/ Cw) = the carrier of V by A12,A24,
XBOOLE_0:def 10;
then
A25: the ModuleStr of V = Lin(B \/ Cw) by A12,VECTSP_4:29;
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 Nat;
let A, B be finite Subset of V such that
A27: card(A) = n and
A28: card(B) = 0 and
A29: the ModuleStr 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 holds P[m] from NAT_1:sch 2(A26, A1);
let A, B be finite Subset of V;
assume the ModuleStr of V = Lin(A) & B is linearly-independent;
hence thesis by A30;
end;
begin
::
:: Finite-Dimensional Vector Spaces
::
theorem Th20:
V is finite-dimensional implies for I being Basis of V holds I is finite
proof
assume V is finite-dimensional;
then consider A being finite Subset of V such that
A1: A is Basis of V by MATRLIN:def 1;
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 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 st i in dom
p & Sum(L) = p.i by A5;
then R c= B by VECTSP_6:def 4;
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;
then v in the ModuleStr of V by VECTSP_4:def 4;
then v in Lin(A) by A1,VECTSP_7:def 3;
then consider LA being Linear_Combination of A such that
A6: v = Sum(LA) by VECTSP_7:7;
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 Th10;
then consider LB being Linear_Combination of B such that
A8: w = Sum(LB) by VECTSP_7:7;
A9: Carrier(LA) c= A by VECTSP_6:def 4;
ex i st i in dom p & w = p.i
proof
consider i being object such that
A10: i in dom p and
A11: w = p.i by A2,A7,A9,FUNCT_1:def 3;
reconsider i as Element of NAT by A10;
take i;
thus thesis by A10,A11;
end;
then
A12: Carrier(LB) in Car by A8;
Carrier(LB) c= C
by A12,TARSKI:def 4;
then LB is Linear_Combination of C by VECTSP_6:def 4;
then w in Lin(C) by A8,VECTSP_7:7;
hence thesis by STRUCT_0:def 5;
end;
then ex LC being Linear_Combination of C st Sum(LA) = Sum(LC) by Th6;
hence v in Lin(C) by A6,VECTSP_7:7;
end;
assume v in Lin(C);
v in the carrier of the ModuleStr of V;
then v in the carrier of (Omega).V by VECTSP_4:def 4;
hence thesis by STRUCT_0:def 5;
end;
then (Omega).V = Lin(C) by VECTSP_4:30;
then
A13: the ModuleStr of V = Lin(C) by VECTSP_4:def 4;
A14: B is linearly-independent by VECTSP_7:def 3;
then C is linearly-independent by A3,VECTSP_7:1;
then
A15: C is Basis of V by A13,VECTSP_7:def 3;
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 A14,A15,Th15,XBOOLE_1:79;
end;
then
A16: B = C by A3,XBOOLE_0:def 10;
defpred P[set, object] means
ex L being Linear_Combination of B st $2 = Carrier
(L) & Sum(L) = p.$1;
A17: 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 Th10;
then consider L being Linear_Combination of B such that
A18: p.i = Sum(L) by VECTSP_7:7;
P[i, Carrier(L)] by A18;
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(A17);
then consider q being FinSequence such that
A19: dom q = Seg len p and
A20: for i being Nat st i in Seg len p holds P[i, q.i];
A21: dom p = dom q by A19,FINSEQ_1:def 3;
A22: for i being Nat, y1, y2 st i in Seg len p & P[i, y1] & P[i, y2] holds
y1 = y2
proof
let i be Nat, y1, y2;
assume that
i in Seg len p and
A23: P[i, y1] and
A24: P[i, y2];
consider L1 being Linear_Combination of B such that
A25: y1 = Carrier(L1) & Sum(L1) = p.i by A23;
consider L2 being Linear_Combination of B such that
A26: y2 = Carrier(L2) & Sum(L2) = p.i by A24;
Carrier(L1) c= B & Carrier(L2) c= B by VECTSP_6:def 4;
hence thesis by A14,A25,A26,MATRLIN:5;
end;
now
let x be object;
assume x in Car;
then consider L being Linear_Combination of B such that
A27: x = Carrier(L) and
A28: ex i st i in dom p & Sum(L) = p.i;
consider i such that
A29: i in dom p and
A30: Sum(L) = p.i by A28;
P[i, q.i] by A19,A20,A21,A29;
then x = q.i by A22,A19,A21,A27,A29,A30;
hence x in rng q by A21,A29,FUNCT_1:def 3;
end;
then
A31: 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 st i in
dom p & Sum(L) = p.i;
hence thesis;
end;
hence thesis by A16,A31,FINSET_1:7;
end;
registration
let F be Field;
let U be finite-dimensional VectSp of F;
cluster -> finite for Basis of U;
coherence by Th20;
end;
theorem
V is finite-dimensional implies for A being Subset of V st
A is linearly-independent holds A is finite
proof
assume
A1: V is finite-dimensional;
let A be Subset of V;
assume A is linearly-independent;
then consider B being Basis of V such that
A2: A c= B by VECTSP_7:19;
B is finite by A1;
hence thesis by A2;
end;
theorem Th22:
V is finite-dimensional implies for A, B being Basis of V holds
card A = card B
proof
assume
A1: V is finite-dimensional;
let A, B be Basis of V;
reconsider A9= A, B9= B as finite Subset of V by A1;
the ModuleStr of V = Lin(B) & A9 is linearly-independent by VECTSP_7:def 3;
then
A2: card A9 <= card B9 by Th19;
the ModuleStr of V = Lin(A) & B9 is linearly-independent by VECTSP_7:def 3;
then card B9 <= card A9 by Th19;
hence thesis by A2,XXREAL_0:1;
end;
theorem Th23:
(0).V is finite-dimensional
proof
reconsider V9= (0).V as strict VectSp of GF;
reconsider I = {}(the carrier of V9) as finite Subset of V9;
the carrier of V9 = {0.V} by VECTSP_4:def 3
.= {0.V9} by VECTSP_4:11
.= the carrier of (0).V9 by VECTSP_4:def 3;
then
A1: V9 = (0).V9 by VECTSP_4:31;
Lin(I) = (0).V9 by VECTSP_7:9;
then I is Basis of V9 by A1,VECTSP_7:def 3;
hence thesis by MATRLIN:def 1;
end;
theorem Th24:
V is finite-dimensional implies W is finite-dimensional
proof
set A = the Basis of W;
consider I being Basis of V such that
A1: A c= I by Th13;
assume V is finite-dimensional;
then I is finite;
hence thesis by A1,MATRLIN:def 1;
end;
registration
let GF be Field, V be VectSp of GF;
cluster strict finite-dimensional for Subspace of V;
existence
proof
take (0).V;
thus thesis by Th23;
end;
end;
registration
let GF be Field, V be finite-dimensional VectSp of GF;
cluster -> finite-dimensional for Subspace of V;
correctness by Th24;
end;
registration
let GF be Field, V be finite-dimensional VectSp of GF;
cluster strict for Subspace of V;
existence
proof
(0).V is strict finite-dimensional Subspace of V;
hence thesis;
end;
end;
begin
::
:: Dimension of a Vector Space
::
definition
let GF be Field, V be VectSp of GF;
assume
A1: V is finite-dimensional;
func dim V -> Nat means
:Def1:
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,MATRLIN:def 1;
consider n being Nat such that
A3: n = card A;
for I being Basis of V holds card I = n by A1,A2,A3,Th22;
hence thesis;
end;
uniqueness
proof
let n, m;
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,MATRLIN:def 1;
card A = n by A4,A6;
hence thesis by A5,A6;
end;
end;
reserve V for finite-dimensional VectSp of GF,
W, W1, W2 for Subspace of V,
u, v for Vector of V;
theorem Th25:
dim W <= dim V
proof
set A = the Basis of W;
reconsider A as Subset of W;
A1: dim W = card A by Def1;
A is linearly-independent by VECTSP_7:def 3;
then reconsider B = A as linearly-independent Subset of V by Th11;
reconsider A9= B as finite Subset of V;
reconsider V9= V as VectSp of GF;
set I = the Basis of V9;
A2: Lin(I) = the ModuleStr of V9 by VECTSP_7:def 3;
reconsider I as finite Subset of V;
card A9 <= card I by A2,Th19;
hence thesis by A1,Def1;
end;
theorem Th26:
for A being Subset of V st A is linearly-independent holds
card A = dim Lin(A)
proof
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,VECTSP_7:8;
then reconsider B = A as linearly-independent Subset of W by A1,Th12,
TARSKI:def 3;
W = Lin(B) by Th17;
then reconsider B as Basis of W by VECTSP_7:def 3;
card B = dim W by Def1;
hence thesis;
end;
theorem Th27:
dim V = dim (Omega).V
proof
consider I being finite Subset of V such that
A1: I is Basis of V by MATRLIN:def 1;
A2: (Omega).V = the ModuleStr of V by VECTSP_4:def 4
.= Lin(I) by A1,VECTSP_7:def 3;
card I = dim V & I is linearly-independent by A1,Def1,VECTSP_7:def 3;
hence thesis by A2,Th26;
end;
theorem
dim V = dim W iff (Omega).V = (Omega).W
proof
consider A being finite Subset of V such that
A1: A is Basis of V by MATRLIN:def 1;
hereby
set A = the Basis of W;
consider B being Basis of V such that
A2: A c= B by Th13;
the carrier of W c= the carrier of V by VECTSP_4:def 2;
then reconsider A9= A as finite Subset of V by XBOOLE_1:1;
reconsider B9= B as finite Subset of V;
assume dim V = dim W;
then
A3: card A = dim V by Def1
.= card B by Def1;
A4: now
assume A <> B;
then A c< B by A2,XBOOLE_0:def 8;
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 ModuleStr of V by VECTSP_4:def 4
.= Lin(B) by VECTSP_7:def 3
.= Lin(A) by A4,Th17
.= the ModuleStr of W by VECTSP_7:def 3
.= (Omega).W by VECTSP_4:def 4;
hence (Omega).V = (Omega).W;
end;
consider B being finite Subset of W such that
A5: B is Basis of W by MATRLIN:def 1;
A6: A is linearly-independent by A1,VECTSP_7:def 3;
assume (Omega).V = (Omega).W;
then the ModuleStr of V = (Omega).W by VECTSP_4:def 4
.= the ModuleStr of W by VECTSP_4:def 4;
then
A7: Lin(A) = the ModuleStr of W by A1,VECTSP_7:def 3
.= Lin(B) by A5,VECTSP_7:def 3;
A8: B is linearly-independent by A5,VECTSP_7:def 3;
reconsider B as Subset of W;
reconsider A as Subset of V;
dim V = card A by A1,Def1
.= dim Lin(B) by A6,A7,Th26
.= card B by A8,Th26
.= dim W by A5,Def1;
hence thesis;
end;
theorem Th29:
dim V = 0 iff (Omega).V = (0).V
proof
consider I being finite Subset of V such that
A1: I is Basis of V by MATRLIN:def 1;
hereby
consider I being finite Subset of V such that
A2: I is Basis of V by MATRLIN:def 1;
assume dim V = 0;
then card I = 0 by A2,Def1;
then
A3: I = {}(the carrier of V);
(Omega).V = the ModuleStr of V by VECTSP_4:def 4
.= Lin(I) by A2,VECTSP_7:def 3
.= (0).V by A3,VECTSP_7:9;
hence (Omega).V = (0).V;
end;
A4: I <> {0.V} by A1,VECTSP_7:3,def 3;
assume (Omega).V = (0).V;
then the ModuleStr of V = (0).V by VECTSP_4:def 4;
then Lin(I) = (0).V by A1,VECTSP_7:def 3;
then I = {} or I = {0.V} by VECTSP_7:10;
hence thesis by A1,A4,Def1,CARD_1:27;
end;
theorem
dim V = 1 iff ex v st v <> 0.V & (Omega).V = Lin{v}
proof
hereby
consider I being finite Subset of V such that
A1: I is Basis of V by MATRLIN:def 1;
assume dim V = 1;
then card I = 1 by A1,Def1;
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,VECTSP_7:def 3;
then
A3: v <> 0.V by VECTSP_7:3;
Lin{v} = the ModuleStr of V by A1,A2,VECTSP_7:def 3;
hence ex v st v <> 0.V & (Omega).V = Lin{v} by A3,VECTSP_4:def 4;
end;
given v such that
A4: v <> 0.V & (Omega).V = Lin{v};
{v} is linearly-independent & Lin{v} = the ModuleStr of V by A4,
VECTSP_4:def 4,VECTSP_7:3;
then
A5: {v} is Basis of V by VECTSP_7:def 3;
card {v} = 1 by CARD_1:30;
hence thesis by A5,Def1;
end;
theorem
dim V = 2 iff ex u, v st u <> v & {u, v} is linearly-independent &
(Omega).V = Lin{u, v}
proof
hereby
consider I being finite Subset of V such that
A1: I is Basis of V by MATRLIN:def 1;
assume dim V = 2;
then
A2: card I = 2 by A1,Def1;
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 be 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 be 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,XBOOLE_0:def 10;
then
A12: {u, v} is linearly-independent by A1,VECTSP_7:def 3;
Lin{u, v} = the ModuleStr of V by A1,A11,VECTSP_7:def 3
.= (Omega).V by VECTSP_4:def 4;
hence
ex u, v st u <> v & {u, v} is linearly-independent & (Omega).V = Lin{
u, v} by A6,A12;
end;
given u, v such that
A13: u <> v and
A14: {u, v} is linearly-independent and
A15: (Omega).V = Lin{u, v};
Lin{u, v} = the ModuleStr of V by A15,VECTSP_4:def 4;
then
A16: {u, v} is Basis of V by A14,VECTSP_7:def 3;
card {u, v} = 2 by A13,CARD_2:57;
hence thesis by A16,Def1;
end;
theorem Th32:
dim(W1 + W2) + dim(W1 /\ W2) = dim W1 + dim W2
proof
reconsider V as VectSp of GF;
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 MATRLIN:def 1;
W1 /\ W2 is Subspace of W2 by VECTSP_5:15;
then consider I2 being Basis of W2 such that
A2: I c= I2 by A1,Th13;
W1 /\ W2 is Subspace of W1 by VECTSP_5:15;
then consider I1 being Basis of W1 such that
A3: I c= I1 by A1,Th13;
reconsider I2 as finite Subset of W2;
reconsider I1 as finite Subset of W1;
A4: now
I1 is linearly-independent by VECTSP_7:def 3;
then reconsider I19 = I1 as linearly-independent Subset of V by Th11;
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 VECTSP_7:8;
then x in the ModuleStr of W1 by VECTSP_7:def 3;
then
A7: x in the carrier of W1 by STRUCT_0:def 5;
A8: the carrier of W1 c= the carrier of V by VECTSP_4:def 2;
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 VECTSP_4:def 2;
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 VECTSP_7:8;
then x in the ModuleStr of W2 by VECTSP_7:def 3;
then x in the carrier of W2 by STRUCT_0:def 5;
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 VECTSP_5:def 2;
then
A12: x in the ModuleStr of W1 /\ W2 by STRUCT_0:def 5;
the carrier of W1 /\ W2 c= the carrier of V by VECTSP_4:def 2;
then reconsider I9= I as Subset of V by XBOOLE_1:1;
A13: Lin(I) = Lin(I9) by Th17;
Ix \ {x} = I \ {x} by XBOOLE_1:40
.= I by A6,ZFMISC_1:57;
then not x9 in Lin(I9) by A10,A11,Th14,VECTSP_7:1;
hence contradiction by A1,A12,A13,VECTSP_7:def 3;
end;
set A = I1 \/ I2;
now
let v be object;
A14: the carrier of W1 c= the carrier of V & the carrier of W2 c= the
carrier of V by VECTSP_4:def 2;
assume v in A;
then
A15: 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 A14;
v9 in W1 or v9 in W2 by A15,STRUCT_0:def 5;
then v9 in W1 + W2 by VECTSP_5:2;
hence v in the carrier of W1 + W2 by STRUCT_0:def 5;
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,XBOOLE_0:def 10;
then
A16: 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 VECTSP_5:7
,VECTSP_7:def 3;
then reconsider I19 = I1 as linearly-independent Subset of W1 + W2 by Th11;
reconsider W29= W2 as Subspace of W1 + W2 by VECTSP_5:7;
reconsider W19= W1 as Subspace of W1 + W2 by VECTSP_5:7;
let L be Linear_Combination of A;
assume
A17: Sum(L) = 0.(W1 + W2);
A18: 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
A19: F is one-to-one and
A20: rng F = Carrier(L) and
A21: Sum(L) = Sum(L (#) F) by VECTSP_6:def 6;
reconsider B as Subset of rng F by A20,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
A22: Carrier(L1) = rng F1 /\ Carrier(L) and
A23: L1 (#) F1 = L (#) F1 by Th4;
F1 is one-to-one by A19,FINSEQ_3:87;
then
A24: Sum(L (#) F1) = Sum(L1) by A22,A23,Th3,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
A25: Carrier(L2) = rng F2 /\ Carrier(L) and
A26: L2 (#) F2 = L (#) F2 by Th4;
F2 is one-to-one by A19,FINSEQ_3:87;
then
A27: Sum(L (#) F2) = Sum(L2) by A25,A26,Th3,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
A28: Carrier(L1) = I1 /\ (Carrier(L) /\ Carrier(L)) by A22,XBOOLE_1:16
.= Carrier(L) /\ I1;
then consider K1 being Linear_Combination of W19 such that
Carrier(K1) = Carrier(L1) and
A29: Sum(K1) = Sum(L1) by Th9;
rng F2 = Carrier(L) \ (Carrier(L) /\ I1) by A20,FINSEQ_3:65
.= Carrier(L) \ I1 by XBOOLE_1:47;
then
A30: Carrier(L2) = Carrier(L) \ I1 by A25,XBOOLE_1:28,36;
then Carrier(L1) /\ Carrier(L2) = Carrier(L) /\ (I1 /\ (Carrier(L) \ I1))
by A28,XBOOLE_1:16
.= Carrier(L) /\ {} by A18,XBOOLE_0:def 7
.= {};
then
A31: Carrier(L1) misses Carrier(L2) by XBOOLE_0:def 7;
A32: Carrier(L) c= I1 \/ I2 by VECTSP_6:def 4;
then
A33: Carrier(L2) c= I2 by A30,XBOOLE_1:43;
Carrier(L2) c= I2 by A32,A30,XBOOLE_1:43;
then consider K2 being Linear_Combination of W29 such that
Carrier(K2) = Carrier(L2) and
A34: Sum(K2) = Sum(L2) by Th9,XBOOLE_1:1;
A35: Sum(K1) in W1 by STRUCT_0:def 5;
ex P being Permutation of dom F st (F - B`) ^ (F - B) = F *P by
FINSEQ_3:115;
then
A36: 0.(W1 + W2) = Sum(L (#) (F1^F2)) by A17,A21,Th1
.= Sum((L (#) F1) ^ (L (#) F2)) by VECTSP_6:13
.= Sum(L1) + Sum(L2) by A24,A27,RLVECT_1:41;
then Sum(L1) = - Sum(L2) by VECTSP_1:16
.= - Sum(K2) by A34,VECTSP_4:15;
then Sum(K1) in W2 by A29,STRUCT_0:def 5;
then Sum(K1) in W1 /\ W2 by A35,VECTSP_5:3;
then Sum(K1) in Lin(I) by A1,VECTSP_7:def 3;
then consider KI being Linear_Combination of I such that
A37: Sum(K1) = Sum(KI) by VECTSP_7:7;
A38: Carrier(L) = Carrier(L1) \/ Carrier(L2) by A28,A30,XBOOLE_1:51;
A39: now
assume not Carrier(L) c= Carrier(L1 + L2);
then consider x being object such that
A40: x in Carrier(L) and
A41: not x in Carrier(L1 + L2);
reconsider x as Vector of W1 + W2 by A40;
A42: 0.GF = (L1 + L2).x by A41,VECTSP_6:2
.= L1.x + L2.x by VECTSP_6:22;
per cases by A38,A40,XBOOLE_0:def 3;
suppose
A43: x in Carrier(L1);
then not x in Carrier(L2) by A31,XBOOLE_0:3;
then
A44: L2.x = 0.GF by VECTSP_6:2;
ex v being Vector of W1 + W2 st x = v & L1.v <> 0.GF by A43,VECTSP_6:1;
hence contradiction by A42,A44,RLVECT_1:4;
end;
suppose
A45: x in Carrier(L2);
then not x in Carrier(L1) by A31,XBOOLE_0:3;
then
A46: L1.x = 0.GF by VECTSP_6:2;
ex v being Vector of W1 + W2 st x = v & L2.v <> 0.GF by A45,VECTSP_6:1;
hence contradiction by A42,A46,RLVECT_1:4;
end;
end;
A47: I \/ I2 = I2 by A2,XBOOLE_1:12;
A48: I2 is linearly-independent by VECTSP_7:def 3;
A49: Carrier(L1) c= I1 by A28,XBOOLE_1:17;
W1 /\ W2 is Subspace of W1 + W2 by VECTSP_5:23;
then consider LI being Linear_Combination of W1 + W2 such that
A50: Carrier(LI) = Carrier(KI) and
A51: Sum(LI) = Sum(KI) by Th8;
Carrier(LI) c= I by A50,VECTSP_6:def 4;
then Carrier(LI) c= I19 by A3;
then
A52: LI = L1 by A49,A29,A37,A51,MATRLIN:5;
Carrier(LI) c= I by A50,VECTSP_6:def 4;
then Carrier(LI + L2) c= Carrier(LI) \/ Carrier(L2) & Carrier(LI) \/
Carrier(L2) c= I2 by A47,A33,VECTSP_6:23,XBOOLE_1:13;
then
A53: Carrier(LI + L2) c= I2;
W2 is Subspace of W1 + W2 by VECTSP_5:7;
then consider K being Linear_Combination of W2 such that
A54: Carrier(K) = Carrier(LI + L2) and
A55: Sum(K) = Sum(LI + L2) by A53,Th9,XBOOLE_1:1;
reconsider K as Linear_Combination of I2 by A53,A54,VECTSP_6:def 4;
0.W2 = Sum(LI) + Sum(L2) by A29,A36,A37,A51,VECTSP_4:12
.= Sum(K) by A55,VECTSP_6:44;
then {} = Carrier(L1 + L2) by A54,A52,A48,VECTSP_7:def 1;
hence thesis by A39;
end;
then
A56: A is linearly-independent by VECTSP_7:def 1;
the carrier of W1 + W2 c= the carrier of V by VECTSP_4:def 2;
then reconsider A9= A as Subset of V by XBOOLE_1:1;
A57: card I2 = dim W2 by Def1;
now
let x be object;
assume x in the carrier of W1 + W2;
then x in W1 + W2 by STRUCT_0:def 5;
then consider w1, w2 being Vector of V such that
A58: w1 in W1 and
A59: w2 in W2 and
A60: x = w1 + w2 by VECTSP_5:1;
reconsider w1 as Vector of W1 by A58,STRUCT_0:def 5;
w1 in Lin(I1) by Th10;
then consider K1 being Linear_Combination of I1 such that
A61: w1 = Sum(K1) by VECTSP_7:7;
reconsider w2 as Vector of W2 by A59,STRUCT_0:def 5;
w2 in Lin(I2) by Th10;
then consider K2 being Linear_Combination of I2 such that
A62: w2 = Sum(K2) by VECTSP_7:7;
consider L2 being Linear_Combination of V such that
A63: Carrier(L2) = Carrier(K2) and
A64: Sum(L2) = Sum(K2) by Th8;
A65: Carrier(L2) c= I2 by A63,VECTSP_6:def 4;
consider L1 being Linear_Combination of V such that
A66: Carrier(L1) = Carrier(K1) and
A67: Sum(L1) = Sum(K1) by Th8;
set L = L1 + L2;
Carrier(L1) c= I1 by A66,VECTSP_6:def 4;
then
Carrier(L) c= Carrier(L1) \/ Carrier(L2) & Carrier(L1) \/ Carrier(L2)
c= I1 \/ I2 by A65,VECTSP_6:23,XBOOLE_1:13;
then Carrier(L) c= I1 \/ I2;
then reconsider L as Linear_Combination of A9 by VECTSP_6:def 4;
x = Sum(L) by A60,A61,A67,A62,A64,VECTSP_6:44;
then x in Lin(A9) by VECTSP_7:7;
hence x in the carrier of Lin(A9) by STRUCT_0:def 5;
end;
then the carrier of W1 + W2 c= the carrier of Lin(A9);
then
A68: W1 + W2 is Subspace of Lin(A9) by VECTSP_4:27;
Lin(A9) = Lin(A) by Th17;
then Lin(A) = W1 + W2 by A68,VECTSP_4:25;
then
A69: A is Basis of W1 + W2 by A56,VECTSP_7:def 3;
card I = dim(W1 /\ W2) by A1,Def1;
then dim(W1 + W2) + dim(W1 /\ W2) = card I1 + card I2 + - card I + card I
by A16,A69,Def1
.= dim W1 + dim W2 by A57,Def1;
hence thesis;
end;
theorem
dim(W1 /\ W2) >= dim W1 + dim W2 - dim V
proof
A1: dim(W1 + W2) <= dim V & dim V + (dim(W1 /\ W2) - dim V) = dim(W1 /\ W2)
by Th25;
dim W1 + dim W2 - dim V = dim(W1 + W2) + dim(W1 /\ W2) - dim V by Th32
.= dim(W1 + W2) + (dim(W1 /\ W2) - dim V);
hence thesis by A1,XREAL_1:6;
end;
theorem
V is_the_direct_sum_of W1, W2 implies dim V = dim W1 + dim W2
proof
assume
A1: V is_the_direct_sum_of W1, W2;
then
A2: the ModuleStr of V = W1 + W2 by VECTSP_5:def 4;
W1 /\ W2 = (0).V by A1,VECTSP_5:def 4;
then (Omega).(W1 /\ W2) = (0).V by VECTSP_4:def 4
.= (0).(W1 /\ W2) by VECTSP_4:36;
then dim(W1 /\ W2) = 0 by Th29;
then dim W1 + dim W2 = dim(W1 + W2) + 0 by Th32
.= dim (Omega).V by A2,VECTSP_4:def 4
.= dim V by Th27;
hence thesis;
end;
::
:: Fixed-Dimensional Subspace Family and Pencil of Subspaces
::
Lm2: n <= dim V implies ex W being strict Subspace of V st dim W = n
proof
consider I being finite Subset of V such that
A1: I is Basis of V by MATRLIN:def 1;
assume n <= dim V;
then n <= card I by A1,Def1;
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,VECTSP_7:def 3;
then dim W = n by A2,Th26,VECTSP_7:1;
hence thesis;
end;
theorem
n <= dim V iff ex W being strict Subspace of V st dim W = n by Lm2,Th25;
definition
let GF be Field, V be finite-dimensional VectSp of GF, n be Nat;
func n Subspaces_of V -> set means
:Def2:
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,Th26;
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 MATRLIN:def 1;
reconsider A as Subset of W;
A is linearly-independent by A4,VECTSP_7:def 3;
then reconsider B = A as linearly-independent Subset of V by Th11;
A5: x = Lin(A) by A2,A4,VECTSP_7:def 3
.= Lin(B) by Th17;
then card B = n by A2,A3,Th26;
hence thesis by A5;
end;
hence thesis;
end;
uniqueness
proof let X1,X2 be set such that
A6: for x being object holds
x in X1 iff ex W being strict Subspace of V st W = x & dim W = n and
A7: for x being object holds
x in X2 iff ex W being strict Subspace of V st W = x & dim W = n;
now let x be object;
x in X1 iff ex W being strict Subspace of V st W = x & dim W = n by A6;
hence x in X1 iff x in X2 by A7;
end;
hence thesis by TARSKI:2;
end;
end;
theorem
n <= dim V implies n Subspaces_of V is non empty
proof
assume n <= dim V;
then ex W being strict Subspace of V st dim W = n by Lm2;
hence thesis by Def2;
end;
theorem
dim V < n implies n Subspaces_of V = {}
proof
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,Def2;
hence contradiction by A1,Th25;
end;
theorem
n Subspaces_of W c= n Subspaces_of V
proof
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 Def2;
reconsider W1 as strict Subspace of V by VECTSP_4:26;
W1 in n Subspaces_of V by A2,Def2;
hence thesis by A1;
end;