let K be Field; for V1 being finite-dimensional VectSp of K
for b1 being OrdBasis of V1
for v1, w1 being Element of V1 holds (v1 + w1) |-- b1 = (v1 |-- b1) + (w1 |-- b1)
let V1 be finite-dimensional VectSp of K; for b1 being OrdBasis of V1
for v1, w1 being Element of V1 holds (v1 + w1) |-- b1 = (v1 |-- b1) + (w1 |-- b1)
let b1 be OrdBasis of V1; for v1, w1 being Element of V1 holds (v1 + w1) |-- b1 = (v1 |-- b1) + (w1 |-- b1)
let v1, w1 be Element of V1; (v1 + w1) |-- b1 = (v1 |-- b1) + (w1 |-- b1)
set vb = v1 |-- b1;
set wb = w1 |-- b1;
set vwb = (v1 + w1) |-- b1;
consider L1 being Linear_Combination of V1 such that
A1:
( v1 = Sum L1 & Carrier L1 c= rng b1 )
and
A2:
for k being Nat st 1 <= k & k <= len (v1 |-- b1) holds
(v1 |-- b1) /. k = L1 . (b1 /. k)
by MATRLIN:def 7;
consider L3 being Linear_Combination of V1 such that
A3:
( v1 + w1 = Sum L3 & Carrier L3 c= rng b1 )
and
A4:
for k being Nat st 1 <= k & k <= len ((v1 + w1) |-- b1) holds
((v1 + w1) |-- b1) /. k = L3 . (b1 /. k)
by MATRLIN:def 7;
A5:
len (w1 |-- b1) = len b1
by MATRLIN:def 7;
reconsider rb1 = rng b1 as Basis of V1 by MATRLIN:def 2;
consider L2 being Linear_Combination of V1 such that
A6:
( w1 = Sum L2 & Carrier L2 c= rng b1 )
and
A7:
for k being Nat st 1 <= k & k <= len (w1 |-- b1) holds
(w1 |-- b1) /. k = L2 . (b1 /. k)
by MATRLIN:def 7;
A8:
len (v1 |-- b1) = len b1
by MATRLIN:def 7;
A9:
len ((v1 + w1) |-- b1) = len b1
by MATRLIN:def 7;
then reconsider vb = v1 |-- b1, wb = w1 |-- b1, vwb = (v1 + w1) |-- b1 as Element of (len b1) -tuples_on the carrier of K by A8, A5, FINSEQ_2:92;
rb1 is linearly-independent
by VECTSP_7:def 3;
then A10:
L3 = L1 + L2
by A1, A6, A3, MATRLIN:6;
now for i being Nat st i in Seg (len b1) holds
vwb . i = (vb + wb) . iA11:
dom b1 = Seg (len b1)
by FINSEQ_1:def 3;
let i be
Nat;
( i in Seg (len b1) implies vwb . i = (vb + wb) . i )assume A12:
i in Seg (len b1)
;
vwb . i = (vb + wb) . iA13:
( 1
<= i &
i <= len b1 )
by A12, FINSEQ_1:1;
dom wb = dom b1
by A5, FINSEQ_3:29;
then A14:
wb . i = wb /. i
by A12, A11, PARTFUN1:def 6;
dom vb = dom b1
by A8, FINSEQ_3:29;
then A15:
vb . i = vb /. i
by A12, A11, PARTFUN1:def 6;
dom vwb = dom b1
by A9, FINSEQ_3:29;
then
vwb . i = vwb /. i
by A12, A11, PARTFUN1:def 6;
hence vwb . i =
(L1 + L2) . (b1 /. i)
by A4, A9, A10, A13
.=
(L1 . (b1 /. i)) + (L2 . (b1 /. i))
by VECTSP_6:22
.=
(vb /. i) + (L2 . (b1 /. i))
by A2, A8, A13
.=
(vb /. i) + (wb /. i)
by A7, A5, A13
.=
(vb + wb) . i
by A12, A15, A14, FVSUM_1:18
;
verum end;
hence
(v1 + w1) |-- b1 = (v1 |-- b1) + (w1 |-- b1)
by FINSEQ_2:119; verum