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;

now :: thesis: for k being Nat st 1 <= k & k <= len (v |-- b) holds
(v |-- b) . k = ((w1 |-- b1) ^ (w2 |-- b2)) . k

let k be Nat; :: thesis: ( 1 <= k & k <= len (v |-- b) implies (v |-- b) . k = ((w1 |-- b1) ^ (w2 |-- b2)) . k )
assume A36: ( 1 <= k & k <= len (v |-- b) ) ; :: thesis: (v |-- b) . k = ((w1 |-- b1) ^ (w2 |-- b2)) . k
A37: k in dom ((w1 |-- b1) ^ (w2 |-- b2)) by A28, A21, A19, A31, A32, A30, A3, A36, FINSEQ_3:25;

now :: thesis: ((w1 |-- b1) ^ (w2 |-- b2)) . k = (v |-- b) . k

per cases ( k in dom (w1 |-- b1) or ex n being Nat st
( n in dom (w2 |-- b2) & k = (len (w1 |-- b1)) + n ) ) by A37, FINSEQ_1:25;

suppose A38: k in dom (w1 |-- b1) ; :: thesis: ((w1 |-- b1) ^ (w2 |-- b2)) . k = (v |-- b) . k

then ( 1 <= k & k <= len (w1 |-- b1) ) by FINSEQ_3:25;
then A39: L1 . (b1 /. k) = (w1 |-- b1) /. k by A16
.= (w1 |-- b1) . k by A38, PARTFUN1:def 6
.= ((w1 |-- b1) ^ (w2 |-- b2)) . k by A38, FINSEQ_1:def 7 ;
reconsider b1k = b1 /. k as Vector of (W1 + W2) by A24, VECTSP_4:10;
A40: K1 . (b1 /. k) = L1 . (b1 /. k) by A27, FUNCT_1:49;
not b1 /. k in Carrier K2

proof

A41: b1 /. k in W1 ;
assume A42: b1 /. k in Carrier K2 ; :: thesis: contradiction
then b1 /. k in W2 by A10;
then b1 /. k in W1 /\ W2 by A41, VECTSP_5:3;
then b1 /. k in the carrier of ((0). V1) by A1;
then b1 /. k in {(0. V1)} by VECTSP_4:def 3;
then b1 /. k = 0. V1 by TARSKI:def 1
.= 0. (W1 + W2) by VECTSP_4:11 ;
hence contradiction by A13, A23, A42, VECTSP_7:2; :: thesis: verum

end;

then K2 . b1k = 0. K ;
then A43: L . b1k = (K1 . b1k) + (0. K) by A35, VECTSP_6:22
.= ((w1 |-- b1) ^ (w2 |-- b2)) . k by A39, A40, RLVECT_1:def 4 ;
b1k = b1 . k by A29, A38, PARTFUN1:def 6
.= b . k by A4, A29, A38, FINSEQ_1:def 7
.= b /. k by A33, A37, PARTFUN1:def 6 ;
hence ((w1 |-- b1) ^ (w2 |-- b2)) . k = (v |-- b) /. k by A18, A36, A43
.= (v |-- b) . k by A33, A20, A37, PARTFUN1:def 6 ;
:: thesis: verum

end;

suppose ex n being Nat st
( n in dom (w2 |-- b2) & k = (len (w1 |-- b1)) + n ) ; :: thesis: ((w1 |-- b1) ^ (w2 |-- b2)) . k = (v |-- b) . k

then consider n being Nat such that
A44: n in dom (w2 |-- b2) and
A45: k = (len (w1 |-- b1)) + n ;
( 1 <= n & n <= len (w2 |-- b2) ) by A44, FINSEQ_3:25;
then A46: L2 . (b2 /. n) = (w2 |-- b2) /. n by A8
.= (w2 |-- b2) . n by A44, PARTFUN1:def 6
.= ((w1 |-- b1) ^ (w2 |-- b2)) . k by A44, A45, FINSEQ_1:def 7 ;
reconsider b2n = b2 /. n as Vector of (W1 + W2) by A9, VECTSP_4:10;
A47: K2 . (b2 /. n) = L2 . (b2 /. n) by A12, FUNCT_1:49;
not b2 /. n in Carrier K1

proof

assume A48: b2 /. n in Carrier K1 ; :: thesis: contradiction
then ( b2 /. n in W2 & b2 /. n in W1 ) by A25;
then b2 /. n in W1 /\ W2 by VECTSP_5:3;
then b2 /. n in the carrier of ((0). V1) by A1;
then b2 /. n in {(0. V1)} by VECTSP_4:def 3;
then b2 /. n = 0. V1 by TARSKI:def 1
.= 0. (W1 + W2) by VECTSP_4:11 ;
hence contradiction by A34, A23, A48, VECTSP_7:2; :: thesis: verum

end;

then K1 . b2n = 0. K ;
then A49: L . b2n = (0. K) + (K2 . b2n) by A35, VECTSP_6:22
.= ((w1 |-- b1) ^ (w2 |-- b2)) . k by A46, A47, RLVECT_1:def 4 ;
b2n = b2 . n by A22, A44, PARTFUN1:def 6
.= b . k by A4, A28, A22, A44, A45, FINSEQ_1:def 7
.= b /. k by A33, A37, PARTFUN1:def 6 ;
hence ((w1 |-- b1) ^ (w2 |-- b2)) . k = (v |-- b) /. k by A18, A36, A49
.= (v |-- b) . k by A33, A20, A37, PARTFUN1:def 6 ;
:: thesis: verum

end;

end;

end;

hence (v |-- b) . k = ((w1 |-- b1) ^ (w2 |-- b2)) . k ; :: thesis: verum

end;

hence v |-- b = (w1 |-- b1) ^ (w2 |-- b2) by A28, A21, A19, A31, A30, A3, Th21; :: thesis: verum