let K be Field; :: thesis: for a being Element of K
for V1 being finite-dimensional VectSp of K
for b1 being OrdBasis of V1
for v1 being Element of V1 holds (a * v1) |-- b1 = a * (v1 |-- b1)
let a be Element of K; :: thesis: for V1 being finite-dimensional VectSp of K
for b1 being OrdBasis of V1
for v1 being Element of V1 holds (a * v1) |-- b1 = a * (v1 |-- b1)
let V1 be finite-dimensional VectSp of K; :: thesis: for b1 being OrdBasis of V1
for v1 being Element of V1 holds (a * v1) |-- b1 = a * (v1 |-- b1)
let b1 be OrdBasis of V1; :: thesis: for v1 being Element of V1 holds (a * v1) |-- b1 = a * (v1 |-- b1)
let v1 be Element of V1; :: thesis: (a * v1) |-- b1 = a * (v1 |-- b1)
set vb = v1 |-- b1;
set avb = (a * v1) |-- 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;
A3: len (v1 |-- 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
A4: a * v1 = Sum L2 and
A5: Carrier L2 c= rng b1 and
A6: for k being Nat st 1 <= k & k <= len ((a * v1) |-- b1) holds
((a * v1) |-- b1) /. k = L2 . (b1 /. k) by MATRLIN:def 7;
A7: len ((a * v1) |-- b1) = len b1 by MATRLIN:def 7;
len (a * (v1 |-- b1)) = len (v1 |-- b1) by MATRIXR1:16;
then reconsider vb9 = v1 |-- b1, avb = (a * v1) |-- b1, Avb = a * (v1 |-- b1) as Element of (len b1) -tuples_on the carrier of K by A3, A7, FINSEQ_2:92;
A8: rb1 is linearly-independent by VECTSP_7:def 3;
now :: thesis: for i being Nat st i in Seg (len b1) holds
avb . i = Avb . i
let i be Nat; :: thesis: ( i in Seg (len b1) implies avb . i = Avb . i )
assume A9: i in Seg (len b1) ; :: thesis: avb . i = Avb . i
A10: ( 1 <= i & i <= len b1 ) by A9, FINSEQ_1:1;
A11: now :: thesis: L2 . (b1 /. i) = a * (vb9 /. i)
per cases ( a <> 0. K or a = 0. K ) ;
suppose a <> 0. K ; :: thesis: L2 . (b1 /. i) = a * (vb9 /. i)
then a * L1 = L2 by A1, A4, A5, A8, MATRLIN:7;
hence L2 . (b1 /. i) = a * (L1 . (b1 /. i)) by VECTSP_6:def 9
.= a * (vb9 /. i) by A2, A3, A10 ;
:: thesis: verum
end;
suppose A12: a = 0. K ; :: thesis: L2 . (b1 /. i) = a * (vb9 /. i)
then A13: a * v1 = 0. V1 by VECTSP_1:14;
( L2 is Linear_Combination of Carrier L2 & Carrier L2 is linearly-independent ) by A5, A8, VECTSP_6:7, VECTSP_7:1;
then not b1 /. i in Carrier L2 by A4, A13;
hence L2 . (b1 /. i) = 0. K
.= a * (vb9 /. i) by A12 ;
:: thesis: verum
end;
end;
end;
A14: dom b1 = Seg (len b1) by FINSEQ_1:def 3;
dom (v1 |-- b1) = dom b1 by A3, FINSEQ_3:29;
then A15: (v1 |-- b1) . i = (v1 |-- b1) /. i by A9, A14, PARTFUN1:def 6;
dom avb = dom b1 by A7, FINSEQ_3:29;
then avb . i = avb /. i by A9, A14, PARTFUN1:def 6;
hence avb . i = L2 . (b1 /. i) by A6, A7, A10
.= Avb . i by A9, A15, A11, FVSUM_1:51 ;
:: thesis: verum
end;
hence (a * v1) |-- b1 = a * (v1 |-- b1) by FINSEQ_2:119; :: thesis: verum