let K be Field; for a being Element of K
for V1 being finite-dimensional VectSp of K
for R being FinSequence of V1 holds Sum (lmlt (((len R) |-> a),R)) = a * (Sum R)
let a be Element of K; for V1 being finite-dimensional VectSp of K
for R being FinSequence of V1 holds Sum (lmlt (((len R) |-> a),R)) = a * (Sum R)
let V1 be finite-dimensional VectSp of K; for R being FinSequence of V1 holds Sum (lmlt (((len R) |-> a),R)) = a * (Sum R)
let R be FinSequence of V1; Sum (lmlt (((len R) |-> a),R)) = a * (Sum R)
defpred S1[ Nat] means for R being FinSequence of V1
for a being Element of K st len R = $1 holds
Sum (lmlt (((len R) |-> a),R)) = a * (Sum R);
A1:
for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be
Nat;
( S1[n] implies S1[n + 1] )
assume A2:
S1[
n]
;
S1[n + 1]
set n1 =
n + 1;
let R be
FinSequence of
V1;
for a being Element of K st len R = n + 1 holds
Sum (lmlt (((len R) |-> a),R)) = a * (Sum R)let a be
Element of
K;
( len R = n + 1 implies Sum (lmlt (((len R) |-> a),R)) = a * (Sum R) )
assume A3:
len R = n + 1
;
Sum (lmlt (((len R) |-> a),R)) = a * (Sum R)
A4:
len (R | n) = n
by A3, FINSEQ_1:59, NAT_1:11;
then A5:
dom (R | n) = Seg n
by FINSEQ_1:def 3;
1
<= n + 1
by NAT_1:11;
then
n + 1
in dom R
by A3, FINSEQ_3:25;
then A6:
R /. (n + 1) = R . (n + 1)
by PARTFUN1:def 6;
A7:
lmlt (
<*a*>,
<*(R /. (n + 1))*>)
= <*(a * (R /. (n + 1)))*>
by FINSEQ_2:74;
A8:
(
len <*a*> = 1 &
len <*(R . (n + 1))*> = 1 )
by FINSEQ_1:39;
A9:
(
(n + 1) |-> a = (n |-> a) ^ <*a*> &
len (n |-> a) = n )
by CARD_1:def 7, FINSEQ_2:60;
R = (R | n) ^ <*(R . (n + 1))*>
by A3, FINSEQ_3:55;
hence Sum (lmlt (((len R) |-> a),R)) =
Sum ((lmlt ((n |-> a),(R | n))) ^ (lmlt (<*a*>,<*(R /. (n + 1))*>)))
by A3, A6, A4, A9, A8, Th9
.=
(Sum (lmlt ((n |-> a),(R | n)))) + (Sum (lmlt (<*a*>,<*(R /. (n + 1))*>)))
by RLVECT_1:41
.=
(a * (Sum (R | n))) + (Sum <*(a * (R /. (n + 1)))*>)
by A2, A4, A7
.=
(a * (Sum (R | n))) + (a * (R /. (n + 1)))
by RLVECT_1:44
.=
a * ((Sum (R | n)) + (R /. (n + 1)))
by VECTSP_1:def 14
.=
a * (Sum R)
by A3, A6, A4, A5, RLVECT_1:38
;
verum
end;
A10:
S1[ 0 ]
proof
let R be
FinSequence of
V1;
for a being Element of K st len R = 0 holds
Sum (lmlt (((len R) |-> a),R)) = a * (Sum R)let a be
Element of
K;
( len R = 0 implies Sum (lmlt (((len R) |-> a),R)) = a * (Sum R) )
assume A11:
len R = 0
;
Sum (lmlt (((len R) |-> a),R)) = a * (Sum R)
set L =
(len R) |-> a;
set M =
lmlt (
((len R) |-> a),
R);
len ((len R) |-> a) = len R
by CARD_1:def 7;
then
dom ((len R) |-> a) = dom R
by FINSEQ_3:29;
then
dom (lmlt (((len R) |-> a),R)) = dom R
by MATRLIN:12;
then
len R = len (lmlt (((len R) |-> a),R))
by FINSEQ_3:29;
then
lmlt (
((len R) |-> a),
R)
= <*> the
carrier of
V1
by A11;
then A12:
Sum (lmlt (((len R) |-> a),R)) = 0. V1
by RLVECT_1:43;
R = <*> the
carrier of
V1
by A11;
then
Sum R = 0. V1
by RLVECT_1:43;
hence
Sum (lmlt (((len R) |-> a),R)) = a * (Sum R)
by A12, VECTSP_1:14;
verum
end;
for n being Nat holds S1[n]
from NAT_1:sch 2(A10, A1);
hence
Sum (lmlt (((len R) |-> a),R)) = a * (Sum R)
; verum