let n be Nat; for K being Field
for L being Element of K st L <> 0. K holds
ex M being Matrix of n,K st
( (Jordan_block (L,n)) ~ = M & ( for i, j being Nat st [i,j] in Indices M holds
( ( i > j implies M * (i,j) = 0. K ) & ( i <= j implies M * (i,j) = - ((power K) . ((- (L ")),((j -' i) + 1))) ) ) ) )
let K be Field; for L being Element of K st L <> 0. K holds
ex M being Matrix of n,K st
( (Jordan_block (L,n)) ~ = M & ( for i, j being Nat st [i,j] in Indices M holds
( ( i > j implies M * (i,j) = 0. K ) & ( i <= j implies M * (i,j) = - ((power K) . ((- (L ")),((j -' i) + 1))) ) ) ) )
let L be Element of K; ( L <> 0. K implies ex M being Matrix of n,K st
( (Jordan_block (L,n)) ~ = M & ( for i, j being Nat st [i,j] in Indices M holds
( ( i > j implies M * (i,j) = 0. K ) & ( i <= j implies M * (i,j) = - ((power K) . ((- (L ")),((j -' i) + 1))) ) ) ) ) )
reconsider N = n as Element of NAT by ORDINAL1:def 12;
defpred S1[ Nat, Nat, set ] means ( ( $1 > $2 implies $3 = 0. K ) & ( $1 <= $2 implies $3 = - ((power K) . ((- (L ")),(($2 -' $1) + 1))) ) );
A1:
for i, j being Nat st [i,j] in [:(Seg N),(Seg N):] holds
ex x being Element of K st S1[i,j,x]
consider M being Matrix of N,K such that
A4:
for i, j being Nat st [i,j] in Indices M holds
S1[i,j,M * (i,j)]
from MATRIX_0:sch 2(A1);
set ONE = 1. (K,n);
set J = Jordan_block (L,n);
A5:
Indices (1. (K,n)) = [:(Seg n),(Seg n):]
by MATRIX_0:24;
assume A6:
L <> 0. K
; ex M being Matrix of n,K st
( (Jordan_block (L,n)) ~ = M & ( for i, j being Nat st [i,j] in Indices M holds
( ( i > j implies M * (i,j) = 0. K ) & ( i <= j implies M * (i,j) = - ((power K) . ((- (L ")),((j -' i) + 1))) ) ) ) )
then A7:
Jordan_block (L,n) is invertible
by Th3;
reconsider M = M as Matrix of n,K ;
set MJ = M * (Jordan_block (L,n));
A8:
( Indices M = Indices (Jordan_block (L,n)) & Indices (Jordan_block (L,n)) = Indices (1. (K,n)) )
by MATRIX_0:26;
A9:
width M = n
by MATRIX_0:24;
A10:
Indices (M * (Jordan_block (L,n))) = Indices (1. (K,n))
by MATRIX_0:26;
A11:
len (Jordan_block (L,n)) = n
by MATRIX_0:24;
now for i, j being Nat st [i,j] in Indices (1. (K,n)) holds
(1. (K,n)) * (i,j) = (M * (Jordan_block (L,n))) * (i,j)let i,
j be
Nat;
( [i,j] in Indices (1. (K,n)) implies (1. (K,n)) * (i,j) = (M * (Jordan_block (L,n))) * (i,j) )assume A12:
[i,j] in Indices (1. (K,n))
;
(1. (K,n)) * (i,j) = (M * (Jordan_block (L,n))) * (i,j)A13:
i in Seg n
by A5, A12, ZFMISC_1:87;
set LL =
Line (
M,
i);
A14:
(M * (Jordan_block (L,n))) * (
i,
j) =
(Line (M,i)) "*" (Col ((Jordan_block (L,n)),j))
by A9, A10, A12, A11, MATRIX_3:def 4
.=
(Col ((Jordan_block (L,n)),j)) "*" (Line (M,i))
by FVSUM_1:90
;
A15:
j in Seg n
by A5, A12, ZFMISC_1:87;
then A16:
(Line (M,i)) . j = M * (
i,
j)
by A9, MATRIX_0:def 7;
A17:
dom (Line (M,i)) = Seg n
by A9, FINSEQ_2:124;
then A18:
(Line (M,i)) /. j = (Line (M,i)) . j
by A15, PARTFUN1:def 6;
now (1. (K,n)) * (i,j) = (M * (Jordan_block (L,n))) * (i,j)per cases
( j = 1 or j <> 1 )
;
suppose A19:
j = 1
;
(1. (K,n)) * (i,j) = (M * (Jordan_block (L,n))) * (i,j)then A20:
(M * (Jordan_block (L,n))) * (
i,
j)
= L * (M * (i,j))
by A9, A15, A18, A16, A14, Th7;
now (M * (Jordan_block (L,n))) * (i,j) = (1. (K,n)) * (i,j)per cases
( i = j or i <> j )
;
suppose A21:
i = j
;
(M * (Jordan_block (L,n))) * (i,j) = (1. (K,n)) * (i,j)hence (M * (Jordan_block (L,n))) * (
i,
j) =
L * (- ((power K) . ((- (L ")),((i -' i) + 1))))
by A4, A8, A12, A20
.=
L * (- ((power K) . ((- (L ")),(0 + 1))))
by XREAL_1:232
.=
L * (- (- (L ")))
by GROUP_1:50
.=
L * (L ")
by RLVECT_1:17
.=
1_ K
by A6, VECTSP_1:def 10
.=
(1. (K,n)) * (
i,
j)
by A12, A21, MATRIX_1:def 3
;
verum end; suppose A22:
i <> j
;
(M * (Jordan_block (L,n))) * (i,j) = (1. (K,n)) * (i,j)
1
<= i
by A13, FINSEQ_1:1;
then
j < i
by A19, A22, XXREAL_0:1;
hence (M * (Jordan_block (L,n))) * (
i,
j) =
L * (0. K)
by A4, A8, A12, A20
.=
0. K
.=
(1. (K,n)) * (
i,
j)
by A12, A22, MATRIX_1:def 3
;
verum end; end; end; hence
(1. (K,n)) * (
i,
j)
= (M * (Jordan_block (L,n))) * (
i,
j)
;
verum end; suppose A23:
j <> 1
;
(M * (Jordan_block (L,n))) * (i,j) = (1. (K,n)) * (i,j)A24:
j >= 1
by A15, FINSEQ_1:1;
then reconsider j1 =
j - 1 as
Element of
NAT by NAT_1:21;
(
j1 <= j1 + 1 &
j <= n )
by A15, FINSEQ_1:1, NAT_1:11;
then A25:
n >= j1
by XXREAL_0:2;
j1 + 1
> 0 + 1
by A23, A24, XXREAL_0:1;
then
j1 >= 1
by NAT_1:14;
then A26:
j1 in Seg n
by A25;
then A27:
[i,j1] in Indices (1. (K,n))
by A5, A13, ZFMISC_1:87;
(
(Line (M,i)) /. j1 = (Line (M,i)) . j1 &
(Line (M,i)) . j1 = M * (
i,
j1) )
by A9, A17, A26, MATRIX_0:def 7, PARTFUN1:def 6;
then A28:
(M * (Jordan_block (L,n))) * (
i,
j)
= (L * (M * (i,j))) + (M * (i,j1))
by A9, A15, A18, A16, A14, A23, Th7;
now (M * (Jordan_block (L,n))) * (i,j) = (1. (K,n)) * (i,j)per cases
( i < j1 + 1 or i = j1 + 1 or i > j1 + 1 )
by XXREAL_0:1;
suppose A29:
i < j1 + 1
;
(M * (Jordan_block (L,n))) * (i,j) = (1. (K,n)) * (i,j)set P =
(power K) . (
(- (L ")),
((j1 -' i) + 1));
A30:
j -' i = j - i
by A29, XREAL_1:233;
A31:
i <= j1
by A29, NAT_1:13;
then A32:
j1 -' i = j1 - i
by XREAL_1:233;
thus (M * (Jordan_block (L,n))) * (
i,
j) =
(L * (M * (i,j))) + (- ((power K) . ((- (L ")),((j1 -' i) + 1))))
by A4, A8, A27, A28, A31
.=
(L * (- ((power K) . ((- (L ")),((j -' i) + 1))))) + (- ((power K) . ((- (L ")),((j1 -' i) + 1))))
by A4, A8, A12, A29
.=
(L * (- ((- (L ")) * ((power K) . ((- (L ")),((j1 -' i) + 1)))))) + (- ((power K) . ((- (L ")),((j1 -' i) + 1))))
by A32, A30, GROUP_1:def 7
.=
(L * ((- (- (L "))) * ((power K) . ((- (L ")),((j1 -' i) + 1))))) + (- ((power K) . ((- (L ")),((j1 -' i) + 1))))
by VECTSP_1:9
.=
(L * ((L ") * ((power K) . ((- (L ")),((j1 -' i) + 1))))) + (- ((power K) . ((- (L ")),((j1 -' i) + 1))))
by RLVECT_1:17
.=
((L * (L ")) * ((power K) . ((- (L ")),((j1 -' i) + 1)))) + (- ((power K) . ((- (L ")),((j1 -' i) + 1))))
by GROUP_1:def 3
.=
((1_ K) * ((power K) . ((- (L ")),((j1 -' i) + 1)))) + (- ((power K) . ((- (L ")),((j1 -' i) + 1))))
by A6, VECTSP_1:def 10
.=
((power K) . ((- (L ")),((j1 -' i) + 1))) + (- ((power K) . ((- (L ")),((j1 -' i) + 1))))
.=
0. K
by RLVECT_1:def 10
.=
(1. (K,n)) * (
i,
j)
by A12, A29, MATRIX_1:def 3
;
verum end; suppose A33:
i = j1 + 1
;
(M * (Jordan_block (L,n))) * (i,j) = (1. (K,n)) * (i,j)then
i > j1
by NAT_1:13;
hence (M * (Jordan_block (L,n))) * (
i,
j) =
(L * (M * (i,j))) + (0. K)
by A4, A8, A27, A28
.=
L * (M * (i,j))
by RLVECT_1:def 4
.=
L * (- ((power K) . ((- (L ")),((i -' i) + 1))))
by A4, A8, A12, A33
.=
L * (- ((power K) . ((- (L ")),(0 + 1))))
by XREAL_1:232
.=
L * (- (- (L ")))
by GROUP_1:50
.=
L * (L ")
by RLVECT_1:17
.=
1_ K
by A6, VECTSP_1:def 10
.=
(1. (K,n)) * (
i,
j)
by A12, A33, MATRIX_1:def 3
;
verum end; suppose A34:
i > j1 + 1
;
(M * (Jordan_block (L,n))) * (i,j) = (1. (K,n)) * (i,j)then
i > j1
by NAT_1:13;
hence (M * (Jordan_block (L,n))) * (
i,
j) =
(L * (M * (i,j))) + (0. K)
by A4, A8, A27, A28
.=
L * (M * (i,j))
by RLVECT_1:def 4
.=
L * (0. K)
by A4, A8, A12, A34
.=
0. K
.=
(1. (K,n)) * (
i,
j)
by A12, A34, MATRIX_1:def 3
;
verum end; end; end; hence
(M * (Jordan_block (L,n))) * (
i,
j)
= (1. (K,n)) * (
i,
j)
;
verum end; end; end; hence
(1. (K,n)) * (
i,
j)
= (M * (Jordan_block (L,n))) * (
i,
j)
;
verum end;
then A35:
1. (K,n) = M * (Jordan_block (L,n))
by MATRIX_0:27;
set JM = (Jordan_block (L,n)) * M;
A36:
len M = n
by MATRIX_0:24;
take
M
; ( (Jordan_block (L,n)) ~ = M & ( for i, j being Nat st [i,j] in Indices M holds
( ( i > j implies M * (i,j) = 0. K ) & ( i <= j implies M * (i,j) = - ((power K) . ((- (L ")),((j -' i) + 1))) ) ) ) )
A37:
( Indices ((Jordan_block (L,n)) * M) = Indices (1. (K,n)) & width (Jordan_block (L,n)) = n )
by MATRIX_0:24, MATRIX_0:26;
now for i, j being Nat st [i,j] in Indices (1. (K,n)) holds
(1. (K,n)) * (i,j) = ((Jordan_block (L,n)) * M) * (i,j)let i,
j be
Nat;
( [i,j] in Indices (1. (K,n)) implies (1. (K,n)) * (i,j) = ((Jordan_block (L,n)) * M) * (i,j) )assume A38:
[i,j] in Indices (1. (K,n))
;
(1. (K,n)) * (i,j) = ((Jordan_block (L,n)) * M) * (i,j)A39:
i in Seg n
by A5, A38, ZFMISC_1:87;
set i1 =
i + 1;
A40:
j in Seg n
by A5, A38, ZFMISC_1:87;
A41:
((Jordan_block (L,n)) * M) * (
i,
j)
= (Line ((Jordan_block (L,n)),i)) "*" (Col (M,j))
by A36, A37, A38, MATRIX_3:def 4;
set C =
Col (
M,
j);
A42:
dom M = Seg n
by A36, FINSEQ_1:def 3;
then A43:
(Col (M,j)) . i = M * (
i,
j)
by A39, MATRIX_0:def 8;
A44:
dom (Col (M,j)) = Seg n
by A36, FINSEQ_2:124;
then A45:
(Col (M,j)) /. i = (Col (M,j)) . i
by A39, PARTFUN1:def 6;
now ((Jordan_block (L,n)) * M) * (i,j) = (1. (K,n)) * (i,j)per cases
( i = n or i <> n )
;
suppose A46:
i = n
;
((Jordan_block (L,n)) * M) * (i,j) = (1. (K,n)) * (i,j)then A47:
((Jordan_block (L,n)) * M) * (
i,
j)
= L * (M * (i,j))
by A36, A39, A45, A43, A41, Th6;
now ((Jordan_block (L,n)) * M) * (i,j) = (1. (K,n)) * (i,j)per cases
( i > j or i <= j )
;
suppose A49:
i <= j
;
((Jordan_block (L,n)) * M) * (i,j) = (1. (K,n)) * (i,j)
j <= n
by A40, FINSEQ_1:1;
then A50:
j = n
by A46, A49, XXREAL_0:1;
hence ((Jordan_block (L,n)) * M) * (
i,
j) =
L * (- ((power K) . ((- (L ")),((n -' n) + 1))))
by A4, A8, A38, A46, A47
.=
L * (- ((power K) . ((- (L ")),(0 + 1))))
by XREAL_1:232
.=
L * (- (- (L ")))
by GROUP_1:50
.=
L * (L ")
by RLVECT_1:17
.=
1_ K
by A6, VECTSP_1:def 10
.=
(1. (K,n)) * (
i,
j)
by A38, A46, A50, MATRIX_1:def 3
;
verum end; end; end; hence
((Jordan_block (L,n)) * M) * (
i,
j)
= (1. (K,n)) * (
i,
j)
;
verum end; suppose A51:
i <> n
;
(1. (K,n)) * (i,j) = ((Jordan_block (L,n)) * M) * (i,j)
i <= n
by A39, FINSEQ_1:1;
then
i < n
by A51, XXREAL_0:1;
then
( 1
<= i + 1 &
i + 1
<= n )
by NAT_1:11, NAT_1:13;
then A52:
i + 1
in Seg n
;
then A53:
[(i + 1),j] in Indices M
by A8, A5, A40, ZFMISC_1:87;
(
(Col (M,j)) /. (i + 1) = (Col (M,j)) . (i + 1) &
(Col (M,j)) . (i + 1) = M * (
(i + 1),
j) )
by A42, A44, A52, MATRIX_0:def 8, PARTFUN1:def 6;
then A54:
((Jordan_block (L,n)) * M) * (
i,
j)
= (L * (M * (i,j))) + (M * ((i + 1),j))
by A36, A39, A45, A43, A41, A51, Th6;
now ((Jordan_block (L,n)) * M) * (i,j) = (1. (K,n)) * (i,j)per cases
( i > j or i = j or i < j )
by XXREAL_0:1;
suppose A55:
i > j
;
((Jordan_block (L,n)) * M) * (i,j) = (1. (K,n)) * (i,j)then
i + 1
> j
by NAT_1:13;
hence ((Jordan_block (L,n)) * M) * (
i,
j) =
(L * (M * (i,j))) + (0. K)
by A4, A53, A54
.=
L * (M * (i,j))
by RLVECT_1:def 4
.=
L * (0. K)
by A4, A8, A38, A55
.=
0. K
.=
(1. (K,n)) * (
i,
j)
by A38, A55, MATRIX_1:def 3
;
verum end; suppose A56:
i = j
;
((Jordan_block (L,n)) * M) * (i,j) = (1. (K,n)) * (i,j)then
i + 1
> j
by NAT_1:13;
hence ((Jordan_block (L,n)) * M) * (
i,
j) =
(L * (M * (i,j))) + (0. K)
by A4, A53, A54
.=
L * (M * (i,i))
by A56, RLVECT_1:def 4
.=
L * (- ((power K) . ((- (L ")),((i -' i) + 1))))
by A4, A8, A38, A56
.=
L * (- ((power K) . ((- (L ")),(0 + 1))))
by XREAL_1:232
.=
L * (- (- (L ")))
by GROUP_1:50
.=
L * (L ")
by RLVECT_1:17
.=
1_ K
by A6, VECTSP_1:def 10
.=
(1. (K,n)) * (
i,
j)
by A38, A56, MATRIX_1:def 3
;
verum end; suppose A57:
i < j
;
((Jordan_block (L,n)) * M) * (i,j) = (1. (K,n)) * (i,j)set P =
(power K) . (
(- (L ")),
((j -' (i + 1)) + 1));
A58:
j -' i = j - i
by A57, XREAL_1:233;
A59:
i + 1
<= j
by A57, NAT_1:13;
then A60:
j -' (i + 1) = j - (i + 1)
by XREAL_1:233;
thus ((Jordan_block (L,n)) * M) * (
i,
j) =
(L * (M * (i,j))) + (- ((power K) . ((- (L ")),((j -' (i + 1)) + 1))))
by A4, A53, A54, A59
.=
(L * (- ((power K) . ((- (L ")),((j -' i) + 1))))) + (- ((power K) . ((- (L ")),((j -' (i + 1)) + 1))))
by A4, A8, A38, A57
.=
(L * (- ((- (L ")) * ((power K) . ((- (L ")),((j -' (i + 1)) + 1)))))) + (- ((power K) . ((- (L ")),((j -' (i + 1)) + 1))))
by A60, A58, GROUP_1:def 7
.=
(L * ((- (- (L "))) * ((power K) . ((- (L ")),((j -' (i + 1)) + 1))))) + (- ((power K) . ((- (L ")),((j -' (i + 1)) + 1))))
by VECTSP_1:9
.=
(L * ((L ") * ((power K) . ((- (L ")),((j -' (i + 1)) + 1))))) + (- ((power K) . ((- (L ")),((j -' (i + 1)) + 1))))
by RLVECT_1:17
.=
((L * (L ")) * ((power K) . ((- (L ")),((j -' (i + 1)) + 1)))) + (- ((power K) . ((- (L ")),((j -' (i + 1)) + 1))))
by GROUP_1:def 3
.=
((1_ K) * ((power K) . ((- (L ")),((j -' (i + 1)) + 1)))) + (- ((power K) . ((- (L ")),((j -' (i + 1)) + 1))))
by A6, VECTSP_1:def 10
.=
((power K) . ((- (L ")),((j -' (i + 1)) + 1))) + (- ((power K) . ((- (L ")),((j -' (i + 1)) + 1))))
.=
0. K
by RLVECT_1:def 10
.=
(1. (K,n)) * (
i,
j)
by A38, A57, MATRIX_1:def 3
;
verum end; end; end; hence
(1. (K,n)) * (
i,
j)
= ((Jordan_block (L,n)) * M) * (
i,
j)
;
verum end; end; end; hence
(1. (K,n)) * (
i,
j)
= ((Jordan_block (L,n)) * M) * (
i,
j)
;
verum end;
then
1. (K,n) = (Jordan_block (L,n)) * M
by MATRIX_0:27;
then
M is_reverse_of Jordan_block (L,n)
by A35, MATRIX_6:def 2;
hence
( (Jordan_block (L,n)) ~ = M & ( for i, j being Nat st [i,j] in Indices M holds
( ( i > j implies M * (i,j) = 0. K ) & ( i <= j implies M * (i,j) = - ((power K) . ((- (L ")),((j -' i) + 1))) ) ) ) )
by A4, A7, MATRIX_6:def 4; verum