let i be Nat; :: thesis: for K being Field
for L being Element of K
for V1 being finite-dimensional VectSp of K
for B1 being FinSequence of V1 st i in dom B1 & i <> len B1 holds
Sum (lmlt (Line (Jordan_block L,(len B1)),i),B1) = (L * (B1 /. i)) + (B1 /. (i + 1))
let K be Field; :: thesis: for L being Element of K
for V1 being finite-dimensional VectSp of K
for B1 being FinSequence of V1 st i in dom B1 & i <> len B1 holds
Sum (lmlt (Line (Jordan_block L,(len B1)),i),B1) = (L * (B1 /. i)) + (B1 /. (i + 1))
let L be Element of K; :: thesis: for V1 being finite-dimensional VectSp of K
for B1 being FinSequence of V1 st i in dom B1 & i <> len B1 holds
Sum (lmlt (Line (Jordan_block L,(len B1)),i),B1) = (L * (B1 /. i)) + (B1 /. (i + 1))
let V1 be finite-dimensional VectSp of K; :: thesis: for B1 being FinSequence of V1 st i in dom B1 & i <> len B1 holds
Sum (lmlt (Line (Jordan_block L,(len B1)),i),B1) = (L * (B1 /. i)) + (B1 /. (i + 1))
let B1 be FinSequence of V1; :: thesis: ( i in dom B1 & i <> len B1 implies Sum (lmlt (Line (Jordan_block L,(len B1)),i),B1) = (L * (B1 /. i)) + (B1 /. (i + 1)) )
assume that
A1: i in dom B1 and
A2: i <> len B1 ; :: thesis: Sum (lmlt (Line (Jordan_block L,(len B1)),i),B1) = (L * (B1 /. i)) + (B1 /. (i + 1))
set N = len B1;
A3: dom B1 = Seg (len B1) by FINSEQ_1:def 3;
i <= len B1 by A1, FINSEQ_3:27;
then i < len B1 by A2, XXREAL_0:1;
then ( 1 <= i + 1 & i + 1 <= len B1 ) by NAT_1:11, NAT_1:13;
then A4: i + 1 in dom B1 by A3;
set ONE = 1. K,(len B1);
A5: len (Line (1. K,(len B1)),(i + 1)) = width (1. K,(len B1)) by FINSEQ_1:def 18;
width (1. K,(len B1)) = len B1 by MATRIX_1:25;
then A6: dom (Line (1. K,(len B1)),(i + 1)) = dom B1 by A5, FINSEQ_3:31;
( len (L * (Line (1. K,(len B1)),i)) = len (Line (1. K,(len B1)),i) & len (Line (1. K,(len B1)),i) = width (1. K,(len B1)) ) by FINSEQ_1:def 18, MATRIXR1:16;
then dom (L * (Line (1. K,(len B1)),i)) = dom (Line (1. K,(len B1)),(i + 1)) by A5, FINSEQ_3:31;
then A7: dom (lmlt (L * (Line (1. K,(len B1)),i)),B1) = dom B1 by A6, MATRLIN:16;
dom (lmlt (Line (1. K,(len B1)),(i + 1)),B1) = dom B1 by A6, MATRLIN:16;
then A8: len (lmlt (L * (Line (1. K,(len B1)),i)),B1) = len (lmlt (Line (1. K,(len B1)),(i + 1)),B1) by A7, FINSEQ_3:31;
thus Sum (lmlt (Line (Jordan_block L,(len B1)),i),B1) = Sum (lmlt ((L * (Line (1. K,(len B1)),i)) + (Line (1. K,(len B1)),(i + 1))),B1) by A1, A2, A3, Th4
.= Sum ((lmlt (L * (Line (1. K,(len B1)),i)),B1) + (lmlt (Line (1. K,(len B1)),(i + 1)),B1)) by MATRLIN2:7
.= (Sum (lmlt (L * (Line (1. K,(len B1)),i)),B1)) + (Sum (lmlt (Line (1. K,(len B1)),(i + 1)),B1)) by A8, MATRLIN2:10
.= (L * (Sum (lmlt (Line (1. K,(len B1)),i),B1))) + (Sum (lmlt (Line (1. K,(len B1)),(i + 1)),B1)) by MATRLIN2:13
.= (L * (B1 /. i)) + (Sum (lmlt (Line (1. K,(len B1)),(i + 1)),B1)) by A1, MATRLIN2:16
.= (L * (B1 /. i)) + (B1 /. (i + 1)) by A4, MATRLIN2:16 ; :: thesis: verum
set J = Jordan_block L,(len B1);