let n be Nat; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 S₁[ 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 S₁[i,j,x]

proof

let i, j be Nat; :: thesis: ( [i,j] in [:(Seg N),(Seg N):] implies ex x being Element of K st S₁[i,j,x] )
assume [i,j] in [:(Seg N),(Seg N):] ; :: thesis: ex x being Element of K st S₁[i,j,x]

per cases ( i > j or i <= j ) ;

suppose A2: i > j ; :: thesis: ex x being Element of K st S₁[i,j,x]

take 0. K ; :: thesis: S₁[i,j, 0. K]
thus S₁[i,j, 0. K] by A2; :: thesis: verum

end;

suppose A3: i <= j ; :: thesis: ex x being Element of K st S₁[i,j,x]

take - ((power K) . ((- (L ")),((j -' i) + 1))) ; :: thesis: S₁[i,j, - ((power K) . ((- (L ")),((j -' i) + 1)))]
thus S₁[i,j, - ((power K) . ((- (L ")),((j -' i) + 1)))] by A3; :: thesis: verum

end;

end;

end;

consider M being Matrix of N,K such that
A4: for i, j being Nat st [i,j] in Indices M holds
S₁[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 ; :: thesis: 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 :: thesis: 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; :: thesis: ( [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)) ; :: thesis: (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 :: thesis: (1. (K,n)) * (i,j) = (M * (Jordan_block (L,n))) * (i,j)

per cases ( j = 1 or j <> 1 ) ;

suppose A19: j = 1 ; :: thesis: (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 :: thesis: (M * (Jordan_block (L,n))) * (i,j) = (1. (K,n)) * (i,j)

per cases ( i = j or i <> j ) ;

suppose A21: i = j ; :: thesis: (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 ;
:: thesis: verum

end;

suppose A22: i <> j ; :: thesis: (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 ;
:: thesis: verum

end;

end;

end;

hence (1. (K,n)) * (i,j) = (M * (Jordan_block (L,n))) * (i,j) ; :: thesis: verum

end;

suppose A23: j <> 1 ; :: thesis: (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 :: thesis: (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 ; :: thesis: (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 ; :: thesis: verum

end;

suppose A33: i = j1 + 1 ; :: thesis: (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 ;
:: thesis: verum

end;

suppose A34: i > j1 + 1 ; :: thesis: (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 ;
:: thesis: verum

end;

end;

end;

hence (M * (Jordan_block (L,n))) * (i,j) = (1. (K,n)) * (i,j) ; :: thesis: verum

end;

end;

end;

hence (1. (K,n)) * (i,j) = (M * (Jordan_block (L,n))) * (i,j) ; :: thesis: 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 ; :: thesis: ( (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 :: thesis: 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; :: thesis: ( [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)) ; :: thesis: (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 :: thesis: ((Jordan_block (L,n)) * M) * (i,j) = (1. (K,n)) * (i,j)

per cases ( i = n or i <> n ) ;

suppose A46: i = n ; :: thesis: ((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 :: thesis: ((Jordan_block (L,n)) * M) * (i,j) = (1. (K,n)) * (i,j)

per cases ( i > j or i <= j ) ;

suppose A48: i > j ; :: thesis: ((Jordan_block (L,n)) * M) * (i,j) = (1. (K,n)) * (i,j)

hence ((Jordan_block (L,n)) * M) * (i,j) = L * (0. K) by A4, A8, A38, A47
.= 0. K
.= (1. (K,n)) * (i,j) by A38, A48, MATRIX_1:def 3 ;
:: thesis: verum

end;

suppose A49: i <= j ; :: thesis: ((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 ;
:: thesis: verum

end;

end;

end;

hence ((Jordan_block (L,n)) * M) * (i,j) = (1. (K,n)) * (i,j) ; :: thesis: verum

end;

suppose A51: i <> n ; :: thesis: (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 :: thesis: ((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 ; :: thesis: ((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 ;
:: thesis: verum

end;

suppose A56: i = j ; :: thesis: ((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 ;
:: thesis: verum

end;

suppose A57: i < j ; :: thesis: ((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 ; :: thesis: verum

end;

end;

end;

hence (1. (K,n)) * (i,j) = ((Jordan_block (L,n)) * M) * (i,j) ; :: thesis: verum

end;

end;

end;

hence (1. (K,n)) * (i,j) = ((Jordan_block (L,n)) * M) * (i,j) ; :: thesis: 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; :: thesis: verum