let K be Field; 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; 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; ( 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
; 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; 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; 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; ( 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
; 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); 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; 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; ( v = v1 + v2 & v1 = w1 & v2 = w2 implies v |-- b = (w1 |-- b1) ^ (w2 |-- b2) )
assume A5:
( v = v1 + v2 & v1 = w1 & v2 = w2 )
; 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 for k being Nat st 1 <= k & k <= len (v |-- b) holds
(v |-- b) . k = ((w1 |-- b1) ^ (w2 |-- b2)) . klet k be
Nat;
( 1 <= k & k <= len (v |-- b) implies (v |-- b) . k = ((w1 |-- b1) ^ (w2 |-- b2)) . k )assume A36:
( 1
<= k &
k <= len (v |-- b) )
;
(v |-- b) . k = ((w1 |-- b1) ^ (w2 |-- b2)) . kA37:
k in dom ((w1 |-- b1) ^ (w2 |-- b2))
by A28, A21, A19, A31, A32, A30, A3, A36, FINSEQ_3:25;
now ((w1 |-- b1) ^ (w2 |-- b2)) . k = (v |-- b) . kper 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)
;
((w1 |-- b1) ^ (w2 |-- b2)) . k = (v |-- b) . kthen
( 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
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
;
verum end; suppose
ex
n being
Nat st
(
n in dom (w2 |-- b2) &
k = (len (w1 |-- b1)) + n )
;
((w1 |-- b1) ^ (w2 |-- b2)) . k = (v |-- b) . kthen 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
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
;
verum end; end; end; hence
(v |-- b) . k = ((w1 |-- b1) ^ (w2 |-- b2)) . k
;
verum end;
hence
v |-- b = (w1 |-- b1) ^ (w2 |-- b2)
by A28, A21, A19, A31, A30, A3, Th21; verum