let n be Nat; :: thesis: for K being Field
for L being Element of K holds Line (Jordan_block L,n),n = L * (Line (1. K,n),n)
let K be Field; :: thesis: for L being Element of K holds Line (Jordan_block L,n),n = L * (Line (1. K,n),n)
let L be Element of K; :: thesis: Line (Jordan_block L,n),n = L * (Line (1. K,n),n)
set ONE = 1. K,n;
set Ln = Line (1. K,n),n;
set J = Jordan_block L,n;
set LJ = Line (Jordan_block L,n),n;
reconsider N = n as Element of NAT by ORDINAL1:def 13;
A1: width (Jordan_block L,n) = n by MATRIX_1:25;
A2: Indices (1. K,n) = Indices (Jordan_block L,n) by MATRIX_1:27;
reconsider Ln = Line (1. K,n),n, LJ = Line (Jordan_block L,n),n as Element of N -tuples_on the carrier of K by MATRIX_1:25;
A3: Indices (1. K,n) = [:(Seg n),(Seg n):] by MATRIX_1:25;
A4: width (1. K,n) = n by MATRIX_1:25;

now

let j be Nat; :: thesis: ( j in Seg n implies (L * Ln) . j = LJ . j )
assume A5: j in Seg n ; :: thesis: (L * Ln) . j = LJ . j
n <> 0 by A5;
then n in Seg n by A5, FINSEQ_1:4, FINSEQ_1:5;
then A6: [n,j] in [:(Seg n),(Seg n):] by A5, ZFMISC_1:106;
Ln . j = (1. K,n) * n,j by A4, A5, MATRIX_1:def 8;
then A7: (L * Ln) . j = L * ((1. K,n) * n,j) by A5, FVSUM_1:63;
A8: LJ . j = (Jordan_block L,n) * n,j by A1, A5, MATRIX_1:def 8;

now

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

suppose A9: n = j ; :: thesis: LJ . j = (L * Ln) . j

hence LJ . j = L by A3, A2, A6, A8, Def1
.= L * (1_ K) by VECTSP_1:def 19
.= (L * Ln) . j by A3, A6, A7, A9, MATRIX_1:def 12 ;
:: thesis: verum

end;

suppose n + 1 = j ; :: thesis: (L * Ln) . j = LJ . j

then j > n by NAT_1:13;
hence (L * Ln) . j = LJ . j by A5, FINSEQ_1:3; :: thesis: verum

end;

suppose A10: ( n <> j & n + 1 <> j ) ; :: thesis: LJ . j = (L * Ln) . j

hence LJ . j = 0. K by A3, A2, A6, A8, Def1
.= L * (0. K) by VECTSP_1:39
.= (L * Ln) . j by A3, A6, A7, A10, MATRIX_1:def 12 ;
:: thesis: verum

end;

end;

end;

hence (L * Ln) . j = LJ . j ; :: thesis: verum

end;

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