let K be Field; :: thesis: for V1 being finite-dimensional VectSp of K
for W1, W2 being Subspace of V1 st W1 /\ W2 = (0). V1 holds
for b1 being OrdBasis of W1
for b2 being OrdBasis of W2
for b being OrdBasis of W1 + W2 st b = b1 ^ b2 holds
for v, v1, v2 being Vector of (W1 + W2)
for w1 being Vector of W1
for w2 being Vector of W2 st v = v1 + v2 & v1 = w1 & v2 = w2 holds
v |-- b = (w1 |-- b1) ^ (w2 |-- b2)
let V1 be finite-dimensional VectSp of K; :: thesis: for W1, W2 being Subspace of V1 st W1 /\ W2 = (0). V1 holds
for b1 being OrdBasis of W1
for b2 being OrdBasis of W2
for b being OrdBasis of W1 + W2 st b = b1 ^ b2 holds
for v, v1, v2 being Vector of (W1 + W2)
for w1 being Vector of W1
for w2 being Vector of W2 st v = v1 + v2 & v1 = w1 & v2 = w2 holds
v |-- b = (w1 |-- b1) ^ (w2 |-- b2)
let W1, W2 be Subspace of V1; :: thesis: ( W1 /\ W2 = (0). V1 implies for b1 being OrdBasis of W1
for b2 being OrdBasis of W2
for b being OrdBasis of W1 + W2 st b = b1 ^ b2 holds
for v, v1, v2 being Vector of (W1 + W2)
for w1 being Vector of W1
for w2 being Vector of W2 st v = v1 + v2 & v1 = w1 & v2 = w2 holds
v |-- b = (w1 |-- b1) ^ (w2 |-- b2) )
assume A1: W1 /\ W2 = (0). V1 ; :: thesis: for b1 being OrdBasis of W1
for b2 being OrdBasis of W2
for b being OrdBasis of W1 + W2 st b = b1 ^ b2 holds
for v, v1, v2 being Vector of (W1 + W2)
for w1 being Vector of W1
for w2 being Vector of W2 st v = v1 + v2 & v1 = w1 & v2 = w2 holds
v |-- b = (w1 |-- b1) ^ (w2 |-- b2)
[#] ((0). V1) = {(0. V1)} by VECTSP_4:def 3;
then A2: card ([#] ((0). V1)) = 1 by CARD_1:30;
A3: (dim W1) + (dim W2) = (dim (W1 + W2)) + (dim (W1 /\ W2)) by VECTSP_9:32
.= (dim (W1 + W2)) + 0 by A1, A2, RANKNULL:5 ;
let b1 be OrdBasis of W1; :: thesis: for b2 being OrdBasis of W2
for b being OrdBasis of W1 + W2 st b = b1 ^ b2 holds
for v, v1, v2 being Vector of (W1 + W2)
for w1 being Vector of W1
for w2 being Vector of W2 st v = v1 + v2 & v1 = w1 & v2 = w2 holds
v |-- b = (w1 |-- b1) ^ (w2 |-- b2)
let b2 be OrdBasis of W2; :: thesis: for b being OrdBasis of W1 + W2 st b = b1 ^ b2 holds
for v, v1, v2 being Vector of (W1 + W2)
for w1 being Vector of W1
for w2 being Vector of W2 st v = v1 + v2 & v1 = w1 & v2 = w2 holds
v |-- b = (w1 |-- b1) ^ (w2 |-- b2)
let b be OrdBasis of W1 + W2; :: thesis: ( b = b1 ^ b2 implies for v, v1, v2 being Vector of (W1 + W2)
for w1 being Vector of W1
for w2 being Vector of W2 st v = v1 + v2 & v1 = w1 & v2 = w2 holds
v |-- b = (w1 |-- b1) ^ (w2 |-- b2) )
assume A4: b = b1 ^ b2 ; :: thesis: for v, v1, v2 being Vector of (W1 + W2)
for w1 being Vector of W1
for w2 being Vector of W2 st v = v1 + v2 & v1 = w1 & v2 = w2 holds
v |-- b = (w1 |-- b1) ^ (w2 |-- b2)
reconsider R = rng b as Basis of (W1 + W2) by MATRLIN:def 2;
let v, v1, v2 be Vector of (W1 + W2); :: thesis: for w1 being Vector of W1
for w2 being Vector of W2 st v = v1 + v2 & v1 = w1 & v2 = w2 holds
v |-- b = (w1 |-- b1) ^ (w2 |-- b2)
let w1 be Vector of W1; :: thesis: for w2 being Vector of W2 st v = v1 + v2 & v1 = w1 & v2 = w2 holds
v |-- b = (w1 |-- b1) ^ (w2 |-- b2)
let w2 be Vector of W2; :: thesis: ( v = v1 + v2 & v1 = w1 & v2 = w2 implies v |-- b = (w1 |-- b1) ^ (w2 |-- b2) )
assume A5: ( v = v1 + v2 & v1 = w1 & v2 = w2 ) ; :: thesis: v |-- b = (w1 |-- b1) ^ (w2 |-- b2)
set wb2 = w2 |-- b2;
consider L2 being Linear_Combination of W2 such that
A6: w2 = Sum L2 and
A7: Carrier L2 c= rng b2 and
A8: for k being Nat st 1 <= k & k <= len (w2 |-- b2) holds
(w2 |-- b2) /. k = L2 . (b2 /. k) by MATRLIN:def 7;
A9: W2 is Subspace of W1 + W2 by VECTSP_5:7;
then consider K2 being Linear_Combination of W1 + W2 such that
A10: Carrier K2 = Carrier L2 and
A11: Sum K2 = Sum L2 and
A12: K2 | the carrier of W2 = L2 by Lm4;
rng b2 c= R by A4, FINSEQ_1:30;
then A13: Carrier K2 c= R by A7, A10;
set wb1 = w1 |-- b1;
set vb = v |-- b;
consider L1 being Linear_Combination of W1 such that
A14: w1 = Sum L1 and
A15: Carrier L1 c= rng b1 and
A16: for k being Nat st 1 <= k & k <= len (w1 |-- b1) holds
(w1 |-- b1) /. k = L1 . (b1 /. k) by MATRLIN:def 7;
consider L being Linear_Combination of W1 + W2 such that
A17: ( v = Sum L & Carrier L c= rng b ) and
A18: for k being Nat st 1 <= k & k <= len (v |-- b) holds
(v |-- b) /. k = L . (b /. k) by MATRLIN:def 7;
A19: len (v |-- b) = len b by MATRLIN:def 7;
then A20: dom (v |-- b) = dom b by FINSEQ_3:29;
A21: len (w2 |-- b2) = len b2 by MATRLIN:def 7;
then A22: dom (w2 |-- b2) = dom b2 by FINSEQ_3:29;
A23: R is linearly-independent by VECTSP_7:def 3;
A24: W1 is Subspace of W1 + W2 by VECTSP_5:7;
then consider K1 being Linear_Combination of W1 + W2 such that
A25: Carrier K1 = Carrier L1 and
A26: Sum K1 = Sum L1 and
A27: K1 | the carrier of W1 = L1 by Lm4;
A28: len (w1 |-- b1) = len b1 by MATRLIN:def 7;
then A29: dom (w1 |-- b1) = dom b1 by FINSEQ_3:29;
A30: len ((w1 |-- b1) ^ (w2 |-- b2)) = (len (w1 |-- b1)) + (len (w2 |-- b2)) by FINSEQ_1:22;
A31: ( len b1 = dim W1 & len b2 = dim W2 ) by Th21;
A32: len b = dim (W1 + W2) by Th21;
then A33: dom b = dom ((w1 |-- b1) ^ (w2 |-- b2)) by A28, A21, A31, A30, A3, FINSEQ_3:29;
rng b1 c= R by A4, FINSEQ_1:29;
then A34: Carrier K1 c= R by A15, A25;
then A35: L = K1 + K2 by A5, A14, A26, A6, A11, A17, A13, A23, MATRLIN:6;
hence v |-- b = (w1 |-- b1) ^ (w2 |-- b2) by A28, A21, A19, A31, A30, A3, Th21; :: thesis: verum