:: Jordan Matrix Decomposition :: by Karol P\c{a}k :: :: Received July 11, 2008 :: Copyright (c) 2008 Association of Mizar Users environ vocabularies BOOLE, ARYTM, FINSEQ_1, FINSEQ_2, FINSEQ_4, TREES_1, RELAT_1, FUNCT_1, INCSP_1, CAT_3, RVSUM_1, RLSUB_1, GROUP_1, CARD_1, MATRIX_1, MATRIX_2, MATRIX_3, MATRIXR1, RLVECT_1, RLVECT_2, RLVECT_3, VECTSP_1, VECTSP_9, PRVECT_1, MATRIX_6, ARYTM_1, FUNCOP_1, CAT_1, RLSUB_2, MATRLIN, RANKNULL, VECTSP10, FINSET_1, SUBSET_1, TARSKI, FUNCT_4, COMPLEX1, SQUARE_1, VECTSP_2, FUNCSDOM, ORDINAL4, SETWISEO, CARD_3, RFINSEQ, REALSET1, MATRIXJ1, MATRLIN2, VECTSP11, MATRIXJ2, POLYNOM5, BCIALG_2, HURWITZ, MATHMORP, ZF_REFLE, ALGSTR_0; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, NUMBERS, CARD_1, XCMPLX_0, ALGSTR_0, XXREAL_0, NAT_1, FINSET_1, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, SETWOP_2, FINSEQ_1, STRUCT_0, FUNCOP_1, RLVECT_1, GROUP_1, VECTSP_1, FINSEQ_2, MATRIX_1, MATRIX_2, FVSUM_1, BINARITH, GROUP_4, MATRIX_3, MATRIX_6, FUNCT_4, DOMAIN_1, VECTSP_4, VECTSP_6, VECTSP_7, VECTSP_9, FINSEQOP, MATRIX13, MATRLIN, FUNCT_7, LAPLACE, MOD_2, RFINSEQ, VECTSP_2, VECTSP_5, MATRIX15, RANKNULL, FUNCSDOM, GRCAT_1, POLYNOM5, WSIERP_1, MATRIXJ1, MATRLIN2, VECTSP11; constructors FINSOP_1, XXREAL_0, GROUP_4, WELLORD2, VECTSP_7, VECTSP_9, MATRIX_6, REALSET1, LAPLACE, VECTSP_5, RANKNULL, MATRIX15, GRCAT_1, POLYNOM1, MONOID_0, POLYNOM4, POLYNOM5, MATRIXJ1, MATRLIN2, VECTSP11, SEQ_1, BINOP_2, REAL_1; registrations XBOOLE_0, FINSET_1, STRUCT_0, VECTSP_1, FUNCT_2, ORDINAL1, XXREAL_0, NAT_1, FINSEQ_1, RELAT_1, CARD_1, FINSEQ_2, SEQM_3, XREAL_0, VECTSP_9, VECTSP_7, VALUED_0, MATRIXJ1, VECTSP11, POLYNOM5, FUNCOP_1; requirements ARITHM, NUMERALS, REAL, BOOLE, SUBSET; definitions STRUCT_0, TARSKI, RLVECT_1, FINSEQ_1, VECTSP_4, RELAT_1, GROUP_4, FVSUM_1, MATRIX_1, FUNCT_1, FUNCOP_1, MATRIXJ1, VECTSP11, MATRLIN2; theorems ZFMISC_1, RLVECT_1, MATRIX_1, MATRIX_2, MATRIX_3, VECTSP_1, NAT_1, FINSEQ_2, BINARITH, 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, RELSET_1, STIRL2_1, STRUCT_0, TARSKI, WELLORD2, VECTSP_4, VECTSP_6, VECTSP_7, VECTSP_9, XBOOLE_0, XBOOLE_1, XREAL_1, XXREAL_0, MATRIX15, MOD_2, VECTSP10, RANKNULL, ANPROJ_1, VECTSP_5, FINSEQ_4, FINSEQ_5, RFINSEQ, RVSUM_1, POLYNOM3, POLYNOM4, MATRIXJ1, MATRLIN2, VECTSP11, GRCAT_1, FUNCT_4, CARD_4; schemes NAT_1, MATRIX_1, 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 & x in dom f; set xy=x.-->y; dom xy = {x} & rng xy = {y} by FUNCOP_1:14,19; then rng(f+*xy) = f.:(dom f\{x})\/{y} by FRECHET:12 .= (f.:(dom f))\(f.:{x})\/{y} by A1,FUNCT_1:123 .= (rng f)\Im(f,x)\/{y} by RELAT_1:146 .= (rng f)\{f.x}\/{y} by A1,FUNCT_1:117; hence thesis by A1,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 reconsider N=n as Element of NAT by ORDINAL1:def 13; 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); A1: for i,j st [i,j] in [:Seg N, Seg N:] for x1,x2 be Element of K st P[i,j,x1] & P[i,j,x2] holds x1 = x2; A2: 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 A3: i=j; take L; thus thesis by A3; end; suppose A4: i+1=j; take 1_K; thus thesis by A4; end; suppose A5: i<>j & i+1<>j; take 0.K; thus thesis by A5; end; end; consider M be Matrix of N,K such that A6: for i,j st [i,j] in Indices M holds P[i,j,M*(i,j)] from MATRIX_1:sch 2(A1,A2); take M; thus thesis by A6,MATRIX_1:25; end; uniqueness proof let M1,M2 be Matrix of K such that A7: len M1 = n & width M1 = n and A8: 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 A9: len M2 = n & width M2 = n and A10: 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 A11: [i,j] in Indices M1; A12: Indices M1 = [:Seg n,Seg n:] by A7,FINSEQ_1:def 3 .= Indices M2 by A9,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 A8,A10,A11,A12; hence M1*(i,j)=M2*(i,j); end; hence thesis by A7,A9,MATRIX_1:21; end; end; definition let K,L,n; redefine func Jordan_block(L,n) -> Upper_Triangular_Matrix of n,K; 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_2:7; 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_2:def 3; end; end; theorem Th1: diagonal_of_Matrix Jordan_block(L,n) = n |-> L proof set B=Jordan_block(L,n); A1: len diagonal_of_Matrix B=n & len (n |-> L)=n by MATRIX_3:def 10,FINSEQ_2:109; now let i such that A2: 1<=i & i<=n; A3: i in Seg n by A2,FINSEQ_1:3; then A4: [i,i] in [:Seg n,Seg n:] & [:Seg n,Seg n:]=Indices B by ZFMISC_1:106,MATRIX_1:25; thus (diagonal_of_Matrix B).i = B*(i,i) by A3,MATRIX_3:def 10 .= L by A4,Def1 .= (n|->L).i by A3,FINSEQ_1:4,FINSEQ_2:71; end; hence thesis by A1,FINSEQ_1:18; 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 A2: Det B<>0.K by LAPLACE:34; assume A3: L=0.K; assume n<>0; then A4: n in Seg n & dom (n|->L)=Seg n by FINSEQ_1:5,FINSEQ_2:144; then (n|->L).n=L by FINSEQ_1:4,FINSEQ_2:71; then 0.K = Product (n|->L) by A3,A4,FVSUM_1:107 .= (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 0.K = Det B by LAPLACE:34 .= (power K).(L,n) by Th2 .= Product (n|->L) by MATRIXJ1:5; then consider k be Element of NAT such that A6: k in dom (n|->L) & (n|->L).k=0.K by FVSUM_1:107; dom (n|->L)=Seg n by FINSEQ_2:144; hence thesis by A5,A6,FINSEQ_1:4,FINSEQ_2:71; 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 A1: i in Seg n & i<>n; set ONE=1.(K,n);set i1=i+1; set Li=Line(ONE,i); set Li1=Line(ONE,i1); set J=Jordan_block(L,n); set LJ=Line(J,i); reconsider N=n as Element of NAT by ORDINAL1:def 13; A2: width ONE=n & width J=n & Indices ONE=[:Seg n,Seg n:] & Indices ONE=Indices J by MATRIX_1:25,27; reconsider Li,Li1,LJ as Element of N-tuples_on the carrier of K by MATRIX_1:25; now let j such that A3: j in Seg n; i<=n by A1,FINSEQ_1:3; then ij by NAT_1:13; thus LJ.j = L by A2,A4,A5,A7,Def1 .= L+0.K by RLVECT_1:def 7 .= L*1_K+0.K by VECTSP_1:def 19 .= L*(ONE*(i,j))+0.K by A2,A4,A7,MATRIX_1:def 12 .= (L*Li+Li1).j by A2,A4,A6,A8,MATRIX_1:def 12; end; suppose A9: i1=j; then A10: ij & i1<>j; hence LJ.j = 0.K by A2,A4,A5,Def1 .= 0.K+0.K by RLVECT_1:def 7 .= L*0.K+0.K by VECTSP_1:39 .= L*(ONE*(i,j))+0.K by A2,A4,A11,MATRIX_1:def 12 .= (L*Li+Li1).j by A2,A4,A6,A11,MATRIX_1:def 12; end; end; hence (L*Li+Li1).j=LJ.j; end; hence thesis by FINSEQ_2:139; 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 13; A1: width ONE=n & width J=n & Indices ONE=[:Seg n,Seg n:] & Indices ONE=Indices J by MATRIX_1:25,27; reconsider Ln,LJ as Element of N-tuples_on the carrier of K by MATRIX_1:25; now let j such that A2: j in Seg n; n in Seg n by A2,FINSEQ_1:5,4; then A3: [n,j] in [:Seg n,Seg n:] by A2,ZFMISC_1:106; A4: Ln.j=ONE*(n,j) & LJ.j=J*(n,j) by A1,A2,MATRIX_1:def 8; then A5: (L*Ln).j=L*(ONE*(n,j)) by A2,FVSUM_1:63; now per cases; suppose A6: n=j; thus LJ.j = L by A1,A3,A4,A6,Def1 .= L*1_K by VECTSP_1:def 19 .= (L*Ln).j by A1,A3,A5,A6,MATRIX_1:def 12; end; suppose n+1=j; then j>n & j<=n by A2,NAT_1:13,FINSEQ_1:3; hence (L*Ln).j=LJ.j; end; suppose A7: n<>j & n+1<>j; hence LJ.j = 0.K by A1,A3,A4,Def1 .= L*0.K by VECTSP_1:39 .= (L*Ln).j by A1,A3,A5,A7,MATRIX_1:def 12; end; end; hence (L*Ln).j=LJ.j; end; hence thesis by FINSEQ_2:139; 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); set Li=Line(J,i); reconsider N=n as Element of NAT by ORDINAL1:def 13; A2: width J=n & Indices J=[:Seg n,Seg n:] by MATRIX_1:25; reconsider Li,f=F as Element of N-tuples_on the carrier of K by MATRIX_1:25; A3: dom mlt(Li,f)=Seg n & dom f=Seg n by FINSEQ_2:144; thus i <> n implies Line(J,i) "*" F = L * (F/.i)+ F/.(i+1) proof assume A4: i<>n; i<=n by A1,FINSEQ_1:3; then ii by NAT_1:13; then A6: [i,i] in Indices J & [i,i+1] in Indices J & f.i=f/.i & f.(i+1)=f/.(i+1) & J*(i,i)=Li.i & J*(i,i+1)=Li.(i+1) by A1,A2,A3,ZFMISC_1:106,PARTFUN1:def 8,MATRIX_1:def 8; A7: mlt(Li,f)/.i = mlt(Li,f).i by A1,A3,PARTFUN1:def 8 .= J*(i,i)*f/.i by A1,A6,FVSUM_1:74 .= L*(f/.i) by A6,Def1; A8: mlt(Li,f)/.(i+1) = mlt(Li,f).(i+1) by A3,A5,PARTFUN1:def 8 .= J*(i,i+1)*f/.(i+1) by A5,A6,FVSUM_1:74 .= 1_K*(f/.(i+1)) by A6,Def1 .= f/.(i+1) by VECTSP_1:def 13; now let j such that A9: j in Seg n & j<>i & j<>i+1; A10: [i,j] in Indices J & f.j=f/.j by A1,A2,A3,A9,ZFMISC_1:106,PARTFUN1:def 8; then 0.K = J*(i,j) by A9,Def1 .= Li.j by A2,A9,MATRIX_1:def 8; hence mlt(Li,f).j = 0.K * (f/.j) by A9,A10,FVSUM_1:74 .= 0.K by VECTSP_1:36; end; hence thesis by A1,A5,A7,A8,A3,MATRIX15:7; end; assume A11: i=n; A12: Line(J,i).i=J*(i,i)& [i,i] in Indices J & f.i=f/.i by A1,A2,A3,MATRIX_1:def 8,ZFMISC_1:106,PARTFUN1:def 8; now let j such that A13: j in Seg n & j<>i; j<=n by A13,FINSEQ_1:3; then A14: j 1 implies Col(Jordan_block(L,n),i) "*" F = L * (F/.i)+F/.(i-1) ) 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); set Ci=Col(J,i); reconsider N=n as Element of NAT by ORDINAL1:def 13; A2: len J=n & dom J=Seg len J & Indices J=[:Seg n,Seg n:] by MATRIX_1:25,FINSEQ_1:def 3; reconsider Ci,f=F as Element of N-tuples_on the carrier of K by MATRIX_1:25; A3: dom mlt(Ci,f)=Seg n & dom f=Seg n by FINSEQ_2:144; thus i = 1 implies Col(J,i) "*" F = L * (F/.i) proof assume A4: i=1; A5: Col(J,i).i=J*(i,i) & [i,i] in Indices J & f.i=f/.i by A1,A2,A3,MATRIX_1:def 9,ZFMISC_1:106,PARTFUN1:def 8; now let j such that A6: j in Seg n & j<>i; 1<=j by A6,FINSEQ_1:3; then A7: i1; A10: n>=i & i>=1 by A1,FINSEQ_1:3; then reconsider i1=i-1 as Element of NAT by NAT_1:21; i1+1>0+1 by A9,A10,XXREAL_0:1; then i1>0 & i1+1>=i1 by NAT_1:11; then i1>=1 & n>=i1 by A10,NAT_1:14,XXREAL_0:2; then A11: i1 in Seg n & i1<>i; then A12: Col(J,i).i=J*(i,i) & Col(J,i).i1=J*(i1,i) & i1+1=i & [i,i] in Indices J & [i1,i] in Indices J & f.i=f/.i & f.i1=f/.i1 by A1,A2,A3,MATRIX_1:def 9,ZFMISC_1:106,PARTFUN1:def 8; A13: mlt(Ci,f)/.i = mlt(Ci,f).i by A1,A3,PARTFUN1:def 8 .= J*(i,i)*f/.i by A1,A12,FVSUM_1:74 .= L*(f/.i) by A12,Def1; A14: mlt(Ci,f)/.i1 = mlt(Ci,f).i1 by A3,A11,PARTFUN1:def 8 .= J*(i1,i)*f/.i1 by A11,A12,FVSUM_1:74 .= 1_K*(f/.i1) by A12,Def1 .= f/.i1 by VECTSP_1:def 13; now let j such that A15: j in Seg n & j<>i & j<>i1; A16: [j,i] in Indices J & f.j=f/.j & j+1<>i by A1,A2,A3,A15,ZFMISC_1:106,PARTFUN1:def 8; then 0.K = J*(j,i) by A15,Def1 .= Ci.j by A2,A15,MATRIX_1:def 9; hence mlt(Ci,f).j = 0.K*(f/.j) by A15,A16,FVSUM_1:74 .= 0.K by VECTSP_1:36; end; hence thesis by A1,A3,A11,A13,A14,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 assume A1: L <> 0.K; reconsider N=n as Element of NAT by ORDINAL1:def 13; defpred P[Nat,Nat,set] means ($1 > $2 implies $3 = 0.K) & ($1<= $2 implies $3 = -power(K).(-L",$2-'$1+1) ); A2: for i,j st [i,j] in [:Seg N, Seg N:] for x1,x2 be Element of K st P[i,j,x1] & P[i,j,x2] holds x1 = x2; A3: 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 A4: i>j; take 0.K; thus thesis by A4;end; suppose A5: i<=j; take P=-power(K).(-L",j-'i+1); thus thesis by A5;end; end; consider M be Matrix of N,K such that A6: for i,j st [i,j] in Indices M holds P[i,j,M*(i,j)] from MATRIX_1:sch 2(A2,A3); reconsider M as Matrix of n,K; take M; set J=Jordan_block(L,n); set ONE=1.(K,n); set JM=J*M; set MJ=M*J; A7: J is invertible & Indices M=Indices J & Indices J=Indices ONE & Indices JM=Indices ONE & Indices MJ=Indices ONE & Indices ONE= [:Seg n,Seg n:] by A1,Th3,MATRIX_1:25,27; A8: len M=n & width M=n & len J=n & width J=n by MATRIX_1:25; now let i,j such that A9: [i,j] in Indices ONE; set C=Col(M,j); set i1=i+1; A10: i in Seg n & j in Seg n & dom M=Seg n & dom C=Seg n by A7,A8,A9,ZFMISC_1:106,FINSEQ_1:def 3,FINSEQ_2:144; then A11: C/.i=C.i & C.i=M*(i,j) by PARTFUN1:def 8,MATRIX_1:def 9; A12: JM*(i,j)=Line(J,i)"*"Col(M,j) by A7,A8,A9,MATRIX_3:def 4; now per cases; suppose A13: i=n; then A14: JM*(i,j)=L*(M*(i,j)) by A12,A8,A10,Th6,A11; now per cases; suppose A15: i>j; hence JM*(i,j) = L*0.K by A7,A9,A14,A6 .= 0.K by VECTSP_1:36 .= ONE*(i,j) by A9,A15,MATRIX_1:def 12;end; suppose A16: i<=j; j<=n by A10,FINSEQ_1:3; then A17: j=n by A13,A16,XXREAL_0:1; hence JM*(i,j) = L*(-power(K).(-L",n-'n+1)) by A7,A9,A14,A13,A6 .= L*(-power(K).(-L",0+1)) by BINARITH:51 .= L*(-(-L")) by GROUP_1:98 .= L*L" by RLVECT_1:30 .= 1_K by A1,VECTSP_1:def 22 .= ONE*(i,j) by A9,A13,A17,MATRIX_1:def 12;end; end; hence JM*(i,j)=ONE*(i,j);end; suppose A18: i<>n; i<=n by A10,FINSEQ_1:3; then ij; then i1>j by NAT_1:13; hence JM*(i,j) = L*(M*(i,j)) + 0.K by A19,A20,A6 .= L*(M*(i,j)) by RLVECT_1:def 7 .= L*0.K by A9,A7,A6,A21 .= 0.K by VECTSP_1:36 .= ONE*(i,j) by A9,A21,MATRIX_1:def 12;end; suppose A22: i=j; then i1>j by NAT_1:13; hence JM*(i,j) = L*(M*(i,j)) + 0.K by A19,A20,A6 .= L*(M*(i,i)) by A22,RLVECT_1:def 7 .= L*(-power(K).(-L",i-'i+1)) by A9,A7,A6,A22 .= L*(-power(K).(-L",0+1)) by BINARITH:51 .= L*(-(-L")) by GROUP_1:98 .= L*L" by RLVECT_1:30 .= 1_K by A1,VECTSP_1:def 22 .= ONE*(i,j) by A9,A22,MATRIX_1:def 12;end; suppose A23: ij; 1<=i by A28,FINSEQ_1:3; then j1; A36: j>=1 by A28,FINSEQ_1:3; then reconsider j1=j-1 as Element of NAT by NAT_1:21; j1+1>0+1 by A35,A36,XXREAL_0:1; then j1>0 & j1<=j1+1 & j<=n by A28,FINSEQ_1:3,NAT_1:11; then n>=j1 & j1>=1 by NAT_1:14,XXREAL_0:2; then j1 in Seg n; then A37: LL/.j1=LL.j1 & LL.j1=M*(i,j1) & [i,j1] in Indices ONE by A7,A8,A28,PARTFUN1:def 8,MATRIX_1:def 8,ZFMISC_1:106; then A38: MJ*(i,j)= L* (M*(i,j))+M*(i,j1) by A8,A28,A29,A35,A30,Th7; now per cases by XXREAL_0:1; suppose A39: ij1 by NAT_1:13; hence MJ*(i,j) = L* (M*(i,j))+0.K by A7,A6,A37,A38 .= L* (M*(i,j)) by RLVECT_1:def 7 .= L* (-power(K).(-L",i-'i+1)) by A7,A42,A27,A6 .= L*(-power(K).(-L",0+1)) by BINARITH:51 .= L*(-(-L")) by GROUP_1:98 .= L*L" by RLVECT_1:30 .= 1_K by A1,VECTSP_1:def 22 .= ONE*(i,j) by A27,A42,MATRIX_1:def 12;end; suppose A43: i>j1+1; then i>j1 by NAT_1:13; hence MJ*(i,j) = L* (M*(i,j))+0.K by A7,A6,A37,A38 .= L* (M*(i,j)) by RLVECT_1:def 7 .= L* 0.K by A7,A43,A27,A6 .= 0.K by VECTSP_1:36 .= ONE*(i,j) by A27,A43,MATRIX_1:def 12;end; end; hence MJ*(i,j)=ONE*(i,j);end; end; hence ONE*(i,j)=MJ*(i,j); end; then ONE=MJ by MATRIX_1:28; then M is_reverse_of J by A26,MATRIX_6:def 2; hence thesis by A6,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 let i,j such that A1: [i,j] in Indices Ja; A2: Indices J=Indices Ja & Indices J=Indices ONE by MATRIX_1:27; now per cases; suppose A3: i=j; hence Ja*(i,j) = L+a by A1,Def1 .= J*(i,j)+a by A1,A2,A3,Def1 .= J*(i,j)+a*1_K by VECTSP_1:def 16 .= J*(i,j)+a*(ONE*(i,j)) by A2,A1,A3,MATRIX_1:def 12 .= J*(i,j)+(a*ONE)*(i,j) by A2,A1,MATRIX_3:def 5 .= (J+a*ONE)*(i,j) by A2,A1,MATRIX_3:def 3; end; suppose A4: i+1=j; then A5: i<>j; thus Ja*(i,j) = 1_K by A1,A4,Def1 .= 1_K+0.K by RLVECT_1:def 7 .= J*(i,j)+0.K by A2,A1,A4,Def1 .= J*(i,j)+a*0.K by VECTSP_1:36 .= J*(i,j)+a*(ONE*(i,j)) by A2,A1,A5,MATRIX_1:def 12 .= J*(i,j)+(a*ONE)*(i,j) by A2,A1,MATRIX_3:def 5 .= (J+a*ONE)*(i,j) by A2,A1,MATRIX_3:def 3; end; suppose A6: i<>j & i+1<>j; hence Ja*(i,j) = 0.K by A1,Def1 .= 0.K+0.K by RLVECT_1:def 7 .= J*(i,j)+0.K by A2,A1,A6,Def1 .= J*(i,j)+a*0.K by VECTSP_1:36 .= J*(i,j)+a*(ONE*(i,j)) by A2,A1,A6,MATRIX_1:def 12 .= J*(i,j)+(a*ONE)*(i,j) by A2,A1,MATRIX_3:def 5 .= (J+a*ONE)*(i,j) by A2,A1,MATRIX_3:def 3; end; end; hence Ja*(i,j)=(J+a*ONE)*(i,j); end; hence thesis by MATRIX_1:28; 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 FinSequence of (the carrier of K)**; existence proof reconsider F=<*>((the carrier of K)**) as FinSequence of (the carrier of K)**; take F; for i st i in dom F ex L,n st F.i = Jordan_block(L,n); hence thesis by Def2; end; end; registration let K; cluster Jordan-block-yielding -> Square-Matrix-yielding 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 such that A2: i in dom F; ex L,n st F.i=Jordan_block(L,n) by A1,A2,Def2; 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 let i such that A1: i in dom <*Jordan_block(L,n)*>; dom <*Jordan_block(L,n)*> ={1} by FINSEQ_1:4,def 8; then <*Jordan_block(L,n)*>.1=Jordan_block(L,n) & i=1 by A1,TARSKI:def 1,FINSEQ_1:def 8; 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 let i such that A2: i in dom JJ; dom JJ ={1} by FINSEQ_1:4,def 8; then JJ.1=Jordan_block(L,n) & i=1 by A2,TARSKI:def 1,FINSEQ_1:def 8; hence ex n st JJ.i = Jordan_block(L,n); end; hence thesis by Def3; end; registration let K,L; cluster non-empty 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 let x such that A1: x in dom JJ; dom JJ ={1} by FINSEQ_1:4,def 8; then JJ.1=Jordan_block(L,1) & x=1 & len Jordan_block(L,1)=1 by A1,TARSKI:def 1,FINSEQ_1:def 8,Def1; hence JJ.x is non empty; end; hence thesis by FUNCT_1:def 15; end; end; registration let K; cluster non-empty FinSequence_of_Jordan_block of K; existence proof consider F be 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 let i such that A2: i in dom (J(+)M); A3: i in dom J & dom J=Seg len J by A2,MATRIXJ1:def 10,FINSEQ_1:def 3; then consider n such that A4: J.i = Jordan_block(L,n) by Def3; take n; len (len J|->a)=len J by FINSEQ_2:69; then dom (len J|->a)=dom J by FINSEQ_3:31; then A5: (len J|->a)/.i = (len J|->a).i by A3,PARTFUN1:def 8 .= a by A3,FINSEQ_2:71,FINSEQ_1:4; A6: dom M=dom 1.(K,Len J) by MATRIXJ1:def 9; A7: dom 1.(K,Len J)=dom Len J by MATRIXJ1:def 8; A8: dom Len J=dom J by MATRIXJ1:def 3; then A9: (Len J).i=len (J.i) & len (J.i)=n by A4,A3,MATRIXJ1:def 3,MATRIX_1:25; M.i = a * 1.(K,Len J).i by A3,A6,A5,A7,A8,MATRIXJ1:def 9 .= a* 1.(K,n) by A9,A3,A7,A8,MATRIXJ1:def 8; hence (J(+)M).i = Jordan_block(L,n) +a* 1.(K,n) by A4,A2,MATRIXJ1:def 10 .= Jordan_block(L+a,n) by Th9; end; J(+)M is Jordan-block-yielding proof let i such that A10: i in dom (J(+)M); ex n st (J(+)M).i=Jordan_block(L+a,n) by A10,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 such that A11: i in dom JM; thus thesis by A11,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; 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:38; suppose i in dom J1; then (J1^J2).i=J1.i & ex L,n st J1.i=Jordan_block(L,n) by FINSEQ_1:def 7,Def2; hence thesis;end; suppose ex n st n in dom J2 & i=len J1 + n; then consider k such that A2: k in dom J2 & i=len J1+k; (J1^J2).i=J2.k & ex L,n st J2.k=Jordan_block(L,n) by A2,FINSEQ_1:def 7,Def2; hence thesis;end; end; hence thesis; end; end; definition let K; let J be FinSequence_of_Jordan_block of K; let n; redefine func J|n -> FinSequence_of_Jordan_block of K; coherence proof now let i such that A1: i in dom (J|n); i in dom J by A1,RELAT_1:86; then (J|n).i=J.i& ex L,k st J.i=Jordan_block(L,k) by A1,FUNCT_1:70,Def2; hence ex L,k st (J|n).i=Jordan_block(L,k); end; hence thesis by Def2; end; redefine func J/^n -> FinSequence_of_Jordan_block of K; coherence proof now let i such that A2: i in dom (J/^n); i+n in dom J by A2,FINSEQ_5:29; then (J/^n).i=(J/^n)/.i & J.(n+i)=J/.(n+i) & ex L,k st J.(n+i)=Jordan_block(L,k) by A2,PARTFUN1:def 8,Def2; hence ex L,k st (J/^n).i=Jordan_block(L,k) by A2,FINSEQ_5:30; 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; 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:38; suppose i in dom J1; then (J1^J2).i=J1.i & ex n st J1.i=Jordan_block(L,n) by FINSEQ_1:def 7,Def3; hence thesis;end; suppose ex n st n in dom J2 & i=len J1 + n; then consider k such that A2: k in dom J2 & i=len J1+k; (J1^J2).i=J2.k & ex n st J2.k=Jordan_block(L,n) by A2,FINSEQ_1:def 7,Def3; hence thesis;end; end; hence thesis; end; end; definition let K,L; let J be FinSequence_of_Jordan_block of L,K; let n; redefine func J|n -> FinSequence_of_Jordan_block of L,K; coherence proof now let i such that A1: i in dom (J|n); i in dom J by A1,RELAT_1:86; then (J|n).i=J.i& ex k st J.i=Jordan_block(L,k) by A1,FUNCT_1:70,Def3; hence ex k st (J|n).i=Jordan_block(L,k); end; hence thesis by Def3; end; redefine func J/^n -> FinSequence_of_Jordan_block of L,K; coherence proof now let i such that A2: i in dom (J/^n); i+n in dom J by A2,FINSEQ_5:29; then (J/^n).i=(J/^n)/.i & J.(n+i)=J/.(n+i) & ex k st J.(n+i)=Jordan_block(L,k) by A2,PARTFUN1:def 8,Def3; hence ex k st (J/^n).i=Jordan_block(L,k) by A2,FINSEQ_5:30; end; hence thesis by Def3; end; end; begin :: Nilpotent Transformations definition let K be doubleLoopStr; let V be non empty VectSpStr 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 VectSpStr 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 VectSpStr 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 by Def4; now let x such that A2: x in dom (f|^n); reconsider v=x as Vector of V by FUNCT_2:def 1,A2; thus (f|^n).x = (f|^n).v .= 0.V by A1; end; then (f|^n) = (dom (f|^n))-->0.V by FUNCOP_1:17 .= (the carrier of V)-->0.V by FUNCT_2:def 1 .= ZeroMap(V,V) by GRCAT_1:def 12; hence ex n st f|^n = ZeroMap(V,V); end; given n such that A3: 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 A3,GRCAT_1:def 12 .= 0.V by FUNCOP_1:13; end; registration let K be doubleLoopStr; let V be non empty VectSpStr over K; cluster nilpotent 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 linear Function of V,V; existence proof take F=ZeroMap(V,V); F|^1=F by VECTSP11:19; hence thesis by Th13,MOD_2:8; 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:18; A1: v1 in KER by STRUCT_0:def 5; thus (fK|^n).v = ((f|^n)|KER).v by VECTSP11:22 .= (f|^n).v1 by FUNCT_1:72 .= 0.V by A1,RANKNULL:10 .= 0.KER by VECTSP_4:19; end; hence thesis by Def4; end; definition let K be doubleLoopStr; let V be non empty VectSpStr 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] and A3: for k st P[k] holds n<=k from NAT_1:sch 5(A1); take n; thus thesis by A2,A3; end; uniqueness proof let i,j such that A4: f|^i = ZeroMap(V,V) & for k st f|^k = ZeroMap(V,V) holds i <= k and A5: f|^j = ZeroMap(V,V) & for k st f|^k = ZeroMap(V,V) holds j <= k; i<=j & j<=i by A4,A5; hence thesis by XXREAL_0:1; end; end; notation let K be doubleLoopStr; let V be non empty VectSpStr 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 VectSpStr 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 VectSpStr over K; let f be nilpotent Function of V,V; hereby assume A1: deg f=0; [#]V c= {0.V} proof let x 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 12; then x = ((the carrier of V)-->0.V).x by A2,FUNCT_1:35 .= 0.V by A2,FUNCOP_1:13; hence thesis by TARSKI:def 1; end; hence [#]V ={0.V} by ZFMISC_1:39; end; assume A3: [#]V={0.V}; now let x such that A5: x in dom (f|^0); reconsider v=x as Vector of V by FUNCT_2:def 1,A5; 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:17 .= (the carrier of V)-->0.V by FUNCT_2:def 1 .= ZeroMap(V,V) by GRCAT_1:def 12; hence thesis by Def5; end; theorem Th16: for K be doubleLoopStr for V be non empty VectSpStr 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 VectSpStr over K; let f be nilpotent Function of V,V; set D=deg f; assume A1: for v be Vector of V ex i st i < D & (f|^i).v=0.V; then consider i such that A2: i < D & (f|^i).(0.V) =0.V; [#]V<>{0.V} by A2,Th15; then consider v be set such that A3: v in [#]V & v<>0.V by ZFMISC_1:41; reconsider v as Vector of V by A3; defpred P[Nat] means 0<$1 & $1 < D & (f|^$1).(0.V)=0.V; consider j such that A4: j < D & (f|^j).v =0.V by A1; j>0 proof assume j<=0; then j=0; then 0.V = id V.v by A4,VECTSP11:18 .= v by FUNCT_1:35; hence thesis by A3; end; then A5: D-j=D-'j & j-j0.V by GRCAT_1:def 12; then 0.V = (f|^D).v by FUNCOP_1:13 .= ((f|^(D-'j))*(f|^j)).v by A6,VECTSP11:20 .= (f|^(D-'j)).(0.V) by A4,A7,FUNCT_1:23; then A9: ex j st P[j] by A5; consider m such that A10: P[m] & for n be Nat st P[n] holds m <= n from NAT_1:sch 5(A9); A11: D-'m=D-m & D-m0 by A14,A19; then reconsider I1=I-1 as Nat by NAT_1:20; D-'m=k+I1*m by A19,A11,A20; hence (f|^(D-'m)).X=0.V by A10,A14,VECTSP11:21; end; suppose A21: MAX0 proof assume A22: MAX=0; then k=0 by A19; then k+1*m0.V by A12,FUNCOP_1:17 .= ZeroMap(V,V) by GRCAT_1:def 12; hence contradiction by A11,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 12 .= ((the carrier of V)/\[#]W) -->0.V by FUNCOP_1:18 .= (the carrier of W)-->0.W by A2,VECTSP_4:19 .= ZeroMap(W,W) by GRCAT_1:def 12; hence f|W is nilpotent Function of W,W 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: dom (fI|^Dn)=[#]IM by FUNCT_2:def 1; now let x such that A3: x in dom (fI|^Dn); reconsider X=x as Vector of IM by FUNCT_2:def 1,A3; reconsider v=X as Vector of V by VECTSP_4:18; X in IM by STRUCT_0:def 5; then consider w be Element of V such that A4: v = (f|^n).w by RANKNULL:13; A5: dom (f|^n) = the carrier of V by FUNCT_2:def 1; (f|^D).w = ZeroMap(V,V).w by Def5 .= ((the carrier of V)-->0.V).w by GRCAT_1:def 12 .= 0.V by FUNCOP_1:13; hence 0.IM = (f|^(Dn+n)).w by VECTSP_4:19 .= ((f|^Dn)*(f|^n)).w by VECTSP11:20 .= (f|^Dn).v by A4,A5,FUNCT_1:23 .= ((f|^Dn)|IM).X by FUNCT_1:72 .= (fI|^Dn).x by A1,VECTSP11:22; end; then fI|^Dn = (the carrier of IM)-->0.IM by A2,FUNCOP_1:17 .= ZeroMap(IM,IM) by GRCAT_1:def 12; then A6: deg fI<=Dn by Def5; deg fI = Dn proof set DI=deg fI; assume DI<>Dn; then DI0.V by Th16; (f|^n).v in IM by RANKNULL:13; then A9: (f|^n).v in the carrier of IM by STRUCT_0:def 5; A10: dom (f|^n)=the carrier of V by FUNCT_2:def 1; fI|^DI = ZeroMap(IM,IM) by Def5 .= (the carrier of IM)-->0.IM by GRCAT_1:def 12; then 0.IM = (fI|^DI).((f|^n).v) by A9,FUNCOP_1:13 .= ((f|^DI)|IM).((f|^n).v) by A1,VECTSP11:22 .= (f|^DI).((f|^n).v) by A9,FUNCT_1:72 .= ((f|^DI)*(f|^n)).v by A10,FUNCT_1:23 .= (f|^(DI+n)).v by VECTSP11:20; hence thesis by A7,A8, VECTSP_4:19; 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 & B2 = Bu1 ^ Bu2 and A2: M = block_diagonal(<*M1,M2*>,0.K) and A3: width M1 = len Bu1 & width M2 = len Bu2; set F=Mx2Tran(M,b1,B2); set F1=Mx2Tran(M1,bw1,Bu1); set F2=Mx2Tran(M2,bw2,Bu2); rng Bu1 c= the carrier of U1 & the carrier of U1 c= the carrier of V2 & 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 rng Bu1 c= the carrier of V2 & rng Bu2 c= the carrier of V2 by XBOOLE_1:1; then reconsider bu1=Bu1,bu2=Bu2 as FinSequence of V2 by FINSEQ_1:def 4; A4: dom bw1 c= dom b1 & dom b1=Seg len b1 by A1,FINSEQ_1:39,def 3; A5: width 1.(K,len b1)=len b1 & len 1.(K,len b1)=len b1 & len M=len b1 & dom 1.(K,len b1)=Seg len 1.(K,len b1) by MATRIX_1:def 3,25,FINSEQ_1:def 3; A6: dom bw1=Seg len bw1 by FINSEQ_1:def 3; A7: width 1.(K,len bw1)=len bw1 & len 1.(K,len bw1)=len bw1 & dom 1.(K,len bw1)=Seg len 1.(K,len bw1) by MATRIX_1:25,FINSEQ_1:def 3; A8: dom bw2=Seg len bw2 by FINSEQ_1:def 3; A9: width 1.(K,len bw2)=len bw2 & len 1.(K,len bw2)=len bw2 & dom 1.(K,len bw2)=Seg len 1.(K,len bw2) by MATRIX_1:25,FINSEQ_1:def 3; A10: len M1=len bw1 & len M2=len bw2 by MATRIX_1:def 3; then A11: dom M1=dom bw1 & dom M2=dom bw2 by FINSEQ_3:31; thus i in dom bw1 implies F.(b1/.i)= F1.(bw1/.i) proof assume A12: i in dom bw1; then A13: Line(M,i)=Line(M1,i)^(width M2|->0.K) & len Line(M1,i)=width M1 & len (width M2|->0.K)=width M2 by A2,A11,MATRIXJ1:23,FINSEQ_2:109; 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 A4,A12,MATRLIN2:19 .= Sum lmlt (Line(LineVec2Mx(Line(1.(K,len b1)*M,i)),1),B2) by A4,A5,A12,MATRLIN2:35 .= Sum lmlt (Line(LineVec2Mx(Line(M,i)),1),B2) by A5,MATRIXR2:68 .= Sum lmlt(Line(M,i),B2) by MATRIX15:25 .= Sum (lmlt(Line(M1,i),bu1)^lmlt(width M2|->0.K,bu2)) by A1,A3,A13,MATRLIN2:9 .= Sum lmlt(Line(M1,i),bu1) + Sum lmlt(width M2|->0.K,bu2) by RLVECT_1:58 .= Sum lmlt(Line(M1,i),bu1) + 0.K*Sum bu2 by A3,MATRLIN2:11 .= Sum lmlt(Line(M1,i),bu1) + 0.V2 by VECTSP_1:59 .= Sum lmlt(Line(M1,i),bu1) by RLVECT_1:def 7 .= 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 A10,MATRIXR2:68 .= Sum lmlt (Line(LineVec2Mx(Line(1.(K,len bw1),i)) * M1,1),Bu1) by A12,A6,A7,A10,MATRLIN2:35 .= Sum lmlt (Line(LineVec2Mx(bw1/.i|--bw1) * M1,1),Bu1) by A12,MATRLIN2:19 .= F1.(bw1/.i) by MATRLIN2:def 3; end; assume A14: i in dom bw2; set BI=len bw1+i; A15: Line(M,BI)=(width M1|->0.K)^Line(M2,i) & len Line(M2,i)=width M2 & len (width M1|->0.K)=width M1 by A2,A14,A10,A11,MATRIXJ1:23,FINSEQ_2:109; A16: BI in dom b1 by A1,A14,FINSEQ_1:41; 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 A16,MATRLIN2:19 .= Sum lmlt (Line(LineVec2Mx(Line(1.(K,len b1)*M,BI)),1),B2) by A4,A5,MATRLIN2:35,A1,A14,FINSEQ_1:41 .= Sum lmlt (Line(LineVec2Mx(Line(M,BI)),1),B2) by A5,MATRIXR2:68 .= Sum lmlt(Line(M,BI),B2) by MATRIX15:25 .= Sum (lmlt(width M1|->0.K,bu1)^lmlt(Line(M2,i),bu2)) by A1,A3,A15,MATRLIN2:9 .= Sum lmlt(width M1|->0.K,bu1) + Sum lmlt(Line(M2,i),bu2) by RLVECT_1:58 .= 0.K*Sum bu1 + Sum lmlt(Line(M2,i),bu2) by A3,MATRLIN2:11 .= 0.V2 + Sum lmlt(Line(M2,i),bu2) by VECTSP_1:59 .= Sum lmlt(Line(M2,i),bu2) by RLVECT_1:def 7 .= 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 A10,MATRIXR2:68 .= Sum lmlt (Line(LineVec2Mx(Line(1.(K,len bw2),i)) * M2,1),Bu2) by A14,A10,A8,A9,MATRLIN2:35 .= Sum lmlt (Line(LineVec2Mx(bw2/.i|--bw2) * M2,1),Bu2) by A14,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 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); set B=block_diagonal(F,0.K); let i,m such that A2: i in dom b1 & m = min(Len F,i); A3: 1<=i & i<=len b1 by A2,FINSEQ_3:27; set ONE=1.(K,len b1); len ONE=len b1 by MATRIX_1:def 3; then A4: dom ONE=dom b1 & width ONE=len b1 & len M=len b1 & dom b1=Seg len b1 & len M=Sum Len F & width M=Sum Width F & width M=len B2 by A3,A1,FINSEQ_1:def 3,FINSEQ_3:31,MATRIX_1:24,MATRIXJ1:def 5; set W=Width F; set L=Len F; set Wm=Sum (W|m); set Wm1=Sum (W|(m-'1)); set Fm=F.m; set B2W=B2|Wm; m in dom Len F & dom L=dom F & dom W=dom F by A2,A4,MATRIXJ1:def 1,def 3,def 4; then A5: 1<=m & m<=len W & W.m=width Fm & m in NAT by FINSEQ_3:27, MATRIXJ1:def 4; W = (W|m)^(W/^m) by RFINSEQ:21; then A6: Sum W=Wm+Sum (W/^m) by RVSUM_1:105; A8: Sum W-'Wm = Sum W-Wm by A6,NAT_1:11,BINARITH:50 .= Sum (W/^m) by A6; W = (W|(m-'1))^<*width Fm*>^(W/^m) by A5,POLYNOM4:3; then A9: Sum W = Sum ((W|(m-'1))^<*width Fm*>)+Sum (W/^m) by RVSUM_1:105 .= Wm1 + width Fm+Sum (W/^m) by RVSUM_1:104; then aa: Sum W=Wm1+(width Fm+Sum (W/^m)); A11: B2=B2W^(B2/^Wm) by RFINSEQ:21; then A12: len B2=len B2W+ len (B2/^Wm) & len B2W =Wm by A4,A6,FINSEQ_1:35,80,NAT_1:11; Wm>=Wm1 by NAT_1:11,A6,A9; then Seg Wm1 c= Seg Wm by FINSEQ_1:7; then B2W|Wm1=B2|Wm1 by RELAT_1:103; then A13: B2W=(B2|Wm1)^(B2W/^Wm1) by RFINSEQ:21; then A14: len B2W=len (B2|Wm1)+len (B2W/^Wm1) & len (B2|Wm1) =Wm1 by A4,aa,FINSEQ_1:35,80,NAT_1:11; A15: B2W/^Wm1 = (B2|Sum(Width F|m))/^Wm1 by MATRIXJ1:21 .= (B2|Sum(Width F|m))/^Sum (Width F|(m-'1)) by MATRIXJ1:21; A16: len (Sum (W|(m-'1))|->0.K)=Sum (W|(m-'1)) & len Line(Fm,i-'Sum (Len F|(m-'1))) =width Fm & len ((Sum W-'Sum (W|m))|->0.K)=Sum (W/^m) by A8,FINSEQ_2:109; A17: len ((Sum (W|(m-'1))|->0.K)^Line(Fm,i-'Sum (Len F|(m-'1))))=Wm by A6,A9,FINSEQ_2:109; 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 A2,MATRLIN2:19 .= Sum lmlt (Line(LineVec2Mx(Line(ONE*M,i)),1),B2) by A2,A4,MATRLIN2:35 .= Sum lmlt (Line(LineVec2Mx(Line(M,i)),1),B2) by A4,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,A2,A4,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 A4,A6,A16,A17,A11,A12,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:58 .= Sum lmlt((Sum (W|(m-'1))|->0.K) ^ Line(Fm,i-'Sum (Len F|(m-'1))),B2W)+ 0.K* Sum (B2/^Wm) by A4,A6,A8,A12,MATRLIN2:11 .= Sum lmlt((Sum (W|(m-'1))|->0.K)^ Line(Fm,i-'Sum (Len F|(m-'1))),B2W)+ 0.V2 by VECTSP_1:59 .= Sum lmlt((Sum (W|(m-'1))|->0.K) ^ Line(Fm,i-'Sum (Len F|(m-'1))),B2W) by RLVECT_1:def 7 .= Sum (lmlt(Sum (W|(m-'1))|->0.K,B2|Wm1) ^ lmlt(Line(Fm,i-'Sum (Len F|(m-'1))),B2W/^Wm1)) by A13,A14,A6,A9,A12,A16,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:58 .= 0.K*Sum (B2|Wm1) + Sum lmlt(Line(Fm,i-'Sum (Len F|(m-'1))),B2W/^Wm1) by A14,MATRLIN2:11 .= 0.V2+Sum lmlt(Line(Fm,i-'Sum (Len F|(m-'1))),B2W/^Wm1) by VECTSP_1:59 .= Sum lmlt(Line(Fm,i-'Sum (Len F|(m-'1))),B2W/^Wm1) by RLVECT_1:def 7; hence thesis by A15,A14,A6,A9,A12; 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 ONE=1.(K,N); set J=Jordan_block(L,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 A1: i in dom B1 & i<>len B1; set N=len B1; set ONE=1.(K,N); set J=Jordan_block(L,N); A2: width ONE=N & dom B1=Seg N by FINSEQ_1:def 3,MATRIX_1:25; i<=N by A1,FINSEQ_3:27; then i len b1 implies Mx2Tran(M,b1,B2).(b1/.i) = L*(B2/.i)+ B2/.(i+1)) proof let M be Matrix of len b1,len B2,K such that A1: M = Jordan_block(L,n); let i such that A2: i in dom b1; set ONE=1.(K,len b1); set J=Jordan_block(L,n); len ONE=len b1 by MATRIX_1:def 3; then A3: dom ONE=dom b1 & width ONE=len b1 & width J=n & len M=len b1 & len M=n & dom b1=Seg len b1 by A1,FINSEQ_1:def 3,FINSEQ_3:31,MATRIX_1:25,26; then n<>0 by A2,FINSEQ_1:4; then A4: width J=len B2 by A1,A3,MATRIX_1:20; then A5: dom B2=dom b1 by A3,FINSEQ_3:31; 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 A2,MATRLIN2:19 .= Sum lmlt (Line(LineVec2Mx(Line(ONE*M,i)),1),B2) by A2,A3,MATRLIN2:35 .= Sum lmlt (Line(LineVec2Mx(Line(M,i)),1),B2) by A3,MATRIXR2:68 .= Sum lmlt (Line(M,i),B2) by MATRIX15:25; hence thesis by Th21,Th22,A1,A2,A3,A4,A5; 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); let i,m such that A2: i in dom b1 & m = min(Len J,i); A3: 1<=i & i<=len b1 by A2,FINSEQ_3:27; set B=block_diagonal(J,0.K); set BBB=(B2|Sum(Width J|m))/^Sum (Width J|(m-'1)); set S=Sum (Len J|(m-'1)); set Sm=Sum (Len J|m); set iS=i-'S; A4: (Len J)|(m-'1) = Len (J|(m-'1)) by MATRIXJ1:17; A5: (Len J)|m = Len (J|m) by MATRIXJ1:17; A6: Mx2Tran(M,b1,B2).(b1/.i) = Sum lmlt(Line(J.m,iS),BBB) & len BBB = width (J.m) by Th20,A1,A2; A7: len M=len b1 & Width J=Len J & dom b1=Seg len b1 & len M=Sum Len J & width M=Sum Width J & width M=len B2 by A3,A1,FINSEQ_1:def 3,MATRIX_1:24,MATRIXJ1:def 5,46; then A8: m-'1=m-1 & S & (Len J).m = len (J.m) & m =m-'1+1 & iS=i-S & (Len J).m=width (J.m) by A7,A4,FINSEQ_5:11,MATRIXJ1:def 3,def 4,BINARITH:50; then A10: Sm=S+len (J.m) by A5,RVSUM_1:104; then S+iS<=S+len (J.m) by A7,A9,A2,A5,MATRIXJ1:def 1; then A11: iS<=len (J.m) by XREAL_1:8; iS<>0 by A7,A9,A2,A4,MATRIXJ1:7; then 1<=iS by NAT_1:14; then A12: iS in dom BBB by A11,A6,A9,FINSEQ_3:27; A13: m in NAT by ORDINAL1:def 13; m <= len Len J by A8,FINSEQ_3:27; then Sm <= Sum ((Len J)|(len Len J)) by A5,A13,POLYNOM3:18; then Sm <= Sum Len J by FINSEQ_1:79; then A14: len (B2|Sm) =Sm by A7,FINSEQ_1:80; then A15: i in dom (B2|Sm) by A3,A8,FINSEQ_3:27; consider n such that A16: J.m = Jordan_block(L,n) by A8,Def3; A17: len (J.m)=n by A16,MATRIX_1:25; A18: BBB/.iS = (B2|Sum(Width J|m))/.(Sum (Width J|(m-'1))+iS) by A12,FINSEQ_5:30 .= (B2|Sum(Width J|m))/.(S+iS) by MATRIXJ1:46 .= (B2|Sum((Len J)|m))/.i by A7,A9,MATRIXJ1:21 .= B2/.i by A5,A15,FINSEQ_4:85; hence i = Sm implies Mx2Tran(M,b1,B2).(b1/.i) = L*(B2/.i) by A6,A9,A10,A12,Th21,A16,A17; assume A19: i<>Sm; then ilen (J.m) by A9,A10,A19; then iS0.V1 by A3,FUNCOP_1:15 .= Z by GRCAT_1:def 12; hence thesis; end; suppose A5: len b1>0; A6: dom J=dom Len J & len M=len b1 & len M = Sum Len J by A1,MATRIX_1:25,MATRIXJ1:def 3; A7: dom (Z*b1)=dom b1 & dom (MTm*b1)=dom b1 by A3,RELAT_1:46; now let x such that A8: x in dom b1; reconsider n=x as Element of NAT by A8; set mm=min(Len J,n); set Sm=Sum ((Len J)|(mm-'1)); A9: n in Seg Sum Len J by A6,A8,FINSEQ_1:def 3; then A10: mm in dom Len J by MATRIXJ1:def 1; then A11: n<=Sum ((Len J)|mm) & (Len J)|mm =Len (J|mm) & Sm < n & mm-'1=mm-1& (Len J).mm=(Len J)/.mm by A9,MATRIXJ1:def 1,17,7,PARTFUN1:def 8; then A12: Sum (Len J|mm)-'n=Sum (Len J|mm) - n & n-'Sm=n-Sm by BINARITH:50; A13: mm-'1+1=mm by A11; A14: (Len J)|mm=((Len J)|(mm-'1))^<*(Len J).mm*> & (Len J).mm = len (J.mm) by A10,A13,FINSEQ_5:11,MATRIXJ1:def 3; then A15: Sum (Len J|mm)=Sm+len (J.mm) by A11,RVSUM_1:104; aa: n-'Sm<>0 by A12,A9,MATRIXJ1:7; A17: now let k such that A18: n+k<=Sum (Len J|mm); 1<=n & n<=n+k by A9,FINSEQ_1:3,NAT_1:11; then A19: 1<=n+k by XXREAL_0:2; mm<=len Len J by A10,FINSEQ_3:27; then Sum (Len J|mm)<= Sum ((Len J)|(len Len J)) by A11,POLYNOM3:18; then Sum (Len J|mm)<= len b1 by A6,FINSEQ_1:79; then n+k <= len b1 by A18,XXREAL_0:2; hence n+k in dom b1 by A19,FINSEQ_3:27; end; A20: now let k such that A21: n+k<=Sum(Len J|mm); A22: 1<=n-'Sm+k by aa,NAT_1:14; n+k-Sm<=Sm+len (J.mm)-Sm by A21,A15,XREAL_1:11; then n-'Sm+k in Seg ((Len J)/.mm) by A22,A11,A12,A14; then min(Len J,n-'Sm+k+Sum ((Len J)|(mm-'1)))=mm by A10,MATRIXJ1:10; hence min(Len J,n+k)=mm by A12; end; defpred P[Nat] means n+$1 < Sum(Len J|mm) implies (MT|^($1+1)).(b1/.n)=b1/.(n+$1+1); A23: P[0] proof assume n+0< Sum(Len J|mm); then MT.(b1/.n) = 0.K*(b1/.n)+ b1/.(n+1) by A1,A8,Th24 .= 0.V1+b1/.(n+1) by VECTSP_1:59 .= b1/.(n+1) by RLVECT_1:def 7; hence b1/.(n+0+1)=(MT|^(0+1)).(b1/.n) by VECTSP11:19; end; A24: for k st P[k] holds P[k+1] proof let k such that A25: P[k];set k1=k+1; assume A26: n+k10; then reconsider S1=(Sum(Len J|mm)-'n)-1 as Element of NAT by NAT_1:20; S1+n=Sum(Len J|mm)-1 & Sum(Len J|mm)-10.V1).(b1/.x) by GRCAT_1:def 12 .= 0.V1 by FUNCOP_1:13 .= MTm.(b1.n) by A42,A8,PARTFUN1:def 8 .= (MTm*b1).x by A8,FUNCT_1:23; end; hence thesis by A5,MATRLIN:26,A7,FUNCT_1:9; 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; 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); A2: len b1 = len M & len M = Sum Len J by A1,MATRIX_1:25; set B=len b1; set m=min(Len J,B); set S=Sum (Len J|m); assume B<>0; then A3: B in Seg B & Seg B=dom b1 by FINSEQ_1:def 3,5; then A4: B<= Sum ((Len J)|m) & Sum ((Len J)|m)=S & m in dom Len J by A2,MATRIXJ1:def 1,17; then m<=len Len J by FINSEQ_3:27; then A5: Sum ((Len J)|m)<=Sum ((Len J)|(len Len J)) & (Len J)|(len Len J)=Len J by POLYNOM3:18,FINSEQ_1:79; then B=S by A2,A4,XXREAL_0:1; then A6: MT.(b1/.S)=L*(b1/.S) by A1,A3,Th24; defpred P[Nat] means (MT|^$1).(b1/.S)=((power K).(L,$1))*(b1/.S); A7: P[0] proof thus (MT|^0).(b1/.S) = (id V1).(b1/.S) by VECTSP11:18 .= b1/.S by FUNCT_1:35 .= 1_K * b1/.S by VECTSP_1:def 26 .= ((power K).(L,0))*b1/.S by GROUP_1:def 8; end; A8: for n st P[n] holds P[n+1] proof let n such that A9: P[n]; A10: dom (MT|^n) = the carrier of V1 by FUNCT_2:def 1; A11: n in NAT by ORDINAL1:def 13; 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 A9,A10,FUNCT_1:23 .= ((power K).(L,n))*(L*(b1/.S)) by A6,MOD_2:def 5 .= (((power K).(L,n))*L)*(b1/.S) by VECTSP_1:def 26 .= ((power K).(L,n+1))*(b1/.S) by A11,GROUP_1:def 8; end; for n holds P[n] from NAT_1:sch 2(A7,A8); hence thesis by A3,A5,A2,A4,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 assume MT is nilpotent; then reconsider MT as nilpotent linear-transformation of V1,V1; set B=len b1; set m=min(Len J,B); set S=Sum (Len J|m); assume A2: B<>0; then A3: ((power K).(L,deg MT))*(b1/.S) = (MT|^(deg MT)).(b1/.S) by A1,Lm3 .= ZeroMap(V1,V1).(b1/.S) by Def5 .= ((the carrier of V1)-->0.V1).(b1/.S) by GRCAT_1:def 12 .= 0.V1 by FUNCOP_1:13 .= 0.K * (b1/.S) by VECTSP_1:59; rng b1 is Basis of V1 & S in dom b1 by A1,A2,Lm3,MATRLIN:def 4; then b1.S in rng b1 & b1/.S=b1.S & rng b1 is linearly-independent Subset of V1 by FUNCT_1:def 5,PARTFUN1:def 8,VECTSP_7:def 3; then b1/.S <>0.V1 by VECTSP_7:3; then 0.K = (power K).(L,deg MT) by A3,VECTSP10:5 .= Product (deg MT|->L) by MATRIXJ1:5; then consider k be Element of NAT such that A4: k in dom (deg MT|->L) & (deg MT|->L).k=0.K by FVSUM_1:107; dom (deg MT|->L)=Seg deg MT by FINSEQ_2:144; hence 0.K=L by A4,FINSEQ_2:71,FINSEQ_1:4; end; assume A5: len b1=0 or L=0.K; per cases by A5; suppose len b1=0; then dim V1=0 by MATRLIN2:21; then (Omega).V1=(0).V1 by VECTSP_9:33; then A6: the carrier of V1 = {0.V1} by VECTSP_4:def 3; rng (MT|^1) c= the carrier of V1 by RELSET_1:12; then rng (MT|^1)={0.V1} by A6,ZFMISC_1:39; then (MT|^1) = (dom (MT|^1))-->0.V1 by FUNCOP_1:15 .= (the carrier of V1)-->0.V1 by FUNCT_2:def 1 .= ZeroMap(V1,V1) by GRCAT_1:def 12; hence thesis by Th13; end; suppose A7: L=0.K; now let i such that A8: i in dom J; A9: dom J=dom (Len J) by MATRIXJ1:def 3; then len (J.i)=(Len J).i by A8,MATRIXJ1:def 3; hence len (J.i) <= Sum Len J by A8,A9,POLYNOM3:4; end; then MT|^(Sum Len J)=ZeroMap(V1,V1) by A1,A7,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; set mm=min(Len J,len b1); A3: len M=len b1 & len M=Sum Len J & len b1 in Seg len b1 & dom b1=Seg len b1 by A1,A2,MATRIX_1:def 3,FINSEQ_1:def 3,5; then A4: min(Len J,len b1) in dom Len J & dom J=dom (Len J) by MATRIXJ1:def 1,def 3; let F be nilpotent Function of V1,V1 such that A5: F = Mx2Tran(M,b1,b1); defpred P[Nat] means for i st i in dom J holds len (J.i) <= $1; now let i such that A6: i in dom J; len (J.i)=(Len J).i by A4,A6,MATRIXJ1:def 3; hence len (J.i) <= Sum Len J by A4,A6,POLYNOM3:4; end; then A7: ex k st P[k]; consider MIN be Nat such that A8: P[MIN] and A9: for m st P[m] holds MIN <= m from NAT_1:sch 5(A7); 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; then len (J.mm)<> MIN & len (J.mm)<=MIN by A4,A8; then len (J.mm) MIN & len (J.i) <= MIN by A8,A11,A12; then len (J.i) < M1+1 by XXREAL_0:1; hence len (J.i) <= M1 by NAT_1:13; end; then M1+1<=M1 by A9; hence thesis by NAT_1:13; end; then consider i such that A13: i in dom J & len (J.i) = MIN; A14: len (J.i)=(Len J).i & (Len J).i=(Len J)/.i by A4,MATRIXJ1:def 3,A13,PARTFUN1:def 8; set S=Sum ((Len J)|(i-'1)); 1<=i & i<=len Len J & i in NAT by A4,A13,FINSEQ_3:27; then Sum ((Len J)|i) <= Sum ((Len J)|(len Len J)) & (Len J)|(len Len J)=Len J & i-'1=i-1 by POLYNOM3:18,FINSEQ_1:79,BINARITH:50; then A15: i=i-'1+1 & Seg Sum ((Len J)|i) c= Seg Sum Len J by FINSEQ_1:7; defpred P[Nat] means $1 in Seg MIN & $1 <> MIN implies (F|^$1).(b1/.(S+1))=b1/.(S+$1+1); A16: P[0] by FINSEQ_1:3; A17: for n st P[n] holds P[n+1] proof let n such that A18: P[n];set n1=n+1; assume A19: n1 in Seg MIN & n1<>MIN; (Len J)|i=((Len J)|(i-'1))^<*MIN*> by A4,A13,A14,A15, FINSEQ_5:11; then A20: Sum ((Len J)|i)=S+MIN by RVSUM_1:104; n1<=MIN by A19,FINSEQ_1:3; then A21: n1=1; A25: 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 A25,FUNCT_1:23 .= b1/.(S+n1+1) by A23,VECTSP11:19,A24,A21,FINSEQ_1:3,A18; end; end; hence thesis; end; A26:for n holds P[n] from NAT_1:sch 2(A16,A17); A27:deg F >= MIN proof set D=deg F; assume A28: D < MIN; 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:33; hence thesis by A2,MATRLIN2:21; end; then D>=1 by NAT_1:14; then D in Seg MIN by A28,FINSEQ_1:3; then A29: b1/.(S+D+1) = (F|^D).(b1/.(S+1)) by A28,A26 .= ZeroMap(V1,V1).(b1/.(S+1)) by Def5 .= ((the carrier of V1)-->0.V1).(b1/.(S+1)) by GRCAT_1:def 12 .= 0.V1 by FUNCOP_1:13; 1<=1+D & D+1<=MIN by A28,NAT_1:11,13; then D+1 in Seg MIN; then S+(D+1) in Seg Sum ((Len J)|i) & rng b1 is Basis of V1 by A4,A13,A14,MATRIXJ1:10,MATRLIN:def 4; then b1/.(S+D+1)=b1.(S+D+1) & b1.(S+D+1) in rng b1 & rng b1 is linearly-independent Subset of V1 by PARTFUN1:def 8,FUNCT_1:def 5,A3,A15,VECTSP_7:def 3; hence thesis by A29,VECTSP_7:3; end; F|^MIN = ZeroMap(V1,V1) by A1,A5,A8,Th25; then deg F <= MIN by Def5; then deg F = MIN by A27,XXREAL_0:1; hence thesis by A8,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 w1,w2 be Vector of W1; thus F.(w1+w2) = (f|W1).w1+(f|W1).w2 by A1,MOD_2:def 5 .= F.w1+F.w2 by A1,VECTSP_4:21; end; 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 5 .= a*(F.w) by A1,VECTSP_4:22; end; hence thesis by A2,MOD_2:def 5; 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; 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)); set Lb=len b1; A4: Lb=0 proof assume Lb<>0; then A5: Lb in Seg Lb & dom b1=Seg Lb by FINSEQ_1:5,def 3; per cases by A3,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 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:27; hence thesis by NAT_1:13; end; end; reconsider J={} as FinSequence_of_Jordan_block of L,K by Th10; for x st x in dom J holds J.x is non empty; then reconsider J as non-empty FinSequence_of_Jordan_block of L,K by FUNCT_1:def 15; take J; len AutMt(F,b1,b2)=0 by A4,MATRIX_1:def 3; then AutMt(F,b1,b2)={} & block_diagonal(J,0.K)={} by MATRIXJ1:22; hence thesis; 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; set Lb=len b1; let F be linear-transformation of V1,V2 such that A9: n1 = Card {i where i is Element of NAT: i in dom b1 & F.(b1/.i) = L * (b2/.i)} and A10: 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 A9,CARD_4:1; consider x such that A11: x in FF by XBOOLE_0:def 1,A9,CARD_1:47; consider ii be Element of NAT such that A12: ii=x & ii in dom b1 & F.(b1/.ii) = L * (b2/.ii) by A11; A13: dom b1=Seg Lb & dom b1=dom b2 & Lb<>0 by A8,A12,FINSEQ_1:4,def 3,FINSEQ_3:31; then A14: Lb in dom b1 & not Lb+1 in dom b1 & Lb>0 by FINSEQ_1:5,FINSEQ_3:9; then F.(b1/.Lb)= L * (b2/.Lb) by A10; then A15: Lb in FF by A14; per cases; suppose A16: n=0; set J=Jordan_block(L,Lb); reconsider JJ=<*J*> as FinSequence_of_Jordan_block of L,K by Th11; now let x such that A17: x in dom JJ; dom JJ ={1} by FINSEQ_1:4,def 8; then JJ.1=J & x=1 & len J=Lb by A17,TARSKI:def 1,FINSEQ_1:def 8,Def1; hence JJ.x is non empty by A13; end; then reconsider JJ as non-empty FinSequence_of_Jordan_block of L,K by FUNCT_1:def 15; take JJ; A18: block_diagonal(JJ,0.K)=J by MATRIXJ1:34; 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); reconsider F'=F as Function of V1,V2; rng b1 c= [#]V1 & dom F=[#]V1 & dom T=[#]V1 by FINSEQ_1:def 4,FUNCT_2:def 1; then A19: dom (F'*b1)=dom b1 & dom (T*b1)=dom b1 by RELAT_1:46; now let y such that A20: y in dom b1; reconsider j=y as Element of NAT by A20; A21: (F'*b1).y=F.(b1.y) & (T*b1).y=T.(b1.y) & b1/.j=b1.j by A20,FUNCT_1:23,PARTFUN1:def 8; now per cases; suppose A22: j = Lb; hence (T*b1).y = L*(b2/.Lb) by A18,A20,A21,Th23 .= (F'*b1).y by A14,A10,A21,A22; end; suppose A23: j <> Lb; then A24: (T*b1).y = L*(b2/.j)+ b2/.(j+1) by A18,A20,A21,Th23; ex z be set st FF={z} by A9,A16,CARD_2:60; then FF={Lb} by A15,TARSKI:def 1; then not j in FF by A23,TARSKI:def 1; then F.(b1/.j) <> L * (b2/.j) by A20; hence (T*b1).y=(F'*b1).y by A20,A21,A24,A10; end; end; hence (F'*b1).y = (T*b1).y; end; then F=T by A14,MATRLIN:26,A19,FUNCT_1:9; hence AutMt(F,b1,b2)=block_diagonal(JJ,0.K) by MATRLIN2:36; end; suppose A25: n<>0; defpred Q[Nat] means $1 in FF & $1 < Lb; A26: for k st Q[k] holds k <= Lb; A27: ex k st Q[k] proof Card FF<>1 by A9,A25; then FF <> {Lb} by CARD_2:60; then consider y such that A28: y in FF & y <> Lb by A15,ZFMISC_1:41; consider j be Element of NAT such that A29: j=y & j in dom b1 & F.(b1/.j) = L * (b2/.j) by A28; take j; j<=Lb by A29,FINSEQ_3:27; hence thesis by A28,A29,XXREAL_0:1; end; consider m such that A30: Q[m] and A31: for k st Q[k] holds k<= m from NAT_1:sch 6(A26,A27); set b1m=b1|m; set b2m=b2|m; set b1'm=b1/^m; set b2'm=b2/^m; A32: len b1m=m & len b2m=m & len b1'm =Lb-m & len b2'm=Lb-m & Lb-m=Lb-'m by A8,A30,FINSEQ_1:80,RFINSEQ:def 2,BINARITH:50; reconsider Rb1=rng b1m, Rb1'=rng b1'm as linearly-independent Subset of V1 by MATRLIN2:22,23; reconsider Rb2=rng b2m, Rb2'=rng b2'm as linearly-independent Subset of V2 by MATRLIN2:22,23; set Lb1=Lin Rb1; set Lb2=Lin Rb2; set Lb1'=Lin Rb1'; set Lb2'=Lin Rb2'; reconsider b1m as OrdBasis of Lb1 by MATRLIN2:22; reconsider b1'm as OrdBasis of Lb1' by MATRLIN2:23; reconsider b2m as OrdBasis of Lb2 by MATRLIN2:22; reconsider b2'm as OrdBasis of Lb2' by MATRLIN2:23; A33: b1=b1m^b1'm & b2=b2m^b2'm by RFINSEQ:21; then A34: dom b1m c= dom b1 & dom b1'm = dom b2'm & dom b1m = dom b2m by A32,FINSEQ_1:39,FINSEQ_3:31; set FRb1=F.:Rb1; A35: the carrier of Lin(FRb1) = F.:(the carrier of Lb1) by VECTSP11:42; A36: 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 A37: i in dom b1m; A38: b1/.i=b1.i & b2/.i=b2.i & b2.i=b2m.i & b1.i=b1m.i & b1m.i=b1m/.i & b2m.i=b2m/.i & F.(b1m/.i)=(F|Lb1).(b1m/.i) by A13,A37,A33,A34,PARTFUN1:def 8,FINSEQ_1:def 7,FUNCT_1:72; set i1=i+1; per cases by A37,A10,A34; suppose F.(b1/.i) = L * (b2/.i); hence thesis by A38,VECTSP_4:22; end; suppose A39: i1 in dom b1 & F.(b1/.i) = L * (b2/.i) +b2/.i1; reconsider rngb2=rng b2 as Basis of V2 by MATRLIN:def 4; A40: i1<=m proof assume i1>m; then i>=m & i<=m & ex ii be Element of NAT st m=ii & ii in dom b1 & F.(b1/.ii) = L * (b2/.ii) by A30,A37,A32,NAT_1:13,FINSEQ_3:27; then i=m & F.(b1/.m)=L*(b2/.m) by XXREAL_0:1; then F.(b1/.i)=L*(b2/.i)+0.V2 by RLVECT_1:def 7; then b2/.i1=0.V2 & b2/.i1=b2.i1 & b2.i1 in rngb2 & rngb2 is linearly-independent by A13,A39,RLVECT_1:21,PARTFUN1:def 8, FUNCT_1:def 5,VECTSP_7:def 3; hence thesis by VECTSP_7:3; end; A41: 1<=i1 by NAT_1:11; then i1 in dom b1m by A40,A32,FINSEQ_3:27; then b2/.i1=b2.i1 & b2.i1=b2m.i1 & b2m.i1=b2m/.i1 & L*(b2/.i)=L*(b2m/.i) by A38,A13,A33,A34,PARTFUN1:def 8, FINSEQ_1:def 7,VECTSP_4:22; hence thesis by A38,A39,A41,VECTSP_4:21,A40,A32,FINSEQ_3:27; end; end; FRb1 c= the carrier of Lb2 proof let y such that A42: y in FRb1; consider x such that A43: x in dom F & x in Rb1 & F.x=y by A42,FUNCT_1:def 12; consider i be set such that A44: i in dom b1m & b1m.i=x by A43,FUNCT_1:def 5; reconsider i as Element of NAT by A44; b1m/.i=b1m.i by A44,PARTFUN1:def 8; then (F|Lb1).(b1m/.i)=y by A43,A44,FUNCT_1:72; then y=L * (b2m/.i) or y=L * (b2m/.i)+b2m/.(i+1) by A44,A36; hence thesis; end; then Lin(FRb1) is Subspace of Lb2 by VECTSP_9:20; then F.:(the carrier of Lb1) c= the carrier of Lb2 & rng (F|Lb1) = F.:(the carrier of Lb1) by A35,RELAT_1:148,VECTSP_4:def 2; then reconsider FL=F|Lb1 as linear-transformation of Lb1,Lb2 by FUNCT_2:8,Lm4; A45: 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 A36; set FF1={i where i is Element of NAT: i in dom b1m & FL.(b1m/.i) = L * (b2m/.i)}; A46: FF1 c= FF\{Lb} proof let x; assume x in FF1; then consider j be Element of NAT such that A47: x=j & j in dom b1m & FL.(b1m/.j) = L * (b2m/.j); b1m/.j=b1m.j & b2m/.j=b2m.j & b1m.j=b1.j & b2m.j=b2.j & FL.(b1m/.j)=F.(b1m/.j) & b2/.j=b2.j & b1/.j=b1.j by A13,A33,A34,A47,PARTFUN1:def 8,FINSEQ_1:def 7,FUNCT_1:72; then F.(b1/.j)=L * (b2/.j) by A47,VECTSP_4:22; then A48: j in FF by A47,A34; j<=m by A47,A32,FINSEQ_3:27; hence thesis by A47,A48,A30,ZFMISC_1:64; end; FF\{Lb} c= FF1 proof let x such that A49: x in FF\{Lb}; A50: x in FF & x <> Lb by A49,ZFMISC_1:64; then consider j be Element of NAT such that A51: j=x & j in dom b1 & F.(b1/.j) = L * (b2/.j); j<=Lb by A51,FINSEQ_3:27; then j as FinSequence_of_Jordan_block of L,K by Th11; set JJJ=J^JJ; now let x such that A54: x in dom JJJ; reconsider i=x as Nat by A54; per cases by A54,FINSEQ_1:38; suppose i in dom J; then J.i is non empty & JJJ.i=J.i by FINSEQ_1:def 7,FUNCT_1:def 15; hence JJJ.x is non empty; end; suppose ex j st j in dom JJ & i=len J + j; then consider j such that A55: j in dom JJ & i=len J+j; dom JJ=Seg 1 by FINSEQ_1:55; then j=1 & len JB=Lb-'m by A55,FINSEQ_1:4,TARSKI:def 1,Def1; then JJJ.i=JJ.1 & JJ.1=JB & len JB<>0 by A30,A32,A55,FINSEQ_1:def 7,FINSEQ_1:57; hence JJJ.x is non empty; end; end; then reconsider JJJ as non-empty FinSequence_of_Jordan_block of L,K by FUNCT_1:def 15; take JJJ; reconsider JB as Matrix of len b1'm,len b2'm,K by A32; A56: block_diagonal(JJJ,0.K)=block_diagonal(<*B,JB*>,0.K) & Sum Len <*B,JB*> = len B + len JB & Sum Width <*B,JB*> = width B + width JB & len B=len b1m & len JB = len b1'm & width B=len b1m & width JB = len b1'm by MATRIX_1:25,MATRIXJ1:16,20,35,A32; then reconsider BB=block_diagonal(<*B,JB*>,0.K) as Matrix of len b1,len b2,K by A8,A32; set T=Mx2Tran(BB,b1,b2); reconsider F'=F as Function of V1,V2; rng b1 c= [#]V1 & dom F=[#]V1 & dom T=[#]V1 by FINSEQ_1:def 4,FUNCT_2:def 1; then A57: dom (F'*b1)=dom b1 & dom (T*b1)=dom b1 by RELAT_1:46; now let x such that A58: x in dom b1; reconsider I=x as Element of NAT by A58; A59: (F'*b1).x=F.(b1.I) & (T*b1).x=T.(b1.I) & b1.I=b1/.I by A58,FUNCT_1:23,PARTFUN1:def 8; now per cases by A58,A33,FINSEQ_1:38; suppose A60: I in dom b1m; then A61: b1m/.I = b1m.I & FL.(b1m/.I) =F.(b1m/.I) & b1.I=b1m.I by A33,PARTFUN1:def 8,FUNCT_1:72,FINSEQ_1:def 7; thus (T*b1).x = Mx2Tran(B,b1m,b2m).(b1m/.I) by A56,A33,Th19,A32,A59,A60 .= FL.(b1m/.I) by A53,MATRLIN2:34 .= (F'*b1).x by A61,A58,FUNCT_1:23; end; suppose ex j st j in dom b1'm & I=len b1m + j; then consider j such that A62: j in dom b1'm & I=len b1m + j; now per cases; suppose A63: j=len b1'm; A64: b2'm/.j=b2'm.j & b2.I = b2'm.j & b2/.I=b2.I by A13,A33,A58,A62,A34,PARTFUN1:def 8,A32, FINSEQ_1:def 7; thus (F'*b1).x = L*(b2/.I) by A59,A63,A14,A10,A62,A32 .= L*(b2'm/.j) by A64,VECTSP_4:22 .= Mx2Tran(JB,b1'm,b2'm).(b1'm/.j) by A63,A62,Th23; end; suppose A65: j<>len b1'm; j<=len b1'm by A62,FINSEQ_3:27; then j L*(b2/.I) + b2/.(I+1); then F.(b1/.I)=L*(b2/.I) & I<>Lb & I<=Lb by A10,A58,A59,A62,A65,A32,FINSEQ_3:27; then I in FF & I < Lb by A58,XXREAL_0:1; then len b1m + j<=len b1m+0 by A62,A31,A32; then j<=0 by XREAL_1:8; hence thesis by A62,FINSEQ_3:27; end; hence (F'*b1).x=Mx2Tran(JB,b1'm,b2'm).(b1'm/.j) by A66; end; end; hence (F'*b1).x=(T*b1).x by A56,A33,Th19,A32,A59,A62; end; end; hence (F'*b1).x=(T*b1).x; end; then F=T by A14,MATRLIN:26,A57,FUNCT_1:9; hence AutMt(F,b1,b2)=block_diagonal(JJJ,0.K) by A56,MATRLIN2:36; end; end; A67:for n holds P[n] from NAT_1:sch 2(A1,A6); let V1,V2,b1,b2,L such that A68:len b1 = len b2; let F be linear-transformation of V1,V2 such that A69: 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;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; P[card FF] by A67; hence thesis by A68,A69; 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; A1:P[0] proof let V1 be finite-dimensional VectSp of K; let F be nilpotent linear-transformation of V1,V1 such that A2:deg F=0; reconsider J={} as FinSequence_of_Jordan_block of 0.K,K by Th10; consider b1 be OrdBasis of V1; take J,b1; [#]V1 = {0.V1} by A2,Th15 .= the carrier of (0).V1 by VECTSP_4:def 3; then (0).V1 = (Omega).V1 by VECTSP_4:37; then 0 = dim V1 by VECTSP_9:33 .= len b1 by MATRLIN2:21 .= len AutMt(F,b1,b1) by MATRIX_1:def 3; hence AutMt(F,b1,b1) = {} .= block_diagonal(J,0.K) by MATRIXJ1:22; thus thesis; end; A3:for n st P[n] holds P[n+1] proof let n such that A4: P[n];set n1=n+1; let V1 be finite-dimensional VectSp of K; let F be nilpotent linear-transformation of V1,V1 such that A5: deg F=n1; 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 A5,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 A4; A8: FI=Mx2Tran(AutMt(FI,b1,b1),b1,b1) by MATRLIN2:34; A9: len b1 = len AutMt(FI,b1,b1) by MATRIX_1:def 3 .= Sum Len J by A6,MATRIXJ1:def 5; then A10: dom b1= Seg Sum Len J by FINSEQ_1:def 3; set LJ=Len J; set S=Sum LJ; set L=len J; defpred Q[Nat,Nat] means $2 in dom LJ & $2 <= $1 & Sum(LJ|($2-'1)) <= $1-'$2; defpred R[set,set] 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; A11: for x st x in Seg(S+L) ex y st y in NAT & R[x,y] proof let x such that A12: x in Seg (S+L); reconsider i=x as Nat by A12; defpred q[Nat] means $1 in dom LJ & $1 <= i & Sum(LJ|($1-'1)) <= i-'$1; A13: for k st q[k] holds k <= L proof let k;assume q[k]; then k<=len LJ & len LJ=L by FINSEQ_3:27,FINSEQ_2:109; hence thesis; end; 1-'1=0 & 0<=len LJ by BINARITH:51; then A14: Sum(LJ|(1-'1))=0 & 0<=i-'1 by RVSUM_1:102; L<>0 proof assume A15: L=0; then LJ=<*>NAT by FINSEQ_2:113; hence thesis by A12,A15,RVSUM_1:102,FINSEQ_1:4; end; then 1<=L & len LJ=L by NAT_1:14,FINSEQ_2:109; then 1 in dom LJ & 1<=i by A12,FINSEQ_3:27,FINSEQ_1:3; then A16: ex k st q[k] by A14; consider k such that A17: q[k] and A18: for n st q[n] holds n <= k from NAT_1:sch 6(A13,A16); take k; thus k in NAT by ORDINAL1:def 13; let i',k' be Nat such that A19: i'=x & k'=k; i-'k <= Sum (LJ|k) proof assume A20: i-'k > Sum (LJ|k); then i-'k >= Sum (LJ|k)+1 by NAT_1:13; then A21: i-'k-1>=Sum (LJ|k)+1-1 by XREAL_1:11; A22: i-'k>=1 & i-'k=i-k by A17,A20,NAT_1:14,BINARITH:50; then A23: i-k+k >=1+k by XREAL_1:8; then A24: i-'(k+1)=i-(k+1) & k+1-'1=k by BINARITH:39,50; A25: k+1<=len LJ proof assume k+1>len LJ; then A26: k>=len LJ & len LJ=L by NAT_1:13,FINSEQ_2:109; then i-k>S by A20,A22,FINSEQ_1:79; then i-k+k>S+k & S+k>=S+L by A26,XREAL_1:8; then i> S+L by XXREAL_0:2; hence thesis by A12,FINSEQ_1:3; end; 1<=k+1 by NAT_1:14; then k+1 in dom LJ & k+1 <=i & Sum(LJ|(k+1-'1)) <= i-'(k+1) by A21,A22,A23,A24,A25,FINSEQ_3:27; then k+1<=k by A18; hence thesis by NAT_1:13; end; hence thesis by A17,A18,A19; end; consider r be Function of Seg (S+L),NAT such that A27: for x st x in Seg (S+L) holds R[x,r.x] from FUNCT_2:sch 1(A11); A28: dom r=Seg (S+L) by FUNCT_2:def 1; defpred P[set,set] 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)))); A29: for x st x in Seg (S+L) ex y st y in the carrier of V1 & P[x,y] proof let x such that A30: x in Seg (S+L); reconsider i=x as Nat by A30; r.i=r/.i by A30,A28,PARTFUN1:def 8; then reconsider k=r.i as Element of NAT; A31: Q[i,k] & i-'k <= Sum (LJ|k) by A30,A27; k<=len LJ by A31,FINSEQ_3:27; then A32: Sum (LJ|k) <= Sum (LJ|(len LJ)) & LJ|(len LJ) =LJ by POLYNOM3:18,FINSEQ_1:79; dom LJ=dom J by MATRIXJ1:def 3; then A33: LJ.k =len (J.k) & LJ.k <> 0 by A7,A31,MATRIXJ1:def 3; 1<=k by A31,FINSEQ_3:27; then A34: k-'1=k-1 by BINARITH:50; then k=k-'1+1; then LJ|k=(LJ|(k-'1))^<*LJ.k*> by A31,FINSEQ_5:11; then A35: Sum (LJ|k)=Sum (LJ|(k-'1)) + len (J.k) by A33,RVSUM_1:104; per cases; suppose A36: i -' k = Sum (LJ|(k-'1)); then i-'k <> Sum (LJ|k) by A33,A35; then i-'k < Sum (LJ|k) by A31,XXREAL_0:1; then i-'k+1 <=Sum(LJ|k) by NAT_1:13; then A37: 1<= i-'k+1 & i-'k+1 <= S by A32,XXREAL_0:2,NAT_1:11; then i-'k+1 in dom b1 by A10; then A38: b1/.(i-'k+1) = b1.(i-'k+1) by PARTFUN1:def 8; b1/.(i-'k+1) in IM & b1/.(i-'k+1) is Element of V1 by STRUCT_0:def 5,VECTSP_4:18; then consider y be Element of V1 such that A39: (F|^1).y=b1/.(i-'k+1) by RANKNULL:13; take y; thus y in the carrier of V1; thus thesis by A10,A36,A37,A38,A39,VECTSP11:19; end; suppose A40: i -' k <> Sum (LJ|(k-'1)); then i -' k>Sum (LJ|(k-'1)) by A31,XXREAL_0:1; then 1<= i-'k & i-'k <= S by NAT_1:14,A31,A32,XXREAL_0:2; then A41: i-'k in dom b1 by A10; take y=b1/.(i-'k); y in IM by STRUCT_0:def 5; then y in V1 by VECTSP_4:17; hence y in the carrier of V1 by STRUCT_0:def 5; let i',k' be Nat such that A42: x=i' & k'=r.i'; i-'k <= Sum (LJ|k) by A30,A27; then A43: min(LJ,i-'k)<=k by A41,A10,MATRIXJ1:def 1; A44: min(LJ,i-'k)=k proof assume min(LJ,i-'k)<>k; then min(LJ,i-'k) Sum (LJ|(k-'1)) & i-'k = Sum (LJ|k)}; A54: RA c= the carrier of V1 proof let x;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;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 A54; A55: Carrier l c= RB\/RA proof let x such that A56: x in Carrier l; reconsider v1=x as Vector of V1 by A56; Carrier l c= RNG by VECTSP_6:def 7; then consider i be set such that A57: i in dom B & B.i=v1 by A56,FUNCT_1:def 5; reconsider i as Nat by A57; r.i=r/.i by A57,A52,A28,PARTFUN1:def 8; then reconsider k=r.i as Element of NAT; A58: i-'k <= Sum (LJ|k) by A27,A57,A52; per cases by A58,XXREAL_0:1; suppose A59: i-'k = Sum (LJ|k); A60: Q[i,k] by A57,A52,A27; then 1<=k by FINSEQ_3:27; then k-'1=k-1 by BINARITH:50; then k-'1+1=k; then LJ|k=(LJ|(k-'1))^<*LJ.k*> & dom LJ=dom J by A60,FINSEQ_5:11,MATRIXJ1:def 3; then i-'k = Sum (LJ|(k-'1))+LJ.k & LJ.k<>0 by A7,A59,A60,RVSUM_1:104; then i-'k <>Sum (LJ|(k-'1)); then v1 in RB or v1 in RA by A57,A59,A52; hence thesis by XBOOLE_0:def 2; end; suppose i-'k < Sum (LJ|k); then v1 in RB or v1 in RA by A57,A52; hence thesis by XBOOLE_0:def 2; end; end; A61: F|RA is one-to-one proof let x1,x2 be set such that A62: x1 in dom (F|RA) & x2 in dom (F|RA) & (F|RA).x1=(F|RA).x2; dom(F|RA)=dom F /\ RA by FUNCT_1:68; then A63: x1 in RA & x2 in RA & (F|RA).x1=F.x1 & (F|RA).x2=F.x2 by A62,XBOOLE_0:def 3,FUNCT_1:70; then consider v1 be Vector of V1 such that A64: x1=v1 and A65: 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 A66: i1 in Seg(L+S) & k1=r.i1 & v1=B.i1 & i1-'k1 < Sum (LJ|k1) by A65; consider v2 be Vector of V1 such that A67: x2 = v2 and A68: ex i2,k2 be Nat st i2 in Seg(L+S) & k2=r.i2 & v2=B.i2 & i2-'k2 < Sum (LJ|k2) by A63; consider i2,k2 be Nat such that A69: i2 in Seg(L+S) & k2=r.i2 & v2=B.i2 & i2-'k2 < Sum (LJ|k2) by A68; A70: b1 is one-to-one by MATRLIN:def 4; A71: k1<=i1 & k2<=i2 & k1 in dom LJ & k2 in dom LJ by A66,A69,A27; then A72: i1-'k1=i1-k1 & i2-'k2=i2-k2 & 1<=k1 & 1<=k2 by BINARITH:50,FINSEQ_3:27; then A73: k1-'1=k1-1 & k2-'1=k2-1 by BINARITH:50; then k1-'1+1<=len LJ & k2-'1+1<=len LJ by A71,FINSEQ_3:27; then A75: k1-'1 <=len LJ & k2-'1 <=len LJ by NAT_1:13; A76: dom LJ=dom J by MATRIXJ1:def 3; A77: k1-'1 in dom LJ implies LJ.(k1-'1)<>0 by A7,A76; A78: k2-'1 in dom LJ implies LJ.(k2-'1)<>0 by A7,A76; per cases; suppose A81: i1-'k1=Sum (LJ|(k1-'1)) & i2-'k2=Sum (LJ|(k2-'1)); then F.v1=b1.(i1 -' k1+1) & i1 -' k1+1 in dom b1 & F.v2=b1.(i2 -' k2+1) & i2 -' k2+1 in dom b1 by A66,A69,A51; then i1-'k1+1=i2-'k2+1 by A62,A63,A64,A67,A70,FUNCT_1:def 8; then k1-'1=k2-'1 by A75,A81,A77,A78,MATRIXJ1:11; then i1-k1=i2-k1 by A72,A73,A81; hence thesis by A64,A66,A67,A69; end; suppose A82: i1-'k1=Sum (LJ|(k1-'1)) & i2-'k2<>Sum (LJ|(k2-'1)); then A83: F.v1=b1.(i1-'k1+1) & i1-'k1+1 in dom b1 & F.v2=b1.(i2-'k2+1)& i2-'k2+1 in dom b1 & min(LJ,i2-'k2)=k2 by A66,A69,A51; then A84: i1-'k1+1=i2-'k2+1 by A62,A63,A64,A67,A70,FUNCT_1:def 8; k1-'1 <>0 proof assume k1-'1=0; then LJ|(k1-'1)=<*>REAL; hence thesis by A82,A27,A69,A84,RVSUM_1:102; end; then k1-'1 >=1 by NAT_1:14; then A85: k1-'1 in dom LJ by A75,FINSEQ_3:27; then LJ.(k1-'1)<>0 by A76,A7; hence thesis by A69,A82,A84,A83,A85,MATRIXJ1:6; end; suppose A86: i1-'k1<>Sum (LJ|(k1-'1)) & i2-'k2=Sum (LJ|(k2-'1)); then A87: F.v1=b1.(i1-'k1+1) & i1-'k1+1 in dom b1 & F.v2=b1.(i2-'k2+1) & i2-'k2+1 in dom b1 & min(LJ,i1-'k1)=k1 by A66,A69,A51; then A88: i1-'k1+1=i2-'k2+1 by A62,A63,A64,A67,A70,FUNCT_1:def 8; k2-'1 <>0 proof assume k2-'1=0; then i1-'k1 =0 by A86,A88,RVSUM_1:102; hence thesis by A86,A27,A66; end; then k2-'1 >=1 by NAT_1:14; then A89: k2-'1 in dom LJ by A75,FINSEQ_3:27; then LJ.(k2-'1)<>0 by A76,A7; hence thesis by A66,A86,A88,A87,A89,MATRIXJ1:6; end; suppose i1-'k1<>Sum (LJ|(k1-'1)) & i2-'k2<>Sum (LJ|(k2-'1)); then A90: F.v1=b1.(i1-'k1+1) & i1-'k1+1 in dom b1 &min(LJ,i2-'k2)=k2& F.v2=b1.(i2-'k2+1) & i2-'k2+1 in dom b1 & min(LJ,i1-'k1)=k1 by A66,A69,A51; then i1-'k1+1=i2-'k2+1 by A62,A63,A64,A67,A70,FUNCT_1:def 8; then i1 - k1 =i2-k1 by A90,A72; hence thesis by A64,A66,A67,A69; end; end; rng b1 is Basis of IM by MATRLIN:def 4; 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:15; F.:RA c= rngb1 proof let y; assume y in F.:RA; then consider x such that A91: x in dom F & x in RA & y=F.x by FUNCT_1:def 12; consider v1 be Vector of V1 such that A92: x=v1 and A93: ex i,k st i in Seg(L+S) & k=r.i & v1=B.i&i-'k < Sum (LJ|k) by A91; consider i,k such that A94: i in Seg(L+S) & k=r.i & v1=B.i & i-'k < Sum (LJ|k) by A93; 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 A94,A51; hence thesis by A91,A92,FUNCT_1:def 5; end; then A95: F.:RA is linearly-independent Subset of V1 by VECTSP_7:2; A96: F.:RB c= {0.V1} proof let y; assume y in F.:RB; then consider x such that A97: x in dom F & x in RB & y=F.x by FUNCT_1:def 12; consider v1 be Vector of V1 such that A98: x=v1 and A99: 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 A97; F.v1= 0.V1 by A51,A99; hence thesis by A97,A98,TARSKI:def 1; end; A100: Carrier l c= RB by A53,A55,A61,A95,A96,VECTSP11:44; RB c= rngb1 proof let x; assume x in RB; then consider v1 be Vector of V1 such that A101: x=v1 and A102: 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 A103: i in Seg(L+S) & k=r.i & v1=B.i & i-'k <> Sum (LJ|(k-'1)) & i-'k = Sum (LJ|k) by A102; v1= b1.(i -' k) & i-'k in dom b1 by A103,A51; hence thesis by A101,FUNCT_1:def 5; end; then Carrier l c= rngb1 by A100,XBOOLE_1:1; then l is Linear_Combination of rngb1 by VECTSP_6:def 7; hence Carrier l ={} by A53,VECTSP_7:def 1; end; then A104: RNG is linearly-independent Subset of V1 by VECTSP_7:def 1; consider BAS be Basis of V1; A105: BAS is linearly-independent & Lin(BAS) = the VectSpStr of V1 by VECTSP_7:def 3; then reconsider BAS,RNG as finite Subset of V1 by VECTSP_9:25; A106: (Omega).Lin(BAS) = (Omega).V1 by VECTSP_7:def 3; consider C be finite Subset of V1 such that A107: C c= BAS & card C = card BAS - card RNG and A108: the VectSpStr of V1= Lin(RNG\/C) by A104,A105,VECTSP_9:23; A109: dim V1= dim Lin(RNG\/C) & dim V1 =dim Lin BAS & dim Lin BAS=card BAS by A105,A108,VECTSP_9:30,32,A106; then A110: card (RNG\/C) >= card BAS by MATRLIN2:6; A111: card (RNG\/C) = card RNG + card C - card (RNG/\C) by CARD_2:64 .= card BAS-card (RNG/\C) by A107; then card (RNG\/C)+card (RNG/\C) =card BAS; then card (RNG\/C) <= card BAS by NAT_1:11; then A112: card (RNG\/C) = card BAS & RNG\/C is linearly-independent by A109,A110,XXREAL_0:1,MATRLIN2:5; 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; A113:W[0] proof assume 0<= card C; card C=card Seg card C by FINSEQ_1:78; then Seg card C,C are_equipotent by CARD_1:21; then consider f be Function such that A114: f is one-to-one & dom f = Seg card C & rng f = C by WELLORD2:def 4; reconsider f as FinSequence by A114,FINSEQ_1:def 2; reconsider f as FinSequence of V1 by A114,FINSEQ_1:def 4; take f; thus f is one-to-one & len f = card C by A114,FINSEQ_1:def 3; RNG/\C={} by A111,A112; hence RNG misses rng f & RNG\/rng f is Basis of V1 by A108,A112,A114,XBOOLE_0:def 7,VECTSP_7:def 3; let i;assume i in dom f & i<=0; hence thesis by FINSEQ_3:27; end; A115:for n st W[n] holds W[n+1] proof let n such that A116: W[n];set n1=n+1; assume A117: n1<=card C; then consider f be FinSequence of V1 such that A118: f is one-to-one and A119: len f = card C and A120: RNG misses rng f & RNG\/rng f is Basis of V1 and A121: for i st i in dom f & i<= n holds F.(f.i)=0.V1 by A116,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 A121,NAT_1:8; hence thesis by A118,A119,A120; end; suppose A122: F.(f.n1)<>0.V1; A123: rng b1 c= F.:RNG proof let y such that A124: y in rng b1; consider x such that A125: x in dom b1 & b1.x=y by A124,FUNCT_1:def 5; reconsider x as Element of NAT by A125; set m=min(LJ,x); set x1=x-'1; set mx=m+x1; A126: m in dom LJ by A125,A10,MATRIXJ1:def 1; then 1<=m & m<=len LJ & len LJ=L & 1<=x & x<=S by A125,A9,FINSEQ_2:109,FINSEQ_3:27; then A127: 1+1<=m+x & m+x<=L+S & x1=x-1 by XREAL_1:9,BINARITH:50; then 2-1<=m+x-1 & m+x-1<=L+S-1 & L+S-1<=L+S-0 by XREAL_1:11,12; then 1<=mx & mx<=L+S by A127,XXREAL_0:2; then A128: mx in Seg (S+L); then r.mx=r/.mx by A28,PARTFUN1:def 8; then reconsider k=r.mx as Element of NAT; A129: Q[mx,k] by A27,A128; A130: m<=mx by NAT_1:11; then A131: mx-'m=mx-m & mx-'k =mx-k & Sum(LJ|(m-'1))< x1+1 &x<= Sum(LJ|m) by A10,A125,A127,A129,BINARITH:50,MATRIXJ1:7,def 1; then Sum(LJ|(m-'1))<= mx-'m by NAT_1:13; then A132: m<=k by A126,A27,A128,A130; A133: m=k proof assume A134: m<>k; then A135: mmx-'m by A128,A131,A27,A134,A132,POLYNOM3:18,BINARITH:59; then Sum(LJ|m) <=mx-'k & mx-'k< mx-'m by XXREAL_0:1,2; then Sum(LJ|m)<=x1 by A131,XXREAL_0:2; hence thesis by A127,A131,NAT_1:13; end; mx-'mSum(LJ|(m-'1))) by A131,A127,NAT_1:13; then F.(B.mx)= b1.(mx-'m+1) & mx-'m+1 =x & B.mx in RNG & dom F=[#]V1 by A51,A52,A127,A128,A131,A133, FUNCT_1:def 5,FUNCT_2:def 1; hence thesis by A125,FUNCT_1:def 12; end; reconsider rngB1=rng b1 as Basis of IM by MATRLIN:def 4; 1<=n1 by NAT_1:14; then A136: n1 in dom f by A117,A119,FINSEQ_3:27; then A137: f/.n1=f.n1 & f.n1 in rng f by PARTFUN1:def 8,FUNCT_1:def 5; 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 A138: F.(f/.n1) = Sum L by VECTSP_7:12; consider K be Linear_Combination of V1 such that A139: Carrier L=Carrier K & Sum L=Sum K by VECTSP_9:12; Carrier L c= rngB1 by VECTSP_6:def 7; then consider M be Linear_Combination of RNG such that A140: F.(Sum M)=Sum K by VECTSP11:41,A139,A123,XBOOLE_1:1; reconsider Rf=RNG\/rng f as finite Subset of V1 by A120; A141: Rf is linearly-independent by A120,VECTSP_7:def 3; set fn=f/.n1; A142: fn in Rf by A137,XBOOLE_0:def 2; RNG c= Rf & not fn in RNG by A137,A120,XBOOLE_1:7,XBOOLE_0:3; then Carrier M c= RNG & Carrier M=Carrier(-M) & RNG c= Rf\{fn} by VECTSP_6:def 7,69,ZFMISC_1:40; then Carrier(-M) c= Rf\{fn} by XBOOLE_1:1; then reconsider M'=-M as Linear_Combination of Rf\{fn} by VECTSP_6:def 7; set fnM=fn+Sum(M'); set fnS=n1 .--> fnM; take ff=f+*(n1,fnM); A143: not fnM in Rf\{fn} proof card Rf <>0 by A137; then reconsider c1=card Rf-1 as Element of NAT by NAT_1:20; assume A144: fnM in Rf\{fn}; c1+1=card Rf; then card (Rf\{fn})= c1 & Rf\{fn}\/ {fnM} = Rf\{fn} & card (Rf\{fn}\/ {fnM})=c1+1 by A144,A142,VECTSP11:40,A141,STIRL2_1:65,ZFMISC_1:46; hence thesis; end; A145: fnM <> fn proof assume fnM=fn; then 0.V1 = fnM-fn by VECTSP_1:63 .= Sum(M')+(fn-fn) by RLVECT_1:def 6 .= Sum(M')+0.V1 by RLVECT_1:def 11 .= Sum(M') by RLVECT_1:def 7 .= -Sum(M) by VECTSP_6:79; then 0.V1=Sum(M) by VECTSP_1:86; hence thesis by A122,A137,A138,A139,A140,RANKNULL:9; end; not fnM in rng f proof assume fnM in rng f; then fnM in Rf by XBOOLE_0:def 2; hence thesis by A143,A145,ZFMISC_1:64; end; then rng f misses {fnM} & rng fnS={fnM} by ZFMISC_1:56,FUNCOP_1:14; then f+*(fnS) is one-to-one by A118,FUNCT_4:98; hence ff is one-to-one by A136,FUNCT_7:def 3; A146: dom ff=dom f by FUNCT_7:32; hence len ff=card C by A119,FINSEQ_3:31; A147: rng ff = (rng f)\{fn} \/{fnM} by Lm1,A118,A136,A137; thus RNG misses rng ff proof assume RNG meets rng ff; then consider x such that A148: x in RNG & x in rng ff by XBOOLE_0:3; not x in (rng f)\{fn} by A148,A120,XBOOLE_0:3; then x in {fnM} by A148,A147,XBOOLE_0:def 2; then x = fnM & not fnM in Rf by A143,A145,TARSKI:def 1,ZFMISC_1:64; hence thesis by A148,XBOOLE_0:def 2; end; A149: not fn in RNG by A120,A137,XBOOLE_0:3; A150: Rf\{fn}\/{fnM} = (RNG\{fn})\/((rng f)\{fn})\/{fnM} by XBOOLE_1:42 .= RNG\/((rng f)\{fn})\/{fnM} by A149,ZFMISC_1:65 .= RNG\/ rng ff by A147,XBOOLE_1:4; then reconsider Rff=RNG\/ rng ff as finite Subset of V1; A151: Rf\{fn}\/{fnM} is linearly-independent by A141,A142,VECTSP11:40; dim V1 = card Rf by A120,VECTSP_9:def 2 .= card (RNG\/ rng ff) by A141,A142,A150,VECTSP11:40; then dim Lin(Rff)=dim V1 by A150,A141,A142,VECTSP11:40,VECTSP_9:30; then (Omega).V1=(Omega).Lin(Rff) by VECTSP_9:32; hence RNG\/ rng ff is Basis of V1 by A150,A151,VECTSP_7:def 3; let i such that A152: i in dom ff & i<= n1; per cases by A152,XXREAL_0:1; suppose i 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 A51,A52,A157; A162: i2 -' k2 = Sum (LJ|(k2-'1)) implies F.(B.x2) = b1.(i2 -' k2+1) & i2-'k2+1 in dom b1 by A51,A52,A157; A163: 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 A51,A52,A157; A164: b1 is one-to-one & rng b1 is Basis of IM by MATRLIN:def 4; then A165: rng b1 is linearly-independent Subset of IM by VECTSP_7:def 3; 1<=k1 & k1<= len LJ & 1<=k2& k2 <= len LJ & k1-'1 <= k1 & k2-'1<=k2 by A158,A159,FINSEQ_3:27,BINARITH:52; then A166: k1-'1=k1-1 & k2-'1=k2-1 & i1-'k1 =i1-k1 & i2-'k2=i2-k2 & k1-'1 <=len LJ & k2-'1 <=len LJ by A158,A159,XXREAL_0:2,BINARITH:50; A167: dom LJ=dom J & 0<=len LJ by MATRIXJ1:def 3; now per cases by A158,A159,XXREAL_0:1; suppose A168: i1 -' k1 = Sum (LJ|(k1-'1)) & i2 -' k2 = Sum (LJ|(k2-'1)); then F.(B.x1) = b1.(i1 -' k1+1) & i1-'k1+1 in dom b1 & F.(B.x2) = b1.(i2 -' k2+1) & i2-'k2+1 in dom b1 by A51,A52,A157; then A169: i1-'k1+1 = i2-'k2+1 by A164,A157,FUNCT_1:def 8; then Sum (LJ|(k1-'1)) = Sum (LJ|(k2-'1)) & (k1-'1 in dom LJ implies LJ.(k1-'1)<>0) & (k2-'1 in dom LJ implies LJ.(k2-'1)<>0) by A168,A167,A7; then k1-'1 = k2-'1 by A166,MATRIXJ1:11; hence i1=i2 by A169,A166; end; suppose A170: i1 -' k1 = Sum (LJ|(k1-'1)) & i2 -' k2 <> Sum (LJ|(k2-'1))& i2-'k2 < Sum (LJ|k2); then A171: F.(B.x1) = b1.(i1-'k1+1) & i1-'k1+1 in dom b1 & F.(B.x2) = b1.(i2-'k2+1) & i2-'k2+1 in dom b1 & min(LJ,i2-'k2)=k2 by A51,A52,A157; then A172: i1-'k1+1 = i2-'k2+1 by A164,A157,FUNCT_1:def 8; k1-'1 <>0 proof assume k1-'1=0; then LJ|(k1-'1)=<*>REAL; hence thesis by A170,A27,A52,A157,A172,RVSUM_1:102; end; then k1-'1 >=1 by NAT_1:14; then A173: k1-'1 in dom LJ by A166,FINSEQ_3:27; then LJ.(k1-'1)<>0 by A167,A7; hence i1=i2 by A170,A172,A171,A173,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 A157,FUNCT_1:def 5,VECTSP_4:19,A160,A163; hence i1 = i2 by A165,VECTSP_7:3; end; suppose A174: i2 -' k2 = Sum (LJ|(k2-'1)) & i1 -' k1 <> Sum (LJ|(k1-'1)) & i1-'k1 < Sum (LJ|k1); then A175: F.(B.x2) = b1.(i2 -' k2+1) & i2-'k2+1 in dom b1 & F.(B.x1) = b1.(i1 -' k1+1) & i1-'k1+1 in dom b1 & min(LJ,i1-'k1)=k1 by A51,A52,A157; A176: i2-'k2+1 = i1-'k1+1 by A175,A164,A157,FUNCT_1:def 8; k2-'1 <>0 proof assume k2-'1=0; then i1-'k1 =0 by A174,A176,RVSUM_1:102; hence thesis by A174,A27,A52,A157; end; then k2-'1 >=1 by NAT_1:14; then A177: k2-'1 in dom LJ by A166,FINSEQ_3:27; then LJ.(k2-'1)<>0 by A167,A7; hence i1=i2 by A174,A176,A175,A177,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 A157,FUNCT_1:def 5,VECTSP_4:19,A162,A161; hence i1= i2 by A165,VECTSP_7:3; end; suppose A178: i1 -' k1 <> Sum (LJ|(k1-'1)) & i2 -' k2 <> Sum (LJ|(k2-'1)); then i2-'k2 = i1-'k1 by A161,A163,A164,A157,FUNCT_1:def 8; then i2-k1=i1-k1 by A178,A166,A161,A51,A52,A157; hence i1=i2; end; end; hence x1=x2; end; then B is one-to-one by FUNCT_1:def 8; then B^f is one-to-one & rng (B^f)=rng B\/rng f by A153,A155,FINSEQ_1:44,FINSEQ_3:98; then reconsider Bf=B^f as OrdBasis of V1 by A155,MATRLIN:def 4; 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 A179: i in dom Bf; A180: Bf/.i=Bf.i by A179,PARTFUN1:def 8; per cases by A179,FINSEQ_1:38; suppose A181: i in dom B; r/.i=r.i by A28,A52,A181,PARTFUN1:def 8; then reconsider k=r.i as Element of NAT; A182: Q[i,k] & i-'k <= Sum (LJ|k) by A27,A52,A181; 1<=k by FINSEQ_3:27,A182; then k-'1=k-1 by BINARITH:50; then k-'1+1=k; then LJ|k=(LJ|(k-'1))^<*LJ.k*> & dom LJ=dom J by A182,FINSEQ_5:11,MATRIXJ1:def 3; then A183: Sum(LJ|k) = Sum (LJ|(k-'1))+LJ.k & LJ.k<>0 by A7,A182,RVSUM_1:104; per cases by A182,XXREAL_0:1; suppose A184: i -' k = Sum (LJ|k); A185: i-'k <>Sum (LJ|(k-'1)) by A183,A184; F.(Bf/.i) = F.(B.i) by A181,A180,FINSEQ_1:def 7 .= 0.V1 by A185,A51,A52,A181,A184 .= 0.K*(Bf/.i) by VECTSP_1:59; hence thesis; end; suppose A186: i -' k < Sum (LJ|k); then A187: i-'k+1<=Sum(LJ|k) & Sum(LJ|(k-'1)) Sum (LJ|(k-'1)); then A188: F.(B.i)=b1.(i -' k+1) & i-'k+1 in dom b1 & dom J=dom LJ by A51,A52,A181,A186,MATRIXJ1:def 3; then A189: 1<=i-'k+1 & i-'k+1<=S & k <= L & i-'k=i-k by A9,A182,FINSEQ_3:27,BINARITH:50; then 1+0<= i-k+1+k & i-k+1+k<=S+L & 1+k<=i-k+1+k by XREAL_1:9; then A190: i+1 in Seg(S+L) & k<=i+1 by NAT_1:13; then r/.(i+1)=r.(i+1) by A28,PARTFUN1:def 8; then reconsider k1=r.(i+1) as Element of NAT; set i1=i+1; A191: Q[i1,k1] by A27,A190; A192: i1-'k=i1-k by A190,BINARITH:50; then Sum (LJ|(k-'1))<=i-'k+1 & i1-'k=i-'k+1 by A182,NAT_1:12,A189; then A193: k<=k1 by A182,A27,A190; k=k1 proof assume A194: k<>k1; then A195: k i1-'k by A194,A192,A27,A190,A193,POLYNOM3:18,BINARITH:59; then Sum(LJ|k)<= i1-'k1 & i1-'k1 < i1-'k by XXREAL_0:1,2; hence thesis by A192,A187,XXREAL_0:2,A189; end; then A196: B.i1 = b1.(i -' k+1) & dom B c= dom Bf by A187,A189,A190,A192,A51,FINSEQ_1:39; then Bf.i1=b1.(i -' k+1) & i1 in dom Bf by A190,A52,FINSEQ_1:def 7; then Bf/.i1=b1.(i -' k+1) by PARTFUN1:def 8; then F.(Bf/.i) = Bf/.i1 by A181,A180,A188,FINSEQ_1:def 7 .= 0.V1+Bf/.i1 by RLVECT_1:def 7 .= 0.K*(Bf/.i)+Bf/.i1 by VECTSP_1:59; hence thesis by A196,A190,A52; end; end; suppose ex j st j in dom f & i=len B + j; then consider j such that A197: j in dom f & i=len B + j; A198: j<=len f by A197,FINSEQ_3:27; F.(Bf/.i) = F.(f.j) by A197,A180,FINSEQ_1:def 7 .= 0.V1 by A154,A156,A197,A198 .= 0.K*(Bf/.i) by VECTSP_1:59; hence thesis; end; end; then consider J be non-empty FinSequence_of_Jordan_block of 0.K,K such that A199: AutMt(F,Bf,Bf) = block_diagonal(J,0.K)by Th28; now let i such that A200: i in dom J; J.i<>{} & dom (Len J)=dom J by A200,FUNCT_1:def 15,MATRIXJ1:def 3; hence (Len J).i <> 0 by A200,MATRIXJ1:def 3; end; hence thesis by A199; end; A201:for n holds P[n] from NAT_1:sch 2(A1,A3); let V1 be finite-dimensional VectSp of K; let F be nilpotent linear-transformation of V1,V1; P[deg F] by A201; then consider J be FinSequence_of_Jordan_block of 0.K,K, b1 be OrdBasis of V1 such that A202: AutMt(F,b1,b1) = block_diagonal(J,0.K) and A203: for i st i in dom J holds (Len J).i <> 0; now let x such that A204: x in dom J; reconsider i=x as Element of NAT by A204; dom J=dom (Len J) by MATRIXJ1:def 3; then (Len J).i <> 0 & (Len J).i=len (J.i) by A203,A204,MATRIXJ1:def 3; hence J.x is non empty; end; then J is non-empty by FUNCT_1:def 15; hence thesis by A202; 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; consider J be non-empty FinSequence_of_Jordan_block of 0.K,K, b1 be OrdBasis of V1 such that A3: AutMt(FLV,b1,b1) = block_diagonal(J,0.K) by Th29; L+0.K=L by RLVECT_1:def 7; 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 such that A4: x in dom JM; reconsider i=x as Nat by A4; dom JM=dom J by MATRIXJ1:def 10; then J.i <> {} & JM.i = J.i + mlt(len J|->L,1.(K,Len J)).i by A4,FUNCT_1:def 15,MATRIXJ1:def 10; hence JM.x is non empty by MATRIX_3:def 3; end; then reconsider JM as non-empty FinSequence_of_Jordan_block of L,K by FUNCT_1:def 15; take JM,b1; A5: Sum Len J = len AutMt(FLV,b1,b1) by A3,MATRIXJ1:def 5 .= len b1 by MATRIX_1:def 3; A6: dom FLV = the carrier of V1 by FUNCT_2:def 1 .= dom (F1+(-L)*(id V1)) by FUNCT_2:def 1; now let x such that A7: x in dom FLV; reconsider v1=x as Vector of V1 by FUNCT_2:def 1,A7; reconsider v=v1 as Vector of V by VECTSP_4:18; (id V).v=v & (id V1).v1=v1 by FUNCT_1:35; then A8: (-L)*((id V).v)=(-L)*((id V1).v1) & F.v1=F1.v1 by A2,VECTSP_4:22,FUNCT_1:72; thus FLV.x = (F+(-L)*id V).v by FUNCT_1:72 .= F.v + ((-L)*id V).v by MATRLIN:def 5 .= F.v+(-L)*((id V).v) by MATRLIN:def 6 .= F1.v1+(-L)*((id V1).v1) by A8,VECTSP_4:21 .= F1.v1+((-L)*id V1).v1 by MATRLIN:def 6 .= (F1+(-L)*id V1).x by MATRLIN:def 5; end; then A9: FLV=F1+(-L)*(id V1) by A6,FUNCT_1:9; set Aid=AutMt(id V1,b1,b1); set AF1=AutMt(F1,b1,b1); A10:now let i,j such that A11: [i,j] in Indices AF1; A12: Indices (AF1+(-L)*Aid)= Indices AF1 & Indices Aid=Indices AF1 by MATRIX_1:27; thus (AF1+(-L)*Aid+L*Aid)*(i,j) = (AF1+(-L)*Aid)*(i,j)+(L*Aid)*(i,j) by A11,A12,MATRIX_3:def 3 .=(AF1*(i,j)+((-L)*Aid)*(i,j))+(L*Aid)*(i,j) by A11,MATRIX_3:def 3 .= AF1*(i,j)+(((-L)*Aid)*(i,j) +(L*Aid)*(i,j)) by RLVECT_1:def 6 .= AF1*(i,j)+((-L)*(Aid*(i,j)) +(L*Aid)*(i,j)) by A11,A12,MATRIX_3:def 5 .= AF1*(i,j)+((-L)*(Aid*(i,j)) +L*(Aid*(i,j))) by A11,A12,MATRIX_3:def 5 .= AF1*(i,j)+(-L+L)*(Aid*(i,j)) by VECTSP_1:def 12 .= AF1*(i,j)+0.K*(Aid*(i,j)) by VECTSP_1:63 .= AF1*(i,j)+0.K by VECTSP_1:39 .= AF1*(i,j) by RLVECT_1:def 7; end; dom Len J=dom 1.(K,Len J) by MATRIXJ1:def 8; then A13: len 1.(K,Len J) = len (Len J) by FINSEQ_3:31 .= len J by FINSEQ_2:109; A14: Len mlt(len J|->L,1.(K,Len J)) = Len 1.(K,Len J) by MATRIXJ1:62 .= Len J by MATRIXJ1:56; A15: 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 A9,MATRLIN:47 .= AF1 by A10,MATRIX_1:28; hence AF1 = block_diagonal(J,0.K)+L*1.(K,Sum Len J) by A3,A5,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 A13,MATRIXJ1:65 .= block_diagonal(J,0.K)+block_diagonal(mlt(len J|->L,1.(K,Len J)),0.K) by VECTSP_1:39 .= block_diagonal(JM,0.K+0.K) by A14,A15,MATRIXJ1:72 .= block_diagonal(JM,0.K) by RLVECT_1:def 7; 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)); A1: P[0] proof let V be non trivial finite-dimensional VectSp of K such that A2: dim V <= 0; dim V=0 by A2; hence thesis by MATRLIN2:42; end; A3: for n st P[n] holds P[n+1] proof let n such that A4: P[n];set n1=n+1; let V be non trivial finite-dimensional VectSp of K such that A5: dim V <= n1; per cases by A5,NAT_1:8; suppose dim V<=n; hence thesis by A4; end; suppose A6: dim V=n1; let F be linear-transformation of V,V; A7: F is with_eigenvalues by VECTSP11:16; then consider v be Vector of V, L be Scalar of K such that A8: v <> 0.V & F.v = L*v by VECTSP11:def 1; set FL=F+(-L)*id V; consider m such that A9: UnionKers FL = ker (FL|^m) by VECTSP11:27; set KER = ker (FL|^m); set IM = im (FL|^m); A10: L is eigenvalue of F & FL|^1=FL by A7,A8,VECTSP11:19,def 2; then ker FL is non trivial & ker FL is Subspace of KER by A7,A9,VECTSP11:14,25; then A11: dim ker FL<>0 & dim ker FL <= dim KER by MATRLIN2:42,VECTSP_9:29; reconsider FK=F|KER as linear-transformation of KER,KER by VECTSP11:29; reconsider FI=F|IM as linear-transformation of IM,IM by VECTSP11:33; consider Jk be non-empty FinSequence_of_Jordan_block of L,K, Bker be OrdBasis of KER such that A12: AutMt(FK,Bker,Bker) = block_diagonal(Jk,0.K) by Th30; A13: len Jk<>0 proof assume len Jk=0; then Len Jk = <*>NAT by FINSEQ_2:113 .= <*>REAL; then 0 = len block_diagonal(Jk,0.K) by MATRIXJ1:def 5,RVSUM_1:102 .= len Bker by A12,MATRIX_1:def 3 .= dim KER by MATRLIN2:21; hence thesis by A11; end; A14: V is_the_direct_sum_of KER,IM & KER/\IM=(0).V by A9,VECTSP11:35,34; then A15: dim V=dim KER + dim IM & KER+IM = (Omega).V & IM is Linear_Compl of KER by VECTSP_9:38,VECTSP_5:def 4,VECTSP_5:47; per cases; suppose A16: IM is trivial; consider Bim be OrdBasis of IM; Bker^Bim is OrdBasis of KER+IM by A14,MATRLIN2:26; then reconsider BB=Bker^Bim as OrdBasis of V by A15,MATRLIN2:4; take Jk,BB; 0 = dim IM by A16,MATRLIN2:42 .= len Bim by MATRLIN2:21 .= len AutMt(FI,Bim,Bim) by MATRIX_1:def 3; then A17: AutMt(FI,Bim,Bim)={}; (dim KER=0 implies dim KER=0) & (dim IM=0 implies dim IM=0); hence AutMt(F,BB,BB) = block_diagonal(<*AutMt(FK,Bker,Bker), AutMt(FI,Bim,Bim)*>,0.K) by A14,MATRLIN2:27 .= block_diagonal(<*AutMt(FK,Bker,Bker)*>,0.K) by A17,MATRIXJ1:40 .= block_diagonal(Jk,0.K) by A12,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 A18: L1 is eigenvalue of F; take i=len Jk; i in Seg len Jk by A13,FINSEQ_1:5; hence A19: i in dom Jk by FINSEQ_1:def 3; consider k such that A20: Jk.i=Jordan_block(L,k) by A19,Def3; L1 = L proof assume L<>L1; then FI is with_eigenvalues & L1 is eigenvalue of FI by A7,A10,A9,A15,A18,VECTSP11:39; then consider v1 be Vector of IM such that A21: v1<>0.IM & FI.v1 = L1*v1 by VECTSP11:def 2; thus thesis by A21,A16,ANPROJ_1:def 8; end; hence thesis by A20,Def1; end; given i such that A22: i in dom Jk & Jk.i = Jordan_block(L1,len (Jk.i)); consider k such that A23: Jk.i=Jordan_block(L,k) by A22,Def3; Jk.i <> {} by A22,FUNCT_1:def 15; then len (Jk.i) in Seg len (Jk.i) by FINSEQ_1:5; then [len (Jk.i),len (Jk.i)] in [:Seg len (Jk.i),Seg len (Jk.i):] by ZFMISC_1:106; then A24: [len (Jk.i),len (Jk.i)] in Indices (Jk.i) by MATRIX_1:25; then L = (Jk.i)*(len (Jk.i),len (Jk.i)) by A23,Def1 .= L1 by A22,A24,Def1; hence L1 is eigenvalue of F by A7,A8,VECTSP11:def 2; end; suppose A25: IM is non trivial; then A26: FI is with_eigenvalues by VECTSP11:16; n1 <> dim IM & dim IM <= n1 by A6,A11,A15,NAT_1:11; then dim IM ,0.K) by A12,A27,A14,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 A31: L1 is eigenvalue of F; per cases; suppose A32: L = L1; take i=len Jk; i in Seg len Jk by A13,FINSEQ_1:5; then A33: i in dom Jk by FINSEQ_1:def 3; then consider k such that A34: Jk.i = Jordan_block(L,k) by Def3; dom Jk c= dom JJ & k=len (Jk.i) & JJ.i=Jk.i by A33,A34,FINSEQ_1:def 7,39,Def1; hence thesis by A32,A33,A34; end; suppose L<>L1; then L1 is eigenvalue of FI by A7,A10,A9,A15,A31,VECTSP11:39; then consider i such that A35: i in dom Ji & Ji.i = Jordan_block(L1,len (Ji.i)) by A28; take ii=len Jk+i; ii in dom JJ & JJ.ii=Ji.i by A35,FINSEQ_1:def 7,41; hence thesis by A35; end; end; given i such that A36: i in dom JJ & JJ.i = Jordan_block(L1,len (JJ.i)); per cases by A36,FINSEQ_1:38; suppose A37: i in dom Jk; then A38: JJ.i = Jk.i by FINSEQ_1:def 7; consider k such that A39: Jk.i = Jordan_block(L,k) by A37,Def3; Jk.i <> {} by A37,FUNCT_1:def 15; then len (Jk.i) in Seg len (Jk.i) by FINSEQ_1:5; then [len (Jk.i),len (Jk.i)] in [:Seg len (Jk.i),Seg len (Jk.i):] by ZFMISC_1:106; then A40: [len (Jk.i),len (Jk.i)] in Indices (Jk.i) by MATRIX_1:25; then L = (Jk.i)*(len (Jk.i),len (Jk.i)) by A39,Def1 .= L1 by A38,A40,A36,Def1; hence thesis by A7,A8,VECTSP11:def 2; end; suppose ex j st j in dom Ji & i = len Jk +j; then consider j such that A41: j in dom Ji & i=len Jk+j; JJ.i=Ji.j by A41,FINSEQ_1:def 7; then L1 is eigenvalue of FI by A36,A41,A28; then consider w be Vector of IM such that A42: w<>0.IM & FI.w = L1*w by A26,VECTSP11:def 2; reconsider W=w as Vector of V by VECTSP_4:18; A43: 0.IM = 0.V by VECTSP_4:19; L1*W = FI.w by A42,VECTSP_4:22 .= F.W by FUNCT_1:72; hence thesis by A7,A42,A43,VECTSP11:def 2; end; end; end; end; A44: for n holds P[n] from NAT_1:sch 2(A1,A3); let V be non trivial finite-dimensional VectSp of K, F be linear-transformation of V,V; P[dim V] by A44; hence thesis; end; 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; reconsider J ={} as FinSequence_of_Jordan_block of K by Lm2; for x st x in dom J holds J.x is non empty; then reconsider J as non-empty FinSequence_of_Jordan_block of K by FUNCT_1:def 15; reconsider P={} as Matrix of n,K by A1,MATRIX_1:13; take J,P; A2: Len J = <*>NAT by FINSEQ_2:113,CARD_1:47 .= <*>REAL; hence Sum Len J=n by A1,RVSUM_1:102; reconsider B=block_diagonal(J,0.K) as Matrix of n,K by A2,A1,RVSUM_1:102; Det P=1_K & 1_K <>0.K by A1,MATRIXR2:41; hence P is invertible by LAPLACE:34; M = P * B * (P~) by A1,MATRIX_1:36; hence thesis; end; suppose A3: n>0; set V=n-VectSp_over K; consider B be OrdBasis of V; A4: len B = dim V by MATRLIN2:21 .= n by MATRIX13:112; then reconsider M'=M as Matrix of len B,K; set T=Mx2Tran(M',B,B); dim V=n by MATRIX13:112; then V is non trivial by A3,MATRLIN2:42; then consider J be non-empty (FinSequence_of_Jordan_block of K), b1 be OrdBasis of V such that A5: 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; A6: len b1 = dim V by MATRLIN2:21 .= n by MATRIX13:112; reconsider P=AutEqMt(id V,B,b1) as Matrix of n,K by A4; take J,P; thus Sum Len J=len AutMt(T,b1,b1) by A5,MATRIXJ1:def 5 .=n by A6,MATRIX_1:def 3; thus P is invertible by A4,MATRLIN2:29; A7: width P=n & len (P~)=n & len AutMt(T,b1,b1) = n & width AutMt(T,b1,b1)=n by A3,A6,MATRIX_1:24; A8: dom T=[#]V & rng T c= [#]V by FUNCT_2:def 1,RELSET_1:12; thus M = AutMt(T,B,B) by MATRLIN2:36 .= AutMt(T*id V,B,B) by A8,RELAT_1:78 .= AutMt(id V,B,b1)* AutMt(T,b1,B) by A3,A4,A6,MATRLIN:46 .= P* AutMt(T,b1,B) by A6,A4,MATRLIN2:def 2 .= P* AutMt((id V)*T,b1,B) by A8,RELAT_1:79 .= P* (AutMt(T,b1,b1)*AutMt(id V,b1,B)) by A3,A6,A4,MATRLIN:46 .= P*(AutMt(T,b1,b1) *AutEqMt(id V,b1,B)) by A6,A4,MATRLIN2:def 2 .= P*(AutMt(T,b1,b1)*(P~)) by A4,MATRLIN2:29 .= P*block_diagonal(J,0.K) *(P~) by A5,A7,MATRIX_3:35; end; end;