let K be Field; for a being Element of K
for V1 being finite-dimensional VectSp of K
for R being FinSequence of V1
for p being FinSequence of K holds Sum (lmlt ((a * p),R)) = a * (Sum (lmlt (p,R)))
let a be Element of K; for V1 being finite-dimensional VectSp of K
for R being FinSequence of V1
for p being FinSequence of K holds Sum (lmlt ((a * p),R)) = a * (Sum (lmlt (p,R)))
let V1 be finite-dimensional VectSp of K; for R being FinSequence of V1
for p being FinSequence of K holds Sum (lmlt ((a * p),R)) = a * (Sum (lmlt (p,R)))
let R be FinSequence of V1; for p being FinSequence of K holds Sum (lmlt ((a * p),R)) = a * (Sum (lmlt (p,R)))
let p be FinSequence of K; Sum (lmlt ((a * p),R)) = a * (Sum (lmlt (p,R)))
set Ma = lmlt ((a * p),R);
set M = lmlt (p,R);
len (a * p) = len p
by MATRIXR1:16;
then A1:
dom (a * p) = dom p
by FINSEQ_3:29;
A2:
dom (lmlt ((a * p),R)) = (dom (a * p)) /\ (dom R)
by Lm1;
A3:
dom (lmlt (p,R)) = (dom p) /\ (dom R)
by Lm1;
A4:
for k being Nat
for v1 being Element of V1 st k in dom (lmlt ((a * p),R)) & v1 = (lmlt (p,R)) . k holds
(lmlt ((a * p),R)) . k = a * v1
proof
let k be
Nat;
for v1 being Element of V1 st k in dom (lmlt ((a * p),R)) & v1 = (lmlt (p,R)) . k holds
(lmlt ((a * p),R)) . k = a * v1let v1 be
Element of
V1;
( k in dom (lmlt ((a * p),R)) & v1 = (lmlt (p,R)) . k implies (lmlt ((a * p),R)) . k = a * v1 )
assume that A5:
k in dom (lmlt ((a * p),R))
and A6:
v1 = (lmlt (p,R)) . k
;
(lmlt ((a * p),R)) . k = a * v1
k in dom R
by A2, A5, XBOOLE_0:def 4;
then A7:
R /. k = R . k
by PARTFUN1:def 6;
k in dom p
by A1, A2, A5, XBOOLE_0:def 4;
then A8:
p /. k = p . k
by PARTFUN1:def 6;
k in dom (a * p)
by A2, A5, XBOOLE_0:def 4;
then
(a * p) . k = a * (p /. k)
by A8, FVSUM_1:50;
hence (lmlt ((a * p),R)) . k =
(a * (p /. k)) * (R /. k)
by A5, A7, FUNCOP_1:22
.=
a * ((p /. k) * (R /. k))
by VECTSP_1:def 16
.=
a * v1
by A1, A3, A2, A5, A6, A8, A7, FUNCOP_1:22
;
verum
end;
len (lmlt (p,R)) = len (lmlt ((a * p),R))
by A1, A3, A2, FINSEQ_3:29;
hence
Sum (lmlt ((a * p),R)) = a * (Sum (lmlt (p,R)))
by A4, RLVECT_2:66; verum