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 13;
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 P = - ((power K) . (- (L " )),((j -' i) + 1)); :: thesis: S₁[i,j,P]
thus S₁[i,j,P] by A3; :: thesis: verum

end;

end;

end;

A4: for i, j being Nat st [i,j] in [:(Seg N),(Seg N):] holds
for x1, x2 being Element of K st S₁[i,j,x1] & S₁[i,j,x2] holds
x1 = x2 ;
consider M being Matrix of N,K such that
A5: for i, j being Nat st [i,j] in Indices M holds
S₁[i,j,M * i,j] from MATRIX_1:sch 2(A4, A1);
set ONE = 1. K,n;
set J = Jordan_block L,n;
A6: Indices (1. K,n) = [:(Seg n),(Seg n):] by MATRIX_1:25;
assume A7: 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 A8: Jordan_block L,n is invertible by Th3;
reconsider M = M as Matrix of n,K ;
set MJ = M * (Jordan_block L,n);
A9: ( Indices M = Indices (Jordan_block L,n) & Indices (Jordan_block L,n) = Indices (1. K,n) ) by MATRIX_1:27;
A10: width M = n by MATRIX_1:25;
A11: ( Indices (M * (Jordan_block L,n)) = Indices (1. K,n) & len (Jordan_block L,n) = n ) by MATRIX_1:25, MATRIX_1:27;

now

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 A6, A12, ZFMISC_1:106;
set LL = Line M,i;
A14: (M * (Jordan_block L,n)) * i,j = (Line M,i) "*" (Col (Jordan_block L,n),j) by A10, A11, A12, MATRIX_3:def 4
.= (Col (Jordan_block L,n),j) "*" (Line M,i) by FVSUM_1:115 ;
A15: j in Seg n by A6, A12, ZFMISC_1:106;
then A16: (Line M,i) . j = M * i,j by A10, MATRIX_1:def 8;
A17: dom (Line M,i) = Seg n by A10, FINSEQ_2:144;
then A18: (Line M,i) /. j = (Line M,i) . j by A15, PARTFUN1:def 8;

now

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 A10, A15, A18, A16, A14, Th7;

now

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 A5, A9, A12, A20
.= L * (- ((power K) . (- (L " )),(0 + 1))) by XREAL_1:234
.= L * (- (- (L " ))) by GROUP_1:98
.= L * (L " ) by RLVECT_1:30
.= 1_ K by A7, VECTSP_1:def 22
.= (1. K,n) * i,j by A12, A21, MATRIX_1:def 12 ;
:: 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:3;
then j < i by A19, A22, XXREAL_0:1;
hence (M * (Jordan_block L,n)) * i,j = L * (0. K) by A5, A9, A12, A20
.= 0. K by VECTSP_1:36
.= (1. K,n) * i,j by A12, A22, MATRIX_1:def 12 ;
:: 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:3;
then reconsider j1 = j - 1 as Element of NAT by NAT_1:21;
( j1 <= j1 + 1 & j <= n ) by A15, FINSEQ_1:3, 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 A6, A13, ZFMISC_1:106;
( (Line M,i) /. j1 = (Line M,i) . j1 & (Line M,i) . j1 = M * i,j1 ) by A10, A17, A26, MATRIX_1:def 8, PARTFUN1:def 8;
then A28: (M * (Jordan_block L,n)) * i,j = (L * (M * i,j)) + (M * i,j1) by A10, A15, A18, A16, A14, A23, Th7;

now

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:235;
A31: i <= j1 by A29, NAT_1:13;
then A32: j1 -' i = j1 - i by XREAL_1:235;
thus (M * (Jordan_block L,n)) * i,j = (L * (M * i,j)) + (- ((power K) . (- (L " )),((j1 -' i) + 1))) by A5, A9, A27, A28, A31
.= (L * (- ((power K) . (- (L " )),((j -' i) + 1)))) + (- ((power K) . (- (L " )),((j1 -' i) + 1))) by A5, A9, A12, A29
.= (L * (- ((- (L " )) * ((power K) . (- (L " )),((j1 -' i) + 1))))) + (- ((power K) . (- (L " )),((j1 -' i) + 1))) by A32, A30, GROUP_1:def 8
.= (L * ((- (- (L " ))) * ((power K) . (- (L " )),((j1 -' i) + 1)))) + (- ((power K) . (- (L " )),((j1 -' i) + 1))) by VECTSP_1:41
.= (L * ((L " ) * ((power K) . (- (L " )),((j1 -' i) + 1)))) + (- ((power K) . (- (L " )),((j1 -' i) + 1))) by RLVECT_1:30
.= ((L * (L " )) * ((power K) . (- (L " )),((j1 -' i) + 1))) + (- ((power K) . (- (L " )),((j1 -' i) + 1))) by GROUP_1:def 4
.= ((1_ K) * ((power K) . (- (L " )),((j1 -' i) + 1))) + (- ((power K) . (- (L " )),((j1 -' i) + 1))) by A7, VECTSP_1:def 22
.= ((power K) . (- (L " )),((j1 -' i) + 1)) + (- ((power K) . (- (L " )),((j1 -' i) + 1))) by VECTSP_1:def 16
.= 0. K by RLVECT_1:def 13
.= (1. K,n) * i,j by A12, A29, MATRIX_1:def 12 ; :: 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 A5, A9, A27, A28
.= L * (M * i,j) by RLVECT_1:def 7
.= L * (- ((power K) . (- (L " )),((i -' i) + 1))) by A5, A9, A12, A33
.= L * (- ((power K) . (- (L " )),(0 + 1))) by XREAL_1:234
.= L * (- (- (L " ))) by GROUP_1:98
.= L * (L " ) by RLVECT_1:30
.= 1_ K by A7, VECTSP_1:def 22
.= (1. K,n) * i,j by A12, A33, MATRIX_1:def 12 ;
:: 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 A5, A9, A27, A28
.= L * (M * i,j) by RLVECT_1:def 7
.= L * (0. K) by A5, A9, A12, A34
.= 0. K by VECTSP_1:36
.= (1. K,n) * i,j by A12, A34, MATRIX_1:def 12 ;
:: 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_1:28;
set JM = (Jordan_block L,n) * M;
A36: len M = n by MATRIX_1:25;
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_1:25, MATRIX_1:27;

now

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 A6, A38, ZFMISC_1:106;
set i1 = i + 1;
A40: j in Seg n by A6, A38, ZFMISC_1:106;
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_1:def 9;
A44: dom (Col M,j) = Seg n by A36, FINSEQ_2:144;
then A45: (Col M,j) /. i = (Col M,j) . i by A39, PARTFUN1:def 8;

now

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

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 A5, A9, A38, A47
.= 0. K by VECTSP_1:36
.= (1. K,n) * i,j by A38, A48, MATRIX_1:def 12 ;
:: 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:3;
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 A5, A9, A38, A46, A47
.= L * (- ((power K) . (- (L " )),(0 + 1))) by XREAL_1:234
.= L * (- (- (L " ))) by GROUP_1:98
.= L * (L " ) by RLVECT_1:30
.= 1_ K by A7, VECTSP_1:def 22
.= (1. K,n) * i,j by A38, A46, A50, MATRIX_1:def 12 ;
:: 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:3;
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 A9, A6, A40, ZFMISC_1:106;
( (Col M,j) /. (i + 1) = (Col M,j) . (i + 1) & (Col M,j) . (i + 1) = M * (i + 1),j ) by A42, A44, A52, MATRIX_1:def 9, PARTFUN1:def 8;
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

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 A5, A53, A54
.= L * (M * i,j) by RLVECT_1:def 7
.= L * (0. K) by A5, A9, A38, A55
.= 0. K by VECTSP_1:36
.= (1. K,n) * i,j by A38, A55, MATRIX_1:def 12 ;
:: 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 A5, A53, A54
.= L * (M * i,i) by A56, RLVECT_1:def 7
.= L * (- ((power K) . (- (L " )),((i -' i) + 1))) by A5, A9, A38, A56
.= L * (- ((power K) . (- (L " )),(0 + 1))) by XREAL_1:234
.= L * (- (- (L " ))) by GROUP_1:98
.= L * (L " ) by RLVECT_1:30
.= 1_ K by A7, VECTSP_1:def 22
.= (1. K,n) * i,j by A38, A56, MATRIX_1:def 12 ;
:: 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:235;
A59: i + 1 <= j by A57, NAT_1:13;
then A60: j -' (i + 1) = j - (i + 1) by XREAL_1:235;
thus ((Jordan_block L,n) * M) * i,j = (L * (M * i,j)) + (- ((power K) . (- (L " )),((j -' (i + 1)) + 1))) by A5, A53, A54, A59
.= (L * (- ((power K) . (- (L " )),((j -' i) + 1)))) + (- ((power K) . (- (L " )),((j -' (i + 1)) + 1))) by A5, A9, A38, A57
.= (L * (- ((- (L " )) * ((power K) . (- (L " )),((j -' (i + 1)) + 1))))) + (- ((power K) . (- (L " )),((j -' (i + 1)) + 1))) by A60, A58, GROUP_1:def 8
.= (L * ((- (- (L " ))) * ((power K) . (- (L " )),((j -' (i + 1)) + 1)))) + (- ((power K) . (- (L " )),((j -' (i + 1)) + 1))) by VECTSP_1:41
.= (L * ((L " ) * ((power K) . (- (L " )),((j -' (i + 1)) + 1)))) + (- ((power K) . (- (L " )),((j -' (i + 1)) + 1))) by RLVECT_1:30
.= ((L * (L " )) * ((power K) . (- (L " )),((j -' (i + 1)) + 1))) + (- ((power K) . (- (L " )),((j -' (i + 1)) + 1))) by GROUP_1:def 4
.= ((1_ K) * ((power K) . (- (L " )),((j -' (i + 1)) + 1))) + (- ((power K) . (- (L " )),((j -' (i + 1)) + 1))) by A7, VECTSP_1:def 22
.= ((power K) . (- (L " )),((j -' (i + 1)) + 1)) + (- ((power K) . (- (L " )),((j -' (i + 1)) + 1))) by VECTSP_1:def 16
.= 0. K by RLVECT_1:def 13
.= (1. K,n) * i,j by A38, A57, MATRIX_1:def 12 ; :: 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_1:28;
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 A5, A8, MATRIX_6:def 4; :: thesis: verum