let i, n be Nat; :: thesis: for K being Field
for L being Element of K st i in Seg n & i <> n holds
Line ((Jordan_block (L,n)),i) = (L * (Line ((1. (K,n)),i))) + (Line ((1. (K,n)),(i + 1)))
let K be Field; :: thesis: for L being Element of K st i in Seg n & i <> n holds
Line ((Jordan_block (L,n)),i) = (L * (Line ((1. (K,n)),i))) + (Line ((1. (K,n)),(i + 1)))
let L be Element of K; :: thesis: ( i in Seg n & i <> n implies Line ((Jordan_block (L,n)),i) = (L * (Line ((1. (K,n)),i))) + (Line ((1. (K,n)),(i + 1))) )
assume that
A1: i in Seg n and
A2: i <> n ; :: thesis: Line ((Jordan_block (L,n)),i) = (L * (Line ((1. (K,n)),i))) + (Line ((1. (K,n)),(i + 1)))
reconsider N = n as Element of NAT by ORDINAL1:def 12;
set J = Jordan_block (L,n);
set i1 = i + 1;
set ONE = 1. (K,n);
set Li = Line ((1. (K,n)),i);
set Li1 = Line ((1. (K,n)),(i + 1));
set LJ = Line ((Jordan_block (L,n)),i);
A3: width (1. (K,n)) = n by MATRIX_0:24;
A4: Indices (1. (K,n)) = Indices (Jordan_block (L,n)) by MATRIX_0:26;
reconsider Li = Line ((1. (K,n)),i), Li1 = Line ((1. (K,n)),(i + 1)), LJ = Line ((Jordan_block (L,n)),i) as Element of N -tuples_on the carrier of K by MATRIX_0:24;
A5: Indices (1. (K,n)) = [:(Seg n),(Seg n):] by MATRIX_0:24;
A6: width (Jordan_block (L,n)) = n by MATRIX_0:24;

now :: thesis: for j being Nat st j in Seg n holds
((L * Li) + Li1) . j = LJ . j

let j be Nat; :: thesis: ( j in Seg n implies ((L * Li) + Li1) . j = LJ . j )
assume A7: j in Seg n ; :: thesis: ((L * Li) + Li1) . j = LJ . j
Li . j = (1. (K,n)) * (i,j) by A3, A7, MATRIX_0:def 7;
then A8: (L * Li) . j = L * ((1. (K,n)) * (i,j)) by A7, FVSUM_1:51;
A9: [i,j] in [:(Seg n),(Seg n):] by A1, A7, ZFMISC_1:87;
i <= n by A1, FINSEQ_1:1;
then i < n by A2, XXREAL_0:1;
then ( 1 <= i + 1 & i + 1 <= n ) by NAT_1:11, NAT_1:13;
then i + 1 in Seg n ;
then A10: [(i + 1),j] in [:(Seg n),(Seg n):] by A7, ZFMISC_1:87;
Li1 . j = (1. (K,n)) * ((i + 1),j) by A3, A7, MATRIX_0:def 7;
then A11: ((L * Li) + Li1) . j = (L * ((1. (K,n)) * (i,j))) + ((1. (K,n)) * ((i + 1),j)) by A7, A8, FVSUM_1:18;
A12: LJ . j = (Jordan_block (L,n)) * (i,j) by A6, A7, MATRIX_0:def 7;

now :: thesis: LJ . j = ((L * Li) + Li1) . j

per cases ( i = j or i + 1 = j or ( i <> j & i + 1 <> j ) ) ;

suppose A13: i = j ; :: thesis: LJ . j = ((L * Li) + Li1) . j

then A14: i + 1 > j by NAT_1:13;
thus LJ . j = L by A5, A4, A9, A12, A13, Def1
.= L + (0. K) by RLVECT_1:def 4
.= (L * (1_ K)) + (0. K)
.= (L * ((1. (K,n)) * (i,j))) + (0. K) by A5, A9, A13, MATRIX_1:def 3
.= ((L * Li) + Li1) . j by A5, A10, A11, A14, MATRIX_1:def 3 ; :: thesis: verum

end;

suppose A15: i + 1 = j ; :: thesis: LJ . j = ((L * Li) + Li1) . j

then A16: i < j by NAT_1:13;
thus LJ . j = 1_ K by A5, A4, A9, A12, A15, Def1
.= (0. K) + (1_ K) by RLVECT_1:def 4
.= (L * (0. K)) + (1_ K)
.= (L * ((1. (K,n)) * (i,j))) + (1_ K) by A5, A9, A16, MATRIX_1:def 3
.= ((L * Li) + Li1) . j by A5, A10, A11, A15, MATRIX_1:def 3 ; :: thesis: verum

end;

suppose A17: ( i <> j & i + 1 <> j ) ; :: thesis: LJ . j = ((L * Li) + Li1) . j

hence LJ . j = 0. K by A5, A4, A9, A12, Def1
.= (0. K) + (0. K) by RLVECT_1:def 4
.= (L * (0. K)) + (0. K)
.= (L * ((1. (K,n)) * (i,j))) + (0. K) by A5, A9, A17, MATRIX_1:def 3
.= ((L * Li) + Li1) . j by A5, A10, A11, A17, MATRIX_1:def 3 ;
:: thesis: verum

end;

end;

end;

hence ((L * Li) + Li1) . j = LJ . j ; :: thesis: verum

end;

hence Line ((Jordan_block (L,n)),i) = (L * (Line ((1. (K,n)),i))) + (Line ((1. (K,n)),(i + 1))) by FINSEQ_2:119; :: thesis: verum