let i, n be Nat; 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; 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; ( 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
; 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 for j being Nat st j in Seg n holds
((L * Li) + Li1) . j = LJ . jlet j be
Nat;
( j in Seg n implies ((L * Li) + Li1) . j = LJ . j )assume A7:
j in Seg n
;
((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 LJ . j = ((L * Li) + Li1) . jper cases
( i = j or i + 1 = j or ( i <> j & i + 1 <> j ) )
;
suppose A13:
i = j
;
LJ . j = ((L * Li) + Li1) . jthen 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
;
verum end; suppose A15:
i + 1
= j
;
LJ . j = ((L * Li) + Li1) . jthen 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
;
verum end; suppose A17:
(
i <> j &
i + 1
<> j )
;
LJ . j = ((L * Li) + Li1) . jhence 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
;
verum end; end; end; hence
((L * Li) + Li1) . j = LJ . j
;
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; verum