:: Jordan Matrix Decomposition
:: by Karol P\c{a}k
::
:: Received July 11, 2008
:: Copyright (c) 2008-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, NAT_1, VECTSP_1, SUBSET_1, FUNCT_1, RELAT_1, FUNCT_4,
XBOOLE_0, FUNCOP_1, MATRIX_1, FINSEQ_1, TREES_1, ARYTM_3, GROUP_1,
SUPINF_2, ZFMISC_1, XXREAL_0, MATRIX_3, FINSEQ_2, ALGSTR_0, SETWISEO,
CARD_3, CARD_1, INCSP_1, MESFUNC1, STRUCT_0, FVSUM_1, PARTFUN1, RVSUM_1,
ARYTM_1, MATRIX_6, MATRIXJ1, MATHMORP, ORDINAL4, RFINSEQ, BCIALG_2,
NEWTON, GRCAT_1, FUNCSDOM, VECTSP_2, RANKNULL, VECTSP10, HURWITZ, TARSKI,
RLSUB_1, RLVECT_5, MATRLIN, MATRLIN2, MATRIXR1, FINSEQ_4, RLVECT_3,
FINSET_1, RLVECT_2, POLYNOM5, VECTSP11, RLSUB_2, PRVECT_1, MATRIXJ2,
UNIALG_1, MSSUBFAM, XCMPLX_0;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS,
CARD_1, XCMPLX_0, ALGSTR_0, XXREAL_0, NAT_1, FINSET_1, RELAT_1,
FUNCT_1, PARTFUN1, FUNCT_2, SETWOP_2, FINSEQ_1, PRVECT_1,
FUNCOP_1, STRUCT_0, RLVECT_1, GROUP_1, VECTSP_1, GCD_1, FINSEQ_2,
MATRIX_0, MATRIX_1, FVSUM_1, NAT_D, GROUP_4, MATRIX_3, MATRIX_6,
FUNCT_4, DOMAIN_1, VECTSP_4, VECTSP_6, VECTSP_7, VECTSP_9,
MATRIX13, MATRLIN, FUNCT_7, LAPLACE, MOD_2, RFINSEQ, VECTSP_2,
VECTSP_5, MATRIX15, RANKNULL, POLYNOM5, WSIERP_1, MATRIXJ1,
MATRLIN2, VECTSP11, GRCAT_1;
constructors FINSOP_1, GROUP_4, WELLORD2, GCD_1, VECTSP_2, VECTSP_7,
VECTSP_9, MATRIX_6, REALSET1, LAPLACE, VECTSP_5, RANKNULL,
MATRIX15, POLYNOM5, MATRIXJ1, MATRLIN2, VECTSP11, REAL_1,
BINARITH, RELSET_1, FUNCT_7, MATRIX13, FVSUM_1, GRCAT_1, MATRIX_1,
NUMBERS, RECDEF_1, MATRIX_3;
registrations XBOOLE_0, FINSET_1, STRUCT_0, VECTSP_1, VECTSP_2, FUNCT_2,
ORDINAL1, XXREAL_0, NAT_1, FINSEQ_1, RELAT_1, CARD_1, FINSEQ_2,
XREAL_0, VECTSP_9, VALUED_0, MATRIXJ1, VECTSP11, POLYNOM5,
FUNCOP_1, RELSET_1, MOD_2, GRCAT_1, PRVECT_1, MATRIX13, MATRLIN2,
MATRIX_6, MATRIX_1, MATRIX_3, LAPLACE;
requirements ARITHM, NUMERALS, REAL, BOOLE, SUBSET;
definitions TARSKI, FUNCT_1, MATRIXJ1;
equalities STRUCT_0, RLVECT_1, FINSEQ_1, VECTSP_4, RELAT_1, GROUP_4, FVSUM_1,
MATRIX_0, FUNCOP_1, MATRLIN2;
expansions STRUCT_0, TARSKI, FINSEQ_1, FUNCT_1;
theorems ZFMISC_1, RLVECT_1, MATRIX_0, MATRIX_1, MATRIX_3, VECTSP_1, NAT_1,
FINSEQ_2, CARD_1, CARD_2, FINSEQ_1, FINSEQ_3, FRECHET, FUNCT_1, FUNCT_2,
FUNCT_7, FUNCOP_1, FVSUM_1, GROUP_1, LAPLACE, MATRIX_6, MATRIX13,
MATRIXR1, MATRIXR2, MATRLIN, ORDINAL1, PARTFUN1, RELAT_1, STIRL2_1,
TARSKI, WELLORD2, VECTSP_4, VECTSP_6, VECTSP_7, VECTSP_9, XBOOLE_0,
XBOOLE_1, XREAL_1, XXREAL_0, MATRIX15, MOD_2, VECTSP10, RANKNULL,
VECTSP_5, FINSEQ_4, FINSEQ_5, RFINSEQ, RVSUM_1, POLYNOM3, POLYNOM4,
MATRIXJ1, MATRLIN2, VECTSP11, FUNCT_4, NAT_D, GRCAT_1, STRUCT_0;
schemes NAT_1, MATRIX_0, FUNCT_2;
begin :: Jordan blocks
reserve i,j,m,n,k for Nat,
x,y for set,
K for Field,
a,L for Element of K;
Lm1: for f be Function st f is one-to-one & x in dom f holds rng (f+*(x,y)) =
(rng f)\{f.x}\/{y}
proof
let f be Function such that
A1: f is one-to-one and
A2: x in dom f;
set xy=x.-->y;
dom xy = {x} & rng xy = {y} by FUNCOP_1:8;
then rng(f+*xy) = f.:(dom f\{x})\/{y} by FRECHET:12
.= (f.:(dom f))\(f.:{x})\/{y} by A1,FUNCT_1:64
.= (rng f)\Im(f,x)\/{y} by RELAT_1:113
.= (rng f)\{f.x}\/{y} by A2,FUNCT_1:59;
hence thesis by A2,FUNCT_7:def 3;
end;
definition
let K,L,n;
func Jordan_block(L,n) -> Matrix of K means
:Def1:
len it = n & width it = n & for i,j st [i,j] in Indices it holds
( i = j implies it*(i,j) = L ) &
( i+1 = j implies it*(i,j) = 1_K ) &
(i<>j & i+1<>j implies it*(i,j) = 0.K );
existence
proof
defpred P[Nat,Nat,set] means ($1 = $2 implies $3 = L) & ($1+1 = $2 implies
$3 = 1_K ) & ($1<>$2 & $1+1<>$2 implies $3 = 0.K);
reconsider N=n as Element of NAT by ORDINAL1:def 12;
A1: for i,j st [i,j] in [:Seg N, Seg N:] ex x be Element of K st P[i,j,x]
proof
let i,j such that
[i,j] in [:Seg N, Seg N:];
per cases;
suppose
A2: i=j;
take L;
thus thesis by A2;
end;
suppose
A3: i+1=j;
take 1_K;
thus thesis by A3;
end;
suppose
A4: i<>j & i+1<>j;
take 0.K;
thus thesis by A4;
end;
end;
consider M be Matrix of N,K such that
A5: for i,j st [i,j] in Indices M holds P[i,j,M*(i,j)] from MATRIX_0:
sch 2(A1);
take M;
thus thesis by A5,MATRIX_0:24;
end;
uniqueness
proof
let M1,M2 be Matrix of K such that
A6: len M1 = n & width M1 = n and
A7: for i,j st [i,j] in Indices M1 holds ( i = j implies M1*(i,j) = L
) & ( i+1 = j implies M1*(i,j) = 1_K ) & (i<>j & i+1<>j implies M1*(i,j) = 0.K
) and
A8: len M2 = n & width M2 = n and
A9: for i,j st [i,j] in Indices M2 holds ( i = j implies M2*(i,j) = L
) & ( i+1 = j implies M2*(i,j) = 1_K ) & (i<>j & i+1<>j implies M2*(i,j) = 0.K
);
now
let i,j such that
A10: [i,j] in Indices M1;
A11: Indices M1 = [:Seg n,Seg n:] by A6,FINSEQ_1:def 3
.= Indices M2 by A8,FINSEQ_1:def 3;
i=j or i+1=j or i<>j & i+1<>j;
then
M1*(i,j)=L & M2*(i,j)=L or M1*(i,j)=1_K & M2*(i,j)=1_K or M1*(i,j)=
0.K & M2*(i,j)=0.K by A7,A9,A10,A11;
hence M1*(i,j)=M2*(i,j);
end;
hence thesis by A6,A8,MATRIX_0:21;
end;
end;
definition
let K,L,n;
redefine func Jordan_block(L,n) -> upper_triangular Matrix of n,K; :: redefines Jordan_block (MATRIXJ2, definition)
coherence
proof
len Jordan_block(L,n)=n & width Jordan_block(L,n)=n by Def1;
then reconsider LBn=Jordan_block(L,n) as Matrix of n,K by MATRIX_0:51;
now
let i,j such that
A1: [i,j] in Indices LBn;
assume
A2: i>j;
then i+1>j by NAT_1:13;
hence LBn*(i,j) = 0.K by A1,A2,Def1;
end;
hence thesis by MATRIX_1:def 12;
end;
end;
theorem Th1:
diagonal_of_Matrix Jordan_block(L,n) = n |-> L
proof
set B=Jordan_block(L,n);
A1: now
A2: [:Seg n,Seg n:]=Indices B by MATRIX_0:24;
let i;
assume 1<=i & i<=n;
then
A3: i in Seg n;
then
A4: [i,i] in [:Seg n,Seg n:] by ZFMISC_1:87;
thus (diagonal_of_Matrix B).i = B*(i,i) by A3,MATRIX_3:def 10
.= L by A4,A2,Def1
.= (n|->L).i by A3,FINSEQ_2:57;
end;
len diagonal_of_Matrix B=n & len (n |-> L)=n by CARD_1:def 7,MATRIX_3:def 10;
hence thesis by A1;
end;
theorem Th2:
Det Jordan_block(L,n) = power(K).(L,n)
proof
thus Det Jordan_block(L,n)=(the multF of K)$$ diagonal_of_Matrix
Jordan_block(L,n) by MATRIX13:7
.= Product(n|->L) by Th1
.= power(K).(L,n) by MATRIXJ1:5;
end;
theorem Th3:
Jordan_block(L,n) is invertible iff n = 0 or L <> 0.K
proof
set B=Jordan_block(L,n);
A1: B is invertible implies L <> 0.K or n=0
proof
assume B is invertible;
then Det B is unital by LAPLACE:34;
then Det B is non zero by LAPLACE:42,43;
then
A2: Det B<>0.K;
assume
A3: L=0.K;
assume n<>0;
then
A4: n in Seg n by FINSEQ_1:3;
then dom (n|->L)=Seg n & (n|->L).n=L by FINSEQ_2:57,124;
then 0.K = Product (n|->L) by A3,A4,FVSUM_1:82
.= (power K).(L,n) by MATRIXJ1:5;
hence thesis by A2,Th2;
end;
n = 0 or L <> 0.K implies B is invertible
proof
assume
A5: n=0 or L<>0.K;
assume not B is invertible;
then Det B is non unital by LAPLACE:34;
then Det B is zero;
then 0.K = Det B
.= (power K).(L,n) by Th2
.= Product (n|->L) by MATRIXJ1:5;
then
A6: ex k be Nat st k in dom (n|->L) & (n|->L).k=0. K by FVSUM_1:82;
dom (n|->L)=Seg n by FINSEQ_2:124;
hence thesis by A5,A6,FINSEQ_2:57;
end;
hence thesis by A1;
end;
theorem Th4:
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)
proof
assume that
A1: i in Seg n and
A2: i<>n;
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(ONE,i);
set Li1=Line(ONE,i1);
set LJ=Line(J,i);
A3: width ONE=n by MATRIX_0:24;
A4: Indices ONE=Indices J by MATRIX_0:26;
reconsider Li,Li1,LJ as Element of N-tuples_on the carrier of K by
MATRIX_0:24;
A5: Indices ONE=[:Seg n,Seg n:] by MATRIX_0:24;
A6: width J=n by MATRIX_0:24;
now
let j such that
A7: j in Seg n;
Li.j=ONE*(i,j) by A3,A7,MATRIX_0:def 7;
then
A8: (L*Li).j=L*(ONE*(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<=i1 & i1<=n by NAT_1:11,13;
then i1 in Seg n;
then
A10: [i1,j] in [:Seg n,Seg n:] by A7,ZFMISC_1:87;
Li1.j=ONE*(i1,j) by A3,A7,MATRIX_0:def 7;
then
A11: (L*Li+Li1).j=L*(ONE*(i,j))+ONE*(i1,j) by A7,A8,FVSUM_1:18;
A12: LJ.j=J*(i,j) by A6,A7,MATRIX_0:def 7;
now
per cases;
suppose
A13: i=j;
then
A14: i1>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*(ONE*(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;
end;
suppose
A15: i1=j;
then
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*(ONE*(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;
end;
suppose
A17: i<>j & i1<>j;
hence 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*(ONE*(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;
end;
end;
hence (L*Li+Li1).j=LJ.j;
end;
hence thesis by FINSEQ_2:119;
end;
theorem Th5:
Line(Jordan_block(L,n),n) = L*Line(1.(K,n),n)
proof
set ONE=1.(K,n);
set Ln=Line(ONE,n);
set J=Jordan_block(L,n);
set LJ=Line(J,n);
reconsider N=n as Element of NAT by ORDINAL1:def 12;
A1: width J=n by MATRIX_0:24;
A2: Indices ONE=Indices J by MATRIX_0:26;
reconsider Ln,LJ as Element of N-tuples_on the carrier of K by MATRIX_0:24;
A3: Indices ONE=[:Seg n,Seg n:] by MATRIX_0:24;
A4: width ONE=n by MATRIX_0:24;
now
let j such that
A5: j in Seg n;
n <> 0 by A5;
then n in Seg n by FINSEQ_1:3;
then
A6: [n,j] in [:Seg n,Seg n:] by A5,ZFMISC_1:87;
Ln.j=ONE*(n,j) by A4,A5,MATRIX_0:def 7;
then
A7: (L*Ln).j=L*(ONE*(n,j)) by A5,FVSUM_1:51;
A8: LJ.j=J*(n,j) by A1,A5,MATRIX_0:def 7;
now
per cases;
suppose
A9: n=j;
hence LJ.j = L by A3,A2,A6,A8,Def1
.= L*1_K
.= (L*Ln).j by A3,A6,A7,A9,MATRIX_1:def 3;
end;
suppose
n+1=j;
then j>n by NAT_1:13;
hence (L*Ln).j=LJ.j by A5,FINSEQ_1:1;
end;
suppose
A10: n<>j & n+1<>j;
hence LJ.j = 0.K by A3,A2,A6,A8,Def1
.= L*0.K
.= (L*Ln).j by A3,A6,A7,A10,MATRIX_1:def 3;
end;
end;
hence (L*Ln).j=LJ.j;
end;
hence thesis by FINSEQ_2:119;
end;
theorem Th6:
for F be Element of n-tuples_on the carrier of K st i in Seg n
holds ( i <> n implies Line(Jordan_block(L,n),i) "*" F = L * (F/.i)+ F/.(i+1))&
( i = n implies Line(Jordan_block(L,n),i) "*" F = L * (F/.i))
proof
let F be Element of n-tuples_on the carrier of K such that
A1: i in Seg n;
set J=Jordan_block(L,n);
A2: width J=n by MATRIX_0:24;
then
A3: Line(J,i).i=J*(i,i) by A1,MATRIX_0:def 7;
A4: Indices J=[:Seg n,Seg n:] by MATRIX_0:24;
then
A5: [i,i] in Indices J by A1,ZFMISC_1:87;
reconsider N=n as Element of NAT by ORDINAL1:def 12;
set Li=Line(J,i);
reconsider Li,f=F as Element of N-tuples_on the carrier of K by MATRIX_0:24;
A6: dom f=Seg n by FINSEQ_2:124;
then
A7: f.i=f/.i by A1,PARTFUN1:def 6;
A8: dom mlt(Li,f)=Seg n by FINSEQ_2:124;
thus i <> n implies Line(J,i) "*" F = L * (F/.i)+ F/.(i+1)
proof
A9: now
let j such that
A10: j in Seg n and
A11: j<>i & j<>i+1;
[i,j] in Indices J by A1,A4,A10,ZFMISC_1:87;
then
A12: 0.K = J*(i,j) by A11,Def1
.= Li.j by A2,A10,MATRIX_0:def 7;
f.j=f/.j by A6,A10,PARTFUN1:def 6;
hence mlt(Li,f).j = 0.K * (f/.j) by A10,A12,FVSUM_1:61
.= 0.K;
end;
A13: [i,i] in Indices J by A1,A4,ZFMISC_1:87;
assume
A14: i<>n;
i<=n by A1,FINSEQ_1:1;
then i<n by A14,XXREAL_0:1;
then 1<=i+1 & i+1<=n by NAT_1:11,13;
then
A15: i+1 in Seg n;
then
A16: [i,i+1] in Indices J by A1,A4,ZFMISC_1:87;
A17: f.i=f/.i & J*(i,i)=Li.i by A1,A2,A6,MATRIX_0:def 7,PARTFUN1:def 6;
A18: mlt(Li,f)/.i = mlt(Li,f).i by A1,A8,PARTFUN1:def 6
.= J*(i,i)*f/.i by A1,A17,FVSUM_1:61
.= L*(f/.i) by A13,Def1;
A19: i+1>i by NAT_1:13;
A20: f.(i+1)=f/.(i+1) & J*(i,i+1)=Li.(i+1) by A2,A6,A15,MATRIX_0:def 7
,PARTFUN1:def 6;
mlt(Li,f)/.(i+1) = mlt(Li,f).(i+1) by A8,A15,PARTFUN1:def 6
.= J*(i,i+1)*f/.(i+1) by A15,A20,FVSUM_1:61
.= 1_K*(f/.(i+1)) by A16,Def1
.= f/.(i+1);
hence thesis by A1,A8,A15,A19,A18,A9,MATRIX15:7;
end;
assume
A21: i=n;
now
let j such that
A22: j in Seg n and
A23: j<>i;
A24: f.j=f/.j by A6,A22,PARTFUN1:def 6;
j<=n by A22,FINSEQ_1:1;
then
A25: j<i+1 by A21,NAT_1:13;
A26: [i,j] in Indices J by A1,A4,A22,ZFMISC_1:87;
Line(J,i).j = J*(i,j) by A2,A22,MATRIX_0:def 7
.= 0.K by A23,A25,A26,Def1;
hence mlt(Line(J,i),f).j = 0.K*f/.j by A8,A22,A24,FVSUM_1:61
.= 0.K;
end;
hence Line(J,i)"*"F = mlt(Line(J,i),f).i by A1,A8,MATRIX_3:12
.= J*(i,i)*(f/.i) by A1,A8,A3,A7,FVSUM_1:61
.= L*(F/.i) by A5,Def1;
end;
theorem Th7:
for F be Element of n-tuples_on the carrier of K st i in Seg n
holds ( i = 1 implies Col(Jordan_block(L,n),i) "*" F = L * (F/.i) ) & ( i <> 1
implies Col(Jordan_block(L,n),i) "*" F = L * (F/.i)+F/.(i-1) )
proof
set J=Jordan_block(L,n);
set Ci=Col(J,i);
reconsider N=n as Element of NAT by ORDINAL1:def 12;
let F be Element of n-tuples_on the carrier of K such that
A1: i in Seg n;
A2: i>=1 by A1,FINSEQ_1:1;
then reconsider i1=i-1 as Element of NAT by NAT_1:21;
A3: len J=n & dom J=Seg len J by FINSEQ_1:def 3,MATRIX_0:24;
then
A4: Col(J,i).i=J*(i,i) by A1,MATRIX_0:def 8;
A5: i1+1>=i1 by NAT_1:11;
n>=i by A1,FINSEQ_1:1;
then
A6: n>=i1 by A5,XXREAL_0:2;
A7: Indices J=[:Seg n,Seg n:] by MATRIX_0:24;
then
A8: [i,i] in Indices J by A1,ZFMISC_1:87;
reconsider Ci,f=F as Element of N-tuples_on the carrier of K by MATRIX_0:24;
A9: dom f=Seg n by FINSEQ_2:124;
then
A10: f.i=f/.i by A1,PARTFUN1:def 6;
A11: dom mlt(Ci,f)=Seg n by FINSEQ_2:124;
then
A12: mlt(Ci,f)/.i = mlt(Ci,f).i by A1,PARTFUN1:def 6
.= J*(i,i)*f/.i by A1,A4,A10,FVSUM_1:61
.= L*(f/.i) by A8,Def1;
thus i = 1 implies Col(J,i) "*" F = L * (F/.i)
proof
A13: Col(J,i).i=J*(i,i) & f.i=f/.i by A1,A3,A9,MATRIX_0:def 8,PARTFUN1:def 6;
A14: [i,i] in Indices J by A1,A7,ZFMISC_1:87;
assume
A15: i=1;
now
let j such that
A16: j in Seg n and
A17: j<>i;
A18: f.j=f/.j by A9,A16,PARTFUN1:def 6;
1<=j by A16,FINSEQ_1:1;
then
A19: i<j+1 by A15,NAT_1:13;
A20: [j,i] in Indices J by A1,A7,A16,ZFMISC_1:87;
Col(J,i).j = J*(j,i) by A3,A16,MATRIX_0:def 8
.= 0.K by A17,A19,A20,Def1;
hence mlt(Col(J,i),f).j = 0.K*f/.j by A11,A16,A18,FVSUM_1:61
.= 0.K;
end;
hence Col(J,i)"*"F = mlt(Col(J,i),f).i by A1,A11,MATRIX_3:12
.= J*(i,i)*(f/.i) by A1,A11,A13,FVSUM_1:61
.= L*(F/.i) by A14,Def1;
end;
A21: i1<>i;
assume i<>1;
then i1+1>0+1 by A2,XXREAL_0:1;
then i1>=1 by NAT_1:14;
then
A22: i1 in Seg n by A6;
then
A23: i1+1=i & [i1,i] in Indices J by A1,A7,ZFMISC_1:87;
A24: now
let j such that
A25: j in Seg n and
A26: j<>i and
A27: j<>i1;
[j,i] in Indices J & j+1<>i by A1,A7,A25,A27,ZFMISC_1:87;
then
A28: 0.K = J*(j,i) by A26,Def1
.= Ci.j by A3,A25,MATRIX_0:def 8;
f.j=f/.j by A9,A25,PARTFUN1:def 6;
hence mlt(Ci,f).j = 0.K*(f/.j) by A25,A28,FVSUM_1:61
.= 0.K;
end;
A29: f.i1=f/.i1 by A9,A22,PARTFUN1:def 6;
A30: Col(J,i).i1=J*(i1,i) by A3,A22,MATRIX_0:def 8;
mlt(Ci,f)/.i1 = mlt(Ci,f).i1 by A11,A22,PARTFUN1:def 6
.= J*(i1,i)*f/.i1 by A22,A30,A29,FVSUM_1:61
.= 1_K*(f/.i1) by A23,Def1
.= f/.i1;
hence thesis by A1,A11,A22,A21,A12,A24,MATRIX15:7;
end;
theorem
L <> 0.K implies ex M be Matrix of n,K st Jordan_block(L,n)~ = M & for
i,j 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))
proof
reconsider N=n as Element of NAT by ORDINAL1:def 12;
defpred P[Nat,Nat,set] means ($1 > $2 implies $3 = 0.K) & ($1<= $2 implies
$3 = -power(K).(-L",$2-'$1+1) );
A1: for i,j st [i,j] in [:Seg N, Seg N:] ex x be Element of K st P[i,j,x]
proof
let i,j such that
[i,j] in [:Seg N,Seg N:];
per cases;
suppose
A2: i>j;
take 0.K;
thus thesis by A2;
end;
suppose
A3: i<=j;
take -power(K).(-L",j-'i+1);
thus thesis by A3;
end;
end;
consider M be Matrix of N,K such that
A4: for i,j st [i,j] in Indices M holds P[i,j,M*(i,j)] from MATRIX_0:sch
2(A1);
set ONE=1.(K,n);
set J=Jordan_block(L,n);
A5: Indices ONE= [:Seg n,Seg n:] by MATRIX_0:24;
assume
A6: L <> 0.K;
then
A7: J is invertible by Th3;
reconsider M as Matrix of n,K;
set MJ=M*J;
A8: Indices M=Indices J & Indices J=Indices ONE by MATRIX_0:26;
A9: width M=n by MATRIX_0:24;
A10: Indices MJ=Indices ONE by MATRIX_0:26;
A11: len J=n by MATRIX_0:24;
now
let i,j such that
A12: [i,j] in Indices ONE;
A13: i in Seg n by A5,A12,ZFMISC_1:87;
set LL=Line(M,i);
A14: MJ*(i,j) = LL"*"Col(J,j) by A9,A10,A12,A11,MATRIX_3:def 4
.= Col(J,j)"*"LL by FVSUM_1:90;
A15: j in Seg n by A5,A12,ZFMISC_1:87;
then
A16: LL.j=M*(i,j) by A9,MATRIX_0:def 7;
A17: dom LL=Seg n by A9,FINSEQ_2:124;
then
A18: LL/.j=LL.j by A15,PARTFUN1:def 6;
now
per cases;
suppose
A19: j=1;
then
A20: MJ*(i,j)= L* (M*(i,j)) by A9,A15,A18,A16,A14,Th7;
now
per cases;
suppose
A21: i=j;
hence MJ*(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
.= ONE*(i,j) by A12,A21,MATRIX_1:def 3;
end;
suppose
A22: i<>j;
1<=i by A13,FINSEQ_1:1;
then j<i by A19,A22,XXREAL_0:1;
hence MJ*(i,j) = L*0.K by A4,A8,A12,A20
.= 0.K
.= ONE*(i,j) by A12,A22,MATRIX_1:def 3;
end;
end;
hence ONE*(i,j)=MJ*(i,j);
end;
suppose
A23: j<>1;
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 ONE by A5,A13,ZFMISC_1:87;
LL/.j1=LL.j1 & LL.j1=M*(i,j1) by A9,A17,A26,MATRIX_0:def 7
,PARTFUN1:def 6;
then
A28: MJ*(i,j)= L* (M*(i,j))+M*(i,j1) by A9,A15,A18,A16,A14,A23,Th7;
now
per cases by XXREAL_0:1;
suppose
A29: i<j1+1;
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 MJ*(i,j) = L* (M*(i,j))+(-P) by A4,A8,A27,A28,A31
.= L*(-power(K).(-L",j-'i+1))+(-P) by A4,A8,A12,A29
.= L*(-(-L")*P)+(-P) by A32,A30,GROUP_1:def 7
.= L*((-(-L"))*P)+(-P) by VECTSP_1:9
.= L*(L"*P)+(-P) by RLVECT_1:17
.= (L*L")*P + (-P) by GROUP_1:def 3
.= 1_K*P + (-P) by A6,VECTSP_1:def 10
.= P + (-P)
.= 0.K by RLVECT_1:def 10
.= ONE*(i,j) by A12,A29,MATRIX_1:def 3;
end;
suppose
A33: i=j1+1;
then i>j1 by NAT_1:13;
hence MJ*(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
.= ONE*(i,j) by A12,A33,MATRIX_1:def 3;
end;
suppose
A34: i>j1+1;
then i>j1 by NAT_1:13;
hence MJ*(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
.= ONE*(i,j) by A12,A34,MATRIX_1:def 3;
end;
end;
hence MJ*(i,j)=ONE*(i,j);
end;
end;
hence ONE*(i,j)=MJ*(i,j);
end;
then
A35: ONE=MJ by MATRIX_0:27;
set JM=J*M;
A36: len M=n by MATRIX_0:24;
take M;
A37: Indices JM=Indices ONE & width J=n by MATRIX_0:24,26;
now
let i,j such that
A38: [i,j] in Indices ONE;
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: JM*(i,j)=Line(J,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: C.i=M*(i,j) by A39,MATRIX_0:def 8;
A44: dom C=Seg n by A36,FINSEQ_2:124;
then
A45: C/.i=C.i by A39,PARTFUN1:def 6;
now
per cases;
suppose
A46: i=n;
then
A47: JM*(i,j)=L*(M*(i,j)) by A36,A39,A45,A43,A41,Th6;
now
per cases;
suppose
A48: i>j;
hence JM*(i,j) = L*0.K by A4,A8,A38,A47
.= 0.K
.= ONE*(i,j) by A38,A48,MATRIX_1:def 3;
end;
suppose
A49: i<=j;
j<=n by A40,FINSEQ_1:1;
then
A50: j=n by A46,A49,XXREAL_0:1;
hence JM*(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
.= ONE*(i,j) by A38,A46,A50,MATRIX_1:def 3;
end;
end;
hence JM*(i,j)=ONE*(i,j);
end;
suppose
A51: i<>n;
i<=n by A39,FINSEQ_1:1;
then i<n by A51,XXREAL_0:1;
then 1<=i1 & i1<=n by NAT_1:11,13;
then
A52: i1 in Seg n;
then
A53: [i1,j] in Indices M by A8,A5,A40,ZFMISC_1:87;
C/.i1=C.i1 & C.i1=M*(i1,j) by A42,A44,A52,MATRIX_0:def 8,PARTFUN1:def 6
;
then
A54: JM*(i,j)=L*(M*(i,j)) + M*(i1,j) by A36,A39,A45,A43,A41,A51,Th6;
now
per cases by XXREAL_0:1;
suppose
A55: i>j;
then i1>j by NAT_1:13;
hence JM*(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
.= ONE*(i,j) by A38,A55,MATRIX_1:def 3;
end;
suppose
A56: i=j;
then i1>j by NAT_1:13;
hence JM*(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
.= ONE*(i,j) by A38,A56,MATRIX_1:def 3;
end;
suppose
A57: i<j;
set P=power(K).(-L",j-'i1+1);
A58: j-'i=j-i by A57,XREAL_1:233;
A59: i1<=j by A57,NAT_1:13;
then
A60: j-'i1=j-i1 by XREAL_1:233;
thus JM*(i,j) = L*(M*(i,j)) + (-P) by A4,A53,A54,A59
.= L*(-power(K).(-L",j-'i+1)) + (-P) by A4,A8,A38,A57
.= L*(-(-L")*P) + (-P) by A60,A58,GROUP_1:def 7
.= L*((-(-L"))*P) + (-P) by VECTSP_1:9
.= L*(L"*P) + (-P) by RLVECT_1:17
.= (L*L")*P + (-P) by GROUP_1:def 3
.= 1_K*P + (-P) by A6,VECTSP_1:def 10
.= P + (-P)
.= 0.K by RLVECT_1:def 10
.= ONE*(i,j) by A38,A57,MATRIX_1:def 3;
end;
end;
hence ONE*(i,j)=JM*(i,j);
end;
end;
hence ONE*(i,j)=JM*(i,j);
end;
then ONE = JM by MATRIX_0:27;
then M is_reverse_of J by A35,MATRIX_6:def 2;
hence thesis by A4,A7,MATRIX_6:def 4;
end;
theorem Th9:
Jordan_block(L,n) + a*1.(K,n)=Jordan_block(L+a,n)
proof
set J=Jordan_block(L,n);
set Ja=Jordan_block(L+a,n);
set ONE=1.(K,n);
now
A1: Indices J=Indices Ja by MATRIX_0:26;
let i,j such that
A2: [i,j] in Indices Ja;
A3: Indices J=Indices ONE by MATRIX_0:26;
now
per cases;
suppose
A4: i=j;
hence Ja*(i,j) = L+a by A2,Def1
.= J*(i,j)+a by A2,A1,A4,Def1
.= J*(i,j)+a*1_K
.= J*(i,j)+a*(ONE*(i,j)) by A2,A1,A3,A4,MATRIX_1:def 3
.= J*(i,j)+(a*ONE)*(i,j) by A2,A1,A3,MATRIX_3:def 5
.= (J+a*ONE)*(i,j) by A2,A1,MATRIX_1:def 6;
end;
suppose
A5: i+1=j;
then
A6: i<>j;
thus Ja*(i,j) = 1_K by A2,A5,Def1
.= 1_K+0.K by RLVECT_1:def 4
.= J*(i,j)+0.K by A2,A1,A5,Def1
.= J*(i,j)+a*0.K
.= J*(i,j)+a*(ONE*(i,j)) by A2,A1,A3,A6,MATRIX_1:def 3
.= J*(i,j)+(a*ONE)*(i,j) by A2,A1,A3,MATRIX_3:def 5
.= (J+a*ONE)*(i,j) by A2,A1,MATRIX_1:def 6;
end;
suppose
A7: i<>j & i+1<>j;
hence Ja*(i,j) = 0.K by A2,Def1
.= 0.K+0.K by RLVECT_1:def 4
.= J*(i,j)+0.K by A2,A1,A7,Def1
.= J*(i,j)+a*0.K
.= J*(i,j)+a*(ONE*(i,j)) by A2,A1,A3,A7,MATRIX_1:def 3
.= J*(i,j)+(a*ONE)*(i,j) by A2,A1,A3,MATRIX_3:def 5
.= (J+a*ONE)*(i,j) by A2,A1,MATRIX_1:def 6;
end;
end;
hence Ja*(i,j)=(J+a*ONE)*(i,j);
end;
hence thesis by MATRIX_0:27;
end;
begin :: Finite Sequences of Jordan blocks
definition
let K;
let G be FinSequence of (the carrier of K)**;
attr G is Jordan-block-yielding means
:Def2:
for i st i in dom G ex L,n st G .i = Jordan_block(L,n);
end;
registration
let K;
cluster Jordan-block-yielding for FinSequence of (the carrier of K)**;
existence
proof
reconsider F=<*>((the carrier of K)**) as FinSequence of (the carrier of K
)**;
take F;
thus thesis;
end;
end;
registration
let K;
cluster Jordan-block-yielding -> Square-Matrix-yielding for
FinSequence of (the
carrier of K)**;
coherence
proof
let F be FinSequence of (the carrier of K)** such that
A1: F is Jordan-block-yielding;
let i;
assume i in dom F;
then ex L,n st F.i=Jordan_block(L,n) by A1;
hence thesis;
end;
end;
definition
let K;
mode FinSequence_of_Jordan_block of K is Jordan-block-yielding FinSequence
of (the carrier of K)**;
end;
Lm2: {} is FinSequence_of_Jordan_block of K
proof
reconsider F=<*>((the carrier of K)**) as FinSequence of (the carrier of K)*
*;
for i st i in dom F ex L,n st F.i = Jordan_block(L,n);
hence thesis by Def2;
end;
definition
let K,L;
mode FinSequence_of_Jordan_block of L,K -> FinSequence_of_Jordan_block of K
means
:Def3:
for i st i in dom it ex n st it.i = Jordan_block(L,n);
existence
proof
reconsider F=<*>{} as FinSequence_of_Jordan_block of K by Lm2;
take F;
thus thesis;
end;
end;
theorem Th10:
{} is FinSequence_of_Jordan_block of L,K
proof
reconsider F=<*>{} as FinSequence_of_Jordan_block of K by Lm2;
for i st i in dom F ex n st F.i = Jordan_block(L,n);
hence thesis by Def3;
end;
theorem Th11:
<*Jordan_block(L,n)*> is FinSequence_of_Jordan_block of L,K
proof
now
A1: dom <*Jordan_block(L,n)*> ={1} by FINSEQ_1:2,def 8;
let i;
assume i in dom <*Jordan_block(L,n)*>;
then <*Jordan_block(L,n)*>.1=Jordan_block(L,n) & i=1 by A1,TARSKI:def 1;
hence ex a,k st <*Jordan_block(L,n)*>.i=Jordan_block(a,k);
end;
then reconsider
JJ=<*Jordan_block(L,n)*> as FinSequence_of_Jordan_block of K by Def2;
now
A2: dom JJ ={1} by FINSEQ_1:2,def 8;
let i;
assume i in dom JJ;
then JJ.1=Jordan_block(L,n) & i=1 by A2,TARSKI:def 1;
hence ex n st JJ.i = Jordan_block(L,n);
end;
hence thesis by Def3;
end;
registration
let K,L;
cluster non-empty for FinSequence_of_Jordan_block of L,K;
existence
proof
reconsider JJ= <*Jordan_block(L,1)*> as FinSequence_of_Jordan_block of L,K
by Th11;
take JJ;
now
A1: dom JJ ={1} by FINSEQ_1:2,def 8;
let x be object;
assume x in dom JJ;
then JJ.1=Jordan_block(L,1) & x=1 by A1,TARSKI:def 1;
hence JJ.x is non empty by Def1;
end;
hence thesis;
end;
end;
registration
let K;
cluster non-empty for FinSequence_of_Jordan_block of K;
existence
proof
set F = the non-empty FinSequence_of_Jordan_block of 1_K,K;
take F;
thus thesis;
end;
end;
theorem Th12:
for J be FinSequence_of_Jordan_block of L,K holds J (+) mlt(len
J|->a,1.(K,Len J)) is FinSequence_of_Jordan_block of (L+a),K
proof
let J be FinSequence_of_Jordan_block of L,K;
set M=mlt(len J|->a,1.(K,Len J));
A1: for i st i in dom (J(+)M) ex n st (J(+)M).i=Jordan_block(L+a,n)
proof
A2: dom M=dom 1.(K,Len J) by MATRIXJ1:def 9;
A3: dom J=Seg len J by FINSEQ_1:def 3;
A4: dom 1.(K,Len J)=dom Len J by MATRIXJ1:def 8;
let i such that
A5: i in dom (J(+)M);
A6: i in dom J by A5,MATRIXJ1:def 10;
then consider n such that
A7: J.i = Jordan_block(L,n) by Def3;
take n;
A8: len (J.i)=n by A7,MATRIX_0:24;
A9: dom Len J=dom J by MATRIXJ1:def 3;
then
A10: (Len J).i=len (J.i) by A6,MATRIXJ1:def 3;
len (len J|->a)=len J by CARD_1:def 7;
then dom (len J|->a)=dom J by FINSEQ_3:29;
then (len J|->a)/.i = (len J|->a).i by A6,PARTFUN1:def 6
.= a by A6,A3,FINSEQ_2:57;
then M.i = a * 1.(K,Len J).i by A6,A2,A4,A9,MATRIXJ1:def 9
.= a* 1.(K,n) by A6,A4,A9,A10,A8,MATRIXJ1:def 8;
hence (J(+)M).i = Jordan_block(L,n) +a* 1.(K,n) by A5,A7,MATRIXJ1:def 10
.= Jordan_block(L+a,n) by Th9;
end;
J(+)M is Jordan-block-yielding
proof
let i;
assume i in dom (J(+)M);
then ex n st (J(+)M).i=Jordan_block(L+a,n) by A1;
hence thesis;
end;
then reconsider JM=J(+)M as FinSequence_of_Jordan_block of K;
JM is FinSequence_of_Jordan_block of (L+a),K
proof
let i;
assume i in dom JM;
hence thesis by A1;
end;
hence thesis;
end;
definition
let K;
let J1,J2 be FinSequence_of_Jordan_block of K;
redefine func J1^J2 -> FinSequence_of_Jordan_block of K; :: redefines ^ (FINSEQ_1, definition)
coherence
proof
J1^J2 is Jordan-block-yielding
proof
let i such that
A1: i in dom (J1^J2);
per cases by A1,FINSEQ_1:25;
suppose
A2: i in dom J1;
then (J1^J2).i=J1.i by FINSEQ_1:def 7;
hence thesis by A2,Def2;
end;
suppose
ex n st n in dom J2 & i=len J1 + n;
then consider k such that
A3: k in dom J2 and
A4: i=len J1+k;
(J1^J2).i=J2.k by A3,A4,FINSEQ_1:def 7;
hence thesis by A3,Def2;
end;
end;
hence thesis;
end;
end;
definition
let K;
let n;
let J be FinSequence_of_Jordan_block of K;
redefine func J|n -> FinSequence_of_Jordan_block of K; :: redefines | (FINSEQ_1, definition)
coherence
proof
now
let i;
assume i in dom (J|n);
then i in dom J & (J|n).i=J.i by FUNCT_1:47,RELAT_1:57;
hence ex L,k st (J|n).i=Jordan_block(L,k) by Def2;
end;
hence thesis by Def2;
end;
redefine func J/^n -> FinSequence_of_Jordan_block of K; :: redefines /^ (RFINSEQ, definition)
coherence
proof
now
let i such that
A1: i in dom (J/^n);
i+n in dom J by A1,FINSEQ_5:26;
then
J.(n+i)=J/.(n+i) & ex L,k st J.(n+i)=Jordan_block(L,k) by Def2,
PARTFUN1:def 6;
hence ex L,k st (J/^n).i=Jordan_block(L,k) by A1,FINSEQ_5:27;
end;
hence thesis by Def2;
end;
end;
definition
let K,L;
let J1,J2 be FinSequence_of_Jordan_block of L,K;
redefine func J1^J2 -> FinSequence_of_Jordan_block of L,K; :: redefines ^ (FINSEQ_1, definition)
coherence
proof
J1^J2 is FinSequence_of_Jordan_block of L,K
proof
let i such that
A1: i in dom (J1^J2);
per cases by A1,FINSEQ_1:25;
suppose
A2: i in dom J1;
then (J1^J2).i=J1.i by FINSEQ_1:def 7;
hence thesis by A2,Def3;
end;
suppose
ex n st n in dom J2 & i=len J1 + n;
then consider k such that
A3: k in dom J2 and
A4: i=len J1+k;
(J1^J2).i=J2.k by A3,A4,FINSEQ_1:def 7;
hence thesis by A3,Def3;
end;
end;
hence thesis;
end;
end;
definition
let K,L;
let n;
let J be FinSequence_of_Jordan_block of L,K;
redefine func J|n -> FinSequence_of_Jordan_block of L,K; :: redefines | (FINSEQ_1, definition)
coherence
proof
now
let i;
assume i in dom (J|n);
then i in dom J & (J|n).i=J.i by FUNCT_1:47,RELAT_1:57;
hence ex k st (J|n).i=Jordan_block(L,k) by Def3;
end;
hence thesis by Def3;
end;
redefine func J/^n -> FinSequence_of_Jordan_block of L,K; :: redefines /^ (RFINSEQ, definition)
coherence
proof
now
let i such that
A1: i in dom (J/^n);
i+n in dom J by A1,FINSEQ_5:26;
then
J.(n+i)=J/.(n+i) & ex k st J.(n+i)=Jordan_block(L,k) by Def3,
PARTFUN1:def 6;
hence ex k st (J/^n).i=Jordan_block(L,k) by A1,FINSEQ_5:27;
end;
hence thesis by Def3;
end;
end;
begin :: Nilpotent Transformations
definition
let K be doubleLoopStr;
let V be non empty ModuleStr over K;
let f be Function of V,V;
attr f is nilpotent means
:Def4:
ex n st for v be Vector of V holds (f|^n).v =0.V;
end;
theorem Th13:
for K be doubleLoopStr for V be non empty ModuleStr over K for f
be Function of V,V holds f is nilpotent iff ex n st f|^n = ZeroMap(V,V)
proof
let K be doubleLoopStr;
let V be non empty ModuleStr over K;
let f be Function of V,V;
hereby
assume f is nilpotent;
then consider n such that
A1: for v be Vector of V holds (f|^n).v=0.V;
now
let x be object;
assume x in dom (f|^n);
then reconsider v=x as Vector of V by FUNCT_2:def 1;
thus (f|^n).x = (f|^n).v .= 0.V by A1;
end;
then (f|^n) = (dom (f|^n))-->0.V by FUNCOP_1:11
.= (the carrier of V)-->0.V by FUNCT_2:def 1
.= ZeroMap(V,V) by GRCAT_1:def 7;
hence ex n st f|^n = ZeroMap(V,V);
end;
given n such that
A2: f|^n = ZeroMap(V,V);
take n;
let v be Vector of V;
thus (f|^n).v = ((the carrier of V)-->0.V).v by A2,GRCAT_1:def 7
.= 0.V;
end;
registration
let K be doubleLoopStr;
let V be non empty ModuleStr over K;
cluster nilpotent for Function of V,V;
existence
proof
take F=ZeroMap(V,V);
F|^1=F by VECTSP11:19;
hence thesis by Th13;
end;
end;
registration
let R be Ring;
let V be LeftMod of R;
cluster nilpotent additive homogeneous for Function of V,V;
existence
proof
take F=ZeroMap(V,V);
F|^1=F by VECTSP11:19;
hence thesis by Th13;
end;
end;
theorem Th14:
for V be VectSp of K,f be linear-transformation of V,V holds f|
ker (f|^n) is nilpotent linear-transformation of ker (f|^n),ker (f|^n)
proof
let V be VectSp of K,f be linear-transformation of V,V;
set KER = ker (f|^n);
reconsider fK=f|KER as linear-transformation of KER,KER by VECTSP11:28;
now
let v be Vector of KER;
reconsider v1=v as Vector of V by VECTSP_4:10;
A1: v1 in KER;
thus (fK|^n).v = ((f|^n) |KER).v by VECTSP11:22
.= (f|^n).v1 by FUNCT_1:49
.= 0.V by A1,RANKNULL:10
.= 0.KER by VECTSP_4:11;
end;
hence thesis by Def4;
end;
definition
let K be doubleLoopStr;
let V be non empty ModuleStr over K;
let f be nilpotent Function of V,V;
func degree_of_nilpotent f -> Nat means
:Def5:
f|^it = ZeroMap(V,V) & for k st f|^k = ZeroMap(V,V) holds it <= k;
existence
proof
defpred P[Nat] means f|^$1 = ZeroMap(V,V);
A1: ex n st P[n] by Th13;
consider n such that
A2: ( P[n])& for k st P[k] holds n<=k from NAT_1:sch 5(A1);
take n;
thus thesis by A2;
end;
uniqueness
proof
let i,j;
assume f|^i = ZeroMap(V,V) & ( for k st f|^k = ZeroMap(V,V) holds i <= k)
& f|^j = ZeroMap(V,V) & for k st f|^k = ZeroMap(V,V) holds j <= k;
then i<=j & j<=i;
hence thesis by XXREAL_0:1;
end;
end;
notation
let K be doubleLoopStr;
let V be non empty ModuleStr over K;
let f be nilpotent Function of V,V;
synonym deg f for degree_of_nilpotent f;
end;
theorem Th15:
for K be doubleLoopStr for V be non empty ModuleStr over K for f
be nilpotent Function of V,V holds deg f = 0 iff [#]V = {0.V}
proof
let K be doubleLoopStr;
let V be non empty ModuleStr over K;
let f be nilpotent Function of V,V;
hereby
assume
A1: deg f=0;
[#]V c= {0.V}
proof
let x be object such that
A2: x in [#]V;
id V = f|^0 by VECTSP11:18
.= ZeroMap(V,V) by A1,Def5
.= (the carrier of V)-->0.V by GRCAT_1:def 7;
then x = ((the carrier of V)-->0.V).x by A2,FUNCT_1:18
.= 0.V by A2,FUNCOP_1:7;
hence thesis by TARSKI:def 1;
end;
hence [#]V ={0.V} by ZFMISC_1:33;
end;
assume
A3: [#]V={0.V};
now
let x be object;
assume x in dom (f|^0);
then reconsider v=x as Vector of V by FUNCT_2:def 1;
thus (f|^0).x = (id V).v by VECTSP11:18
.= 0.V by A3,TARSKI:def 1;
end;
then (f|^0) = (dom (f|^0))-->0.V by FUNCOP_1:11
.= (the carrier of V)-->0.V by FUNCT_2:def 1
.= ZeroMap(V,V) by GRCAT_1:def 7;
hence thesis by Def5;
end;
theorem Th16:
for K be doubleLoopStr for V be non empty ModuleStr over K for f
be nilpotent Function of V,V ex v be Vector of V st for i st i < deg f holds (f
|^i).v <> 0.V
proof
let K be doubleLoopStr;
let V be non empty ModuleStr over K;
let f be nilpotent Function of V,V;
set D=deg f;
defpred P[Nat] means 0<$1 & $1 < D & (f|^$1).(0.V)=0.V;
assume
A1: for v be Vector of V ex i st i < D & (f|^i).v=0.V;
then ex i st i < D & (f|^i).(0.V) =0.V;
then [#]V<>{0.V} by Th15;
then consider v be object such that
A2: v in [#]V and
A3: v<>0.V by ZFMISC_1:35;
reconsider v as Vector of V by A2;
consider j such that
A4: j < D and
A5: (f|^j).v =0.V by A1;
A6: j-j<D-j by A4,XREAL_1:9;
j>0
proof
assume j<=0;
then j=0;
then 0.V = id V.v by A5,VECTSP11:18
.= v by FUNCT_1:18;
hence thesis by A3;
end;
then
A7: D-j<D-0 by XREAL_1:10;
A8: dom (f|^j)=[#]V by FUNCT_2:def 1;
A9: D-j=D-'j by A4,XREAL_1:233;
then
A10: D=(D-'j)+j;
A11: f|^D = ZeroMap(V,V) by Def5
.= (the carrier of V)-->0.V by GRCAT_1:def 7;
then 0.V = (f|^D).v
.= ((f|^(D-'j))*(f|^j)).v by A10,VECTSP11:20
.= (f|^(D-'j)).(0.V) by A5,A8,FUNCT_1:13;
then
A12: ex j st P[j] by A9,A6,A7;
consider m such that
A13: P[m] & for n be Nat st P[n] holds m <= n from NAT_1:sch 5(A12);
A14: D-'m=D-m by A13,XREAL_1:233;
A15: now
let x be object;
assume x in dom (f|^(D-'m));
then reconsider X=x as Vector of V by FUNCT_2:def 1;
consider k such that
A16: k < D and
A17: (f|^k).X =0.V by A1;
defpred F[Nat] means $1<=D & ex i st $1=k+i*m;
k=k+0*m;
then
A18: ex k st F[k] by A16;
A19: for i be Nat st F[i] holds i <= D;
consider MAX be Nat such that
A20: F[MAX] and
A21: for k be Nat st F[k] holds k <= MAX from NAT_1:sch 6(A19,A18);
consider I be Nat such that
A22: MAX=k+I*m by A20;
now
per cases by A20,XXREAL_0:1;
suppose
A23: MAX=D;
then I<>0 by A16,A22;
then reconsider I1=I-1 as Nat by NAT_1:20;
D-'m=k+I1*m by A14,A22,A23;
hence (f|^(D-'m)).X=0.V by A13,A17,VECTSP11:21;
end;
suppose
A24: MAX<D;
MAX<>0
proof
assume
A25: MAX=0;
then k=0 by A22;
then k+1*m<D by A13;
hence thesis by A13,A21,A25;
end;
then
A26: D-MAX <D-0 by XREAL_1:10;
A27: (f|^MAX).X=0.V & dom (f|^MAX)= the carrier of V by A13,A17,A22,
FUNCT_2:def 1,VECTSP11:21;
A28: MAX-MAX < D-MAX by A24,XREAL_1:9;
A29: D-MAX=D-'MAX by A24,XREAL_1:233;
then
A30: D=D-'MAX+MAX;
0.V = (f|^D).X by A11
.= ((f|^(D-'MAX))*(f|^MAX)).X by A30,VECTSP11:20
.= (f|^(D-'MAX)).(0.V) by A27,FUNCT_1:13;
then m <= D-'MAX by A13,A29,A28,A26;
then
A31: MAX+m <= MAX+(D-MAX) by A29,XREAL_1:6;
MAX+m=k+(I+1)*m by A22;
then MAX+m<=MAX+0 by A21,A31;
hence (f|^(D-'m)).X=0.V by A13,XREAL_1:6;
end;
end;
hence (f|^(D-'m)).x=0.V;
end;
A32: D-m<D-0 by A13,XREAL_1:10;
dom (f|^(D-'m))=[#]V by FUNCT_2:def 1;
then f|^(D-'m) = (the carrier of V)-->0.V by A15,FUNCOP_1:11
.= ZeroMap(V,V) by GRCAT_1:def 7;
hence contradiction by A14,A32,Def5;
end;
theorem Th17:
for K be Field, V be VectSp of K, W be Subspace of V for f be
nilpotent Function of V,V st f|W is Function of W,W holds f|W is nilpotent
Function of W,W
proof
let K be Field,V be VectSp of K,W be Subspace of V;
let f be nilpotent Function of V,V;
assume f|W is Function of W,W;
then reconsider fW=f|W as Function of W,W;
consider n such that
A1: f|^n =ZeroMap(V,V) by Th13;
[#]W c= [#]V by VECTSP_4:def 2;
then
A2: [#]W=[#]V/\[#]W by XBOOLE_1:28;
fW|^n = ZeroMap(V,V) |W by A1,VECTSP11:22
.= ((the carrier of V)-->0.V) |[#]W by GRCAT_1:def 7
.= ((the carrier of V)/\[#]W) -->0.V by FUNCOP_1:12
.= (the carrier of W)-->0.W by A2,VECTSP_4:11
.= ZeroMap(W,W) by GRCAT_1:def 7;
hence thesis by Th13;
end;
theorem Th18:
for K be Field, V be VectSp of K, W be Subspace of V for f be
nilpotent linear-transformation of V,V, fI be nilpotent Function of im (f|^n),
im (f|^n) st fI = f|im (f|^n) & n <= deg f holds deg fI + n = deg f
proof
let K be Field,V be VectSp of K,W be Subspace of V;
let f be nilpotent linear-transformation of V,V;
set IM=im (f|^n);
let fI be nilpotent Function of IM,IM;
assume
A1: fI=f|IM;
set D=deg f;
assume n<=D;
then reconsider Dn=D-n as Element of NAT by NAT_1:21;
A2: now
let x be object;
assume x in dom (fI|^Dn);
then reconsider X=x as Vector of IM by FUNCT_2:def 1;
reconsider v=X as Vector of V by VECTSP_4:10;
A3: dom (f|^n) = the carrier of V by FUNCT_2:def 1;
X in IM;
then consider w be Element of V such that
A4: v = (f|^n).w by RANKNULL:13;
(f|^D).w = ZeroMap(V,V).w by Def5
.= ((the carrier of V)-->0.V).w by GRCAT_1:def 7
.= 0.V;
hence 0.IM = (f|^(Dn+n)).w by VECTSP_4:11
.= ((f|^Dn)*(f|^n)).w by VECTSP11:20
.= (f|^Dn).v by A4,A3,FUNCT_1:13
.= ((f|^Dn) |IM).X by FUNCT_1:49
.= (fI|^Dn).x by A1,VECTSP11:22;
end;
dom (fI|^Dn)=[#]IM by FUNCT_2:def 1;
then fI|^Dn = (the carrier of IM)-->0.IM by A2,FUNCOP_1:11
.= ZeroMap(IM,IM) by GRCAT_1:def 7;
then
A5: deg fI<=Dn by Def5;
deg fI = Dn
proof
set DI=deg fI;
A6: dom (f|^n)=the carrier of V by FUNCT_2:def 1;
assume DI<>Dn;
then DI<Dn by A5,XXREAL_0:1;
then
A7: DI+n<Dn+n by XREAL_1:6;
consider v be Vector of V such that
A8: for i st i < D holds (f|^i).v<>0.V by Th16;
(f|^n).v in IM by RANKNULL:13;
then
A9: (f|^n).v in the carrier of IM;
fI|^DI = ZeroMap(IM,IM) by Def5
.= (the carrier of IM)-->0.IM by GRCAT_1:def 7;
then 0.IM = (fI|^DI).((f|^n).v) by A9,FUNCOP_1:7
.= ((f|^DI) |IM).((f|^n).v) by A1,VECTSP11:22
.= (f|^DI).((f|^n).v) by A9,FUNCT_1:49
.= ((f|^DI)*(f|^n)).v by A6,FUNCT_1:13
.= (f|^(DI+n)).v by VECTSP11:20;
hence thesis by A7,A8,VECTSP_4:11;
end;
hence thesis;
end;
reserve V1,V2 for finite-dimensional VectSp of K,
W1,W2 for Subspace of V1,
U1 ,U2 for Subspace of V2,
b1 for OrdBasis of V1,
B1 for FinSequence of V1,
b2 for OrdBasis of V2,
B2 for FinSequence of V2,
bw1 for OrdBasis of W1,
bw2 for OrdBasis of W2,
Bu1 for FinSequence of U1,
Bu2 for FinSequence of U2;
theorem Th19:
for M be Matrix of len b1,len B2,K, M1 be Matrix of len bw1,len
Bu1,K, M2 be Matrix of len bw2,len Bu2,K st b1 = bw1 ^ bw2 & B2 = Bu1 ^ Bu2 & M
= block_diagonal(<*M1,M2*>,0.K) & width M1 = len Bu1 & width M2 = len Bu2 holds
(i in dom bw1 implies Mx2Tran(M,b1,B2).(b1/.i) = Mx2Tran(M1,bw1,Bu1).(bw1/.i))&
(i in dom bw2 implies Mx2Tran(M,b1,B2).(b1/.(i+len bw1)) = Mx2Tran(M2,bw2,Bu2).
(bw2/.i))
proof
let M be Matrix of len b1,len B2,K, M1 be Matrix of len bw1,len Bu1,K, M2 be
Matrix of len bw2,len Bu2,K such that
A1: b1 = bw1 ^ bw2 and
A2: B2 = Bu1 ^ Bu2 and
A3: M = block_diagonal(<*M1,M2*>,0.K) and
A4: width M1 = len Bu1 and
A5: width M2 = len Bu2;
A6: dom bw1 c= dom b1 by A1,FINSEQ_1:26;
rng Bu2 c= the carrier of U2 & the carrier of U2 c= the carrier of V2 by
FINSEQ_1:def 4,VECTSP_4:def 2;
then
A7: rng Bu2 c= the carrier of V2;
rng Bu1 c= the carrier of U1 & the carrier of U1 c= the carrier of V2 by
FINSEQ_1:def 4,VECTSP_4:def 2;
then rng Bu1 c= the carrier of V2;
then reconsider bu1=Bu1,bu2=Bu2 as FinSequence of V2 by A7,FINSEQ_1:def 4;
set F1=Mx2Tran(M1,bw1,Bu1);
set F=Mx2Tran(M,b1,B2);
A8: dom b1=Seg len b1 & len 1.(K,len b1)=len b1 by FINSEQ_1:def 3,MATRIX_0:24;
A9: dom 1.(K,len bw1)=Seg len 1.(K,len bw1) by FINSEQ_1:def 3;
A10: dom 1.(K,len b1)=Seg len 1.(K,len b1) by FINSEQ_1:def 3;
set BI=len bw1+i;
A11: dom bw2=Seg len bw2 & len 1.(K,len bw2)=len bw2 by FINSEQ_1:def 3
,MATRIX_0:24;
set F2=Mx2Tran(M2,bw2,Bu2);
A12: width 1.(K,len b1)=len b1 by MATRIX_0:24;
A13: len Line(M2,i)=width M2 & len (width M1|->0.K)=width M1 by CARD_1:def 7;
A14: dom bw1=Seg len bw1 & len 1.(K,len bw1)=len bw1 by FINSEQ_1:def 3
,MATRIX_0:24;
A15: len M=len b1 by MATRIX_0:def 2;
A16: len M1=len bw1 by MATRIX_0:def 2;
then
A17: dom M1=dom bw1 by FINSEQ_3:29;
thus i in dom bw1 implies F.(b1/.i)= F1.(bw1/.i)
proof
A18: len Line(M1,i)=width M1 & len (width M2|->0.K)=width M2 by CARD_1:def 7;
assume
A19: i in dom bw1;
then
A20: Line(M,i)=Line(M1,i)^(width M2|->0.K) by A3,A17,MATRIXJ1:23;
thus F.(b1/.i) = Sum lmlt (Line(LineVec2Mx(b1/.i|--b1) * M,1),B2) by
MATRLIN2:def 3
.= Sum lmlt (Line(LineVec2Mx(Line(1.(K,len b1),i)) * M,1),B2) by A6,A19,
MATRLIN2:19
.= Sum lmlt (Line(LineVec2Mx(Line(1.(K,len b1)*M,i)),1),B2) by A6,A8,A15
,A10,A19,MATRIX_0:24,MATRLIN2:35
.= Sum lmlt (Line(LineVec2Mx(Line(M,i)),1),B2) by A15,MATRIXR2:68
.= Sum lmlt(Line(M,i),B2) by MATRIX15:25
.= Sum (lmlt(Line(M1,i),bu1)^lmlt(width M2|->0.K,bu2)) by A2,A4,A5,A20
,A18,MATRLIN2:9
.= Sum lmlt(Line(M1,i),bu1) + Sum lmlt(width M2|->0.K,bu2) by RLVECT_1:41
.= Sum lmlt(Line(M1,i),bu1) + 0.K*Sum bu2 by A5,MATRLIN2:11
.= Sum lmlt(Line(M1,i),bu1) + 0.V2 by VECTSP_1:14
.= Sum lmlt(Line(M1,i),bu1) by RLVECT_1:def 4
.= Sum lmlt(Line(M1,i),Bu1) by MATRLIN2:14,15
.= Sum lmlt (Line(LineVec2Mx(Line(M1,i)),1),Bu1) by MATRIX15:25
.= Sum lmlt (Line(LineVec2Mx(Line(1.(K,len bw1)*M1,i)),1),Bu1) by A16,
MATRIXR2:68
.= Sum lmlt (Line(LineVec2Mx(Line(1.(K,len bw1),i)) * M1,1),Bu1) by A14
,A9,A16,A19,MATRIX_0:24,MATRLIN2:35
.= Sum lmlt (Line(LineVec2Mx(bw1/.i|--bw1) * M1,1),Bu1) by A19,
MATRLIN2:19
.= F1.(bw1/.i) by MATRLIN2:def 3;
end;
A21: dom 1.(K,len bw2)=Seg len 1.(K,len bw2) by FINSEQ_1:def 3;
assume
A22: i in dom bw2;
then
A23: BI in dom b1 by A1,FINSEQ_1:28;
A24: len M2=len bw2 by MATRIX_0:def 2;
then dom M2=dom bw2 by FINSEQ_3:29;
then
A25: Line(M,BI)=(width M1|->0.K)^Line(M2,i) by A3,A16,A22,MATRIXJ1:23;
thus F.(b1/.(i+len bw1)) = Sum lmlt (Line(LineVec2Mx(b1/.BI|--b1) * M,1),B2)
by MATRLIN2:def 3
.= Sum lmlt (Line(LineVec2Mx(Line(1.(K,len b1),BI)) * M,1),B2) by A23,
MATRLIN2:19
.= Sum lmlt (Line(LineVec2Mx(Line(1.(K,len b1)*M,BI)),1),B2) by A1,A12,A8
,A15,A10,A22,FINSEQ_1:28,MATRLIN2:35
.= Sum lmlt (Line(LineVec2Mx(Line(M,BI)),1),B2) by A15,MATRIXR2:68
.= Sum lmlt(Line(M,BI),B2) by MATRIX15:25
.= Sum (lmlt(width M1|->0.K,bu1)^lmlt(Line(M2,i),bu2)) by A2,A4,A5,A25,A13,
MATRLIN2:9
.= Sum lmlt(width M1|->0.K,bu1) + Sum lmlt(Line(M2,i),bu2) by RLVECT_1:41
.= 0.K*Sum bu1 + Sum lmlt(Line(M2,i),bu2) by A4,MATRLIN2:11
.= 0.V2 + Sum lmlt(Line(M2,i),bu2) by VECTSP_1:14
.= Sum lmlt(Line(M2,i),bu2) by RLVECT_1:def 4
.= Sum lmlt(Line(M2,i),Bu2) by MATRLIN2:14,15
.= Sum lmlt (Line(LineVec2Mx(Line(M2,i)),1),Bu2) by MATRIX15:25
.= Sum lmlt (Line(LineVec2Mx(Line(1.(K,len bw2)*M2,i)),1),Bu2) by A24,
MATRIXR2:68
.= Sum lmlt (Line(LineVec2Mx(Line(1.(K,len bw2),i)) * M2,1),Bu2) by A11,A21
,A24,A22,MATRIX_0:24,MATRLIN2:35
.= Sum lmlt (Line(LineVec2Mx(bw2/.i|--bw2) * M2,1),Bu2) by A22,MATRLIN2:19
.= F2.(bw2/.i) by MATRLIN2:def 3;
end;
theorem Th20:
for M be Matrix of len b1,len B2,K, F be FinSequence_of_Matrix
of K st M = block_diagonal(F,0.K) for i,m st i in dom b1 & m = min(Len F,i)
holds Mx2Tran(M,b1,B2).(b1/.i) = Sum lmlt(Line(F.m,i-'Sum (Len F| (m-'1))),
(B2|Sum(Width F|m))/^Sum (Width F| (m-'1))) & len ((B2|Sum(Width F|m))/^
Sum (Width F| (m-'1))) = width (F.m)
proof
set ONE=1.(K,len b1);
let M be Matrix of len b1,len B2,K, F be FinSequence_of_Matrix of K such
that
A1: M = block_diagonal(F,0.K);
A2: width M=Sum Width F by A1,MATRIXJ1:def 5;
len ONE=len b1 by MATRIX_0:def 2;
then
A3: dom ONE=dom b1 by FINSEQ_3:29;
set L=Len F;
set W=Width F;
let i,m such that
A4: i in dom b1 and
A5: m = min(Len F,i);
A6: 1<=i & i<=len b1 by A4,FINSEQ_3:25;
then
A7: len M=len b1 by MATRIX_0:23;
set Fm=F.m;
set Wm1=Sum (W| (m-'1));
A8: len (Sum (W| (m-'1)) |->0.K)=Sum (W| (m-'1)) & len Line(Fm,i-'Sum (Len F| (
m-'1) )) =width Fm by CARD_1:def 7;
set Wm=Sum (W|m);
W = (W|m)^(W/^m) by RFINSEQ:8;
then
A9: Sum W=Wm+Sum (W/^m) by RVSUM_1:75;
then
A10: Sum W-'Wm = Sum W-Wm by NAT_1:11,XREAL_1:233
.= Sum (W/^m) by A9;
then
A11: len ((Sum W-'Sum (W|m)) |->0.K)=Sum (W/^m) by CARD_1:def 7;
A12: dom b1=Seg len b1 & len M=Sum Len F by A1,FINSEQ_1:def 3,MATRIXJ1:def 5;
then
A13: m in dom Len F by A4,A5,A7,MATRIXJ1:def 1;
then
A14: 1<=m by FINSEQ_3:25;
reconsider wF= width Fm as Element of NAT by ORDINAL1:def 12;
dom L=dom F & dom W=dom F by MATRIXJ1:def 3,def 4;
then m<=len W & W.m=width Fm by A13,FINSEQ_3:25,MATRIXJ1:def 4;
then W = (W| (m-'1))^<*width Fm*>^(W/^m) by A5,A14,POLYNOM4:1;
then
A15: Sum W = Sum ((W| (m-'1))^<*wF*>)+Sum (W/^m) by RVSUM_1:75
.= Wm1 + width Fm+Sum (W/^m) by RVSUM_1:74;
then
A16: len ((Sum (W| (m-'1)) |->0.K)^Line(Fm,i-'Sum (Len F| (m-'1))))=Wm by A9,
CARD_1:def 7;
set B2W=B2|Wm;
A17: B2W/^Wm1 = (B2|Sum(Width F|m))/^Wm1 by MATRIXJ1:21
.= (B2|Sum(Width F|m))/^Sum (Width F| (m-'1)) by MATRIXJ1:21;
A18: width M=len B2 by A6,MATRIX_0:23;
then
A19: len B2W =Wm by A2,A9,FINSEQ_1:59,NAT_1:11;
Sum W=Wm1+(width Fm+Sum (W/^m)) by A15;
then
A20: len (B2|Wm1) =Wm1 by A2,A18,FINSEQ_1:59,NAT_1:11;
Wm>=Wm1 by A9,A15,NAT_1:11;
then Seg Wm1 c= Seg Wm by FINSEQ_1:5;
then B2W|Wm1=B2|Wm1 by RELAT_1:74;
then
A21: B2W=(B2|Wm1)^(B2W/^Wm1) by RFINSEQ:8;
then
A22: len B2W=len (B2|Wm1)+len (B2W/^Wm1) by FINSEQ_1:22;
A23: B2=B2W^(B2/^Wm) by RFINSEQ:8;
then
A24: len B2=len B2W+ len (B2/^Wm) by FINSEQ_1:22;
Mx2Tran(M,b1,B2).(b1/.i) = Sum lmlt (Line(LineVec2Mx(b1/.i|--b1) * M,1)
,B2) by MATRLIN2:def 3
.= Sum lmlt (Line(LineVec2Mx(Line(ONE,i)) * M,1),B2) by A4,MATRLIN2:19
.= Sum lmlt (Line(LineVec2Mx(Line(ONE*M,i)),1),B2) by A4,A6,A3,A7,
MATRIX_0:23,MATRLIN2:35
.= Sum lmlt (Line(LineVec2Mx(Line(M,i)),1),B2) by A7,MATRIXR2:68
.= Sum lmlt (Line(M,i),B2) by MATRIX15:25
.= Sum lmlt((Sum (Width F| (m-'1)) |->0.K)^Line(Fm,i-'Sum (Len F| (m-'1)))^
((Sum W-'Sum (Width F|m)) |->0.K),B2) by A1,A4,A5,A7,A12,MATRIXJ1:37
.= Sum lmlt((Sum (W| (m-'1)) |->0.K) ^ Line(Fm,i-'Sum (Len F| (m-'1)))^ ((
Sum W-'Sum (Width F|m)) |->0.K),B2) by MATRIXJ1:21
.= Sum lmlt((Sum (W| (m-'1)) |->0.K) ^ Line(Fm,i-'Sum (Len F| (m-'1)))^ ((
Sum W-'Sum (W|m)) |->0.K),B2) by MATRIXJ1:21
.= Sum (lmlt((Sum (W| (m-'1)) |->0.K) ^ Line(Fm,i-'Sum (Len F| (m-'1))),B2W
)^ lmlt(((Sum W-'Sum (W|m)) |->0.K),B2/^Wm)) by A2,A18,A9,A23,A24,A19,A11,A16,
MATRLIN2:9
.= Sum lmlt((Sum (W| (m-'1)) |->0.K)^Line(Fm,i-'Sum (Len F| (m-'1))),B2W)+
Sum lmlt(((Sum W-'Sum (W|m)) |->0.K),B2/^Wm) by RLVECT_1:41
.= Sum lmlt((Sum (W| (m-'1)) |->0.K) ^ Line(Fm,i-'Sum (Len F| (m-'1))),B2W)
+ 0.K* Sum (B2/^Wm) by A2,A18,A9,A10,A24,A19,MATRLIN2:11
.= Sum lmlt((Sum (W| (m-'1)) |->0.K)^ Line(Fm,i-'Sum (Len F| (m-'1))),B2W)+
0.V2 by VECTSP_1:14
.= Sum lmlt((Sum (W| (m-'1)) |->0.K) ^ Line(Fm,i-'Sum (Len F| (m-'1))),B2W)
by RLVECT_1:def 4
.= Sum (lmlt(Sum (W| (m-'1)) |->0.K,B2|Wm1) ^ lmlt(Line(Fm,i-'Sum (Len F| (
m-'1))),B2W/^Wm1)) by A9,A15,A19,A21,A22,A20,A8,MATRLIN2:9
.= Sum lmlt(Sum (W| (m-'1)) |->0.K,B2|Wm1) + Sum lmlt(Line(Fm,i-'Sum (Len
F| (m-'1))),B2W/^Wm1) by RLVECT_1:41
.= 0.K*Sum (B2|Wm1) + Sum lmlt(Line(Fm,i-'Sum (Len F| (m-'1))),B2W/^Wm1)
by A20,MATRLIN2:11
.= 0.V2+Sum lmlt(Line(Fm,i-'Sum (Len F| (m-'1))),B2W/^Wm1) by VECTSP_1:14
.= Sum lmlt(Line(Fm,i-'Sum (Len F| (m-'1))),B2W/^Wm1) by RLVECT_1:def 4;
hence thesis by A9,A15,A19,A22,A20,A17;
end;
theorem Th21:
len B1 in dom B1 implies Sum lmlt (Line(Jordan_block(L,len B1),
len B1),B1)= L*(B1/.(len B1))
proof
set N=len B1;
assume
A1: N in dom B1;
set J=Jordan_block(L,N);
set ONE=1.(K,N);
thus Sum lmlt (Line(J,N),B1) = Sum lmlt(L*Line(ONE,N),B1) by Th5
.= L* Sum lmlt (Line(ONE,N),B1) by MATRLIN2:13
.= L* (B1/.N) by A1,MATRLIN2:16;
end;
theorem Th22:
i in dom B1 & i <> len B1 implies Sum lmlt (Line(Jordan_block(L,
len B1),i),B1)= L*(B1/.i)+B1/.(i+1)
proof
assume that
A1: i in dom B1 and
A2: i<>len B1;
set N=len B1;
A3: dom B1=Seg N by FINSEQ_1:def 3;
i<=N by A1,FINSEQ_3:25;
then i<N by A2,XXREAL_0:1;
then 1<=i+1 & i+1<=N by NAT_1:11,13;
then
A4: i+1 in dom B1 by A3;
set ONE=1.(K,N);
A5: len Line(ONE,i+1)=width ONE by CARD_1:def 7;
width ONE=N by MATRIX_0:24;
then
A6: dom Line(ONE,i+1)= dom B1 by A5,FINSEQ_3:29;
len (L*Line(ONE,i))=len Line(ONE,i) & len Line(ONE,i)=width ONE by
CARD_1:def 7,MATRIXR1:16;
then dom (L*Line(ONE,i))=dom Line(ONE,i+1) by A5,FINSEQ_3:29;
then
A7: dom lmlt(L*Line(ONE,i),B1) =dom B1 by A6,MATRLIN:12;
dom lmlt(Line(ONE,i+1),B1) =dom B1 by A6,MATRLIN:12;
then
A8: len lmlt (L*Line(ONE,i),B1)=len lmlt(Line(ONE,i+1),B1) by A7,FINSEQ_3:29;
thus Sum lmlt (Line(Jordan_block(L,len B1),i),B1) = Sum lmlt (L*Line(ONE,i)+
Line(ONE,i+1),B1) by A1,A2,A3,Th4
.= Sum (lmlt (L*Line(ONE,i),B1)+lmlt(Line(ONE,i+1),B1)) by MATRLIN2:7
.= (Sum lmlt (L*Line(ONE,i),B1))+(Sum lmlt(Line(ONE,i+1),B1)) by A8,
MATRLIN2:10
.= (L*Sum lmlt (Line(ONE,i),B1))+(Sum lmlt(Line(ONE,i+1),B1)) by
MATRLIN2:13
.= L*(B1/.i)+(Sum lmlt(Line(ONE,i+1),B1)) by A1,MATRLIN2:16
.= L*(B1/.i)+B1/.(i+1) by A4,MATRLIN2:16;
end;
theorem Th23:
for M be Matrix of len b1,len B2,K st M = Jordan_block(L,n) for
i st i in dom b1 holds (i = len b1 implies Mx2Tran(M,b1,B2).(b1/.i) = L*(B2/.i)
) & (i <> len b1 implies Mx2Tran(M,b1,B2).(b1/.i) = L*(B2/.i)+ B2/.(i+1))
proof
set ONE=1.(K,len b1);
set J=Jordan_block(L,n);
let M be Matrix of len b1,len B2,K such that
A1: M = Jordan_block(L,n);
A2: len M=n by A1,MATRIX_0:24;
len ONE=len b1 by MATRIX_0:def 2;
then
A3: dom ONE=dom b1 by FINSEQ_3:29;
let i such that
A4: i in dom b1;
A5: len M=len b1 by MATRIX_0:25;
A6: Mx2Tran(M,b1,B2).(b1/.i) = Sum lmlt (Line(LineVec2Mx(b1/.i|--b1) * M,1)
,B2) by MATRLIN2:def 3
.= Sum lmlt (Line(LineVec2Mx(Line(ONE,i))*M,1),B2) by A4,MATRLIN2:19
.= Sum lmlt (Line(LineVec2Mx(Line(ONE*M,i)),1),B2) by A4,A3,A5,MATRIX_0:24
,MATRLIN2:35
.= Sum lmlt (Line(LineVec2Mx(Line(M,i)),1),B2) by A5,MATRIXR2:68
.= Sum lmlt (Line(M,i),B2) by MATRIX15:25;
dom b1=Seg len b1 by FINSEQ_1:def 3;
then n<>0 by A4,A5,A2;
then
A7: width J=n & width J=len B2 by A1,A5,A2,MATRIX_0:20;
then dom B2=dom b1 by A5,A2,FINSEQ_3:29;
hence thesis by A1,A4,A5,A2,A7,A6,Th21,Th22;
end;
theorem Th24:
for J be FinSequence_of_Jordan_block of L,K for M be Matrix of
len b1,len B2,K st M = block_diagonal(J,0.K) for i,m st i in dom b1 & m = min(
Len J,i) holds (i = Sum (Len J|m) implies Mx2Tran(M,b1,B2).(b1/.i) = L*(B2/.i))
& (i <> Sum (Len J|m) implies Mx2Tran(M,b1,B2).(b1/.i) = L*(B2/.i)+ B2/.(i+1))
proof
let J be FinSequence_of_Jordan_block of L,K;
let M be Matrix of len b1,len B2,K such that
A1: M = block_diagonal(J,0.K);
A2: dom b1=Seg len b1 & len M=Sum Len J by A1,FINSEQ_1:def 3,MATRIXJ1:def 5;
let i,m such that
A3: i in dom b1 and
A4: m = min(Len J,i);
set Sm=Sum (Len J|m);
A5: 1<=i by A3,FINSEQ_3:25;
A6: i<=len b1 by A3,FINSEQ_3:25;
then
A7: len M=len b1 by A5,MATRIX_0:23;
then
A8: m in dom Len J by A3,A4,A2,MATRIXJ1:def 1;
then
A9: (Len J).m = len (J.m) by MATRIXJ1:def 3;
set S=Sum (Len J| (m-'1));
set iS=i-'S;
set BBB=(B2|Sum(Width J|m))/^Sum (Width J| (m-'1));
A10: Mx2Tran(M,b1,B2).(b1/.i) = Sum lmlt(Line(J.m,iS),BBB) by A1,A3,A4,Th20;
A11: width M=Sum Width J by A1,MATRIXJ1:def 5;
A12: len BBB = width (J.m) by A1,A3,A4,Th20;
A13: (Len J) |m = Len (J|m) by MATRIXJ1:17;
then
A14: i<=Sm by A3,A4,A7,A2,MATRIXJ1:def 1;
A15: (Len J) | (m-'1) = Len (J| (m-'1)) by MATRIXJ1:17;
then S<i by A3,A4,A7,A2,MATRIXJ1:7;
then
A16: iS=i-S by XREAL_1:233;
A17: m-'1=m-1 by A3,A4,A7,A2,MATRIXJ1:7;
then (Len J) | (m-'1+1)=(Len J| (m-'1))^<*(Len J).m*> by A15,A8,FINSEQ_5:10;
then
A18: Sm=S+len (J.m) by A13,A17,A9,RVSUM_1:74;
then S+iS<=S+len (J.m) by A3,A4,A13,A7,A2,A16,MATRIXJ1:def 1;
then
A19: iS<=len (J.m) by XREAL_1:6;
dom Len J=dom J by MATRIXJ1:def 3;
then consider n such that
A20: J.m = Jordan_block(L,n) by A8,Def3;
m in NAT & m <= len Len J by A8,FINSEQ_3:25;
then Sm <= Sum ((Len J) | (len Len J)) by A13,POLYNOM3:18;
then
A21: Sm <= Sum Len J by FINSEQ_1:58;
A22: Width J=Len J by MATRIXJ1:46;
then
A23: (Len J).m=width (J.m) by A8,MATRIXJ1:def 4;
width M=len B2 by A5,A6,MATRIX_0:23;
then
A24: len (B2|Sm) =Sm by A22,A11,A21,FINSEQ_1:59;
then
A25: i in dom (B2|Sm) by A5,A14,FINSEQ_3:25;
A26: len (J.m)=n by A20,MATRIX_0:24;
iS<>0 by A3,A4,A15,A7,A2,A16,MATRIXJ1:7;
then 1<=iS by NAT_1:14;
then
A27: iS in dom BBB by A12,A9,A23,A19,FINSEQ_3:25;
then
A28: BBB/.iS = (B2|Sum(Width J|m))/.(Sum (Width J| (m-'1))+iS) by FINSEQ_5:27
.= (B2|Sum(Width J|m))/.(S+iS) by MATRIXJ1:46
.= (B2|Sum((Len J) |m))/.i by A22,A16,MATRIXJ1:21
.= B2/.i by A13,A25,FINSEQ_4:70;
hence i = Sm implies Mx2Tran(M,b1,B2).(b1/.i) = L*(B2/.i) by A10,A12,A9,A16
,A23,A18,A27,A20,A26,Th21;
assume
A29: i<>Sm;
then i<Sm by A14,XXREAL_0:1;
then 1<=i+1 & i+1<=Sm by NAT_1:11,13;
then
A30: i+1 in dom (B2|Sm) by A24,FINSEQ_3:25;
A31: iS<>len (J.m) by A16,A18,A29;
then iS<len (J.m) by A19,XXREAL_0:1;
then 1<=iS+1 & iS+1<=len (J.m) by NAT_1:11,13;
then iS+1 in dom BBB by A12,A9,A23,FINSEQ_3:25;
then BBB/.(iS+1) = (B2|Sum(Width J|m))/.(Sum (Width J| (m-'1))+(iS+1)) by
FINSEQ_5:27
.= (B2|Sum(Width J|m))/.(Sum ((Len J) | (m-'1))+(iS+1)) by A22,MATRIXJ1:21
.= (B2|Sum((Len J) |m))/.(i+1) by A15,A22,A16,MATRIXJ1:21
.= B2/.(i+1) by A13,A30,FINSEQ_4:70;
hence thesis by A10,A12,A9,A23,A27,A20,A26,A28,A31,Th22;
end;
theorem Th25:
for J be FinSequence_of_Jordan_block of 0.K,K for M be Matrix of
len b1,len b1,K st M = block_diagonal(J,0.K) for m st for i st i in dom J holds
len (J.i) <= m holds Mx2Tran(M,b1,b1) |^ m = ZeroMap(V1,V1)
proof
let J be FinSequence_of_Jordan_block of 0.K,K;
let M be Matrix of len b1,len b1,K such that
A1: M = block_diagonal(J,0.K);
reconsider Z=ZeroMap(V1,V1) as linear-transformation of V1,V1;
set MT=Mx2Tran(M,b1,b1);
let m such that
A2: for i st i in dom J holds len (J.i) <= m;
A3: dom Z=the carrier of V1 & rng b1 c= the carrier of V1 by FUNCT_2:def 1
,RELAT_1:def 19;
set MTm=MT|^m;
A4: dom MTm=the carrier of V1 by FUNCT_2:def 1;
per cases;
suppose
len b1=0;
then dim V1=0 by MATRLIN2:21;
then (Omega).V1=(0).V1 by VECTSP_9:29;
then
A5: the carrier of V1 = {0.V1} by VECTSP_4:def 3;
rng MTm c= the carrier of V1 by RELAT_1:def 19;
then rng MTm={0.V1} by A5,ZFMISC_1:33;
then MTm = (the carrier of V1)-->0.V1 by A4,FUNCOP_1:9
.= Z by GRCAT_1:def 7;
hence thesis;
end;
suppose
A6: len b1>0;
A7: dom J=dom Len J by MATRIXJ1:def 3;
A8: len M=len b1 & len M = Sum Len J by A1,MATRIX_0:24;
A9: now
let x be object such that
A10: x in dom b1;
reconsider n=x as Element of NAT by A10;
set mm=min(Len J,n);
A11: n in Seg Sum Len J by A8,A10,FINSEQ_1:def 3;
then
A12: mm in dom Len J by MATRIXJ1:def 1;
then
A13: (Len J).mm = len (J.mm) by MATRIXJ1:def 3;
A14: (Len J) |mm =Len (J|mm) by MATRIXJ1:17;
A15: now
mm<=len Len J by A12,FINSEQ_3:25;
then Sum (Len J|mm)<= Sum ((Len J) | (len Len J)) by A14,POLYNOM3:18;
then
A16: Sum (Len J|mm)<= len b1 by A8,FINSEQ_1:58;
let k;
assume n+k<=Sum (Len J|mm);
then
A17: n+k <= len b1 by A16,XXREAL_0:2;
1<=n & n<=n+k by A11,FINSEQ_1:1,NAT_1:11;
then 1<=n+k by XXREAL_0:2;
hence n+k in dom b1 by A17,FINSEQ_3:25;
end;
defpred Q[Nat] means (MT|^($1+1)).(b1/.n)=0.V1;
defpred P[Nat] means n+$1 < Sum(Len J|mm) implies (MT|^($1+1)).(b1/.n)=
b1/.(n+$1+1);
set Sm=Sum ((Len J) | (mm-'1));
A18: (Len J).mm=(Len J)/.mm by A12,PARTFUN1:def 6;
mm-'1=mm-1 by A11,MATRIXJ1:7;
then mm-'1+1=mm;
then (Len J) |mm=((Len J) | (mm-'1))^<*(Len J).mm*> by A12,FINSEQ_5:10;
then
A19: Sum (Len J|mm)=Sm+len (J.mm) by A14,A13,RVSUM_1:74;
A20: Sm < n by A11,MATRIXJ1:7;
then
A21: n-'Sm=n-Sm by XREAL_1:233;
then
A22: n-'Sm<>0 by A11,MATRIXJ1:7;
A23: now
let k;
assume n+k<=Sum(Len J|mm);
then
A24: n+k-Sm<=Sm+len (J.mm)-Sm by A19,XREAL_1:9;
1<=n-'Sm+k by A22,NAT_1:14;
then n-'Sm+k in Seg ((Len J)/.mm) by A18,A21,A13,A24;
then min(Len J,n-'Sm+k+Sum ((Len J) | (mm-'1)))=mm by A12,MATRIXJ1:10;
hence min(Len J,n+k)=mm by A21;
end;
A25: for k st P[k] holds P[k+1]
proof
let k such that
A26: P[k];
set k1=k+1;
A27: the carrier of V1= dom (MT|^k1) & n+k1=n+k+1 by FUNCT_2:def 1;
assume
A28: n+k1<Sum(Len J|mm);
then n+k1<Sum(Len J|min(Len J,n+k1)) & n+k1 in dom b1 by A15,A23;
then
A29: MT.(b1/.(n+k1)) = 0.K*(b1/.(n+k1))+ b1/.(n+k1+1) by A1,Th24
.= 0.V1+b1/.(n+k1+1) by VECTSP_1:14
.= b1/.(n+k1+1) by RLVECT_1:def 4;
thus (MT|^(k1+1)).(b1/.n) = ((MT|^1)*(MT|^k1)).(b1/.n) by VECTSP11:20
.= (MT|^1).(b1/.(n+k1)) by A26,A28,A27,FUNCT_1:13,NAT_1:13
.= b1/.(n+k1+1) by A29,VECTSP11:19;
end;
n<=Sum ((Len J) |mm) by A11,MATRIXJ1:def 1;
then
A30: Sum (Len J|mm)-'n=Sum (Len J|mm) - n by A14,XREAL_1:233;
A31: P[0]
proof
assume n+0< Sum(Len J|mm);
then MT.(b1/.n) = 0.K*(b1/.n)+ b1/.(n+1) by A1,A10,Th24
.= 0.V1+b1/.(n+1) by VECTSP_1:14
.= b1/.(n+1) by RLVECT_1:def 4;
hence thesis by VECTSP11:19;
end;
A32: for k holds P[k] from NAT_1:sch 2(A31,A25);
A33: Q[Sum(Len J|mm)-'n]
proof
per cases;
suppose
A34: Sum(Len J|mm)-'n=0;
then MT.(b1/.n) = 0.K*(b1/.n) by A1,A10,A30,Th24
.= 0.V1 by VECTSP_1:14;
hence thesis by A34,VECTSP11:19;
end;
suppose
Sum(Len J|mm)-'n>0;
then reconsider S1=(Sum(Len J|mm)-'n)-1 as Element of NAT by NAT_1:20
;
A35: the carrier of V1= dom (MT|^(Sum(Len J|mm)-'n)) by FUNCT_2:def 1;
Sum(Len J|mm)-1<Sum(Len J|mm)-0 by XREAL_1:10;
then
A36: (MT|^(S1+1)).(b1/.n) = b1/.(n+S1+1) by A30,A32
.= b1/.Sum(Len J|mm) by A30;
Sum(Len J|mm)-'n+n = Sum(Len J|mm) by A30;
then Sum(Len J|mm) in dom b1 & min(Len J,Sum(Len J|mm))=mm by A15,A23
;
then
A37: MT.(b1/.Sum(Len J|mm)) = 0.K*(b1/.Sum(Len J|mm)) by A1,Th24
.= 0.V1 by VECTSP_1:14;
thus (MT|^(Sum(Len J|mm)-'n+1)).(b1/.n) = ((MT|^1)*(MT|^(Sum(Len J|
mm)-'n))).(b1/.n) by VECTSP11:20
.= (MT|^1).((MT|^(Sum(Len J|mm)-'n)).(b1/.n)) by A35,FUNCT_1:13
.= 0.V1 by A36,A37,VECTSP11:19;
end;
end;
Sm-n <n-n by A20,XREAL_1:9;
then
A38: len (J.mm)+(Sm-n) < len (J.mm)+0 by XREAL_1:6;
then 0<m by A2,A7,A12,A30,A19;
then reconsider m1=m-1 as Element of NAT by NAT_1:20;
len (J.mm) <= m by A2,A7,A12;
then Sum (Len J|mm)-'n<m1+1 by A30,A19,A38,XXREAL_0:2;
then
A39: Sum (Len J|mm)-'n <= m1 by NAT_1:13;
A40: for k st Sum(Len J|mm)-'n <=k holds Q[k] implies Q[k+1]
proof
let k such that
Sum(Len J|mm)-'n <=k;
set k1=k+1;
assume
A41: Q[k];
A42: dom (MT|^k1)=the carrier of V1 by FUNCT_2:def 1;
thus (MT|^(k1+1)).(b1/.n) = ((MT|^1)*(MT|^k1)).(b1/.n) by VECTSP11:20
.= (MT|^1).((MT|^k1).(b1/.n)) by A42,FUNCT_1:13
.= MT.(0.V1) by A41,VECTSP11:19
.= MT.(0.K*0.V1) by VECTSP_1:14
.= 0.K*MT.(0.V1) by MOD_2:def 2
.= 0.V1 by VECTSP_1:14;
end;
for k st Sum(Len J|mm)-'n <= k holds Q[k] from NAT_1:sch 8(A33,A40);
then
A43: (MT|^(m1+1)).(b1/.n) = 0.V1 by A39;
thus (Z*b1).x = Z.(b1.x) by A10,FUNCT_1:13
.= Z.(b1/.x) by A10,PARTFUN1:def 6
.= ((the carrier of V1)-->0.V1).(b1/.x) by GRCAT_1:def 7
.= 0.V1
.= MTm.(b1.n) by A10,A43,PARTFUN1:def 6
.= (MTm*b1).x by A10,FUNCT_1:13;
end;
dom (Z*b1)=dom b1 & dom (MTm*b1)=dom b1 by A4,A3,RELAT_1:27;
hence thesis by A6,A9,FUNCT_1:2,MATRLIN:22;
end;
end;
Lm3: for J be FinSequence_of_Jordan_block of L,K for M be Matrix of len b1,len
b1,K st M = block_diagonal(J,0.K) & len b1<>0 holds (Mx2Tran(M,b1,b1) |^n).
(b1/.
Sum (Len J|min(Len J,len b1)))= ((power K).(L,n))*(b1/.Sum (Len J|min(Len J,len
b1))) & Sum (Len J|min(Len J,len b1)) in dom b1
proof
let J be FinSequence_of_Jordan_block of L,K;
set B=len b1;
set m=min(Len J,B);
set S=Sum (Len J|m);
A1: Seg B=dom b1 by FINSEQ_1:def 3;
let M be Matrix of len b1,len b1,K such that
A2: M = block_diagonal(J,0.K);
A3: len b1 = len M & len M = Sum Len J by A2,MATRIX_0:24;
set MT=Mx2Tran(M,b1,b1);
defpred P[Nat] means (MT|^$1).(b1/.S)=((power K).(L,$1))*(b1/.S);
(MT|^0).(b1/.S) = (id V1).(b1/.S) by VECTSP11:18
.= b1/.S by FUNCT_1:18
.= 1_K * b1/.S
.= ((power K).(L,0))*b1/.S by GROUP_1:def 7;
then
A4: P[0];
A5: Sum ((Len J) |m)=S & (Len J) | (len Len J)=Len J by FINSEQ_1:58,MATRIXJ1:17
;
assume B<>0;
then
A6: B in Seg B by FINSEQ_1:3;
then m in dom Len J by A3,MATRIXJ1:def 1;
then m<=len Len J by FINSEQ_3:25;
then
A7: Sum ((Len J) |m)<=Sum ((Len J) | (len Len J)) by POLYNOM3:18;
A8: B<= Sum ((Len J) |m) by A3,A6,MATRIXJ1:def 1;
then B=S by A3,A7,A5,XXREAL_0:1;
then
A9: MT.(b1/.S)=L*(b1/.S) by A2,A6,A1,Th24;
A10: for n st P[n] holds P[n+1]
proof
let n such that
A11: P[n];
A12: dom (MT|^n) = the carrier of V1 by FUNCT_2:def 1;
thus (MT|^(n+1)).(b1/.S) = ((MT|^1)*(MT|^n)).(b1/.S) by VECTSP11:20
.= (MT*(MT|^n)).(b1/.S) by VECTSP11:19
.= MT.(((power K).(L,n))*(b1/.S)) by A11,A12,FUNCT_1:13
.= ((power K).(L,n))*(L*(b1/.S)) by A9,MOD_2:def 2
.= (((power K).(L,n))*L)*(b1/.S) by VECTSP_1:def 16
.= ((power K).(L,n+1))*(b1/.S) by GROUP_1:def 7;
end;
for n holds P[n] from NAT_1:sch 2(A4,A10);
hence thesis by A3,A6,A1,A8,A7,A5,XXREAL_0:1;
end;
theorem
for J be FinSequence_of_Jordan_block of L,K for M be Matrix of len b1,
len b1,K st M = block_diagonal(J,0.K) holds Mx2Tran(M,b1,b1) is nilpotent iff
len b1 = 0 or L = 0.K
proof
let J be FinSequence_of_Jordan_block of L,K;
let M be Matrix of len b1,len b1,K such that
A1: M = block_diagonal(J,0.K);
set MT=Mx2Tran(M,b1,b1);
thus MT is nilpotent implies len b1 = 0 or L = 0.K
proof
set B=len b1;
set m=min(Len J,B);
set S=Sum (Len J|m);
assume MT is nilpotent;
then reconsider MT as nilpotent linear-transformation of V1,V1;
rng b1 is Basis of V1 by MATRLIN:def 2;
then
A2: rng b1 is linearly-independent Subset of V1 by VECTSP_7:def 3;
assume
A3: B<>0;
then S in dom b1 by A1,Lm3;
then b1.S in rng b1 & b1/.S=b1.S by FUNCT_1:def 3,PARTFUN1:def 6;
then
A4: b1/.S <>0.V1 by A2,VECTSP_7:2;
((power K).(L,deg MT))*(b1/.S) = (MT|^(deg MT)).(b1/.S) by A1,A3,Lm3
.= ZeroMap(V1,V1).(b1/.S) by Def5
.= ((the carrier of V1)-->0.V1).(b1/.S) by GRCAT_1:def 7
.= 0.V1
.= 0.K * (b1/.S) by VECTSP_1:14;
then 0.K = (power K).(L,deg MT) by A4,VECTSP10:4
.= Product (deg MT|->L) by MATRIXJ1:5;
then
A5: ex k be Nat st k in dom (deg MT|->L) & (deg MT|->L).k=0.K
by FVSUM_1:82;
dom (deg MT|->L)=Seg deg MT by FINSEQ_2:124;
hence thesis by A5,FINSEQ_2:57;
end;
assume
A6: len b1=0 or L=0.K;
per cases by A6;
suppose
len b1=0;
then dim V1=0 by MATRLIN2:21;
then (Omega).V1=(0).V1 by VECTSP_9:29;
then
A7: the carrier of V1 = {0.V1} by VECTSP_4:def 3;
rng (MT|^1) c= the carrier of V1 by RELAT_1:def 19;
then rng (MT|^1)={0.V1} by A7,ZFMISC_1:33;
then (MT|^1) = (dom (MT|^1))-->0.V1 by FUNCOP_1:9
.= (the carrier of V1)-->0.V1 by FUNCT_2:def 1
.= ZeroMap(V1,V1) by GRCAT_1:def 7;
hence thesis by Th13;
end;
suppose
A8: L=0.K;
now
A9: dom J=dom (Len J) by MATRIXJ1:def 3;
let i such that
A10: i in dom J;
len (J.i)=(Len J).i by A10,A9,MATRIXJ1:def 3;
hence len (J.i) <= Sum Len J by A10,A9,POLYNOM3:4;
end;
then MT|^(Sum Len J)=ZeroMap(V1,V1) by A1,A8,Th25;
hence thesis by Th13;
end;
end;
theorem
for J be FinSequence_of_Jordan_block of 0.K,K for M be Matrix of len
b1,len b1,K st M = block_diagonal(J,0.K) & len b1 > 0 for F be nilpotent
Function of V1,V1 st F = Mx2Tran(M,b1,b1) holds (ex i st i in dom J & len (J.i)
= deg F) & for i st i in dom J holds len (J.i) <= deg F
proof
let J be FinSequence_of_Jordan_block of 0.K,K;
let M be Matrix of len b1,len b1,K such that
A1: M = block_diagonal(J,0.K) and
A2: len b1 > 0;
A3: len M=len b1 & len M=Sum Len J by A1,MATRIX_0:def 2;
defpred P[Nat] means for i st i in dom J holds len (J.i) <= $1;
set mm=min(Len J,len b1);
A4: dom J=dom (Len J) by MATRIXJ1:def 3;
now
let i such that
A5: i in dom J;
len (J.i)=(Len J).i by A4,A5,MATRIXJ1:def 3;
hence len (J.i) <= Sum Len J by A4,A5,POLYNOM3:4;
end;
then
A6: ex k st P[k];
consider MIN be Nat such that
A7: P[MIN] and
A8: for m st P[m] holds MIN <= m from NAT_1:sch 5(A6);
len b1 in Seg len b1 by A2,FINSEQ_1:3;
then
A9: min(Len J,len b1) in dom Len J by A3,MATRIXJ1:def 1;
A10: ex i st i in dom J & len (J.i) = MIN
proof
assume
A11: for i st i in dom J holds len (J.i) <> MIN;
len (J.mm)<=MIN by A9,A4,A7;
then len (J.mm)<MIN by A9,A4,A11,XXREAL_0:1;
then reconsider M1=MIN-1 as Element of NAT by NAT_1:20;
now
let i such that
A12: i in dom J;
len (J.i) <= MIN by A7,A12;
then len (J.i) < M1+1 by A11,A12,XXREAL_0:1;
hence len (J.i) <= M1 by NAT_1:13;
end;
then M1+1<=M1 by A8;
hence thesis by NAT_1:13;
end;
A13: (Len J) | (len Len J)=Len J by FINSEQ_1:58;
let F be nilpotent Function of V1,V1 such that
A14: F = Mx2Tran(M,b1,b1);
consider i such that
A15: i in dom J and
A16: len (J.i) = MIN by A10;
A17: (Len J).i=(Len J)/.i by A4,A15,PARTFUN1:def 6;
set S=Sum ((Len J) | (i-'1));
defpred P[Nat] means $1 in Seg MIN & $1 <> MIN implies (F|^$1).(b1/.(S+1))=
b1/.(S+$1+1);
A18: len (J.i)=(Len J).i by A4,A15,MATRIXJ1:def 3;
i<=len Len J by A4,A15,FINSEQ_3:25;
then Sum ((Len J) |i) <= Sum ((Len J) | (len Len J)) by POLYNOM3:18;
then
A19: dom b1=Seg len b1 & Seg Sum ((Len J) |i) c= Seg Sum Len J by A13,
FINSEQ_1:5,def 3;
1<=i by A15,FINSEQ_3:25;
then i-'1=i-1 by XREAL_1:233;
then
A20: i=i-'1+1;
A21: for n st P[n] holds P[n+1]
proof
(Len J) |i=((Len J) | (i-'1))^<*MIN*> by A4,A15,A16,A18,A20,FINSEQ_5:10;
then
A22: Sum ((Len J) |i)=S+MIN by RVSUM_1:74;
let n such that
A23: P[n];
A24: (Len J) |i=Len J|i by MATRIXJ1:17;
set n1=n+1;
assume that
A25: n1 in Seg MIN and
A26: n1<>MIN;
A27: n1<=MIN by A25,FINSEQ_1:1;
then n1<MIN by A26,XXREAL_0:1;
then
A28: S+n1 < Sum ((Len J) |i) by A22,XREAL_1:6;
S+n1 in Seg Sum ((Len J) |i) & min(Len J,S+n1) = i by A4,A15,A16,A18,A17
,A25,MATRIXJ1:10;
then
A29: F.(b1/.(S+n1)) = 0.K*(b1/.(S+n1))+ (b1/.(S+n1+1)) by A1,A3,A14,A19,A28,A24
,Th24
.= 0.V1+b1/.(S+n1+1) by VECTSP_1:14
.= b1/.(S+n1+1) by RLVECT_1:def 4;
A30: n<MIN by A27,NAT_1:13;
now
per cases by NAT_1:14;
suppose
n=0;
hence thesis by A29,VECTSP11:19;
end;
suppose
A31: n>=1;
A32: dom (F|^n)= the carrier of V1 by FUNCT_2:def 1;
thus (F|^n1).(b1/.(S+1)) = ((F|^1)*(F|^n)).(b1/.(S+1)) by VECTSP11:20
.= (F|^1).((F|^n).(b1/.(S+1))) by A32,FUNCT_1:13
.= b1/.(S+n1+1) by A23,A30,A29,A31,VECTSP11:19;
end;
end;
hence thesis;
end;
A33: P[0];
A34: for n holds P[n] from NAT_1:sch 2(A33,A21);
A35: deg F >= MIN
proof
set D=deg F;
rng b1 is Basis of V1 by MATRLIN:def 2;
then
A36: rng b1 is linearly-independent Subset of V1 by VECTSP_7:def 3;
assume
A37: D < MIN;
then 1<=1+D & D+1<=MIN by NAT_1:11,13;
then D+1 in Seg MIN;
then S+(D+1) in Seg Sum ((Len J) |i) by A4,A15,A16,A18,A17,MATRIXJ1:10;
then
A38: b1/.(S+D+1)=b1.(S+D+1) & b1.(S+D+1) in rng b1 by A3,A19,FUNCT_1:def 3
,PARTFUN1:def 6;
D<>0
proof
assume D=0;
then [#]V1={0.V1} by Th15;
then (Omega).V1=(0).V1 by VECTSP_4:def 3;
then dim V1=0 by VECTSP_9:29;
hence thesis by A2,MATRLIN2:21;
end;
then D>=1 by NAT_1:14;
then D in Seg MIN by A37;
then b1/.(S+D+1) = (F|^D).(b1/.(S+1)) by A34,A37
.= ZeroMap(V1,V1).(b1/.(S+1)) by Def5
.= ((the carrier of V1)-->0.V1).(b1/.(S+1)) by GRCAT_1:def 7
.= 0.V1;
hence thesis by A38,A36,VECTSP_7:2;
end;
F|^MIN = ZeroMap(V1,V1) by A1,A14,A7,Th25;
then deg F <= MIN by Def5;
then deg F = MIN by A35,XXREAL_0:1;
hence thesis by A7,A10;
end;
Lm4: for V1,V2 be VectSp of K, f be linear-transformation of V1,V2 for W1 be
Subspace of V1,W2 be Subspace of V2 for F be Function of W1,W2 st F=f|W1 holds
F is linear-transformation of W1,W2
proof
let V1,V2 be VectSp of K,f be linear-transformation of V1,V2;
let W1 be Subspace of V1;
let W2 be Subspace of V2;
let F be Function of W1,W2 such that
A1: F=f|W1;
A2: now
let a be Scalar of K,w be Vector of W1;
thus F.(a*w) = a*(f|W1).w by A1,MOD_2:def 2
.= a*(F.w) by A1,VECTSP_4:14;
end;
now
let w1,w2 be Vector of W1;
thus F.(w1+w2) = (f|W1).w1+(f|W1).w2 by A1,VECTSP_1:def 20
.= F.w1+F.w2 by A1,VECTSP_4:13;
end;
then F is additive homogeneous by A2,MOD_2:def 2,VECTSP_1:def 20;
hence thesis;
end;
theorem Th28:
for V1,V2,b1,b2,L st len b1 = len b2 for F be
linear-transformation of V1,V2 st for i st i in dom b1 holds F.(b1/.i) = L * (
b2/.i) or i+1 in dom b1 & F.(b1/.i) = L * (b2/.i) +b2/.(i+1) ex J be non-empty
FinSequence_of_Jordan_block of L,K st AutMt(F,b1,b2) = block_diagonal(J,0.K)
proof
defpred P[Nat] means for V1,V2,b1,b2,L st len b1 = len b2 for F be
linear-transformation of V1,V2 st $1= card {i where i is Element of NAT: i in
dom b1 & F.(b1/.i) = L * (b2/.i)} & for i st i in dom b1 holds F.(b1/.i) = L *
(b2/.i) or (i+1 in dom b1 & F.(b1/.i) = L * (b2/.i) +b2/.(i+1)) ex J be
non-empty FinSequence_of_Jordan_block of L,K st AutMt(F,b1,b2) = block_diagonal
(J,0.K);
A1: P[0]
proof
let V1,V2,b1,b2,L such that
len b1 = len b2;
set Lb=len b1;
reconsider J={} as FinSequence_of_Jordan_block of L,K by Th10;
let F be linear-transformation of V1,V2 such that
A2: 0 = card {i where i is Element of NAT: i in dom b1 & F.(b1/.i) = L
* (b2/.i)} and
A3: for i st i in dom b1 holds F.(b1/.i) = L * (b2/.i) or i+1 in dom
b1 & F.(b1/.i) = L * (b2/.i) +b2/.(i+1);
reconsider J as non-empty FinSequence_of_Jordan_block of L,K;
take J;
Lb=0
proof
assume Lb<>0;
then
A4: Lb in Seg Lb by FINSEQ_1:3;
A5: dom b1=Seg Lb by FINSEQ_1:def 3;
per cases by A3,A4,A5;
suppose
F.(b1/.Lb)= L * (b2/.Lb);
then
Lb in {i where i is Element of NAT: i in dom b1 & F.(b1/.i) = L *
(b2/.i)} by A4,A5;
hence thesis by A2;
end;
suppose
Lb+1 in dom b1 & F.(b1/.Lb) = L *(b2/.Lb)+b2/.(Lb+1);
then Lb+1<=Lb by FINSEQ_3:25;
hence thesis by NAT_1:13;
end;
end;
then len AutMt(F,b1,b2)=0 by MATRIX_0:def 2;
then AutMt(F,b1,b2)={};
hence thesis by MATRIXJ1:22;
end;
A6: for n st P[n] holds P[n+1]
proof
let n such that
A7: P[n];
set n1=n+1;
let V1,V2,b1,b2,L such that
A8: len b1 = len b2;
A9: dom b1=dom b2 by A8,FINSEQ_3:29;
set Lb=len b1;
let F be linear-transformation of V1,V2 such that
A10: n1 = card {i where i is Element of NAT: i in dom b1 & F.(b1/.i) =
L * (b2/.i)} and
A11: for i st i in dom b1 holds F.(b1/.i) = L * (b2/.i) or i+1 in dom
b1 & F.(b1/.i) = L * (b2/.i) +b2/.(i+1);
set FF={i where i is Element of NAT: i in dom b1 & F.(b1/.i) = L * (b2/.i)
};
reconsider FF as finite set by A10;
consider x being object such that
A12: x in FF by A10,CARD_1:27,XBOOLE_0:def 1;
ex ii be Element of NAT st ii=x & ii in dom b1 & F.(b1 /.ii) = L * (b2
/.ii) by A12;
then
dom b1 <> {};
then
Seg Lb <> {} by FINSEQ_1:def 3;
then
A13: Lb<>0;
A14: dom b1=Seg Lb by FINSEQ_1:def 3;
then
A15: not Lb+1 in dom b1 by FINSEQ_3:8;
A16: Lb in dom b1 by A14,A13,FINSEQ_1:3;
then F.(b1/.Lb)= L * (b2/.Lb) by A11,A15;
then
A17: Lb in FF by A16;
per cases;
suppose
A18: n=0;
set J=Jordan_block(L,Lb);
reconsider JJ=<*J*> as FinSequence_of_Jordan_block of L,K by Th11;
now
A19: dom JJ ={1} by FINSEQ_1:2,def 8;
let x be object;
assume x in dom JJ;
then JJ.1=J & x=1 by A19,TARSKI:def 1;
hence JJ.x is non empty by A13,Def1;
end;
then reconsider JJ as non-empty FinSequence_of_Jordan_block of L,K by
FUNCT_1:def 9;
reconsider F9=F as Function of V1,V2;
reconsider BB=block_diagonal(JJ,0.K) as Matrix of len b1,len b2,K by A8,
MATRIXJ1:34;
set T=Mx2Tran(BB,b1,b2);
A20: block_diagonal(JJ,0.K)=J by MATRIXJ1:34;
A21: now
let y be object such that
A22: y in dom b1;
reconsider j=y as Element of NAT by A22;
A23: (T*b1).y=T.(b1.y) by A22,FUNCT_1:13;
A24: b1/.j=b1.j by A22,PARTFUN1:def 6;
A25: (F9*b1).y=F.(b1.y) by A22,FUNCT_1:13;
now
per cases;
suppose
A26: j = Lb;
hence (T*b1).y = L*(b2/.Lb) by A20,A22,A23,A24,Th23
.= (F9*b1).y by A11,A16,A15,A25,A24,A26;
end;
suppose
A27: j <> Lb;
ex z be object st FF={z} by A10,A18,CARD_2:42;
then FF={Lb} by A17,TARSKI:def 1;
then not j in FF by A27,TARSKI:def 1;
then
A28: F.(b1/.j) <> L * (b2/.j) by A22;
(T*b1).y = L*(b2/.j)+ b2/.(j+1) by A20,A22,A23,A24,A27,Th23;
hence (T*b1).y=(F9*b1).y by A11,A22,A25,A24,A28;
end;
end;
hence (F9*b1).y = (T*b1).y;
end;
take JJ;
A29: rng b1 c= [#]V1 by FINSEQ_1:def 4;
dom T=[#]V1 by FUNCT_2:def 1;
then
A30: dom (T*b1)=dom b1 by A29,RELAT_1:27;
dom F=[#]V1 by FUNCT_2:def 1;
then dom (F9*b1)=dom b1 by A29,RELAT_1:27;
then F=T by A13,A30,A21,FUNCT_1:2,MATRLIN:22;
hence thesis by MATRLIN2:36;
end;
suppose
A31: n<>0;
defpred Q[Nat] means $1 in FF & $1 < Lb;
A32: ex k st Q[k]
proof
card FF<>1 by A10,A31;
then FF <> {Lb} by CARD_2:42;
then consider y being object such that
A33: y in FF and
A34: y <> Lb by A17,ZFMISC_1:35;
consider j be Element of NAT such that
A35: j=y and
A36: j in dom b1 and
F.(b1/.j) = L * (b2/.j) by A33;
take j;
j<=Lb by A36,FINSEQ_3:25;
hence thesis by A33,A34,A35,XXREAL_0:1;
end;
A37: for k st Q[k] holds k <= Lb;
consider m such that
A38: Q[m] and
A39: for k st Q[k] holds k<= m from NAT_1:sch 6(A37,A32);
set b1m=b1|m;
A40: len b1m=m by A38,FINSEQ_1:59;
set JB=Jordan_block(L,Lb-'m);
reconsider JJ=<*JB*> as FinSequence_of_Jordan_block of L,K by Th11;
set b19m=b1/^m;
A41: len b19m =Lb-m by A38,RFINSEQ:def 1;
set b29m=b2/^m;
A42: len b29m=Lb-m by A8,A38,RFINSEQ:def 1;
set b2m=b2|m;
A43: len b2m=m by A8,A38,FINSEQ_1:59;
reconsider Rb2=rng b2m, Rb29=rng b29m as linearly-independent Subset of
V2 by MATRLIN2:22,23;
reconsider Rb1=rng b1m, Rb19=rng b19m as linearly-independent Subset of
V1 by MATRLIN2:22,23;
set Lb1=Lin Rb1;
set Lb2=Lin Rb2;
set Lb19=Lin Rb19;
set Lb29=Lin Rb29;
set FRb1=F.:Rb1;
A44: rng (F|Lb1) = F.:(the carrier of Lb1) by RELAT_1:115;
reconsider b2m as OrdBasis of Lb2 by MATRLIN2:22;
reconsider b1m as OrdBasis of Lb1 by MATRLIN2:22;
A45: dom b1m = dom b2m by A40,A43,FINSEQ_3:29;
reconsider b19m as OrdBasis of Lb19 by MATRLIN2:23;
reconsider b29m as OrdBasis of Lb29 by MATRLIN2:23;
A46: b2=b2m^b29m by RFINSEQ:8;
A47: b1=b1m^b19m by RFINSEQ:8;
then
A48: dom b1m c= dom b1 by FINSEQ_1:26;
A49: for i st i in dom b1m holds (F|Lb1).(b1m/.i) = L * (b2m/.i) or i+1
in dom b1m & (F|Lb1).(b1m/.i) = L * (b2m/.i) +b2m/.(i+1)
proof
let i such that
A50: i in dom b1m;
A51: b1m.i=b1m/.i by A50,PARTFUN1:def 6;
set i1=i+1;
A52: F.(b1m/.i)=(F|Lb1).(b1m/.i) by FUNCT_1:49;
A53: b2/.i=b2.i & b2.i=b2m.i by A9,A46,A48,A45,A50,FINSEQ_1:def 7
,PARTFUN1:def 6;
A54: b1/.i=b1.i & b1.i=b1m.i by A47,A48,A50,FINSEQ_1:def 7,PARTFUN1:def 6;
per cases by A11,A48,A50;
suppose
F.(b1/.i) = L * (b2/.i);
hence thesis by A45,A50,A53,A54,A51,A52,PARTFUN1:def 6,VECTSP_4:14;
end;
suppose
A55: i1 in dom b1 & F.(b1/.i) = L * (b2/.i) +b2/.i1;
reconsider rngb2=rng b2 as Basis of V2 by MATRLIN:def 2;
A56: i1<=m
proof
assume i1>m;
then
A57: i>=m by NAT_1:13;
i<=m by A40,A50,FINSEQ_3:25;
then
A58: i=m by A57,XXREAL_0:1;
ex ii be Element of NAT st m=ii & ii in dom b1 & F.(b1/.ii) =
L * (b2/. ii) by A38;
then F.(b1/.i)=L*(b2/.i)+0.V2 by A58,RLVECT_1:def 4;
then
A59: b2/.i1=0.V2 by A55,RLVECT_1:8;
A60: rngb2 is linearly-independent by VECTSP_7:def 3;
b2/.i1=b2.i1 & b2.i1 in rngb2 by A9,A55,FUNCT_1:def 3
,PARTFUN1:def 6;
hence thesis by A59,A60,VECTSP_7:2;
end;
A61: 1<=i1 by NAT_1:11;
then
A62: i1 in dom b1m by A40,A56,FINSEQ_3:25;
then
A63: b2m.i1=b2m/.i1 by A45,PARTFUN1:def 6;
A64: L*(b2/.i)=L*(b2m/.i) by A45,A50,A53,PARTFUN1:def 6,VECTSP_4:14;
b2/.i1=b2.i1 & b2.i1=b2m.i1 by A9,A46,A48,A45,A62,FINSEQ_1:def 7
,PARTFUN1:def 6;
hence thesis by A40,A54,A51,A52,A55,A56,A61,A63,A64,FINSEQ_3:25
,VECTSP_4:13;
end;
end;
FRb1 c= the carrier of Lb2
proof
let y be object;
assume y in FRb1;
then consider x being object such that
x in dom F and
A65: x in Rb1 and
A66: F.x=y by FUNCT_1:def 6;
consider i be object such that
A67: i in dom b1m and
A68: b1m.i=x by A65,FUNCT_1:def 3;
reconsider i as Element of NAT by A67;
b1m/.i=b1m.i by A67,PARTFUN1:def 6;
then (F|Lb1).(b1m/.i)=y by A66,A68,FUNCT_1:49;
then y=L * (b2m/.i) or y=L * (b2m/.i)+b2m/.(i+1) by A49,A67;
hence thesis;
end;
then the carrier of Lin(FRb1) = F.:(the carrier of Lb1) & Lin(FRb1) is
Subspace of Lb2 by VECTSP11:42,VECTSP_9:16;
then F.:(the carrier of Lb1) c= the carrier of Lb2 by VECTSP_4:def 2;
then reconsider FL=F|Lb1 as linear-transformation of Lb1,Lb2 by A44,Lm4,
FUNCT_2:6;
A69: for i st i in dom b1m holds FL.(b1m/.i) = L * (b2m/.i) or i+1 in
dom b1m & FL.(b1m/.i) = L * (b2m/.i) +b2m/.(i+1) by A49;
set FF1={i where i is Element of NAT: i in dom b1m & FL.(b1m/.i) = L * (
b2m/.i)};
A70: FF\{Lb} c= FF1
proof
let x be object such that
A71: x in FF\{Lb};
A72: x <> Lb by A71,ZFMISC_1:56;
x in FF by A71;
then consider j be Element of NAT such that
A73: j=x and
A74: j in dom b1 and
A75: F.(b1/.j) = L * (b2/.j);
j<=Lb by A74,FINSEQ_3:25;
then j <Lb by A72,A73,XXREAL_0:1;
then
A76: j<=m by A39,A71,A73;
1<=j by A74,FINSEQ_3:25;
then
A77: j in dom b1m by A40,A76,FINSEQ_3:25;
then
A78: b1m/.j=b1m.j & b1m.j=b1.j by A47,FINSEQ_1:def 7,PARTFUN1:def 6;
A79: FL.(b1m/.j)=F.(b1m/.j) & b1/.j=b1.j by A48,A77,FUNCT_1:49
,PARTFUN1:def 6;
b2m.j=b2.j & b2/.j=b2.j by A9,A46,A48,A45,A77,FINSEQ_1:def 7
,PARTFUN1:def 6;
then FL.(b1m/.j)=L * (b2m/.j) by A45,A75,A77,A78,A79,PARTFUN1:def 6
,VECTSP_4:14;
hence thesis by A73,A77;
end;
FF1 c= FF\{Lb}
proof
let x be object;
assume x in FF1;
then consider j be Element of NAT such that
A80: x=j and
A81: j in dom b1m and
A82: FL.(b1m/.j) = L * (b2m/.j);
A83: b1m/.j=b1m.j & b1m.j=b1.j by A47,A81,FINSEQ_1:def 7,PARTFUN1:def 6;
A84: FL.(b1m/.j)=F.(b1m/.j) & b1/.j=b1.j by A48,A81,FUNCT_1:49
,PARTFUN1:def 6;
b2m.j=b2.j & b2/.j=b2.j by A9,A46,A48,A45,A81,FINSEQ_1:def 7
,PARTFUN1:def 6;
then F.(b1/.j)=L * (b2/.j) by A45,A81,A82,A83,A84,PARTFUN1:def 6
,VECTSP_4:14;
then
A85: j in FF by A48,A81;
j<=m by A40,A81,FINSEQ_3:25;
hence thesis by A38,A80,A85,ZFMISC_1:56;
end;
then FF1=FF\{Lb} by A70,XBOOLE_0:def 10;
then card FF1=n by A10,A17,STIRL2_1:55;
then consider
J be non-empty FinSequence_of_Jordan_block of L,K such that
A86: AutMt(FL,b1m,b2m) = block_diagonal(J,0.K) by A7,A40,A43,A69;
set JJJ=J^JJ;
A87: Lb-m=Lb-'m by A38,XREAL_1:233;
A88: now
let x be object such that
A89: x in dom JJJ;
reconsider i=x as Nat by A89;
per cases by A89,FINSEQ_1:25;
suppose
A90: i in dom J;
then J.i is non empty by FUNCT_1:def 9;
hence JJJ.x is non empty by A90,FINSEQ_1:def 7;
end;
suppose
A91: ex j st j in dom JJ & i=len J + j;
len JB=Lb-'m by Def1;
then
A92: len JB<>0 by A38,A87;
consider j such that
A93: j in dom JJ and
A94: i=len J+j by A91;
dom JJ=Seg 1 by FINSEQ_1:38;
then j=1 by A93,FINSEQ_1:2,TARSKI:def 1;
then JJJ.i=JJ.1 by A93,A94,FINSEQ_1:def 7;
hence JJJ.x is non empty by A92;
end;
end;
len b19m = len b29m by A8,A38,A41,RFINSEQ:def 1;
then reconsider JB as Matrix of len b19m,len b29m,K by A41,A87;
A95: width JB = len b19m by A41,A42,MATRIX_0:24;
reconsider JJJ as non-empty FinSequence_of_Jordan_block of L,K by A88,
FUNCT_1:def 9;
take JJJ;
reconsider F9=F as Function of V1,V2;
reconsider B=block_diagonal(J,0.K) as Matrix of len b1m,len b2m,K by A86;
A96: width B=len b1m by A40,A43,MATRIX_0:24;
A97: Sum Len <*B,JB*> = len B + len JB & Sum Width <*B,JB*> = width B +
width JB by MATRIXJ1:16,20;
set BB = block_diagonal(<*B,JB*>,0.K);
A98: len B=len b1m by A40,A43,MATRIX_0:24;
A99: Sum Len <*B,JB*> = len b1
by A40,A41,A42,A97,A96,A95,A98,MATRIX_0:24;
Sum Width <*B,JB*> = len b2
by A8,A40,A41,A97,A96,A95;
then reconsider BB as Matrix of len b1,len b2,K
by A99;
set T=Mx2Tran(BB,b1,b2);
A100: dom b19m = dom b29m by A41,A42,FINSEQ_3:29;
A101: now
let x be object such that
A102: x in dom b1;
reconsider I=x as Element of NAT by A102;
A103: (T*b1).x=T.(b1.I) by A102,FUNCT_1:13;
A104: b1.I=b1/.I by A102,PARTFUN1:def 6;
A105: (F9*b1).x=F.(b1.I) by A102,FUNCT_1:13;
now
per cases by A47,A102,FINSEQ_1:25;
suppose
A106: I in dom b1m;
then
A107: b1m/.I = b1m.I & b1.I=b1m.I by A47,FINSEQ_1:def 7,PARTFUN1:def 6;
A108: FL.(b1m/.I) =F.(b1m/.I) by FUNCT_1:49;
thus (T*b1).x = Mx2Tran(B,b1m,b2m).(b1m/.I) by A40,A43,A41,A42,A47
,A46,A96,A95,A103,A104,A106,Th19
.= FL.(b1m/.I) by A86,MATRLIN2:34
.= (F9*b1).x by A102,A108,A107,FUNCT_1:13;
end;
suppose
ex j st j in dom b19m & I=len b1m + j;
then consider j such that
A109: j in dom b19m and
A110: I=len b1m + j;
now
per cases;
suppose
A111: j=len b19m;
A112: b2.I = b29m.j & b2/.I=b2.I by A9,A40,A43,A46,A100,A102,A109
,A110,FINSEQ_1:def 7,PARTFUN1:def 6;
thus (F9*b1).x = L*(b2/.I) by A11,A16,A15,A40,A41,A105,A104
,A110,A111
.= L*(b29m/.j) by A100,A109,A112,PARTFUN1:def 6,VECTSP_4:14
.= Mx2Tran(JB,b19m,b29m).(b19m/.j) by A109,A111,Th23;
end;
suppose
A113: j<>len b19m;
A114: (F9*b1).x = L*(b2/.I) + b2/.(I+1)
proof
assume (F9*b1).x <> L*(b2/.I) + b2/.(I+1);
then F.(b1/.I)=L*(b2/.I) by A11,A102,A105,A104;
then
A115: I in FF by A102;
I<>Lb & I<=Lb by A40,A41,A102,A110,A113,FINSEQ_3:25;
then I < Lb by XXREAL_0:1;
then len b1m + j<=len b1m+0 by A39,A40,A110,A115;
then j<=0 by XREAL_1:6;
hence thesis by A109,FINSEQ_3:25;
end;
j<=len b19m by A109,FINSEQ_3:25;
then j<len b19m by A113,XXREAL_0:1;
then 1<=j+1 & j+1<=len b19m by NAT_1:11,13;
then
A116: j+1 in dom b19m by FINSEQ_3:25;
then b29m/.(j+1)=b29m.(j+1) & b2.(len b1m+(j+1))=b29m.(j+1)
by A40,A43,A46,A100,FINSEQ_1:def 7,PARTFUN1:def 6;
then
A117: b29m/.(j+1)=b2/.(I+1) by A9,A47,A110,A116,FINSEQ_1:28
,PARTFUN1:def 6;
b2.I = b29m.j & b2/.I=b2.I by A9,A40,A43,A46,A100,A102,A109
,A110,FINSEQ_1:def 7,PARTFUN1:def 6;
then L*(b29m/.j) = L*(b2/.I) by A100,A109,PARTFUN1:def 6
,VECTSP_4:14;
then L*(b2/.I) + b2/.(I+1) = L*(b29m/.j) + b29m/.(j+1) by A117,
VECTSP_4:13
.= Mx2Tran(JB,b19m,b29m).(b19m/.j) by A109,A113,Th23;
hence (F9*b1).x=Mx2Tran(JB,b19m,b29m).(b19m/.j) by A114;
end;
end;
hence
(F9*b1).x=(T*b1).x by A40,A43,A41,A42,A47,A46,A96,A95,A103,A104
,A109,A110,Th19;
end;
end;
hence (F9*b1).x=(T*b1).x;
end;
A118: rng b1 c= [#]V1 by FINSEQ_1:def 4;
dom T=[#]V1 by FUNCT_2:def 1;
then
A119: dom (T*b1)=dom b1 by A118,RELAT_1:27;
dom F=[#]V1 by FUNCT_2:def 1;
then dom (F9*b1)=dom b1 by A118,RELAT_1:27;
then block_diagonal(JJJ,0.K)=block_diagonal(<*B,JB*>,0.K) & F=T by A13
,A119,A101,FUNCT_1:2,MATRIXJ1:35,MATRLIN:22;
hence thesis by MATRLIN2:36;
end;
end;
let V1,V2,b1,b2,L such that
A120: len b1 = len b2;
let F be linear-transformation of V1,V2 such that
A121: for i st i in dom b1 holds F.(b1/.i) = L * (b2/.i) or i+1 in dom
b1 & F.(b1/.i) = L * (b2/.i) +b2/.(i+1);
set FF={i where i is Element of NAT: i in dom b1 & F.(b1/.i) = L * (b2/.i)};
FF c= dom b1
proof
let x be object;
assume x in FF;
then ex i be Element of NAT st x=i & i in dom b1 & F.(b1/.i) = L * (b2/.i
);
hence thesis;
end;
then reconsider FF as finite set;
for n holds P[n] from NAT_1:sch 2(A1,A6);
then P[card FF];
hence thesis by A120,A121;
end;
theorem Th29:
for V1 be finite-dimensional VectSp of K for F be nilpotent
linear-transformation of V1,V1 ex J be non-empty FinSequence_of_Jordan_block of
0.K,K, b1 be OrdBasis of V1 st AutMt(F,b1,b1) = block_diagonal(J,0.K)
proof
defpred P[Nat] means for V1 be finite-dimensional VectSp of K for F be
nilpotent linear-transformation of V1,V1 st deg F=$1 holds ex J be
FinSequence_of_Jordan_block of 0.K,K, b1 be OrdBasis of V1 st AutMt(F,b1,b1) =
block_diagonal(J,0.K) & for i st i in dom J holds (Len J).i <> 0;
let V1 be finite-dimensional VectSp of K;
let F be nilpotent linear-transformation of V1,V1;
A1: for n st P[n] holds P[n+1]
proof
let n such that
A2: P[n];
let V1 be finite-dimensional VectSp of K;
set n1=n+1;
let F be nilpotent linear-transformation of V1,V1 such that
A3: deg F=n1;
set BAS = the Basis of V1;
A4: BAS is linearly-independent by VECTSP_7:def 3;
A5: Lin(BAS) = the ModuleStr of V1 by VECTSP_7:def 3;
set IM=im F|^1;
reconsider FI=F|IM as linear-transformation of IM,IM by VECTSP11:32;
reconsider FI as nilpotent linear-transformation of IM,IM by Th17;
deg FI+1=n1 by A3,Th18,NAT_1:11;
then consider
J be FinSequence_of_Jordan_block of 0.K,K, b1 be OrdBasis of IM
such that
A6: AutMt(FI,b1,b1) = block_diagonal(J,0.K) and
A7: for i st i in dom J holds (Len J).i <> 0 by A2;
A8: len b1 = len AutMt(FI,b1,b1) by MATRIX_0:def 2
.= Sum Len J by A6,MATRIXJ1:def 5;
then
A9: dom b1= Seg Sum Len J by FINSEQ_1:def 3;
set L=len J;
set LJ=Len J;
set S=Sum LJ;
defpred Q[Nat,Nat] means $2 in dom LJ & $2 <= $1 & Sum(LJ| ($2-'1)) <= $1-'
$2;
defpred R[object,object] means
for i,k st i=$1 & k=$2 holds Q[i,k] & i-'k <= Sum
(LJ|k) & for n st Q[i,n] holds n<=k;
A10: for x being object st x in Seg(S+L)
ex y being object st y in NAT & R[x,y]
proof
let x be object such that
A11: x in Seg (S+L);
reconsider i=x as Nat by A11;
L<>0
proof
assume
A12: L=0;
then LJ=<*>NAT;
hence thesis by A11,A12,RVSUM_1:72;
end;
then
A13: 1<=L by NAT_1:14;
1-'1=0 by XREAL_1:232;
then
A14: Sum(LJ| (1-'1))=0 by RVSUM_1:72;
defpred q[Nat] means $1 in dom LJ & $1 <= i & Sum(LJ| ($1-'1)) <= i-'$1;
A15: for k st q[k] holds k <= L
proof
let k;
assume q[k];
then k<=len LJ by FINSEQ_3:25;
hence thesis by CARD_1:def 7;
end;
len LJ=L by CARD_1:def 7;
then
A16: 0<=i-'1 & 1 in dom LJ by A13,FINSEQ_3:25;
1<=i by A11,FINSEQ_1:1;
then
A17: ex k st q[k] by A14,A16;
consider k such that
A18: q[k] and
A19: for n st q[n] holds n <= k from NAT_1:sch 6(A15,A17);
A20: i-'k <= Sum (LJ|k)
proof
assume
A21: i-'k > Sum (LJ|k);
then i-'k >= Sum (LJ|k)+1 by NAT_1:13;
then
A22: i-'k-1>=Sum (LJ|k)+1-1 by XREAL_1:9;
A23: i-'k=i-k by A18,XREAL_1:233;
A24: k+1<=len LJ
proof
assume k+1>len LJ;
then
A25: k>=len LJ by NAT_1:13;
then i-k>S by A21,A23,FINSEQ_1:58;
then
A26: i-k+k>S+k by XREAL_1:6;
len LJ=L by CARD_1:def 7;
then S+k>=S+L by A25,XREAL_1:6;
then i> S+L by A26,XXREAL_0:2;
hence thesis by A11,FINSEQ_1:1;
end;
1<=k+1 by NAT_1:14;
then
A27: k+1 in dom LJ by A24,FINSEQ_3:25;
i-'k>=1 by A21,NAT_1:14;
then
A28: i-k+k >=1+k by A23,XREAL_1:6;
then i-'(k+1)=i-(k+1) by XREAL_1:233;
then Sum(LJ| (k+1-'1)) <= i-'(k+1) by A22,A23,NAT_D:34;
then k+1<=k by A19,A28,A27;
hence thesis by NAT_1:13;
end;
take k;
thus k in NAT by ORDINAL1:def 12;
let i9,k9 be Nat;
assume i9=x & k9=k;
hence thesis by A18,A19,A20;
end;
consider r be Function of Seg (S+L),NAT such that
A29: for x being object st x in Seg (S+L) holds R[x,r.x]
from FUNCT_2:sch 1(A10);
defpred P[object,object] means
for i,k st i=$1 & k=r.i holds (i -' k = Sum (LJ| (
k-'1)) implies (F.$2 = b1.(i -' k+1) & i-'k+1 in dom b1)) & (i -' k <> Sum (LJ|
(k-'1)) implies ($2 = b1.(i -' k) & i-'k in dom b1 & min(LJ,i-'k)=k & ((i-'k <
Sum (LJ|k) implies F.$2 = b1.(i -' k+1) & i -' k+1 in dom b1) & (i-'k = Sum (LJ
|k) implies F.$2 = 0.V1))));
A30: dom r=Seg (S+L) by FUNCT_2:def 1;
A31: FI=Mx2Tran(AutMt(FI,b1,b1),b1,b1) by MATRLIN2:34;
A32: for x being object st x in Seg (S+L)
ex y being object st y in the carrier of V1 & P[x,y]
proof
let x be object such that
A33: x in Seg (S+L);
reconsider i=x as Nat by A33;
r.i=r/.i by A30,A33,PARTFUN1:def 6;
then reconsider k=r.i as Element of NAT;
A34: i-'k <= Sum (LJ|k) by A29,A33;
A35: Q[i,k] by A29,A33;
then
A36: LJ.k =len (J.k) by MATRIXJ1:def 3;
k<=len LJ by A35,FINSEQ_3:25;
then
A37: Sum (LJ|k) <= Sum (LJ| (len LJ)) by POLYNOM3:18;
1<=k by A35,FINSEQ_3:25;
then
A38: k-'1=k-1 by XREAL_1:233;
then k=k-'1+1;
then LJ|k=(LJ| (k-'1))^<*LJ.k*> by A35,FINSEQ_5:10;
then
A39: dom LJ=dom J & Sum (LJ|k)=Sum (LJ| (k-'1)) + len (J.k) by A36,
MATRIXJ1:def 3,RVSUM_1:74;
A40: LJ| (len LJ) =LJ by FINSEQ_1:58;
per cases;
suppose
A41: i -' k = Sum (LJ| (k-'1));
b1/.(i-'k+1) in IM & b1/.(i-'k+1) is Element of V1 by VECTSP_4:10;
then consider y be Element of V1 such that
A42: (F|^1).y=b1/.(i-'k+1) by RANKNULL:13;
take y;
thus y in the carrier of V1;
i-'k <> Sum (LJ|k) by A7,A35,A36,A39,A41;
then i-'k < Sum (LJ|k) by A34,XXREAL_0:1;
then i-'k+1 <=Sum(LJ|k) by NAT_1:13;
then
A43: 1<= i-'k+1 & i-'k+1 <= S by A37,A40,NAT_1:11,XXREAL_0:2;
then i-'k+1 in dom b1 by A9;
then b1/.(i-'k+1) = b1.(i-'k+1) by PARTFUN1:def 6;
hence thesis by A9,A41,A43,A42,VECTSP11:19;
end;
suppose
A44: i -' k <> Sum (LJ| (k-'1));
take y=b1/.(i-'k);
y in IM;
then y in V1 by VECTSP_4:9;
hence y in the carrier of V1;
i -' k>Sum (LJ| (k-'1)) by A35,A44,XXREAL_0:1;
then
A45: 1<= i-'k by NAT_1:14;
i-'k <= S by A34,A37,A40,XXREAL_0:2;
then
A46: i-'k in dom b1 by A9,A45;
i-'k <= Sum (LJ|k) by A29,A33;
then
A47: min(LJ,i-'k)<=k by A9,A46,MATRIXJ1:def 1;
A48: min(LJ,i-'k)=k
proof
assume min(LJ,i-'k)<>k;
then min(LJ,i-'k)<k-'1+1 by A38,A47,XXREAL_0:1;
then min(LJ,i-'k) <=k-'1 by NAT_1:13;
then
A49: Sum(LJ|min(LJ,i-'k)) <= Sum (LJ| (k-'1)) by POLYNOM3:18;
i-'k <= Sum(LJ|min(LJ,i-'k)) by A9,A46,MATRIXJ1:def 1;
then i-'k <= Sum (LJ| (k-'1)) by A49,XXREAL_0:2;
hence thesis by A35,A44,XXREAL_0:1;
end;
A50: Len J|k=LJ|k by MATRIXJ1:17;
A51: now
assume
A52: i-'k = Sum (LJ|k);
F.(b1/.(i-'k)) = FI.(b1/.(i-'k)) by FUNCT_1:49
.= 0.K*(b1/.(i-'k)) by A6,A31,A46,A48,A50,A52,Th24
.= 0.IM by VECTSP_1:14
.= 0.V1 by VECTSP_4:11;
hence F.y = 0.V1;
end;
A53: now
assume
A54: i-'k < Sum (LJ|k);
then i-'k+1<=Sum (LJ|k) by NAT_1:13;
then
A55: 1<=i-'k+1 & i-'k+1<=S by A37,A40,NAT_1:11,XXREAL_0:2;
then
A56: i-'k+1 in dom b1 by A9;
F.(b1/.(i-'k)) = FI.(b1/.(i-'k)) by FUNCT_1:49
.= 0.K*(b1/.(i-'k))+(b1/.(i-'k+1)) by A6,A31,A46,A48,A50,A54,Th24
.= 0.IM+(b1/.(i-'k+1)) by VECTSP_1:14
.= b1/.(i-'k+1) by RLVECT_1:def 4
.= b1.(i-'k+1) by A56,PARTFUN1:def 6;
hence F.y = b1.(i -' k+1) & i -' k+1 in dom b1 by A9,A55;
end;
let i9,k9 be Nat;
assume x=i9 & k9=r.i9;
hence thesis by A44,A46,A48,A53,A51,PARTFUN1:def 6;
end;
end;
consider B be Function of Seg (S+L),the carrier of V1 such that
A57: for x being object st x in Seg (S+L) holds P[x,B.x]
from FUNCT_2:sch 1(A32);
A58: rng B c= the carrier of V1 by RELAT_1:def 19;
A59: dom B=Seg (S+L) by FUNCT_2:def 1;
then reconsider B as FinSequence by FINSEQ_1:def 2;
reconsider B as FinSequence of V1 by A58,FINSEQ_1:def 4;
reconsider RNG=rng B as Subset of V1 by FINSEQ_1:def 4;
now
rng b1 is Basis of IM by MATRLIN:def 2;
then rng b1 is linearly-independent Subset of IM by VECTSP_7:def 3;
then reconsider rngb1=rng b1 as linearly-independent Subset of V1 by
VECTSP_9:11;
set RB={v1 where v1 is Vector of V1: ex i,k st i in Seg(L+S) & k=r.i &
v1=B.i & i-'k <> Sum (LJ| (k-'1)) & i-'k = Sum (LJ|k)};
set RA={v1 where v1 is Vector of V1: ex i,k st i in Seg(L+S) & k=r.i &
v1=B.i & i-'k < Sum (LJ|k)};
A60: RA c= the carrier of V1
proof
let x be object;
assume x in RA;
then ex v1 be Vector of V1 st x=v1 & ex i,k st i in Seg(L+S) & k=r.i
& v1=B.i & i-'k < Sum (LJ|k);
hence thesis;
end;
RB c= the carrier of V1
proof
let x be object;
assume x in RB;
then ex v1 be Vector of V1 st x=v1 & ex i,k st i in Seg(L+S) & k=r.i
& v1=B.i & i-'k <> Sum (LJ| (k-'1)) & i-'k = Sum (LJ|k);
hence thesis;
end;
then reconsider RA,RB as Subset of V1 by A60;
let l be Linear_Combination of RNG such that
A61: Sum l = 0.V1;
A62: F|RA is one-to-one
proof
let x1,x2 be object such that
A63: x1 in dom (F|RA) and
A64: x2 in dom (F|RA) and
A65: (F|RA).x1=(F|RA).x2;
A66: (F|RA).x1=F.x1 & (F|RA).x2=F.x2 by A63,A64,FUNCT_1:47;
A67: dom(F|RA)=dom F /\ RA by RELAT_1:61;
then x1 in RA by A63,XBOOLE_0:def 4;
then consider v1 be Vector of V1 such that
A68: x1=v1 and
A69: ex i1,k1 be Nat st i1 in Seg(L+S) & k1=r.i1 & v1=B.i1 & i1-'
k1 < Sum (LJ|k1);
consider i1,k1 be Nat such that
A70: i1 in Seg(L+S) & k1=r.i1 and
A71: v1=B.i1 and
A72: i1-'k1 < Sum (LJ|k1) by A69;
k1<=i1 by A29,A70;
then
A73: i1-'k1=i1-k1 by XREAL_1:233;
A74: k1 in dom LJ by A29,A70;
then 1<=k1 by FINSEQ_3:25;
then
A75: k1-'1=k1-1 by XREAL_1:233;
then k1-'1+1<=len LJ by A74,FINSEQ_3:25;
then
A76: k1-'1 <=len LJ by NAT_1:13;
A77: b1 is one-to-one by MATRLIN:def 2;
A78: dom LJ=dom J by MATRIXJ1:def 3;
then
A79: k1-'1 in dom LJ implies LJ.(k1-'1)<>0 by A7;
x2 in RA by A64,A67,XBOOLE_0:def 4;
then consider v2 be Vector of V1 such that
A80: x2 = v2 and
A81: ex i2,k2 be Nat st i2 in Seg(L+S) & k2=r.i2 & v2=B.i2 & i2-'
k2 < Sum (LJ|k2);
consider i2,k2 be Nat such that
A82: i2 in Seg(L+S) & k2=r.i2 and
A83: v2=B.i2 and
A84: i2-'k2 < Sum (LJ|k2) by A81;
A85: k2<=i2 by A29,A82;
then
A86: i2-'k2=i2-k2 by XREAL_1:233;
A87: k2 in dom LJ by A29,A82;
then 1<=k2 by FINSEQ_3:25;
then
A88: k2-'1=k2-1 by XREAL_1:233;
then k2-'1+1<=len LJ by A87,FINSEQ_3:25;
then
A89: k2-'1 <=len LJ by NAT_1:13;
A90: k2-'1 in dom LJ implies LJ.(k2-'1)<>0 by A7,A78;
per cases;
suppose
A91: i1-'k1=Sum (LJ| (k1-'1)) & i2-'k2=Sum (LJ| (k2-'1));
then
A92: F.v2=b1.(i2 -' k2+1) & i2 -' k2+1 in dom b1 by A57,A82,A83;
F.v1=b1.(i1 -' k1+1) & i1 -' k1+1 in dom b1 by A57,A70,A71,A91;
then i1-'k1+1=i2-'k2+1 by A65,A66,A68,A80,A77,A92;
then k1-'1=k2-'1 by A76,A89,A79,A90,A91,MATRIXJ1:11;
then i1-k1=i2-k1 by A85,A73,A75,A88,A91,XREAL_1:233;
hence thesis by A68,A71,A80,A83;
end;
suppose
A93: i1-'k1=Sum (LJ| (k1-'1)) & i2-'k2<>Sum (LJ| (k2-'1));
then
A94: min(LJ,i2-'k2)=k2 by A57,A82;
A95: F.v1=b1.(i1-'k1+1) & i1-'k1+1 in dom b1 by A57,A70,A71,A93;
F.v2=b1.(i2-'k2+1) & i2-'k2+1 in dom b1 by A57,A82,A83,A84,A93;
then
A96: i1-'k1+1=i2-'k2+1 by A65,A66,A68,A80,A77,A95;
k1-'1 <>0
proof
assume k1-'1=0;
then LJ| (k1-'1)=<*>REAL;
hence thesis by A29,A82,A93,A96,RVSUM_1:72;
end;
then k1-'1 >=1 by NAT_1:14;
then
A97: k1-'1 in dom LJ by A76,FINSEQ_3:25;
then LJ.(k1-'1)<>0 by A7,A78;
hence thesis by A84,A93,A94,A96,A97,MATRIXJ1:6;
end;
suppose
A98: i1-'k1<>Sum (LJ| (k1-'1)) & i2-'k2=Sum (LJ| (k2-'1));
then
A99: min(LJ,i1-'k1)=k1 by A57,A70;
A100: F.v2=b1.(i2-'k2+1) & i2-'k2+1 in dom b1 by A57,A82,A83,A98;
F.v1=b1.(i1-'k1+1) & i1-'k1+1 in dom b1 by A57,A70,A71,A72,A98;
then
A101: i1-'k1+1=i2-'k2+1 by A65,A66,A68,A80,A77,A100;
k2-'1 <>0
proof
assume k2-'1=0;
then i1-'k1 =0 by A98,A101,RVSUM_1:72;
hence thesis by A29,A70,A98;
end;
then k2-'1 >=1 by NAT_1:14;
then
A102: k2-'1 in dom LJ by A89,FINSEQ_3:25;
then LJ.(k2-'1)<>0 by A7,A78;
hence thesis by A72,A98,A99,A101,A102,MATRIXJ1:6;
end;
suppose
A103: i1-'k1<>Sum (LJ| (k1-'1)) & i2-'k2<>Sum (LJ| (k2-'1));
then
A104: min(LJ,i2-'k2)=k2 by A57,A82;
A105: F.v2=b1.(i2-'k2+1) & i2-'k2+1 in dom b1 by A57,A82,A83,A84,A103;
F.v1=b1.(i1-'k1+1) & i1-'k1+1 in dom b1 by A57,A70,A71,A72,A103;
then i1-'k1+1=i2-'k2+1 by A65,A66,A68,A80,A77,A105;
then i1 - k1 =i2-k1 by A57,A70,A73,A86,A103,A104;
hence thesis by A68,A71,A80,A83;
end;
end;
A106: RB c= rngb1
proof
let x be object;
assume x in RB;
then consider v1 be Vector of V1 such that
A107: x=v1 and
A108: ex i,k st i in Seg(L+S) & k=r.i & v1=B.i & i-'k <> Sum (LJ| (
k-'1)) & i-'k = Sum (LJ|k);
consider i,k such that
A109: i in Seg(L+S) & k=r.i & v1=B.i & i-'k <> Sum (LJ| (k-'1)) and
i-'k = Sum (LJ|k) by A108;
v1= b1.(i -' k) & i-'k in dom b1 by A57,A109;
hence thesis by A107,FUNCT_1:def 3;
end;
A110: Carrier l c= RB\/RA
proof
let x be object such that
A111: x in Carrier l;
reconsider v1=x as Vector of V1 by A111;
Carrier l c= RNG by VECTSP_6:def 4;
then consider i be object such that
A112: i in dom B and
A113: B.i=v1 by A111,FUNCT_1:def 3;
reconsider i as Nat by A112;
r.i=r/.i by A30,A59,A112,PARTFUN1:def 6;
then reconsider k=r.i as Element of NAT;
A114: i-'k <= Sum (LJ|k) by A29,A59,A112;
per cases by A114,XXREAL_0:1;
suppose
A115: i-'k = Sum (LJ|k);
A116: Q[i,k] by A29,A59,A112;
then 1<=k by FINSEQ_3:25;
then k-'1=k-1 by XREAL_1:233;
then k-'1+1=k;
then LJ|k=(LJ| (k-'1))^<*LJ.k*> by A116,FINSEQ_5:10;
then dom LJ=dom J & i-'k = Sum (LJ| (k-'1))+LJ.k by A115,
MATRIXJ1:def 3,RVSUM_1:74;
then i-'k <>Sum (LJ| (k-'1)) by A7,A116;
then v1 in RB or v1 in RA by A59,A112,A113,A115;
hence thesis by XBOOLE_0:def 3;
end;
suppose
i-'k < Sum (LJ|k);
then v1 in RB or v1 in RA by A59,A112,A113;
hence thesis by XBOOLE_0:def 3;
end;
end;
F.:RA c= rngb1
proof
let y be object;
assume y in F.:RA;
then consider x being object such that
x in dom F and
A117: x in RA and
A118: y=F.x by FUNCT_1:def 6;
consider v1 be Vector of V1 such that
A119: x=v1 and
A120: ex i,k st i in Seg(L+S) & k=r.i & v1=B.i&i-'k < Sum (LJ|k) by A117;
consider i,k such that
A121: i in Seg(L+S) & k=r.i & v1=B.i & i-'k < Sum (LJ|k) by A120;
i-'k <> Sum (LJ| (k-'1)) or i-'k = Sum (LJ| (k-'1));
then F.v1= b1.(i -' k+1) & i -' k+1 in dom b1 by A57,A121;
hence thesis by A118,A119,FUNCT_1:def 3;
end;
then
A122: F.:RA is linearly-independent Subset of V1 by VECTSP_7:1;
F.:RB c= {0.V1}
proof
let y be object;
assume y in F.:RB;
then consider x being object such that
x in dom F and
A123: x in RB and
A124: y=F.x by FUNCT_1:def 6;
consider v1 be Vector of V1 such that
A125: x=v1 and
A126: ex i,k st i in Seg(L+S) & k=r.i & v1=B.i & i-'k <> Sum (LJ| (
k-'1)) & i-'k = Sum (LJ|k) by A123;
F.v1= 0.V1 by A57,A126;
hence thesis by A124,A125,TARSKI:def 1;
end;
then Carrier l c= RB by A61,A110,A62,A122,VECTSP11:44;
then Carrier l c= rngb1 by A106;
then l is Linear_Combination of rngb1 by VECTSP_6:def 4;
hence Carrier l ={} by A61,VECTSP_7:def 1;
end;
then
A127: RNG is linearly-independent Subset of V1 by VECTSP_7:def 1;
reconsider BAS,RNG as finite Subset of V1;
consider C be finite Subset of V1 such that
C c= BAS and
A128: card C = card BAS - card RNG and
A129: the ModuleStr of V1= Lin(RNG\/C) by A127,A5,VECTSP_9:19;
A130: (Omega).Lin(BAS) = (Omega).V1 by VECTSP_7:def 3;
then
A131: dim V1 =dim Lin BAS by VECTSP_9:28;
defpred W[Nat] means $1 <= card C implies ex f be FinSequence of V1 st f
is one-to-one & len f = card C & RNG misses rng f & RNG\/rng f is Basis of V1 &
for i st i in dom f & i<= $1 holds F.(f.i)=0.V1;
A132: for n st W[n] holds W[n+1]
proof
let n such that
A133: W[n];
set n1=n+1;
assume
A134: n1<=card C;
then consider f be FinSequence of V1 such that
A135: f is one-to-one and
A136: len f = card C and
A137: RNG misses rng f and
A138: RNG\/rng f is Basis of V1 and
A139: for i st i in dom f & i<= n holds F.(f.i)=0.V1 by A133,NAT_1:13;
per cases;
suppose
F.(f.n1)=0.V1;
then for i st i in dom f & i<=n1 holds F.(f.i)=0.V1 by A139,NAT_1:8;
hence thesis by A135,A136,A137,A138;
end;
suppose
A140: F.(f.n1)<>0.V1;
reconsider Rf=RNG\/rng f as finite Subset of V1 by A138;
reconsider rngB1=rng b1 as Basis of IM by MATRLIN:def 2;
set fn=f/.n1;
1<=n1 by NAT_1:14;
then
A141: n1 in dom f by A134,A136,FINSEQ_3:25;
then
A142: f/.n1=f.n1 by PARTFUN1:def 6;
A143: rng b1 c= F.:RNG
proof
A144: dom F=[#]V1 by FUNCT_2:def 1;
let y be object;
assume y in rng b1;
then consider x being object such that
A145: x in dom b1 and
A146: b1.x=y by FUNCT_1:def 3;
reconsider x as Element of NAT by A145;
A147: len LJ=L & x<=S by A8,A145,CARD_1:def 7,FINSEQ_3:25;
set m=min(LJ,x);
A148: x<= Sum(LJ|m) by A9,A145,MATRIXJ1:def 1;
A149: m in dom LJ by A9,A145,MATRIXJ1:def 1;
then m<=len LJ by FINSEQ_3:25;
then m+x<=L+S by A147,XREAL_1:7;
then
A150: m+x-1<=L+S-1 by XREAL_1:9;
set x1=x-'1;
A151: 1<=x by A145,FINSEQ_3:25;
then
A152: x1=x-1 by XREAL_1:233;
1<=m by A149,FINSEQ_3:25;
then 1+1<=m+x by A151,XREAL_1:7;
then
A153: 2-1<=m+x-1 by XREAL_1:9;
set mx=m+x1;
A154: mx-'m=mx-m by NAT_1:11,XREAL_1:233;
L+S-1<=L+S-0 by XREAL_1:10;
then mx<=L+S by A152,A150,XXREAL_0:2;
then
A155: mx in Seg (S+L) by A152,A153;
then r.mx=r/.mx by A30,PARTFUN1:def 6;
then reconsider k=r.mx as Element of NAT;
A156: B.mx in RNG by A59,A155,FUNCT_1:def 3;
A157: Sum(LJ| (m-'1))< x1+1 by A9,A145,A152,MATRIXJ1:7;
then m<=mx & Sum(LJ| (m-'1))<= mx-'m by A154,NAT_1:11,13;
then
A158: m<=k by A29,A149,A155;
A159: m=k
proof
assume m<>k;
then
A160: m<k by A158,XXREAL_0:1;
then reconsider k1=k-1 as Element of NAT by NAT_1:20;
A161: k=k1+1;
then m<=k1 by A160,NAT_1:13;
then
A162: Sum(LJ|m)<=Sum(LJ|k1) by POLYNOM3:18;
A163: mx-'k<=mx-'m by A158,NAT_D:41;
k-'1=k1 by A161,NAT_D:34;
then Sum(LJ|k1) <=mx-'k by A29,A155;
then Sum(LJ|m) <=mx-'k by A162,XXREAL_0:2;
then Sum(LJ|m)<=x1 by A154,A163,XXREAL_0:2;
hence thesis by A152,A157,A148,NAT_1:13;
end;
A164: mx-'m =Sum(LJ| (m-'1)) or mx-'m <>Sum(LJ| (m-'1));
mx-'m<Sum(LJ|m) by A152,A154,A157,A148,NAT_1:13;
then F.(B.mx)= b1.(mx-'m+1) by A57,A155,A159,A164;
hence thesis by A146,A152,A154,A156,A144,FUNCT_1:def 6;
end;
F.(f/.n1) in im F & F|^1=F by RANKNULL:13,VECTSP11:19;
then F.(f/.n1) in Lin(rngB1) by VECTSP_7:def 3;
then consider L be Linear_Combination of rngB1 such that
A165: F.(f/.n1) = Sum L by VECTSP_7:7;
consider K be Linear_Combination of V1 such that
A166: Carrier L=Carrier K and
A167: Sum L=Sum K by VECTSP_9:8;
Carrier L c= rngB1 by VECTSP_6:def 4;
then consider M be Linear_Combination of RNG such that
A168: F.(Sum M)=Sum K by A143,A166,VECTSP11:41,XBOOLE_1:1;
A169: f.n1 in rng f by A141,FUNCT_1:def 3;
then
A170: fn in Rf by A142,XBOOLE_0:def 3;
A171: not fn in RNG by A137,A142,A169,XBOOLE_0:3;
not fn in RNG by A137,A142,A169,XBOOLE_0:3;
then
A172: RNG c= Rf\{fn} by XBOOLE_1:7,ZFMISC_1:34;
Carrier M c= RNG & Carrier M=Carrier(-M) by VECTSP_6:38,def 4;
then Carrier(-M) c= Rf\{fn} by A172;
then reconsider M9=-M as Linear_Combination of Rf\{fn} by
VECTSP_6:def 4;
set fnM=fn+Sum(M9);
A173: fnM <> fn
proof
assume fnM=fn;
then 0.V1 = fnM-fn by VECTSP_1:16
.= Sum(M9)+(fn-fn) by RLVECT_1:def 3
.= Sum(M9)+0.V1 by RLVECT_1:def 10
.= Sum(M9) by RLVECT_1:def 4
.= -Sum(M) by VECTSP_6:46;
then 0.V1=Sum(M) by VECTSP_1:28;
hence thesis by A140,A142,A165,A167,A168,RANKNULL:9;
end;
take ff=f+*(n1,fnM);
set fnS=n1 .--> fnM;
A174: Rf is linearly-independent by A138,VECTSP_7:def 3;
A175: not fnM in Rf\{fn}
proof
card Rf <>0 by A169;
then reconsider c1=card Rf-1 as Element of NAT by NAT_1:20;
assume fnM in Rf\{fn};
then
A176: Rf\{fn}\/ {fnM} = Rf\{fn} by ZFMISC_1:40;
c1+1=card Rf;
then
A177: card (Rf\{fn})= c1 by A170,STIRL2_1:55;
card (Rf\{fn}\/ {fnM})=c1+1 by A174,A170,VECTSP11:40;
hence thesis by A177,A176;
end;
not fnM in rng f
proof
assume fnM in rng f;
then fnM in Rf by XBOOLE_0:def 3;
hence thesis by A175,A173,ZFMISC_1:56;
end;
then
A178: rng f misses {fnM} by ZFMISC_1:50;
rng fnS={fnM} by FUNCOP_1:8;
then f+*(fnS) is one-to-one by A135,A178,FUNCT_4:92;
hence ff is one-to-one by A141,FUNCT_7:def 3;
A179: dom ff=dom f by FUNCT_7:30;
hence len ff=card C by A136,FINSEQ_3:29;
A180: rng ff = (rng f)\{fn} \/{fnM} by A135,A141,A142,Lm1;
thus RNG misses rng ff
proof
assume RNG meets rng ff;
then consider x being object such that
A181: x in RNG and
A182: x in rng ff by XBOOLE_0:3;
not x in (rng f)\{fn} by A137,A181,XBOOLE_0:3;
then x in {fnM} by A180,A182,XBOOLE_0:def 3;
then
A183: x = fnM by TARSKI:def 1;
not fnM in Rf by A175,A173,ZFMISC_1:56;
hence thesis by A181,A183,XBOOLE_0:def 3;
end;
A184: Rf\{fn}\/{fnM} = (RNG\{fn})\/((rng f)\{fn})\/{fnM} by XBOOLE_1:42
.= RNG\/((rng f)\{fn})\/{fnM} by A171,ZFMISC_1:57
.= RNG\/ rng ff by A180,XBOOLE_1:4;
then reconsider Rff=RNG\/ rng ff as finite Subset of V1;
dim V1 = card Rf by A138,VECTSP_9:def 1
.= card (RNG\/ rng ff) by A174,A170,A184,VECTSP11:40;
then dim Lin(Rff)=dim V1 by A174,A170,A184,VECTSP11:40,VECTSP_9:26;
then
A185: (Omega).V1=(Omega).Lin(Rff) by VECTSP_9:28;
Rf\{fn}\/{fnM} is linearly-independent by A174,A170,VECTSP11:40;
hence RNG\/ rng ff is Basis of V1 by A184,A185,VECTSP_7:def 3;
let i such that
A186: i in dom ff and
A187: i<= n1;
per cases by A187,XXREAL_0:1;
suppose
i<n1;
then ff.i=f.i & i<=n by FUNCT_7:32,NAT_1:13;
hence thesis by A139,A179,A186;
end;
suppose
i=n1;
then ff.i=fnM by A179,A186,FUNCT_7:31;
hence F.(ff.i) = F.(fn - Sum M) by VECTSP_6:46
.= F.fn-F.(Sum M) by RANKNULL:8
.= 0.V1 by A165,A167,A168,RLVECT_1:def 10;
end;
end;
end;
A188: card (RNG\/C) = card RNG + card C - card (RNG/\C) by CARD_2:45
.= card BAS-card (RNG/\C) by A128;
then card (RNG\/C)+card (RNG/\C) =card BAS;
then
A189: card (RNG\/C) <= card BAS by NAT_1:11;
A190: dim Lin BAS=card BAS by A4,VECTSP_9:26;
then
A191: card (RNG\/C) >= card BAS by A130,A129,MATRLIN2:6;
then
A192: card (RNG\/C) = card BAS by A189,XXREAL_0:1;
dim V1= dim Lin(RNG\/C) by A130,A129,VECTSP_9:28;
then
A193: RNG\/C is linearly-independent by A131,A190,A191,A189,MATRLIN2:5
,XXREAL_0:1;
A194: W[0]
proof
assume 0<= card C;
card C=card Seg card C by FINSEQ_1:57;
then Seg card C,C are_equipotent by CARD_1:5;
then consider f be Function such that
A195: f is one-to-one and
A196: dom f = Seg card C and
A197: rng f = C by WELLORD2:def 4;
reconsider f as FinSequence by A196,FINSEQ_1:def 2;
reconsider f as FinSequence of V1 by A197,FINSEQ_1:def 4;
take f;
thus f is one-to-one & len f = card C by A195,A196,FINSEQ_1:def 3;
RNG/\C={} by A188,A192;
hence RNG misses rng f & RNG\/rng f is Basis of V1 by A129,A193,A197,
VECTSP_7:def 3,XBOOLE_0:def 7;
let i;
assume i in dom f & i<=0;
hence thesis by FINSEQ_3:25;
end;
for n holds W[n] from NAT_1:sch 2(A194,A132);
then consider f be FinSequence of V1 such that
A198: f is one-to-one and
A199: len f = card C and
A200: RNG misses rng f and
A201: RNG\/rng f is Basis of V1 and
A202: for i st i in dom f & i<= card C holds F.(f.i)=0.V1;
A203: rng (B^f)=rng B\/rng f by FINSEQ_1:31;
now
let x1,x2 be object such that
A204: x1 in dom B and
A205: x2 in dom B and
A206: B.x1 = B.x2;
reconsider i1=x1,i2=x2 as Nat by A204,A205;
r/.i1=r.i1 & r/.i2=r.i2 by A30,A59,A204,A205,PARTFUN1:def 6;
then reconsider k1=r.i1,k2=r.i2 as Element of NAT;
A207: i1 -' k1 = Sum (LJ| (k1-'1)) implies F.(B.x1) = b1.(i1 -' k1+1)& i1
-'k1+1 in dom b1 by A57,A59,A204;
A208: Q[i1,k1] by A29,A59,A204;
then
A209: i1-'k1 =i1-k1 by XREAL_1:233;
A210: Q[i2,k2] by A29,A59,A205;
then
A211: i2-'k2=i2-k2 by XREAL_1:233;
A212: k2-'1<=k2 by NAT_D:35;
A213: i1 -' k1 <> Sum (LJ| (k1-'1)) implies B.x1 = b1.(i1 -' k1) & i1-'k1
in dom b1 & min(LJ,i1-'k1)=k1 & (i1-'k1 < Sum (LJ|k1) implies F.(B.x1) = b1.(i1
-' k1+1) & i1 -' k1+1 in dom b1) & (i1-'k1 = Sum (LJ|k1) implies F.(B.x1) = 0.
V1) by A57,A59,A204;
k2 <= len LJ by A210,FINSEQ_3:25;
then
A214: k2-'1 <=len LJ by A212,XXREAL_0:2;
1<=k1 by A208,FINSEQ_3:25;
then
A215: k1-'1=k1-1 by XREAL_1:233;
A216: i2 -' k2 <> Sum (LJ| (k2-'1)) implies B.x2 = b1.(i2 -' k2) & i2-'k2
in dom b1 & min(LJ,i2-'k2)=k2 & (i2-'k2 < Sum (LJ|k2) implies F.(B.x2) = b1.(i2
-' k2+1) & i2 -' k2+1 in dom b1) & (i2-'k2 = Sum (LJ|k2) implies F.(B.x2) = 0.
V1) by A57,A59,A205;
1<=k2 by A210,FINSEQ_3:25;
then
A217: k2-'1=k2-1 by XREAL_1:233;
A218: i2 -' k2 = Sum (LJ| (k2-'1)) implies F.(B.x2) = b1.(i2 -' k2+1) &
i2-'k2+1 in dom b1 by A57,A59,A205;
A219: k1-'1 <= k1 by NAT_D:35;
k1<= len LJ by A208,FINSEQ_3:25;
then
A220: k1-'1 <=len LJ by A219,XXREAL_0:2;
A221: dom LJ=dom J by MATRIXJ1:def 3;
rng b1 is Basis of IM by MATRLIN:def 2;
then
A222: rng b1 is linearly-independent Subset of IM by VECTSP_7:def 3;
A223: b1 is one-to-one by MATRLIN:def 2;
A224: i1-'k1 <= Sum (LJ|k1) & i2-'k2 <= Sum (LJ|k2) by A29,A59,A204,A205;
now
per cases by A224,XXREAL_0:1;
suppose
A225: i1 -' k1 = Sum (LJ| (k1-'1)) & i2 -' k2 = Sum (LJ| (k2-'1));
then
A226: F.(B.x2) = b1.(i2 -' k2+1) & i2-'k2+1 in dom b1 by A57,A59,A205;
F.(B.x1) = b1.(i1 -' k1+1) & i1-'k1+1 in dom b1 by A57,A59,A204,A225;
then
A227: i1-'k1+1 = i2-'k2+1 by A206,A223,A226;
A228: k2-'1 in dom LJ implies LJ.(k2-'1)<>0 by A7,A221;
k1-'1 in dom LJ implies LJ.(k1-'1)<>0 by A7,A221;
then k1-'1 = k2-'1 by A220,A214,A225,A227,A228,MATRIXJ1:11;
hence i1=i2 by A215,A217,A209,A211,A227;
end;
suppose
A229: i1 -' k1 = Sum (LJ| (k1-'1)) & i2 -' k2 <> Sum (LJ| (k2-'1))
& i2-'k2 < Sum (LJ|k2);
then
A230: min(LJ,i2-'k2)=k2 by A57,A59,A205;
A231: F.(B.x2) = b1.(i2-'k2+1) & i2-'k2+1 in dom b1 by A57,A59,A205,A229;
F.(B.x1) = b1.(i1-'k1+1) & i1-'k1+1 in dom b1 by A57,A59,A204,A229;
then
A232: i1-'k1+1 = i2-'k2+1 by A206,A223,A231;
k1-'1 <>0
proof
assume k1-'1=0;
then LJ| (k1-'1)=<*>REAL;
hence thesis by A29,A59,A205,A229,A232,RVSUM_1:72;
end;
then k1-'1 >=1 by NAT_1:14;
then
A233: k1-'1 in dom LJ by A220,FINSEQ_3:25;
then LJ.(k1-'1)<>0 by A7,A221;
hence i1=i2 by A229,A230,A232,A233,MATRIXJ1:6;
end;
suppose
i1 -' k1 = Sum (LJ| (k1-'1)) & i2 -' k2 <> Sum (LJ| (k2-'1))
& i2-'k2 = Sum (LJ|k2);
then b1.(i1 -' k1+1) =0.IM & b1.(i1 -' k1+1) in rng b1 by A206,A207
,A216,FUNCT_1:def 3,VECTSP_4:11;
hence i1 = i2 by A222,VECTSP_7:2;
end;
suppose
A234: i2 -' k2 = Sum (LJ| (k2-'1)) & i1 -' k1 <> Sum (LJ| (k1-'1))
& i1-'k1 < Sum (LJ|k1);
then
A235: min(LJ,i1-'k1)=k1 by A57,A59,A204;
A236: F.(B.x1) = b1.(i1 -' k1+1) & i1-'k1+1 in dom b1 by A57,A59,A204,A234;
F.(B.x2) = b1.(i2 -' k2+1) & i2-'k2+1 in dom b1 by A57,A59,A205,A234;
then
A237: i2-'k2+1 = i1-'k1+1 by A206,A223,A236;
k2-'1 <>0
proof
assume k2-'1=0;
then i1-'k1 =0 by A234,A237,RVSUM_1:72;
hence thesis by A29,A59,A204,A234;
end;
then k2-'1 >=1 by NAT_1:14;
then
A238: k2-'1 in dom LJ by A214,FINSEQ_3:25;
then LJ.(k2-'1)<>0 by A7,A221;
hence i1=i2 by A234,A235,A237,A238,MATRIXJ1:6;
end;
suppose
i2 -' k2 = Sum (LJ| (k2-'1)) & i1 -' k1 <> Sum (LJ| (k1-'1))
& i1-'k1 = Sum (LJ|k1);
then b1.(i2 -' k2+1) =0.IM & b1.(i2 -' k2+1) in rng b1 by A206,A213
,A218,FUNCT_1:def 3,VECTSP_4:11;
hence i1= i2 by A222,VECTSP_7:2;
end;
suppose
A239: i1 -' k1 <> Sum (LJ| (k1-'1)) & i2 -' k2 <> Sum (LJ| (k2-'1) );
then i2-'k2 = i1-'k1 by A206,A213,A216,A223;
then i2-k1=i1-k1 by A57,A59,A205,A213,A209,A211,A239;
hence i1=i2;
end;
end;
hence x1=x2;
end;
then B is one-to-one;
then B^f is one-to-one by A198,A200,FINSEQ_3:91;
then reconsider Bf=B^f as OrdBasis of V1 by A201,A203,MATRLIN:def 2;
for i st i in dom Bf holds F.(Bf/.i) = 0.K * (Bf/.i) or i+1 in dom
Bf & F.(Bf/.i) = 0.K * (Bf/.i) +Bf/.(i+1)
proof
let i such that
A240: i in dom Bf;
A241: Bf/.i=Bf.i by A240,PARTFUN1:def 6;
per cases by A240,FINSEQ_1:25;
suppose
A242: i in dom B;
then r/.i=r.i by A30,A59,PARTFUN1:def 6;
then reconsider k=r.i as Element of NAT;
A243: i-'k <= Sum (LJ|k) by A29,A59,A242;
A244: Q[i,k] by A29,A59,A242;
then 1<=k by FINSEQ_3:25;
then k-'1=k-1 by XREAL_1:233;
then k-'1+1=k;
then LJ|k=(LJ| (k-'1))^<*LJ.k*> by A244,FINSEQ_5:10;
then
A245: dom LJ=dom J & Sum(LJ|k) = Sum (LJ| (k-'1))+LJ.k by MATRIXJ1:def 3
,RVSUM_1:74;
per cases by A243,XXREAL_0:1;
suppose
A246: i -' k = Sum (LJ|k);
then
A247: i-'k <>Sum (LJ| (k-'1)) by A7,A244,A245;
F.(Bf/.i) = F.(B.i) by A241,A242,FINSEQ_1:def 7
.= 0.V1 by A57,A59,A242,A246,A247
.= 0.K*(Bf/.i) by VECTSP_1:14;
hence thesis;
end;
suppose
A248: i -' k < Sum (LJ|k);
A249: i -' k = Sum (LJ| (k-'1)) or i -' k <> Sum (LJ| (k-'1));
then
A250: F.(B.i)=b1.(i -' k+1) by A57,A59,A242,A248;
dom J=dom LJ by MATRIXJ1:def 3;
then
A251: k <= L by A244,FINSEQ_3:25;
A252: i-'k+1<=Sum(LJ|k) by A248,NAT_1:13;
A253: i-'k=i-k by A244,XREAL_1:233;
A254: i-'k+1 in dom b1 by A57,A59,A242,A248,A249;
then
A255: 1<=i-'k+1 by FINSEQ_3:25;
then
A256: 1+0<= i-k+1+k by A253,XREAL_1:7;
i-'k+1<=S by A8,A254,FINSEQ_3:25;
then i-k+1+k<=S+L by A251,A253,XREAL_1:7;
then
A257: i+1 in Seg(S+L) by A256;
then r/.(i+1)=r.(i+1) by A30,PARTFUN1:def 6;
then reconsider k1=r.(i+1) as Element of NAT;
set i1=i+1;
A258: dom B c= dom Bf by FINSEQ_1:26;
1+k<=i-k+1+k by A255,A253,XREAL_1:7;
then
A259: k<=i+1 by NAT_1:13;
then
A260: i1-'k=i1-k by XREAL_1:233;
Sum (LJ| (k-'1))<=i-'k+1 by A244,NAT_1:12;
then
A261: k<=k1 by A29,A244,A253,A257,A259,A260;
A262: Q[i1,k1] by A29,A257;
A263: k=k1
proof
assume
A264: k<>k1;
then
A265: k<k1 by A261,XXREAL_0:1;
then reconsider K1=k1-1 as Element of NAT by NAT_1:20;
A266: i1-'k1 <= i1-'k by A261,NAT_D:41;
i1-k1=i1-'k1 by A262,XREAL_1:233;
then i1-'k1 <> i1-'k by A260,A264;
then
A267: i1-'k1 < i1-'k by A266,XXREAL_0:1;
A268: k1=K1+1;
then k<=K1 by A265,NAT_1:13;
then
A269: Sum(LJ|k)<=Sum(LJ|K1) by POLYNOM3:18;
k1-'1=K1 by A268,NAT_D:34;
then Sum(LJ|K1) <= i1-'k1 by A29,A257;
then Sum(LJ|k)<= i1-'k1 by A269,XXREAL_0:2;
hence thesis by A252,A253,A260,A267,XXREAL_0:2;
end;
Sum(LJ| (k-'1))<i-'k+1 by A244,NAT_1:13;
then B.i1 = b1.(i -' k+1) by A57,A253,A257,A260,A263;
then Bf.i1=b1.(i -' k+1) by A59,A257,FINSEQ_1:def 7;
then Bf/.i1=b1.(i -' k+1) by A59,A257,A258,PARTFUN1:def 6;
then F.(Bf/.i) = Bf/.i1 by A241,A242,A250,FINSEQ_1:def 7
.= 0.V1+Bf/.i1 by RLVECT_1:def 4
.= 0.K*(Bf/.i)+Bf/.i1 by VECTSP_1:14;
hence thesis by A59,A257,A258;
end;
end;
suppose
ex j st j in dom f & i=len B + j;
then consider j such that
A270: j in dom f and
A271: i=len B + j;
A272: j<=len f by A270,FINSEQ_3:25;
F.(Bf/.i) = F.(f.j) by A241,A270,A271,FINSEQ_1:def 7
.= 0.V1 by A199,A202,A270,A272
.= 0.K*(Bf/.i) by VECTSP_1:14;
hence thesis;
end;
end;
then consider
J be non-empty FinSequence_of_Jordan_block of 0.K,K such that
A273: AutMt(F,Bf,Bf) = block_diagonal(J,0.K)by Th28;
now
A274: dom (Len J)=dom J by MATRIXJ1:def 3;
let i such that
A275: i in dom J;
J.i<>{} by A275,FUNCT_1:def 9;
hence (Len J).i <> 0 by A275,A274,MATRIXJ1:def 3;
end;
hence thesis by A273;
end;
A276: P[0]
proof
reconsider J={} as FinSequence_of_Jordan_block of 0.K,K by Th10;
let V1 be finite-dimensional VectSp of K;
set b1 = the OrdBasis of V1;
let F be nilpotent linear-transformation of V1,V1;
assume deg F=0;
then [#]V1 = {0.V1} by Th15
.= the carrier of (0).V1 by VECTSP_4:def 3;
then (0).V1 = (Omega).V1 by VECTSP_4:29;
then
A277: 0 = dim V1 by VECTSP_9:29
.= len b1 by MATRLIN2:21
.= len AutMt(F,b1,b1) by MATRIX_0:def 2;
take J,b1;
thus AutMt(F,b1,b1) = {} by A277
.= block_diagonal(J,0.K) by MATRIXJ1:22;
thus thesis;
end;
for n holds P[n] from NAT_1:sch 2(A276,A1);
then P[deg F];
then consider
J be FinSequence_of_Jordan_block of 0.K,K, b1 be OrdBasis of V1
such that
A278: AutMt(F,b1,b1) = block_diagonal(J,0.K) and
A279: for i st i in dom J holds (Len J).i <> 0;
now
let x be object such that
A280: x in dom J;
reconsider i=x as Element of NAT by A280;
dom J=dom (Len J) & (Len J).i <> 0 by A279,A280,MATRIXJ1:def 3;
then J.i is non empty by A280,MATRIXJ1:def 3;
hence J.x is non empty;
end;
then J is non-empty;
hence thesis by A278;
end;
theorem Th30:
for V be VectSp of K for F be linear-transformation of V,V, V1
be finite-dimensional Subspace of V, F1 be linear-transformation of V1,V1 st V1
= ker ((F+(-L)*id V) |^n) & F|V1=F1 ex J be non-empty
FinSequence_of_Jordan_block of L,K, b1 be OrdBasis of V1 st AutMt(F1,b1,b1) =
block_diagonal(J,0.K)
proof
let V be VectSp of K;
let F be linear-transformation of V,V;
let V1 be finite-dimensional Subspace of V;
let F1 be linear-transformation of V1,V1 such that
A1: V1 = ker ((F+(-L)*id V) |^n) and
A2: F|V1=F1;
set FL=F+(-L)*id V;
reconsider FLV=FL|V1 as nilpotent linear-transformation of V1,V1 by A1,Th14;
A3: now
let x be object;
assume x in dom FLV;
then reconsider v1=x as Vector of V1 by FUNCT_2:def 1;
reconsider v=v1 as Vector of V by VECTSP_4:10;
(id V).v=v by FUNCT_1:18;
then
A4: (-L)*((id V).v)=(-L)*((id V1).v1) by FUNCT_1:18,VECTSP_4:14;
A5: F.v1=F1.v1 by A2,FUNCT_1:49;
thus FLV.x = (F+(-L)*id V).v by FUNCT_1:49
.= F.v + ((-L)*id V).v by MATRLIN:def 3
.= F.v+(-L)*((id V).v) by MATRLIN:def 4
.= F1.v1+(-L)*((id V1).v1) by A4,A5,VECTSP_4:13
.= F1.v1+((-L)*id V1).v1 by MATRLIN:def 4
.= (F1+(-L)*id V1).x by MATRLIN:def 3;
end;
dom FLV = the carrier of V1 by FUNCT_2:def 1
.= dom (F1+(-L)*(id V1)) by FUNCT_2:def 1;
then
A6: FLV=F1+(-L)*(id V1) by A3;
consider J be non-empty FinSequence_of_Jordan_block of 0.K,K, b1 be OrdBasis
of V1 such that
A7: AutMt(FLV,b1,b1) = block_diagonal(J,0.K) by Th29;
L+0.K=L by RLVECT_1:def 4;
then reconsider JM=J (+) mlt(len J|->L,1.(K,Len J)) as
FinSequence_of_Jordan_block of L,K by Th12;
now
let x be object such that
A8: x in dom JM;
reconsider i=x as Nat by A8;
A9: JM.i = J.i + mlt(len J|->L,1.(K,Len J)).i by A8,MATRIXJ1:def 10;
dom JM=dom J by MATRIXJ1:def 10;
then J.i <> {} by A8,FUNCT_1:def 9;
hence JM.x is non empty by A9,MATRIX_1:def 6;
end;
then reconsider JM as non-empty FinSequence_of_Jordan_block of L,K by
FUNCT_1:def 9;
take JM,b1;
set Aid=AutMt(id V1,b1,b1);
set AF1=AutMt(F1,b1,b1);
A10: now
A11: Indices Aid=Indices AF1 by MATRIX_0:26;
let i,j such that
A12: [i,j] in Indices AF1;
Indices (AF1+(-L)*Aid)= Indices AF1 by MATRIX_0:26;
hence (AF1+(-L)*Aid+L*Aid)*(i,j) = (AF1+(-L)*Aid)*(i,j)+(L*Aid)*(i,j) by
A12,MATRIX_1:def 6
.=(AF1*(i,j)+((-L)*Aid)*(i,j))+(L*Aid)*(i,j) by A12,MATRIX_1:def 6
.= AF1*(i,j)+(((-L)*Aid)*(i,j) +(L*Aid)*(i,j)) by RLVECT_1:def 3
.= AF1*(i,j)+((-L)*(Aid*(i,j)) +(L*Aid)*(i,j)) by A12,A11,MATRIX_3:def 5
.= AF1*(i,j)+((-L)*(Aid*(i,j)) +L*(Aid*(i,j))) by A12,A11,MATRIX_3:def 5
.= AF1*(i,j)+(-L+L)*(Aid*(i,j)) by VECTSP_1:def 3
.= AF1*(i,j)+0.K*(Aid*(i,j)) by VECTSP_1:16
.= AF1*(i,j)+0.K
.= AF1*(i,j) by RLVECT_1:def 4;
end;
A13: Len mlt(len J|->L,1.(K,Len J)) = Len 1.(K,Len J) by MATRIXJ1:62
.= Len J by MATRIXJ1:56;
dom Len J=dom 1.(K,Len J) by MATRIXJ1:def 8;
then
A14: len 1.(K,Len J) = len (Len J) by FINSEQ_3:29
.= len J by CARD_1:def 7;
A15: Sum Len J = len AutMt(FLV,b1,b1) by A7,MATRIXJ1:def 5
.= len b1 by MATRIX_0:def 2;
A16: Width mlt(len J|->L,1.(K,Len J)) = Width 1.(K,Len J) by MATRIXJ1:62
.= Len J by MATRIXJ1:56
.= Width J by MATRIXJ1:46;
Mx2Tran(AutMt((-L)*(id V1),b1,b1),b1,b1) = (-L)*(id V1) by MATRLIN2:34
.= (-L)*Mx2Tran(Aid,b1,b1) by MATRLIN2:34
.= Mx2Tran((-L)*Aid,b1,b1) by MATRLIN2:38;
then AutMt((-L)*(id V1),b1,b1) = (-L)*Aid by MATRLIN2:39;
then AutMt(FLV,b1,b1)+L*Aid = AF1+(-L)*Aid+L*Aid by A6,MATRLIN:42
.= AF1 by A10,MATRIX_0:27;
hence AF1 = block_diagonal(J,0.K)+L*1.(K,Sum Len J) by A7,A15,MATRLIN2:28
.= block_diagonal(J,0.K)+L*block_diagonal(1.(K,Len J),0.K) by MATRIXJ1:61
.= block_diagonal(J,0.K)+ block_diagonal(mlt(len J|->L,1.(K,Len J)),L*0.
K) by A14,MATRIXJ1:65
.= block_diagonal(J,0.K)+block_diagonal(mlt(len J|->L,1.(K,Len J)),0.K)
.= block_diagonal(JM,0.K+0.K) by A13,A16,MATRIXJ1:72
.= block_diagonal(JM,0.K) by RLVECT_1:def 4;
end;
begin :: The Main Theorem
theorem Th31:
for K be algebraic-closed Field for V be non trivial
finite-dimensional VectSp of K, F be linear-transformation of V,V ex J be
non-empty (FinSequence_of_Jordan_block of K), b1 be OrdBasis of V st AutMt(F,b1
,b1) = block_diagonal(J,0.K) & for L be Scalar of K holds L is eigenvalue of F
iff ex i st i in dom J & J.i = Jordan_block(L,len (J.i))
proof
let K be algebraic-closed Field;
defpred P[Nat] means for V be non trivial finite-dimensional VectSp of K st
dim V <= $1 for F be linear-transformation of V,V ex J be non-empty (
FinSequence_of_Jordan_block of K), b1 be OrdBasis of V st AutMt(F,b1,b1) =
block_diagonal(J,0.K) & for L be Scalar of K holds L is eigenvalue of F iff ex
i st i in dom J & J.i = Jordan_block(L,len (J.i));
let V be non trivial finite-dimensional VectSp of K, F be
linear-transformation of V,V;
A1: for n st P[n] holds P[n+1]
proof
let n such that
A2: P[n];
set n1=n+1;
let V be non trivial finite-dimensional VectSp of K such that
A3: dim V <= n1;
per cases by A3,NAT_1:8;
suppose
dim V<=n;
hence thesis by A2;
end;
suppose
A4: dim V=n1;
let F be linear-transformation of V,V;
A5: F is with_eigenvalues by VECTSP11:16;
then consider v be Vector of V, L be Scalar of K such that
A6: v <> 0.V & F.v = L*v by VECTSP11:def 1;
set FL=F+(-L)*id V;
L is eigenvalue of F by A5,A6,VECTSP11:def 2;
then ker FL is non trivial by A5,VECTSP11:14;
then
A7: dim ker FL<>0 by MATRLIN2:42;
consider m such that
A8: UnionKers FL = ker (FL|^m) by VECTSP11:27;
set IM = im (FL|^m);
set KER = ker (FL|^m);
A9: dim V=dim KER + dim IM by A8,VECTSP11:35,VECTSP_9:34;
A10: IM is Linear_Compl of KER by A8,VECTSP11:35,VECTSP_5:37;
reconsider FK=F|KER as linear-transformation of KER,KER by VECTSP11:29;
consider Jk be non-empty FinSequence_of_Jordan_block of L,K, Bker be
OrdBasis of KER such that
A11: AutMt(FK,Bker,Bker) = block_diagonal(Jk,0.K) by Th30;
FL|^1=FL by VECTSP11:19;
then
A12: ker FL is Subspace of KER by A8,VECTSP11:25;
A13: len Jk<>0
proof
assume len Jk=0;
then Len Jk = <*>NAT .= <*>REAL;
then 0 = len block_diagonal(Jk,0.K) by MATRIXJ1:def 5,RVSUM_1:72
.= len Bker by A11,MATRIX_0:def 2
.= dim KER by MATRLIN2:21;
hence thesis by A12,A7,VECTSP_9:25;
end;
reconsider FI=F|IM as linear-transformation of IM,IM by VECTSP11:33;
A14: KER/\IM=(0).V by A8,VECTSP11:34;
A15: V is_the_direct_sum_of KER,IM by A8,VECTSP11:35;
then
A16: KER+IM = (Omega).V by VECTSP_5:def 4;
per cases;
suppose
A17: IM is trivial;
set Bim = the OrdBasis of IM;
0 = dim IM by A17,MATRLIN2:42
.= len Bim by MATRLIN2:21
.= len AutMt(FI,Bim,Bim) by MATRIX_0:def 2;
then
A18: AutMt(FI,Bim,Bim)={};
Bker^Bim is OrdBasis of KER+IM by A14,MATRLIN2:26;
then reconsider BB=Bker^Bim as OrdBasis of V by A16,MATRLIN2:4;
take Jk,BB;
A19: dim IM=0 implies dim IM=0;
dim KER=0 implies dim KER=0;
hence AutMt(F,BB,BB) = block_diagonal(<*AutMt(FK,Bker,Bker), AutMt(FI,
Bim,Bim)*>,0.K) by A15,A19,MATRLIN2:27
.= block_diagonal(<*AutMt(FK,Bker,Bker)*>,0.K) by A18,MATRIXJ1:40
.= block_diagonal(Jk,0.K) by A11,MATRIXJ1:34;
let L1 be Scalar of K;
thus L1 is eigenvalue of F implies ex i st i in dom Jk & Jk.i =
Jordan_block(L1,len (Jk.i))
proof
assume
A20: L1 is eigenvalue of F;
A21: L1 = L
proof
assume L<>L1;
then
FI is with_eigenvalues & L1 is eigenvalue of FI by A5,A8,A10,A20,
VECTSP11:39;
then ex v1 be Vector of IM st v1<>0.IM & FI.v1 = L1*v1 by
VECTSP11:def 2;
hence thesis by A17;
end;
take i=len Jk;
i in Seg len Jk by A13,FINSEQ_1:3;
hence i in dom Jk by FINSEQ_1:def 3;
then ex k st Jk.i=Jordan_block(L,k) by Def3;
hence thesis by A21,Def1;
end;
given i such that
A22: i in dom Jk and
A23: Jk.i = Jordan_block(L1,len (Jk.i));
Jk.i <> {} by A22,FUNCT_1:def 9;
then len (Jk.i) in Seg len (Jk.i) by FINSEQ_1:3;
then [len (Jk.i),len (Jk.i)] in [:Seg len (Jk.i),Seg len (Jk.i):] by
ZFMISC_1:87;
then
A24: [len (Jk.i),len (Jk.i)] in Indices (Jk.i) by MATRIX_0:24;
ex k st Jk.i=Jordan_block(L,k) by A22,Def3;
then L = (Jk.i)*(len (Jk.i),len (Jk.i)) by A24,Def1
.= L1 by A23,A24,Def1;
hence thesis by A5,A6,VECTSP11:def 2;
end;
suppose
A25: IM is non trivial;
n1 <> dim IM & dim IM <= n1 by A4,A12,A7,A9,VECTSP_9:25;
then dim IM <n1 by XXREAL_0:1;
then dim IM <=n by NAT_1:13;
then consider
Ji be non-empty (FinSequence_of_Jordan_block of K), Bim be
OrdBasis of IM such that
A26: AutMt(FI,Bim,Bim) = block_diagonal(Ji,0.K) and
A27: for L be Scalar of K holds L is eigenvalue of FI iff ex i st
i in dom Ji & Ji.i = Jordan_block(L,len (Ji.i)) by A2,A25;
Bker^Bim is OrdBasis of KER+IM by A14,MATRLIN2:26;
then reconsider BB=Bker^Bim as OrdBasis of V by A16,MATRLIN2:4;
set JJ=Jk^Ji;
A28: now
let x be object such that
A29: x in dom JJ;
reconsider i=x as Nat by A29;
now
per cases by A29,FINSEQ_1:25;
suppose
A30: i in dom Jk;
then JJ.i=Jk.i by FINSEQ_1:def 7;
hence JJ.i is non empty by A30,FUNCT_1:def 9;
end;
suppose
ex j st j in dom Ji & i = len Jk +j;
then consider j such that
A31: j in dom Ji and
A32: i=len Jk+j;
JJ.i=Ji.j by A31,A32,FINSEQ_1:def 7;
hence JJ.i is non empty by A31,FUNCT_1:def 9;
end;
end;
hence JJ.x is non empty;
end;
A33: FI is with_eigenvalues by A25,VECTSP11:16;
A34: dim IM=0 implies dim IM=0;
reconsider JJ as non-empty FinSequence_of_Jordan_block of K by A28,
FUNCT_1:def 9;
take JJ,BB;
dim KER=0 implies dim KER=0;
hence AutMt(F,BB,BB) = block_diagonal(<*block_diagonal(Jk,0.K),
block_diagonal(Ji,0.K)*>,0.K) by A11,A15,A26,A34,MATRLIN2:27
.= block_diagonal(<*block_diagonal(Jk,0.K)*>^Ji,0.K) by MATRIXJ1:36
.= block_diagonal(JJ,0.K) by MATRIXJ1:35;
let L1 be Scalar of K;
thus L1 is eigenvalue of F implies ex i st i in dom JJ & JJ.i =
Jordan_block(L1,len (JJ.i))
proof
assume
A35: L1 is eigenvalue of F;
per cases;
suppose
A36: L = L1;
take i=len Jk;
A37: dom Jk c= dom JJ by FINSEQ_1:26;
i in Seg len Jk by A13,FINSEQ_1:3;
then
A38: i in dom Jk by FINSEQ_1:def 3;
then (ex k st Jk.i = Jordan_block(L,k) )& JJ.i=Jk.i by Def3,
FINSEQ_1:def 7;
hence thesis by A36,A38,A37,Def1;
end;
suppose
L<>L1;
then L1 is eigenvalue of FI by A5,A8,A10,A35,VECTSP11:39;
then consider i such that
A39: i in dom Ji and
A40: Ji.i = Jordan_block(L1,len (Ji.i)) by A27;
take ii=len Jk+i;
JJ.ii=Ji.i by A39,FINSEQ_1:def 7;
hence thesis by A39,A40,FINSEQ_1:28;
end;
end;
given i such that
A41: i in dom JJ and
A42: JJ.i = Jordan_block(L1,len (JJ.i));
per cases by A41,FINSEQ_1:25;
suppose
A43: i in dom Jk;
then Jk.i <> {} by FUNCT_1:def 9;
then len (Jk.i) in Seg len (Jk.i) by FINSEQ_1:3;
then
[len (Jk.i),len (Jk.i)] in [:Seg len (Jk.i),Seg len (Jk.i):] by
ZFMISC_1:87;
then
A44: [len (Jk.i),len (Jk.i)] in Indices (Jk.i) by MATRIX_0:24;
A45: JJ.i = Jk.i by A43,FINSEQ_1:def 7;
ex k st Jk.i = Jordan_block(L,k) by A43,Def3;
then L = (Jk.i)*(len (Jk.i),len (Jk.i)) by A44,Def1
.= L1 by A42,A45,A44,Def1;
hence thesis by A5,A6,VECTSP11:def 2;
end;
suppose
ex j st j in dom Ji & i = len Jk +j;
then consider j such that
A46: j in dom Ji and
A47: i=len Jk+j;
JJ.i=Ji.j by A46,A47,FINSEQ_1:def 7;
then L1 is eigenvalue of FI by A27,A42,A46;
then consider w be Vector of IM such that
A48: w<>0.IM and
A49: FI.w = L1*w by A33,VECTSP11:def 2;
A50: 0.IM = 0.V by VECTSP_4:11;
reconsider W=w as Vector of V by VECTSP_4:10;
L1*W = FI.w by A49,VECTSP_4:14
.= F.W by FUNCT_1:49;
hence thesis by A5,A48,A50,VECTSP11:def 2;
end;
end;
end;
end;
A51: P[0]
proof
let V be non trivial finite-dimensional VectSp of K;
assume dim V <= 0;
then dim V=0;
hence thesis by MATRLIN2:42;
end;
for n holds P[n] from NAT_1:sch 2(A51,A1);
then P[dim V];
hence thesis;
end;
::$N Jordan Matrix Decomposition Theorem
::$L https://en.wikipedia.org/wiki/Jordan_matrix Jordan Matrix Decomposition Theorem
theorem
for K be algebraic-closed Field, M be Matrix of n,K ex J be non-empty
(FinSequence_of_Jordan_block of K), P be Matrix of n,K st Sum Len J = n & P is
invertible & M = P * block_diagonal(J,0.K) * (P~)
proof
let K be algebraic-closed Field, M be Matrix of n,K;
per cases;
suppose
A1: n=0;
then reconsider P={} as Matrix of n,K by MATRIX_0:13;
reconsider J ={} as FinSequence_of_Jordan_block of K by Lm2;
reconsider J as non-empty FinSequence_of_Jordan_block of K;
take J,P;
A2: Len J = <*>NAT
.= <*>REAL;
thus Sum Len J=n by A1,RVSUM_1:72;
A3: 1_K <>0.K;
Det P=1_K by A1,MATRIXR2:41;
then Det P is unital;
hence P is invertible by LAPLACE:34;
reconsider B=block_diagonal(J,0.K) as Matrix of n,K by A1,A2,RVSUM_1:72;
M = P * B * (P~) by A1,MATRIX_0:45;
hence thesis;
end;
suppose
A4: n>0;
set V=n-VectSp_over K;
set B = the OrdBasis of V;
A5: len B = dim V by MATRLIN2:21
.= n by MATRIX13:112;
then reconsider M9=M as Matrix of len B,K;
set T=Mx2Tran(M9,B,B);
dim V=n by MATRIX13:112;
then V is non trivial by A4,MATRLIN2:42;
then consider
J be non-empty (FinSequence_of_Jordan_block of K), b1 be OrdBasis
of V such that
A6: AutMt(T,b1,b1) = block_diagonal(J,0.K) and
for L be Scalar of K holds L is eigenvalue of T iff ex i st i in dom J
& J.i = Jordan_block(L,len (J.i)) by Th31;
A7: dom T=[#]V by FUNCT_2:def 1;
reconsider P=AutEqMt(id V,B,b1) as Matrix of n,K by A5;
take J,P;
A8: width P=n & len (P~)=n by A4,MATRIX_0:23;
A9: rng T c= [#]V by RELAT_1:def 19;
A10: len b1 = dim V by MATRLIN2:21
.= n by MATRIX13:112;
then
A11: len AutMt(T,b1,b1) = n & width AutMt(T,b1,b1)=n by A4,MATRIX_0:23;
thus Sum Len J=len AutMt(T,b1,b1) by A6,MATRIXJ1:def 5
.=n by A10,MATRIX_0:def 2;
thus P is invertible by A5,MATRLIN2:29;
thus M = AutMt(T,B,B) by MATRLIN2:36
.= AutMt(T*id V,B,B) by A7,RELAT_1:52
.= AutMt(id V,B,b1)* AutMt(T,b1,B) by A4,A5,A10,MATRLIN:41
.= P* AutMt(T,b1,B) by A5,A10,MATRLIN2:def 2
.= P* AutMt((id V)*T,b1,B) by A9,RELAT_1:53
.= P* (AutMt(T,b1,b1)*AutMt(id V,b1,B)) by A4,A10,MATRLIN:41
.= P*(AutMt(T,b1,b1) *AutEqMt(id V,b1,B)) by A5,A10,MATRLIN2:def 2
.= P*(AutMt(T,b1,b1)*(P~)) by A5,MATRLIN2:29
.= P*block_diagonal(J,0.K) *(P~) by A6,A8,A11,MATRIX_3:33;
end;
end;