:: Eigenvalues of a Linear Transformation :: by Karol P\c{a}k :: :: Received July 11, 2008 :: Copyright (c) 2008 Association of Mizar Users environ vocabularies BOOLE, ARYTM, ARYTM_1, FINSEQ_1, FINSEQ_2, FINSEQ_4, RELAT_1, FUNCT_1, FUNCT_2, INCSP_1, RLSUB_1, GROUP_1, BINOP_1, FINSET_1, SGRAPH1, CARD_1, CARD_3, GR_CY_1, FREEALG, SEQ_1, MATRIX_1, MATRIX_2, MATRIX_3, LAPLACE, RLVECT_1, RLVECT_2, RLVECT_3, VECTSP_1, VECTSP_2, VECTSP_9, PRVECT_1, ALGSTR_0, RLSUB_2, MATRLIN, RANKNULL, VECTSP10, SUBSET_1, LATTICES, SQUARE_1, ARYTM_3, REALSET1, MONOID_0, POLYNOM1, ALGSEQ_1, POLYNOM3, POLYNOM2, MCART_1, POLYNOM5, MATRLIN2, VECTSP11; 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, FINSEQ_1, BINOP_1, STRUCT_0, RLVECT_1, GROUP_1, VECTSP_1, FINSEQ_2, MATRIX_1, MATRIX_2, BINARITH, GROUP_4, MATRIX_3, DOMAIN_1, PSCOMP_1, VECTSP_4, VECTSP_5, VECTSP_6, VECTSP_7, VECTSP_9, FINSEQOP, MATRIX13, MATRLIN, LAPLACE, MOD_2, RANKNULL, POLYNOM1, POLYNOM3, MONOID_0, ALGSEQ_1, POLYNOM4, POLYNOM5, MATRLIN2; constructors FINSOP_1, XXREAL_0, GROUP_4, VECTSP_7, VECTSP_9, MATRIX13, REALSET1, LAPLACE, VECTSP_5, RANKNULL, MONOID_0, POLYNOM1, POLYNOM4, POLYNOM5, SEQ_1, MATRLIN2, BINOP_2; registrations XBOOLE_0, FUNCT_1, FINSET_1, STRUCT_0, VECTSP_1, FUNCT_2, ORDINAL1, XXREAL_0, NAT_1, FINSEQ_1, RELAT_1, FINSEQ_2, SEQM_3, MATRLIN, MATRIX13, XREAL_0, VECTSP_9, VECTSP_7, FRAENKEL, RANKNULL, POLYNOM3, POLYNOM5, MONOID_0, MATRIX_1, CARD_1; requirements ARITHM, NUMERALS, REAL, BOOLE, SUBSET; definitions STRUCT_0, TARSKI, XBOOLE_0, RLVECT_1, FINSEQ_1, VECTSP_4, FVSUM_1, LAPLACE, MATRIX13, RANKNULL, VECTSP_6, MATRLIN2; theorems ZFMISC_1, RLVECT_1, MATRIX_1, MATRIX_3, VECTSP_1, NAT_1, FINSEQ_1, FINSEQ_3, FINSEQ_2, BINARITH, CARD_1, CARD_2, FINSEQOP, FINSOP_1, FUNCT_1, FUNCT_2, FVSUM_1, GROUP_1, LAPLACE, MATRIX13, MATRIXR2, MATRLIN, ORDINAL1, PARTFUN1, RELAT_1, RELSET_1, STIRL2_1, STRUCT_0, TARSKI, VECTSP_3, VECTSP_4, VECTSP_5, VECTSP_6, VECTSP_7, VECTSP_9, VECTSP10, XBOOLE_0, XBOOLE_1, XREAL_1, XXREAL_0, MOD_2, RANKNULL, ANPROJ_1, MONOID_0, GROUP_4, SYSREL, SUBSET_1, FINSEQ_5, ALGSEQ_1, POLYNOM4, POLYNOM5, HILBASIS, MATRIXJ1, MATRLIN2, VALUED_0; schemes NAT_1, FUNCT_2; begin :: Preliminaries reserve i,j,m,n,k for Nat, x,y for set, K for Field, a,a1,a2 for Element of K; theorem Th1: for A,B be Matrix of K for nt be Element of n-tuples_on NAT, mt be Element of m-tuples_on NAT st [:rng nt,rng mt:] c= Indices A holds Segm(A+B,nt,mt) = Segm(A,nt,mt) + Segm(B,nt,mt) proof let A,B be Matrix of K; let nt be Element of n-tuples_on NAT, mt be Element of m-tuples_on NAT such that A1: [:rng nt,rng mt:] c= Indices A; now let i,j such that A2: [i,j] in Indices Segm(A+B,nt,mt); A3: Indices Segm(A+B,nt,mt) = Indices Segm(A,nt,mt) & Indices Segm(A,nt,mt) = Indices Segm(B,nt,mt) by MATRIX_1:27; A4: [nt.i,mt.j] in Indices A by A1,A2,A3,MATRIX13:17; reconsider nti = nt.i, mtj = mt.j as Nat by VALUED_0:12; thus Segm(A+B,nt,mt)*(i,j) = (A+B)*(nti,mtj) by A2,MATRIX13:def 1 .= A*(nti,mtj)+B*(nti,mtj) by A4,MATRIX_3:def 3 .= Segm(A,nt,mt)*(i,j) + B*(nti,mtj) by A2,A3,MATRIX13:def 1 .= Segm(A,nt,mt)*(i,j) + Segm(B,nt,mt)*(i,j) by A2,A3,MATRIX13:def 1 .= (Segm(A,nt,mt) + Segm(B,nt,mt))*(i,j) by A2,A3,MATRIX_3:def 3; end; hence thesis by MATRIX_1:28; end; theorem Th2: for P be without_zero finite Subset of NAT st P c= Seg n holds Segm(1.(K,n),P,P) = 1.(K,card P) proof let P be without_zero finite Subset of NAT such that A1: P c= Seg n; set S=Segm(1.(K,n),P,P); now let i,j such that A2: [i,j] in Indices 1.(K,card P); set SP=Sgm P; A3: Indices 1.(K,n) = [:Seg n,Seg n:] & Indices S=[:Seg card P,Seg card P:]& [:P,P:] c= [:Seg n,Seg n:] & Indices 1.(K,card P) = Indices S & rng SP = P & SP is one-to-one & dom SP=Seg card P by A1,MATRIX_1:25,27,ZFMISC_1:119,FINSEQ_1:def 13,FINSEQ_3:45,99; then A4: [SP.i,SP.j] in Indices 1.(K,n) & i in dom SP & j in dom SP by A2,MATRIX13:17,ZFMISC_1:106; reconsider Spi = SP.i, Spj = SP.j as Nat by VALUED_0:12; A5: S*(i,j) = 1.(K,n)*(Spi,Spj) by A2,A3,MATRIX13:def 1; i=j or i<>j; then S*(i,j)=1_K & 1.(K,card P)*(i,j)=1_K or 1.(K,card P)*(i,j)=0.K & SP.i<>SP.j by A2,A3,A4,A5,MATRIX_1:def 12,FUNCT_1:def 8; hence 1.(K,card P)*(i,j)=S*(i,j) by A4,A5,MATRIX_1:def 12; end; hence thesis by MATRIX_1:28; end; theorem Th3: for A,B be Matrix of K for P, Q be without_zero finite Subset of NAT st [:P,Q:] c= Indices A holds Segm(A+B,P,Q) = Segm(A,P,Q) + Segm(B,P,Q) proof let A,B be Matrix of K; let P, Q be without_zero finite Subset of NAT such that A1: [:P,Q:] c= Indices A; consider n such that A2: P c= Seg n by MATRIX13:43; consider m such that A3: Q c= Seg m by MATRIX13:43; rng (Sgm P)=P & rng (Sgm Q)=Q by A2,A3,FINSEQ_1:def 13; hence thesis by A1,Th1; end; theorem Th4: for A,B be Matrix of n,K st i in Seg n & j in Seg n holds Delete(A+B,i,j)=Delete(A,i,j) + Delete(B,i,j) proof let A,B be Matrix of n,K such that A1: i in Seg n & j in Seg n; Seg n\{i} c= Seg n & Seg n\{j} c= Seg n by XBOOLE_1:36; then A2: [:Seg n\{i},Seg n\{j}:] c= [:Seg n,Seg n:] & Indices A = [:Seg n,Seg n:] by MATRIX_1:25,ZFMISC_1:119; thus Delete(A+B,i,j) = Deleting(A+B,i,j) by A1,LAPLACE:def 1 .= Segm(A+B,Seg n\{i},Seg n\{j}) by MATRIX13:58 .= Segm(A,Seg n\{i},Seg n\{j})+Segm(B,Seg n\{i},Seg n\{j}) by A2,Th3 .= Deleting(A,i,j)+Segm(B,Seg n\{i},Seg n\{j}) by MATRIX13:58 .= Deleting(A,i,j) + Deleting(B,i,j) by MATRIX13:58 .= Delete(A,i,j) + Deleting(B,i,j) by A1,LAPLACE:def 1 .= Delete(A,i,j) + Delete(B,i,j) by A1,LAPLACE:def 1; end; theorem Th5: for A be Matrix of n,K st i in Seg n & j in Seg n holds Delete(a*A,i,j)=a*Delete(A,i,j) proof let A be Matrix of n,K such that A1: i in Seg n & j in Seg n; Seg n\{i} c= Seg n & Seg n\{j} c= Seg n by XBOOLE_1:36; then A2: [:Seg n\{i},Seg n\{j}:] c= [:Seg n,Seg n:] & Indices A = [:Seg n,Seg n:] by MATRIX_1:25,ZFMISC_1:119; thus Delete(a*A,i,j) = Deleting(a*A,i,j) by A1,LAPLACE:def 1 .= Segm(a*A,Seg n\{i},Seg n\{j}) by MATRIX13:58 .= a*Segm(A,Seg n\{i},Seg n\{j}) by A2,MATRIX13:63 .= a*Deleting(A,i,j) by MATRIX13:58 .= a*Delete(A,i,j) by A1,LAPLACE:def 1; end; theorem Th6: i in Seg n implies Delete(1.(K,n),i,i)=1.(K,n-'1) proof assume A1: i in Seg n; then n-'1=n-1 by BINARITH:50,NAT_1:14,FINSEQ_1:4; then card Seg n=n-'1+1 by FINSEQ_1:78; then A2: card (Seg n\{i})=n-'1 by A1,STIRL2_1:65; thus Delete(1.(K,n),i,i) = Deleting(1.(K,n),i,i) by A1,LAPLACE:def 1 .= Segm(1.(K,n),Seg n\{i},Seg n\{i}) by MATRIX13:58 .= 1.(K,n-'1) by XBOOLE_1:36,A2,Th2; end; theorem Th7: for A,B be Matrix of n,K ex P be Polynomial of K st len P <= n+1 & for x be Element of K holds eval(P,x) = Det(A+x*B) proof defpred P[Nat] means for A,B be Matrix of $1,K ex P be Polynomial of K st len P <= $1+1 & for x be Element of K holds eval(P,x) = Det(A+x*B); A1: P[0] proof let A,B be Matrix of 0,K; take P=1_.(K); thus len P <=0+1 by POLYNOM4:7; let x be Element of K; thus Det(A+x*B) = 1_K by MATRIXR2:41 .= eval(P,x) by POLYNOM4:21; end; A2: for n st P[n] holds P[n+1] proof let n such that A3: P[n];set n1=n+1; let A,B be Matrix of n1,K; A4: n1 in Seg n1 by FINSEQ_1:6; defpred Q[Nat] means $1 <= n1 implies ex P be Polynomial of K st len P <= n1+1 & for x be Element of K holds eval(P,x) = Sum (LaplaceExpL(A+x*B,n1)|$1); A5: Q[0] proof assume 0<=n1; take P=0_.(K); thus len P <=n1+1 by POLYNOM4:6; let x be Element of K; LaplaceExpL(A+x*B,n1)|0 = <*>(the carrier of K); hence Sum (LaplaceExpL(A+x*B,n1)|0) = 0.K by RLVECT_1:60 .= eval(P,x) by POLYNOM4:20; end; A6: for m st Q[m] holds Q[m+1] proof let m such that A7: Q[m];set m1=m+1; assume A8: m1 <= n1; then consider P be Polynomial of K such that A9: len P <= n1+1 and A10: for x be Element of K holds eval(P,x) = Sum (LaplaceExpL(A+x*B,n1)|m) by A7,NAT_1:13; set DA=Delete(A,n1,m1); set DB=Delete(B,n1,m1); n1-'1=n by BINARITH:39; then consider P1 be Polynomial of K such that A11: len P1 <= n+1 and A12: for x be Element of K holds eval(P1,x) = Det(DA+x*DB) by A3; set pow=power(K).(-1_K,m1+n1); set P2=<% A*(n1,m1)*pow,B*(n1,m1)*pow %>; take PP=P+(P1*'P2); len P2 <= 2 by POLYNOM5:40; then (len P1)+(len P2) <= n1+2 by A11,XREAL_1:9; then (len P1)+(len P2)-'1 <=n1+2-'1 & n+2+1-'1=n+2 & len (P1*'P2) <= (len P1)+(len P2)-'1 by BINARITH:39,60,HILBASIS:21; then len (P1*'P2) <= n1+1 by XXREAL_0:2; hence len PP<=n1+1 by A9,POLYNOM4:9; let x be Element of K; set L=LaplaceExpL(A+x*B,n1); 1<=m1 & n1=len L by NAT_1:11,LAPLACE:def 7; then A13: m1 in Seg n1 & dom L=Seg n1 by A8,FINSEQ_1:def 3; then A14: [n1,m1] in [:Seg n1,Seg n1:] & Indices B=[:Seg n1,Seg n1:] & Indices A=[:Seg n1,Seg n1:] by A4,ZFMISC_1:106,MATRIX_1:25; A15: A*(n1,m1)*pow+B*(n1,m1)*pow*x = A*(n1,m1)*pow+B*(n1,m1)*x*pow by GROUP_1:def 4 .= (A*(n1,m1)+B*(n1,m1)*x)*pow by VECTSP_1:def 11 .= (A*(n1,m1)+(x*B)*(n1,m1))*pow by A14,MATRIX_3:def 5 .= (A+x*B)*(n1,m1)*pow by A14,MATRIX_3:def 3; A16: DA+x*DB = DA+Delete(x*B,n1,m1) by A4,A13,Th5 .= Delete(A+x*B,n1,m1) by A4,A13,Th4; A17: eval(P1*'P2,x) = eval(P1,x)*eval(P2,x) by POLYNOM4:27 .= Det(DA+x*DB) * eval(P2,x) by A12 .= Minor(A+x*B,n1,m1)*((A+x*B)*(n1,m1)*pow) by A15,A16,POLYNOM5:45 .=(A+x*B)*(n1,m1)*Cofactor(A+x*B,n1,m1) by GROUP_1:def 4 .= L.m1 by A13,LAPLACE:def 7; L|m1 = (L|m)^<*L.m1*> by A13,FINSEQ_5:11; hence Sum (L|m1) = Sum (L|m) + eval(P1*'P2,x) by A17,FVSUM_1:87 .= eval(P,x)+eval(P1*'P2,x) by A10 .= eval(PP,x) by POLYNOM4:22; end; for m holds Q[m] from NAT_1:sch 2(A5,A6); then consider P be Polynomial of K such that A18: len P <= n1+1 and A19: for x be Element of K holds eval(P,x)=Sum (LaplaceExpL(A+x*B,n1)|n1); take P; thus len P <= n1+1 by A18; let x be Element of K; A20: len LaplaceExpL(A+x*B,n1)=n1 by LAPLACE:def 7; thus eval(P,x) = Sum (LaplaceExpL(A+x*B,n1)|n1) by A19 .= Sum LaplaceExpL(A+x*B,n1) by A20,FINSEQ_1:79 .= Det (A+x*B) by A4,LAPLACE:25; end; for n holds P[n] from NAT_1:sch 2(A1,A2); hence thesis; end; :: The Characteristic Polynomials of Square Matrixs theorem Th8: for A be Matrix of n,K ex P be Polynomial of K st len P = n+1 & for x be Element of K holds eval(P,x) = Det(A+x*1.(K,n)) proof defpred P[Nat] means for A be Matrix of $1,K ex P be Polynomial of K st len P = $1+1 & for x be Element of K holds eval(P,x) = Det(A+x*1.(K,$1)); A1: P[0] proof let A be Matrix of 0,K; take P=1_.(K); thus len P =0+1 by POLYNOM4:7; let x be Element of K; thus Det(A+x*1.(K,0)) = 1_K by MATRIXR2:41 .= eval(P,x) by POLYNOM4:21; end; A2: for n st P[n] holds P[n+1] proof let n such that A3: P[n];set n1=n+1; let A be Matrix of n1,K; set ONE=1.(K,n1); A4: Indices ONE=Indices A & Indices A=[:Seg n1,Seg n1:] by MATRIX_1:25,27; A5: 1<=n1 by NAT_1:11; then A6: 1 in Seg n1 & n1-'1=n by BINARITH:39; defpred Q[Nat] means 1<= $1 & $1 <= n1 implies ex P be Polynomial of K st len P = n1+1 & for x be Element of K holds eval(P,x) = Sum (LaplaceExpL(A+x*1.(K,n1),1)|$1); A7: Q[0]; A8: for k st Q[k] holds Q[k+1] proof let k such that A9: Q[k];set k1=k+1; assume A10: 1<=k1 & k1<=n1; then A11: k1 in Seg n1; then A12: [1,k1] in Indices A by A6,A4,ZFMISC_1:106; set pow=power(K).(-1_K,k1+1); set P2=<% A*(1,k1)*pow,ONE*(1,k1)*pow %>; per cases by NAT_1:14; suppose A13: k=0; consider P be Polynomial of K such that A14: len P = n1 and A15: for x be Element of K holds eval(P,x) = Det(Delete(A,1,1)+x*1.(K,n)) by A3,A6; take PP=P2*'P; pow = (-1_K) * (-1_K) by A13,GROUP_1:99 .= 1_K * 1_K by VECTSP_1:42 .= 1_K by VECTSP_1:def 13; then ONE*(1,k1)*pow = 1_K*1_K by A4,A12,A13,MATRIX_1:def 12 .= 1_K by VECTSP_1:def 13; then ONE*(1,k1)*pow<>0.K; then A16: len P2=2 & 2-'1=2-1 & P2.1 <>0.K & P.n <> 0.K by A14,POLYNOM5:39,41,BINARITH:50,ALGSEQ_1:25; then P2.(len P2-'1)*P.(len P-'1) <>0.K by A6,A14,VECTSP_1:44; hence len PP = n1+2-1 by A14,A16,POLYNOM4:13 .= n1+1; let x be Element of K; set L=LaplaceExpL(A+x*ONE,1); A17: dom L=Seg len L & len L=n1 by LAPLACE:def 7,FINSEQ_1:def 3; A18: A*(1,k1)*pow+ONE*(1,k1)*pow*x = A*(1,k1)*pow+ONE*(1,k1)*x*pow by GROUP_1:def 4 .= (A*(1,k1)+ONE*(1,k1)*x)*pow by VECTSP_1:def 11 .= (A*(1,k1)+(x*ONE)*(1,k1))*pow by A4,A12,MATRIX_3:def 5 .= (A+x*ONE)*(1,k1)*pow by A12,MATRIX_3:def 3; A19: Delete(A,1,1)+x*1.(K,n) = Delete(A,1,1)+x*Delete(ONE,1,1) by A6,Th6 .= Delete(A,1,1)+Delete(x*ONE,1,1) by A13,A11,Th5 .= Delete(A+x*ONE,1,1) by A6,Th4; A20: eval(P2*'P,x) = eval(P2,x)*eval(P,x) by POLYNOM4:27 .= eval(P2,x) * Det(Delete(A,1,1)+x*1.(K,n)) by A15 .= Minor(A+x*ONE,1,1)*((A+x*ONE)*(1,1)*pow) by A13,A18,A19,POLYNOM5:45 .= (A+x*ONE)*(1,1) * Cofactor(A+x*ONE,1,1) by A13,GROUP_1:def 4 .= L.1 by A6,A17,LAPLACE:def 7; thus Sum (L|k1) = Sum <*L/.1*> by A13,FINSEQ_5:23,A17,CARD_1:47 .= Sum <* eval(P2*'P,x) *> by A6,A17,A20,PARTFUN1:def 8 .= eval(PP,x) by FINSOP_1:12; end; suppose A21: k>=1; then consider P be Polynomial of K such that A22: len P = n1+1 and A23: for x be Element of K holds eval(P,x) = Sum (LaplaceExpL(A+x*1.(K,n1),1)|k) by A10,NAT_1:13,A9; consider P1 be Polynomial of K such that A24: len P1 <= n+1 and A25: for x be Element of K holds eval(P1,x)=Det(Delete(A,1,k1)+x*Delete(ONE,1,k1))by A6,Th7; take PP=P+(A*(1,k1)*pow)*P1; A*(1,k1)*pow=0.K or A*(1,k1)*pow<>0.K; then len ((A*(1,k1)*pow)*P1)<=n1 by A24,POLYNOM5:25,26; then A26: len ((A*(1,k1)*pow)*P1) < len P by A22,NAT_1:13; hence len PP = max(len ((A*(1,k1)*pow)*P1),len P) by POLYNOM4:10 .= n1+1 by A22,A26,XXREAL_0:def 9; let x be Element of K; A27: k1<>1 by A21,NAT_1:13; set L=LaplaceExpL(A+x*ONE,1); A28: dom L=Seg len L & len L=n1 by LAPLACE:def 7,FINSEQ_1:def 3; A29: A*(1,k1)*pow = (A*(1,k1)+0.K)*pow by RLVECT_1:def 7 .= (A*(1,k1)+x*0.K)*pow by VECTSP_1:39 .= (A*(1,k1)+x*(ONE*(1,k1)))*pow by A27,A4,A12,MATRIX_1:def 12 .= (A*(1,k1)+(x*ONE)*(1,k1))*pow by A4,A12,MATRIX_3:def 5 .= (A+x*ONE)*(1,k1)*pow by A12,MATRIX_3:def 3; A30: Delete(A,1,k1)+x*Delete(ONE,1,k1) = Delete(A,1,k1)+Delete(x*ONE,1,k1) by A11,Th5,A6 .= Delete(A+x*ONE,1,k1) by A6,A11,Th4; A31: eval((A*(1,k1)*pow)*P1,x) = (A*(1,k1)*pow)*eval(P1,x) by POLYNOM5:31 .= Minor(A+x*ONE,1,k1)*((A+x*ONE)*(1,k1)*pow) by A25,A29,A30 .= (A+x*ONE)*(1,k1)*Cofactor(A+x*ONE,1,k1) by GROUP_1:def 4 .= L.k1 by A11,A28,LAPLACE:def 7; L|k1 = (L|k)^<*L.k1*> by A28,A11,FINSEQ_5:11; hence Sum (L|k1) = Sum (L|k) + eval((A*(1,k1)*pow)*P1,x) by A31,FVSUM_1:87 .= eval(P,x)+eval((A*(1,k1)*pow)*P1,x) by A23 .= eval(PP,x) by POLYNOM4:22; end; end; for k holds Q[k] from NAT_1:sch 2(A7,A8); then consider P be Polynomial of K such that A32: len P = n1+1 and A33: for x be Element of K holds eval(P,x) = Sum (LaplaceExpL(A+x*1.(K,n1),1)|n1) by A5; take P; thus len P=n1+1 by A32; let x be Element of K; set L=LaplaceExpL(A+x*1.(K,n1),1); len L=n1 by LAPLACE:def 7; hence eval(P,x) = Sum (L|(len L)) by A33 .= Sum L by FINSEQ_1:79 .= Det (A+x*1.(K,n1)) by A6,LAPLACE:25; end; for n holds P[n] from NAT_1:sch 2(A1,A2); hence thesis; end; Lm1: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; registration let K; cluster non trivial finite-dimensional VectSp of K; existence proof take V=1-VectSp_over K; dim V=1 by MATRIX13:112; then ex v be Vector of V st v <> 0.V & (Omega).V = Lin{v} by VECTSP_9:34; hence thesis by ANPROJ_1:def 8; end; end; begin :: Maps with Eigenvalues definition let R be non empty doubleLoopStr; let V be non empty VectSpStr over R; let IT be Function of V,V; attr IT is with_eigenvalues means :Def1: ex v be Vector of V, a be Scalar of R st v <> 0.V & IT.v = a*v; end; reserve V for non trivial VectSp of K, V1,V2 for VectSp of K, f for linear-transformation of V1,V1, v,w for Vector of V, v1,w1 for Vector of V1, L for Scalar of K; Lm2:id V is with_eigenvalues & ex v st v<>0.V & id V.v=1_K*v proof consider v such that A1: v <> 0.V by ANPROJ_1:def 8; id V.v = v by FUNCT_1:34 .= 1_K*v by VECTSP_1:def 26; hence thesis by A1,Def1; end; registration let K,V; cluster with_eigenvalues linear-transformation of V,V; existence proof take F=id V; thus thesis by Lm2; end; end; definition let R be non empty doubleLoopStr; let V be non empty VectSpStr over R; let f be Function of V,V such that A1:f is with_eigenvalues; mode eigenvalue of f -> Element of R means :Def2: ex v be Vector of V st v <> 0.V & f.v = it * v; existence proof ex v be Vector of V, a be Scalar of R st v <> 0.V & f.v = a*v by A1,Def1; hence thesis; end; end; definition let R be non empty doubleLoopStr; let V be non empty VectSpStr over R; let f be Function of V,V; let L be Scalar of R such that A1:f is with_eigenvalues & L is eigenvalue of f; mode eigenvector of f,L -> Vector of V means :Def3: f.it = L * it; existence proof ex v be Vector of V st v <> 0.V & f.v = L * v by A1,Def2; hence thesis; end; end; theorem for a st a <> 0.K for f be with_eigenvalues Function of V,V for L be eigenvalue of f holds a*f is with_eigenvalues & a*L is eigenvalue of a*f & ( w is eigenvector of f,L iff w is eigenvector of a*f,a*L ) proof let a such that A1:a<>0.K; let f be with_eigenvalues Function of V,V; let L be eigenvalue of f; consider v such that A2: v <> 0.V & f.v = L * v by Def2; A3: (a*f).v = a*(L*v) by MATRLIN:def 6,A2 .= (a*L)*v by VECTSP_1:def 26; hence A4: a*f is with_eigenvalues by A2,Def1; thus A5: a*L is eigenvalue of a*f by A2,A3,A4,Def2; hereby assume A6: w is eigenvector of f,L; (a*f).w = a*(f.w) by MATRLIN:def 6 .= a*(L*w) by A6,Def3 .= (a*L)*w by VECTSP_1:def 26; hence w is eigenvector of a*f,a*L by A4,A5,Def3; end; assume A7: w is eigenvector of a*f,a*L; a*f.w = (a*f).w by MATRLIN:def 6 .= (a*L)*w by A4,A5,A7,Def3 .= a*(L*w) by VECTSP_1:def 26; then 0.V = a*f.w+-a*(L*w) by VECTSP_1:63 .= a*f.w+a*(-(L*w)) by VECTSP_1:69 .= a*(f.w-(L*w)) by VECTSP_1:def 26; then f.w-(L*w)=0.V by A1,VECTSP_1:60; then -f.w=-(L*w) by VECTSP_1:63; then f.w=L*w by RLVECT_1:31; hence thesis by Def3; end; theorem for f1,f2 be with_eigenvalues Function of V,V for L1,L2 be Scalar of K st L1 is eigenvalue of f1 & L2 is eigenvalue of f2 & ex v st v is eigenvector of f1,L1 & v is eigenvector of f2,L2 & v<>0.V holds f1+f2 is with_eigenvalues & L1+L2 is eigenvalue of f1+f2 & for w st w is eigenvector of f1,L1 & w is eigenvector of f2,L2 holds w is eigenvector of f1+f2,L1+L2 proof let f1,f2 be with_eigenvalues Function of V,V; let L1,L2 be Scalar of K; set g=f1+f2; assume A1: L1 is eigenvalue of f1 & L2 is eigenvalue of f2; given v such that A2: v is eigenvector of f1,L1 & v is eigenvector of f2,L2 & v<>0.V; A3: g.v = f1.v+f2.v by MATRLIN:def 5 .= L1*v+f2.v by A1,A2,Def3 .= L1*v+L2*v by A1,A2,Def3 .= (L1+L2)*v by VECTSP_1:def 26; hence A4: g is with_eigenvalues by A2,Def1; thus A5: L1+L2 is eigenvalue of g by A2,A3,A4,Def2; let w such that A6: w is eigenvector of f1,L1 & w is eigenvector of f2,L2; g.w = f1.w+f2.w by MATRLIN:def 5 .= L1*w+f2.w by A1,A6,Def3 .= L1*w+L2*w by A1,A6,Def3 .= (L1+L2)*w by VECTSP_1:def 26; hence thesis by A4,A5,Def3; end; theorem Th11: id V is with_eigenvalues & 1_K is eigenvalue of id V & for v holds v is eigenvector of id V,1_K proof thus A1:id V is with_eigenvalues by Lm2; consider v such that A2:v<>0.V & id V.v=1_K*v by Lm2; thus A3: 1_K is eigenvalue of id V by A1,A2,Def2; let w; id V.w = w by FUNCT_1:34 .= 1_K*w by VECTSP_1:def 26; hence thesis by A1,A3,Def3; end; theorem for L be eigenvalue of id V holds L = 1_K proof let L be eigenvalue of id V; id V is with_eigenvalues by Th11; then consider v be Vector of V such that A1: v<>0.V & id V.v = L*v by Def2; L*v = v by A1,FUNCT_1:34 .= 1_K*v by VECTSP_1:def 26; hence thesis by A1,VECTSP10:5; end; theorem ker f is non trivial implies f is with_eigenvalues & 0.K is eigenvalue of f proof assume A1:ker f is non trivial; consider v be Vector of ker f such that A2: v<>0.ker f by A1,ANPROJ_1:def 8; reconsider v as Vector of V1 by VECTSP_4:18; A3: v<>0.V1 by A2,VECTSP_4:19; A4: f.v = 0.V1 by RANKNULL:14 .= 0.K*v by VECTSP_1:59; then f is with_eigenvalues by A3,Def1; hence thesis by A3,A4,Def2; end; theorem Th14: f is with_eigenvalues & L is eigenvalue of f iff ker (f+(-L)*id V1) is non trivial proof hereby assume f is with_eigenvalues & L is eigenvalue of f; then consider v1 such that A1: v1<>0.V1 & f.v1=L*v1 by Def2; (f+(-L)*id V1).v1 = f.v1+((-L)*id V1).v1 by MATRLIN:def 5 .= f.v1+(-L)*(id V1.v1) by MATRLIN:def 6 .= f.v1+(-L)*v1 by FUNCT_1:34 .= (L+-L)*v1 by A1,VECTSP_1:def 26 .= 0.K*v1 by VECTSP_1:66 .= 0.V1 by VECTSP_1:60; then v1 in ker (f+(-L)*id V1) by RANKNULL:10; then v1 is Element of ker (f+(-L)*id V1) & v1<>0.ker (f+(-L)*id V1) by A1,VECTSP_4:19,STRUCT_0:def 5; hence ker (f+(-L)*id V1) is non trivial by ANPROJ_1:def 8; end; assume ker (f+(-L)*id V1) is non trivial; then consider v be Vector of ker (f+(-L)*id V1) such that A2: v<>0.ker (f+(-L)*id V1) by ANPROJ_1:def 8; A3: v in ker (f+(-L)*id V1) by STRUCT_0:def 5; reconsider v as Vector of V1 by VECTSP_4:18; 0.V1 = (f+(-L)*id V1).v by A3,RANKNULL:10 .= f.v+((-L)*id V1).v by MATRLIN:def 5 .= f.v+(-L)*(id V1.v) by MATRLIN:def 6 .= f.v+(-L)*v by FUNCT_1:34; then A4: f.v = -(-L)*v by VECTSP_1:63 .= (--L)*v by VECTSP_1:68 .= L*v by RLVECT_1:30; A5: v<>0.V1 by A2,VECTSP_4:19; then f is with_eigenvalues by A4,Def1; hence thesis by A4,A5,Def2; end; theorem Th15: for V1 be finite-dimensional VectSp of K, b1,b1' be OrdBasis of V1 for f be linear-transformation of V1,V1 holds f is with_eigenvalues & L is eigenvalue of f iff Det AutEqMt(f+(-L)*id V1,b1,b1') =0.K proof let V1 be finite-dimensional VectSp of K, b1,b1' be OrdBasis of V1; let f be linear-transformation of V1,V1; A1: dim V1=dim V1; hereby assume f is with_eigenvalues & L is eigenvalue of f; then ker (f+(-L)*id V1) is non trivial by Th14; hence Det AutEqMt(f+(-L)*id V1,b1,b1') =0.K by A1,MATRLIN2:50; end; assume Det AutEqMt(f+(-L)*id V1,b1,b1') =0.K; then ker (f+(-L)*id V1) is non trivial by A1,MATRLIN2:50; hence thesis by Th14; end; theorem for K be algebraic-closed Field, V1 be non trivial finite-dimensional VectSp of K, f be linear-transformation of V1,V1 holds f is with_eigenvalues proof let K be algebraic-closed Field, V1 be non trivial finite-dimensional VectSp of K, f be linear-transformation of V1,V1; consider b1 be OrdBasis of V1; set AutA=AutMt(f,b1,b1); consider P be Polynomial of K such that A1: len P = len b1+1 and A2: for x be Element of K holds eval(P,x) = Det(AutA+x*1.(K,len b1)) by Th8; dim V1<>0 & dim V1 = len b1 by MATRLIN2:21,42; then len P>1+0 by A1,XREAL_1:10; then P is with_roots by POLYNOM5:def 8; then consider L be Element of K such that A3: L is_a_root_of P by POLYNOM5:def 7; A4: Mx2Tran(L*AutMt(id V1,b1,b1),b1,b1) = L*Mx2Tran(AutMt(id V1,b1,b1),b1,b1) by MATRLIN2:38 .= L*id V1 by MATRLIN2:34 .= Mx2Tran(AutMt(L*id V1,b1,b1),b1,b1) by MATRLIN2:34; 0.K = eval(P,L) by A3,POLYNOM5:def 6 .= Det(AutA+L*1.(K,len b1)) by A2 .= Det(AutA+L*AutMt(id V1,b1,b1)) by MATRLIN2:28 .= Det(AutA+AutMt(L*id V1,b1,b1)) by A4,MATRLIN2:39 .= Det(AutMt(f+L*id V1,b1,b1)) by MATRLIN:47 .= Det(AutMt(f+(-(-L))*id V1,b1,b1)) by RLVECT_1:30 .= Det(AutEqMt(f+(-(-L))*id V1,b1,b1)) by MATRLIN2:def 2; hence thesis by Th15; end; theorem Th17: for f,L st f is with_eigenvalues & L is eigenvalue of f holds v1 is eigenvector of f,L iff v1 in ker (f+(-L)*id V1) proof let f,L such that A1: f is with_eigenvalues & L is eigenvalue of f; hereby assume v1 is eigenvector of f,L; then A2: f.v1=L*v1 by A1,Def3; (f+(-L)*id V1).v1 = f.v1+((-L)*id V1).v1 by MATRLIN:def 5 .= f.v1+(-L)*(id V1.v1) by MATRLIN:def 6 .= f.v1+(-L)*v1 by FUNCT_1:34 .= (L+-L)*v1 by A2,VECTSP_1:def 26 .= 0.K*v1 by VECTSP_1:66 .= 0.V1 by VECTSP_1:60; hence v1 in ker (f+(-L)*id V1) by RANKNULL:10; end; assume v1 in ker (f+(-L)*id V1); then 0.V1 = (f+(-L)*id V1).v1 by RANKNULL:10 .= f.v1+((-L)*id V1).v1 by MATRLIN:def 5 .= f.v1+(-L)*(id V1.v1) by MATRLIN:def 6 .= f.v1+(-L)*v1 by FUNCT_1:34; then f.v1 = -(-L)*v1 by VECTSP_1:63 .= (--L)*v1 by VECTSP_1:68 .= L*v1 by RLVECT_1:30; hence thesis by A1,Def3; end; definition let S be 1-sorted; let F be Function of S,S; let n be Nat; func F |^ n -> Function of S,S means :Def4: for F' be Element of GFuncs the carrier of S st F'=F holds it = Product(n|-> F'); existence proof reconsider F'=F as Element of GFuncs the carrier of S by MONOID_0:82; reconsider P=Product(n|-> F') as Function of S,S by MONOID_0:82; take P; thus thesis; end; uniqueness proof let F1,F2 be Function of S,S such that A1: for F' be Element of GFuncs the carrier of S st F'=F holds F1 = Product(n|-> F') and A2: for F' be Element of GFuncs the carrier of S st F'=F holds F2 = Product(n|-> F'); reconsider F'=F as Element of GFuncs the carrier of S by MONOID_0:82; thus F1 = Product(n|-> F') by A1 .= F2 by A2; end; end; reserve S for 1-sorted, F for Function of S,S; theorem Th18: F |^ 0 = id S proof set G=GFuncs the carrier of S; reconsider F'=F as Element of G by MONOID_0:82; 0|->F'=<*>the carrier of G by FINSEQ_2:72; then Product(0|->F') = 1_G by GROUP_4:11 .= the_unity_wrt the multF of G by GROUP_1:33 .= id S by MONOID_0:84; hence thesis by Def4; end; theorem Th19: F |^ 1 = F proof set G=GFuncs the carrier of S; reconsider F'=F as Element of G by MONOID_0:82; Product(1|->F') = Product<*F'*> by FINSEQ_2:73 .= F' by GROUP_4:12; hence thesis by Def4; end; theorem Th20: F |^(i+j) = (F |^ i) * (F |^ j) proof set G=GFuncs the carrier of S; reconsider Fg=F as Element of G by MONOID_0:82; reconsider G as associative unital (non empty multMagma); reconsider F'=F as Element of G by MONOID_0:82; Product((i+j)|->F') = Product((i|->F')^(j|->F')) by FINSEQ_2:143 .= (Product(i|->F'))*(Product(j|->F')) by GROUP_4:8 .= Product(i|->Fg)(*)Product(j|->Fg) by MONOID_0:79 .= (F|^i)(*)Product(j|->Fg) by Def4 .= (F|^i)(*)(F|^j) by Def4; hence thesis by Def4; end; theorem for s1,s2 be Element of S,n,m st (F|^m).s1 = s2 & (F|^n).s2 = s2 holds (F|^(m+i*n)).s1 = s2 proof let s1,s2 be Element of S,n,m such that A1: (F|^m).s1 = s2 & (F|^n).s2 = s2; defpred P[Nat] means (F|^(m+$1*n)).s1 = s2; A2:P[0] by A1; A3:for i st P[i] holds P[i+1] proof let i such that A4: P[i]; A5: dom (F|^(m+i*n))=the carrier of S by FUNCT_2:67; per cases; suppose A6: the carrier of S<>{}; thus (F|^(m+(i+1)*n)).s1 = (F|^(n+(m+i*n))).s1 .= ((F|^n)*(F|^(m+i*n))).s1 by Th20 .= s2 by A1,A4,A5,A6,FUNCT_1:23; end; suppose the carrier of S={}; then not s1 in dom (F|^(m+(i+1)*n)) & s2={} by FUNCT_2:67,SUBSET_1:def 2; hence (F|^(m+(i+1)*n)).s1=s2 by FUNCT_1:def 4; end; end; for i holds P[i] from NAT_1:sch 2(A2,A3); hence thesis; end; theorem for K be add-associative right_zeroed right_complementable Abelian associative well-unital distributive(non empty doubleLoopStr), V1 be Abelian add-associative right_zeroed right_complementable VectSp-like (non empty VectSpStr over K) for W be Subspace of V1, f be Function of V1,V1, fW be Function of W,W st fW=f|W holds (f|^n)|W=fW|^n proof let K be add-associative right_zeroed right_complementable Abelian associative well-unital distributive(non empty doubleLoopStr), V1 be Abelian add-associative right_zeroed right_complementable VectSp-like (non empty VectSpStr over K); let W be Subspace of V1,f be Function of V1,V1,fW be Function of W,W such that A1: fW=f|W; defpred P[Nat] means (f|^$1)|W=fW|^$1; A2:P[0] proof [#]W c= [#]V1 by VECTSP_4:def 2; then A3: [#]W=[#]V1/\[#]W by XBOOLE_1:28; thus (f|^0)|W = (id V1)|W by Th18 .= (id V1)*id W by RELAT_1:94 .= id W by FUNCT_1:43,A3 .= fW|^0 by Th18; end; A4:for n st P[n] holds P[n+1] proof let n such that A5: P[n]; A6: rng (fW|^n) c= [#]W by RELSET_1:12; thus (f|^(n+1))|W = ((f|^1)*(f|^n))|W by Th20 .= (f|^1)*((f|^n)|W) by RELAT_1:112 .= (f|^1)*((id W)*(fW|^n)) by A5,A6,RELAT_1:79 .= ((f|^1)*(id W))*(fW|^n) by RELAT_1:55 .=(f*id W)*(fW|^n) by Th19 .= fW*(fW|^n) by A1,RELAT_1:94 .= (fW|^1)*(fW|^n) by Th19 .=fW|^(n+1) by Th20; end; for n holds P[n] from NAT_1:sch 2(A2,A4); hence thesis; end; definition let K,V1; let f be linear-transformation of V1,V1; let n be Nat; redefine func f |^ n -> linear-transformation of V1,V1; coherence proof defpred P[Nat] means f|^ $1 is linear-transformation of V1,V1; f|^0=id V1 by Th18; then A1: P[0]; A2: for k st P[k] holds P[k+1] proof let k; assume P[k]; then reconsider fk=f|^k as linear-transformation of V1,V1; f|^(k+1) = fk * f|^1 by Th20 .= fk*f by Th19; hence thesis; end; for k holds P[k] from NAT_1:sch 2(A1,A2); hence thesis; end; end; theorem Th23: (f|^i).v1 = 0.V1 implies (f|^(i+j)).v1=0.V1 proof assume A1: (f|^i).v1 = 0.V1; A2: dom (f|^i)=the carrier of V1 by FUNCT_2:def 1; thus (f|^(i+j)).v1 = ((f|^j)*(f|^i)).v1 by Th20 .= (f|^j).(0.V1) by A1,A2,FUNCT_1:23 .=0.V1 by RANKNULL:9; end; begin :: Generalized Eigenspace of a Linear Transformation definition let K,V1,f; func UnionKers f -> strict Subspace of V1 means :Def5: the carrier of it = {v where v is Vector of V1:ex n st (f|^n).v = 0.V1}; existence proof set S={v where v is Vector of V1:ex n st (f|^n).v=0.V1}; S c= the carrier of V1 proof let x such that A1: x in S; ex v be Vector of V1 st x=v & ex n st (f|^n).v=0.V1 by A1; hence thesis; end; then reconsider S as Subset of V1; (f|^0).(0.V1) = (id V1).0.V1 by Th18 .= 0.V1 by FUNCT_1:34; then A2: 0.V1 in S; A3: now let v,u be Element of V1 such that A4: v in S & u in S; consider v' be Vector of V1 such that A5: v'=v & ex n st (f|^n).v'=0.V1 by A4; consider n such that A6: (f|^n).v=0.V1 by A5; consider u' be Vector of V1 such that A7: u'=u & ex m st (f|^m).u'=0.V1 by A4; consider m such that A8: (f|^m).u=0.V1 by A7; now per cases; suppose m<=n; then reconsider i=n-m as Nat by NAT_1:21; (f|^n).(v+u) = (f|^n).v +(f|^(m+i)).u by MOD_2:def 5 .= 0.V1+0.V1 by A6,A8,Th23 .= 0.V1 by RLVECT_1:def 7; hence v+u in S; end; suppose m>n; then reconsider i=m-n as Nat by NAT_1:21; (f|^m).(v+u) = (f|^m).v +(f|^(n+i)).u by MOD_2:def 5 .= 0.V1+0.V1 by A6,A8,Th23 .= 0.V1 by RLVECT_1:def 7; hence v+u in S; end; end; hence v + u in S; end; now let a be Element of K,v be Element of V1 such that A9: v in S; consider v' be Vector of V1 such that A10: v'=v & ex n st (f|^n).v'=0.V1 by A9; consider n such that A11: (f|^n).v=0.V1 by A10; (f|^n).(a*v) = a*0.V1 by A11,MOD_2:def 5 .= 0.V1 by VECTSP_1:59; hence a * v in S; end; then S is linearly-closed by A3,VECTSP_4:def 1; hence thesis by A2,VECTSP_4:42; end; uniqueness by VECTSP_4:37; end; theorem Th24: v1 in UnionKers f iff ex n st (f|^n).v1 = 0.V1 proof hereby assume v1 in UnionKers f; then v1 in the carrier of UnionKers f by STRUCT_0:def 5; then v1 in {w where w is Vector of V1:ex n st (f|^n).w = 0.V1} by Def5; then ex w be Vector of V1 st v1=w & ex m st (f|^m).w=0.V1; hence ex n st (f|^n).v1=0.V1; end; assume ex n st (f|^n).v1=0.V1; then v1 in {w where w is Vector of V1:ex n st (f|^n).w = 0.V1}; then v1 in the carrier of UnionKers f by Def5; hence thesis by STRUCT_0:def 5; end; theorem Th25: ker (f|^i) is Subspace of UnionKers f proof the carrier of ker (f|^i) c= the carrier of UnionKers f proof let x such that A1: x in the carrier of ker (f|^i); reconsider v=x as Element of ker (f|^i) by A1; (f|^i).v=0.V1 & v is Vector of V1 by RANKNULL:14,VECTSP_4:18; then x in UnionKers f by Th24; hence thesis by STRUCT_0:def 5; end; hence ker (f|^i) is Subspace of UnionKers f by VECTSP_4:35; end; theorem Th26: ker (f|^i) is Subspace of ker (f|^(i+j)) proof the carrier of ker (f|^i) c= the carrier of ker (f|^(i+j)) proof let x such that A1: x in the carrier of ker(f|^i); reconsider v = x as Vector of V1 by A1,VECTSP_4:18; (f|^i).v = 0.V1 by A1,RANKNULL:14; then (f|^(i+j)).v = 0.V1 by Th23; then v in ker (f|^(i+j)) by RANKNULL:10; hence thesis by STRUCT_0:def 5; end; hence thesis by VECTSP_4:35; end; theorem for V be finite-dimensional VectSp of K,f be linear-transformation of V,V ex n st UnionKers f = ker (f|^n) proof let V be finite-dimensional VectSp of K; let f be linear-transformation of V,V; defpred P[Nat] means for n holds dim ker(f|^n)<=$1; P[dim UnionKers f] proof let n; ker (f|^n) is Subspace of UnionKers f by Th25; hence thesis by VECTSP_9:29; end; then A1: ex k st P[k]; ex k st P[k] & for n st P[n] holds k<=n from NAT_1:sch 5(A1); then consider k such that A2: P[k] & for n st P[n] holds k<=n; ex m st dim ker(f|^m)=k proof assume A3: for m holds dim ker(f|^m)<>k; then dim ker(f|^0)<>k & dim ker (f|^0)<=k by A2; then dim ker(f|^0)k & dim ker (f|^n)<=k by A3,A2; then dim ker(f|^n)ker (f|^m); then consider v be Element of UnionKers f such that A6: not v in ker (f|^m) by A5,VECTSP_4:40; A7: v in UnionKers f by STRUCT_0:def 5; reconsider v as Vector of V by VECTSP_4:18; consider i such that A8: (f|^i).v=0.V by A7,Th24; i>m proof assume i<=m; then reconsider j=m-i as Element of NAT by NAT_1:21; (f|^(j+i)).v=0.V by A8,Th23; hence thesis by A6,RANKNULL:10; end; then reconsider j=i-m as Element of NAT by NAT_1:21; A9: ker (f|^m) is Subspace of ker (f|^(m+j)) by Th26; (Omega).(ker (f|^m))<>(Omega).(ker(f|^i)) by A6,A8,RANKNULL:10; then k <> dim ker (f|^i) & k<=dim ker(f|^i) by A4,A9,VECTSP_9:29,32; then k < dim ker (f|^i) by XXREAL_0:1; hence thesis by A2; end; theorem Th28: f|ker (f|^n) is linear-transformation of ker (f|^n),ker (f|^n) proof set KER=ker (f|^n); rng (f|KER)c= the carrier of KER proof let y such that A1: y in rng (f|KER); consider x such that A2: x in dom (f|KER) & (f|KER).x=y by A1,FUNCT_1:def 5; x in the carrier of KER by A2,FUNCT_2:def 1; then A3: x in KER by STRUCT_0:def 5; then x in V1 by VECTSP_4:17; then reconsider v=x as Vector of V1 by STRUCT_0:def 5; A4: dom f = the carrier of V1 by FUNCT_2:def 1; (f|^n).v = 0.V1 by A3,RANKNULL:10; then 0.V1 = (f|^(n+1)).v by Th23 .= ((f|^n)*(f|^1)).v by Th20 .= ((f|^n)*f).v by Th19 .= (f|^n).(f.v) by A4,FUNCT_1:23; then f.v in KER & y=f.v by RANKNULL:10,A2,FUNCT_1:70; hence thesis by STRUCT_0:def 5; end; hence thesis by FUNCT_2:8,Lm1; end; theorem f|ker ((f+L*id V1)|^n) is linear-transformation of ker ((f+L*id V1)|^n), ker ((f+L*id V1)|^n) proof set fid= f+L*id V1; set KER=ker (fid|^n); reconsider fidK=fid|KER as linear-transformation of KER,KER by Th28; rng (f|KER) c= the carrier of KER proof let y such that A1: y in rng (f|KER); consider x such that A2: x in dom (f|KER) & (f|KER).x=y by A1,FUNCT_1:def 5; A3: x in the carrier of KER by A2,FUNCT_2:def 1; then A4: x in KER by STRUCT_0:def 5; then x in V1 by VECTSP_4:17; then reconsider v=x as Vector of V1 by STRUCT_0:def 5; fid.v = f.v+(L*id V1).v by MATRLIN:def 5 .= f.v +L*((id V1).v) by MATRLIN:def 6 .= f.v +L*v by FUNCT_1:35; then A5: fid.v + (-L)*v = f.v + (L*v+ (-L)*v) by RLVECT_1:def 6 .= f.v+((L+(-L))*v) by VECTSP_1:def 26 .= f.v+(0.K *v) by VECTSP_1:63 .= f.v+0.V1 by VECTSP_1:59 .= f.v by RLVECT_1:def 7; dom fidK=the carrier of KER by FUNCT_2:def 1; then fidK.v = fid.v & fidK/.v=fidK.v by A3,FUNCT_1:70,PARTFUN1:def 8; then fid.v in KER & (-L)*v in KER by A4,STRUCT_0:def 5,VECTSP_4:29; then f.v in KER & (f|KER).v =f.v by A2,A5,VECTSP_4:28,FUNCT_1:70; hence thesis by A2,STRUCT_0:def 5; end; hence thesis by FUNCT_2:8,Lm1; end; theorem Th30: f|(UnionKers f) is linear-transformation of UnionKers f,UnionKers f proof set U=UnionKers f; rng (f|U)c= the carrier of U proof let y such that A1: y in rng (f|U); consider x such that A2: x in dom (f|U) & (f|U).x=y by A1,FUNCT_1:def 5; x in the carrier of U by A2,FUNCT_2:def 1; then A3: x in U by STRUCT_0:def 5; then x in V1 by VECTSP_4:17; then reconsider v=x as Vector of V1 by STRUCT_0:def 5; consider n such that A4: (f|^n).v=0.V1 by A3,Th24; A5: dom f =[#]V1 by FUNCT_2:def 1; 0.V1 = (f|^(n+1)).v by A4,Th23 .= ((f|^n)*(f|^1)).v by Th20 .= ((f|^n)*f).v by Th19 .=(f|^n).(f.v) by A5,FUNCT_1:23; then f.v in U & y=f.v by A2,FUNCT_1:70,Th24; hence thesis by STRUCT_0:def 5; end; hence thesis by FUNCT_2:8,Lm1; end; theorem Th31: f|(UnionKers (f+L*id V1)) is linear-transformation of UnionKers (f+L*id V1), UnionKers (f+L*id V1) proof set fid= f+L*id V1; set U=UnionKers fid; reconsider fidU=fid|U as linear-transformation of U,U by Th30; rng (f|U) c= the carrier of U proof let y such that A1: y in rng (f|U); consider x such that A2: x in dom (f|U) & (f|U).x=y by A1,FUNCT_1:def 5; A3: x in the carrier of U by A2,FUNCT_2:def 1; then A4: x in U by STRUCT_0:def 5; then x in V1 by VECTSP_4:17; then reconsider v=x as Vector of V1 by STRUCT_0:def 5; fid.v = f.v+(L*id V1).v by MATRLIN:def 5 .= f.v +L*((id V1).v) by MATRLIN:def 6 .= f.v +L*v by FUNCT_1:35; then A5: fid.v + (-L)*v = f.v + (L*v+ (-L)*v) by RLVECT_1:def 6 .= f.v+((L+(-L))*v) by VECTSP_1:def 26 .= f.v+(0.K *v) by VECTSP_1:63 .= f.v+0.V1 by VECTSP_1:59 .= f.v by RLVECT_1:def 7; dom fidU=the carrier of U by FUNCT_2:def 1; then fidU.v=fid.v & fidU/.v=fidU.v by A3,FUNCT_1:70,PARTFUN1:def 8; then fid.v in U & (-L)*v in U by A4,STRUCT_0:def 5,VECTSP_4:29; then f.v in U & (f|U).v =f.v by A2,A5,VECTSP_4:28,FUNCT_1:70; hence thesis by A2,STRUCT_0:def 5; end; hence thesis by FUNCT_2:8,Lm1; end; theorem Th32: f|im (f|^n) is linear-transformation of im (f|^n),im (f|^n) proof set IM=im (f|^n); rng(f|IM) c= the carrier of IM proof let y such that A1: y in rng (f|IM); consider x such that A2: x in dom (f|IM) & (f|IM).x=y by A1,FUNCT_1:def 5; x in the carrier of IM by A2,FUNCT_2:def 1; then A3: x in IM by STRUCT_0:def 5; then x in V1 by VECTSP_4:17; then reconsider v=x as Vector of V1 by STRUCT_0:def 5; consider w be Vector of V1 such that A4: (f|^n).w=v by A3,RANKNULL:13; A5: the carrier of V1=dom (f|^n) & the carrier of V1 = dom (f|^1) by FUNCT_2:def 1; y = f.x by A2,FUNCT_1:70 .= (f*(f|^n)).w by A4,A5,FUNCT_1:23 .= ((f|^1)*(f|^n)).w by Th19 .= (f|^(1+n)).w by Th20 .= ((f|^n)*(f|^1)).w by Th20 .= (f|^n).((f|^1).w) by A5,FUNCT_1:23; then y in IM by RANKNULL:13; hence thesis by STRUCT_0:def 5; end; hence thesis by Lm1,FUNCT_2:8; end; theorem f|im ((f+L*id V1)|^n) is linear-transformation of im ((f+L*id V1)|^n), im ((f+L*id V1)|^n) proof set fid =f+L*id V1; set IM=im(fid|^n); reconsider fidI=fid|IM as linear-transformation of IM,IM by Th32; rng (f|IM) c= the carrier of IM proof let y such that A1: y in rng (f|IM); consider x such that A2: x in dom (f|IM) & (f|IM).x=y by A1,FUNCT_1:def 5; A3: x in the carrier of IM by A2,FUNCT_2:def 1; then A4: x in IM by STRUCT_0:def 5; then x in V1 by VECTSP_4:17; then reconsider v=x as Vector of V1 by STRUCT_0:def 5; fid.v = f.v+(L*id V1).v by MATRLIN:def 5 .= f.v +L*((id V1).v) by MATRLIN:def 6 .= f.v +L*v by FUNCT_1:35; then A5: fid.v + (-L)*v = f.v + (L*v+ (-L)*v) by RLVECT_1:def 6 .= f.v+((L+(-L))*v) by VECTSP_1:def 26 .= f.v+(0.K *v) by VECTSP_1:63 .= f.v+0.V1 by VECTSP_1:59 .= f.v by RLVECT_1:def 7; dom fidI=the carrier of IM by FUNCT_2:def 1; then fidI.v=fid.v & fidI/.v=fidI.v by A3,FUNCT_1:70,PARTFUN1:def 8; then fid.v in IM & (-L)*v in IM by A4,STRUCT_0:def 5,VECTSP_4:29; then f.v in IM & (f|IM).v =f.v by A2,A5,VECTSP_4:28,FUNCT_1:70; hence thesis by A2,STRUCT_0:def 5; end; hence thesis by FUNCT_2:8,Lm1; end; theorem Th34: UnionKers f = ker (f|^n) implies ker (f|^n) /\ im (f|^n) = (0).V1 proof assume A1: UnionKers f = ker (f|^n); set KER=ker (f|^n); set IM = im (f|^n); A2: the carrier of KER /\ IM c= {0.V1} proof let x such that A3: x in the carrier of KER/\IM; A4: x in KER/\IM by A3,STRUCT_0:def 5; then x in V1 by VECTSP_4:17; then reconsider v=x as Vector of V1 by STRUCT_0:def 5; A5: v in KER by A4,VECTSP_5:7; v in IM by A4,VECTSP_5:7; then consider w be Element of V1 such that A6: (f|^n).w=v by RANKNULL:13; A7: dom (f|^n) = the carrier of V1 by FUNCT_2:def 1; 0.V1 = (f|^n).((f|^n).w) by A5,A6,RANKNULL:10 .= ((f|^n)*(f|^n)).w by A7,FUNCT_1:23 .= (f|^(n+n)).w by Th20; then w in ker(f|^n) by A1,Th24; then v=0.V1 by A6,RANKNULL:10; hence thesis by TARSKI:def 1; end; the carrier of KER/\IM = {0.V1} by A2,ZFMISC_1:39 .= the carrier of (0).V1 by VECTSP_4:def 3; hence KER/\IM=(0).V1 by VECTSP_4:37; end; theorem for V be finite-dimensional VectSp of K, f be linear-transformation of V,V,n st UnionKers f = ker (f|^n) holds V is_the_direct_sum_of ker (f|^n),im (f|^n) proof let V be finite-dimensional VectSp of K,f be linear-transformation of V,V,n; assume A1: UnionKers f = ker (f|^n); set KER=ker (f|^n); set IM=im (f|^n); (Omega).(IM/\KER) = (0).V by A1,Th34 .= (0).(IM/\KER) by VECTSP_4:47; then A2: dim (IM/\KER)=0 by VECTSP_9:33; dim V = rank (f|^n)+nullity (f|^n) by RANKNULL:44 .= dim (IM+KER)+dim (IM/\KER) by VECTSP_9:36; then (Omega).V=(Omega).(IM+KER) by A2,VECTSP_9:32; then KER + IM = (Omega).V & KER/\IM=(0).V by A1,VECTSP_5:9,Th34; hence thesis by VECTSP_5:def 4; end; theorem Th36: for I be Linear_Compl of UnionKers f holds f|I is one-to-one proof let I be Linear_Compl of UnionKers f; set fI=f|I; set U=UnionKers f; A1: the carrier of ker fI c= {0.I} proof let x such that A2: x in the carrier of ker fI; A3: x in ker fI by A2,STRUCT_0:def 5; then A4: x in I by VECTSP_4:17; then reconsider v=x as Vector of I by STRUCT_0:def 5; reconsider w=v as Vector of V1 by VECTSP_4:18; A5: U/\I = (0).V1 by VECTSP_5:50; 0.I = 0.V1 by VECTSP_4:19 .= (f|I).v by A3,RANKNULL:10 .= f.v by FUNCT_1:72; then (f|^1).w = 0.I by Th19 .= 0.V1 by VECTSP_4:19; then v in U by Th24; then v in U/\I by A4,VECTSP_5:7; then v in the carrier of (0).V1 by A5,STRUCT_0:def 5; then v in {0.V1} by VECTSP_4:def 3; then v = 0.V1 by TARSKI:def 1 .= 0.I by VECTSP_4:19; hence thesis by TARSKI:def 1; end; the carrier of ker fI = {0.I} by A1,ZFMISC_1:39 .= the carrier of (0).I by VECTSP_4:def 3; then ker fI = (0).I by VECTSP_4:37; hence thesis by MATRLIN2:43; end; theorem Th37: for I be Linear_Compl of UnionKers (f+(-L)*id V1), fI be linear-transformation of I,I st fI = f|I for v be Vector of I st fI.v = L * v holds v = 0.V1 proof set V=V1; set fi=f+(-L)*id V; let I be Linear_Compl of UnionKers fi, fI be linear-transformation of I,I such that A1: fI = f|I; A2: fi|I is one-to-one by Th36; let v be Vector of I such that A3: fI.v = L * v; reconsider v1=v as Vector of V by VECTSP_4:18; A4: f.v = fI.v by A1,FUNCT_1:72 .= L*v1 by A3,VECTSP_4:22; (fi|I).v1 = fi.v1 by FUNCT_1:72 .= f.v1+((-L)*id V).v1 by MATRLIN:def 5 .= f.v1 +(-L)*(id V.v1) by MATRLIN:def 6 .= L*v1 +(-L)*v1 by A4,FUNCT_1:35 .= (L+(-L))*v1 by VECTSP_1:def 26 .= 0.K*v1 by VECTSP_1:66 .= 0.V by VECTSP_1:59; then v1 in ker (fi|I) & ker (fi|I)=(0).I by A2,RANKNULL:10,MATRLIN2:43; hence v = 0.I by VECTSP_4:46 .= 0.V by VECTSP_4:19; end; Lm3:for a,b be Scalar of K holds (a*b)*f=a*(b*f) proof let a,b be Scalar of K; A1: dom ((a*b)*f)=[#]V1 & dom (a*(b*f))=[#]V1 by FUNCT_2:def 1; now let x such that A2: x in dom ((a*b)*f); reconsider v=x as Element of V1 by FUNCT_2:def 1,A2; thus ((a*b)*f).x = (a*b)*(f.v) by MATRLIN:def 6 .= a*(b*f.v) by VECTSP_1:def 26 .= a*(b*f).v by MATRLIN:def 6 .= (a*(b*f)).x by MATRLIN:def 6; end; hence thesis by A1,FUNCT_1:9; end; Lm4:for f,g be Function of V1,V1 holds L*(f*g)=(L*f)*g proof let f,g be Function of V1,V1; A1: dom (L*(f*g))=[#]V1 & dom ((L*f)*g)=[#]V1 & dom g=[#]V1 by FUNCT_2:def 1; now let x such that A2: x in dom (L*(f*g)); reconsider v=x as Element of V1 by FUNCT_2:def 1,A2; thus (L*(f*g)).x = L* (f*g).v by MATRLIN:def 6 .= L*(f.(g.v)) by A1,FUNCT_1:23 .= (L*f).(g.v) by MATRLIN:def 6 .= ((L*f)*g).x by A1,FUNCT_1:22; end; hence thesis by A1,FUNCT_1:9; end; Lm5:for f,g be Function of V1,V1 st f is linear holds L*(f*g)=f*(L*g) proof let f,g be Function of V1,V1 such that A1: f is linear; A2: dom (L*(f*g))=[#]V1 & dom (f*(L*g))=[#]V1 & dom g=[#]V1 by FUNCT_2:def 1; now let x such that A3: x in dom (L*(f*g)); reconsider v=x as Element of V1 by FUNCT_2:def 1,A3; thus (L*(f*g)).x = L* (f*g).v by MATRLIN:def 6 .= L*(f.(g.v)) by A2,FUNCT_1:23 .= f.(L*(g.v)) by A1,MOD_2:def 5 .= f.((L*g).v) by MATRLIN:def 6 .= (f*(L*g)).x by A2,FUNCT_1:22; end; hence thesis by A2,FUNCT_1:9; end; Lm6:for f1,f2,g be Function of V1,V1 holds (f1+f2)*g=(f1*g)+(f2*g) proof let f1,f2,g be Function of V1,V1; A1: dom ((f1+f2)*g)=[#]V1 & dom ((f1*g)+(f2*g))=[#]V1 & dom g=[#]V1 by FUNCT_2:def 1; now let x such that A2: x in dom g; reconsider v=x as Element of V1 by FUNCT_2:def 1,A2; thus ((f1+f2)*g).x = (f1+f2).(g.v) by A1,FUNCT_1:22 .= f1.(g.v)+f2.(g.v) by MATRLIN:def 5 .= (f1*g).v+f2.(g.v) by A1,FUNCT_1:23 .= (f1*g).v+(f2*g).v by A1,FUNCT_1:23 .= ((f1*g)+(f2*g)).x by MATRLIN:def 5; end; hence thesis by A1,FUNCT_1:9; end; Lm7:for f1,f2,g be Function of V1,V1 st g is linear holds g*(f1+f2)=(g*f1)+(g*f2) proof let f1,f2,g be Function of V1,V1 such that A1: g is linear; A2: dom (g*(f1+f2))=[#]V1 & dom ((g*f1)+(g*f2))=[#]V1 & dom f1 = [#]V1 & dom f2 = [#]V1 by FUNCT_2:def 1; now let x such that A3: x in dom (g*(f1+f2)); reconsider v=x as Element of V1 by FUNCT_2:def 1,A3; thus (g*(f1+f2)).x = g.((f1+f2).v) by A2,FUNCT_1:22 .= g.(f1.v+f2.v) by MATRLIN:def 5 .= g.(f1.v)+g.(f2.v) by A1,MOD_2:def 5 .= (g*f1).v+g.(f2.v) by A2,FUNCT_1:23 .= (g*f1).v+(g*f2).v by A2,FUNCT_1:23 .= ((g*f1)+(g*f2)).x by MATRLIN:def 5; end; hence thesis by A2,FUNCT_1:9; end; Lm8: for f1,f2,f3 be Function of V1,V1 holds f1+f2+f3=f1+(f2+f3) proof let f1,f2,f3 be Function of V1,V1; A1: dom (f1+f2+f3)=[#]V1 & dom (f1+(f2+f3))=[#]V1 by FUNCT_2:def 1; now let x such that A2: x in dom (f1+f2+f3); reconsider v=x as Element of V1 by FUNCT_2:def 1,A2; thus (f1+f2+f3).x = (f1+f2).v+f3.v by MATRLIN:def 5 .= (f1.v+f2.v)+f3.v by MATRLIN:def 5 .= f1.v+(f2.v+f3.v) by RLVECT_1:def 6 .= f1.v+(f2+f3).v by MATRLIN:def 5 .= (f1+(f2+f3)).x by MATRLIN:def 5; end; hence thesis by A1,FUNCT_1:9; end; Lm9:(L*id V1) |^ n = (power K).(L,n)*id V1 proof defpred P[Nat] means (L*id V1) |^ $1 = (power K).(L,$1)*id V1; A1:P[0] proof A2: (L*id V1) |^ 0 = id V1 & (power K).(L,0)=1_K by Th18,GROUP_1:def 8; A3: dom id V1 = [#]V1 & dom (1_K*id V1)=[#]V1 by FUNCT_2:def 1; now let x such that A4: x in [#]V1; reconsider v=x as Vector of V1 by A4; (id V1).x=v & 1_K*v=v by FUNCT_1:35,VECTSP_1:def 26; hence (id V1).x=(1_K*id V1).x by MATRLIN:def 6; end; hence thesis by A2,A3,FUNCT_1:9; end; A5:for n st P[n] holds P[n+1] proof let n such that A6: P[n]; A7: n in NAT by ORDINAL1:def 13; thus (L*id V1) |^ (n+1) = ((L*id V1) |^ 1)*((power K).(L,n)*id V1) by A6,Th20 .= L*(id V1)*((power K).(L,n)*id V1) by Th19 .= (power K).(L,n)*(L*(id V1)*(id V1)) by Lm5 .= (power K).(L,n)*(L*((id V1)*(id V1))) by Lm4 .= (power K).(L,n)*(L*id V1) by SYSREL:29 .= ((power K).(L,n)*L)*id V1 by Lm3 .=(power K).(L,n+1)*id V1 by A7,GROUP_1:def 8; end; for n holds P[n] from NAT_1:sch 2(A1,A5); hence thesis; end; Lm10:for a,b be Scalar of K holds (a+b)*f = a*f + b*f proof let a,b be Scalar of K; A1: dom ((a+b)*f)=[#]V1 & dom (a*f + b*f)=[#]V1 by FUNCT_2:def 1; now let x such that A2: x in dom ((a+b)*f); reconsider v=x as Element of V1 by FUNCT_2:def 1,A2; thus ((a+b)*f).x = (a+b)*(f.v) by MATRLIN:def 6 .= a*f.v+b*f.v by VECTSP_1:def 26 .= (a*f).v+b*f.v by MATRLIN:def 6 .= (a*f).v+(b*f).v by MATRLIN:def 6 .=(a*f + b*f).x by MATRLIN:def 5; end; hence thesis by A1,FUNCT_1:9; end; theorem Th38: n >= 1 implies ex h be linear-transformation of V1,V1 st (f + L*id V1) |^ n = f * h + ((L*id V1) |^ n) & for i holds (f |^ i) * h = h * (f |^ i) proof set g=L*id V1; defpred P[Nat] means ex h be linear-transformation of V1,V1 st (f+g)|^$1 = f * h + (g|^$1) & for i holds (f |^i) * h = h * (f|^i); A1: P[1] proof take h=id V1; thus (f+g)|^1 = f+g by Th19 .= (f|^(1+0))+g by Th19 .= (f|^1)*(f|^0)+g by Th20 .= (f|^1)*h+g by Th18 .= f*h+g by Th19 .= f*h+(g|^1) by Th19; let i; thus (f |^i) * h = (f |^i) * (f|^0) by Th18 .= f|^(i+0) by Th20 .= (f |^0) * (f|^i) by Th20 .= h * (f|^i) by Th18; end; A2: for n st 1<=n holds P[n] implies P[n+1] proof let n such that 1<=n; assume P[n]; then consider h be linear-transformation of V1,V1 such that A3: (f+g)|^n = f * h + (g|^n) and A4: for i holds (f |^i) * h = h * (f|^i); take H=f*h+(g|^n)+L*h; A5: rng (f * h) c= [#] V1 by RELSET_1:12; thus (f+g)|^(n+1) = ((f+g)|^1)*((f+g)|^n) by Th20 .= (f+g)*(f * h + (g|^n)) by A3,Th19 .= (f*(f * h + (g|^n)))+ (g*(f * h + (g|^n))) by Lm6 .= (f*(f * h + (g|^n)))+ (g*(f * h) + (g*(g|^n))) by Lm7 .= (f*(f * h + (g|^n)))+ g*(f * h) + (g*(g|^n)) by Lm8 .= (f*(f * h + (g|^n)))+ L*(id V1*(f * h))+(g*(g|^n)) by Lm4 .= (f*(f * h + (g|^n)))+ L*(f * h) + (g*(g|^n)) by A5,RELAT_1:79 .= (f*(f * h + (g|^n)))+ f * (L*h) + (g*(g|^n)) by Lm5 .= f*H + (g*(g|^n)) by Lm7 .= f*H + ((g|^1)*(g|^n)) by Th19 .= f*H + (g|^(n+1)) by Th20; let i; A6: (f |^i)*(L*h) = L*((f |^i)*h) by Lm5 .= L*(h*(f|^i)) by A4 .= (L*h)*(f|^i) by Lm4; A7: (f |^i) *(f*h) = (f |^i) *f*h by RELAT_1:55 .= ((f |^i) *(f|^1))*h by Th19 .= (f |^(i+1))*h by Th20 .= h*(f |^(i+1)) by A4 .= h*((f |^1)* (f |^i)) by Th20 .= (h*(f|^1))* (f |^i) by RELAT_1:55 .= ((f|^1)*h)* (f |^i) by A4 .= (f*h)* (f |^i) by Th19; A8: (f |^i) * (g|^n) = (f |^i) * ((power K).(L,n)*id V1) by Lm9 .= (power K).(L,n) *((f |^i) * id V1) by Lm5 .= (power K).(L,n) *((f |^i) * (f|^0)) by Th18 .= (power K).(L,n) *(f |^(i+0)) by Th20 .= (power K).(L,n) *((f |^0) * (f|^i)) by Th20 .= (power K).(L,n) *((id V1) * (f|^i)) by Th18 .= ((power K).(L,n) *id V1) * (f|^i) by Lm4 .= (g|^n) * (f|^i) by Lm9; thus (f |^i) * H = ((f |^i) *(f*h+(g|^n)))+(L*h)*(f|^i) by A6,Lm7 .= ((f*h)* (f |^i))+ ((g|^n) * (f|^i))+(L*h)*(f|^i) by A7,A8,Lm7 .= (((f*h)+(g|^n)) * (f|^i))+(L*h)*(f|^i) by Lm6 .= H*(f|^i) by Lm6; end; for n st 1<=n holds P[n] from NAT_1:sch 8(A1,A2); hence thesis; end; theorem for L1,L2 be Scalar of K st f is with_eigenvalues & L1 <> L2 & L1 is eigenvalue of f & L2 is eigenvalue of f for I be Linear_Compl of UnionKers (f+(-L1)*id V1), fI be linear-transformation of I,I st fI = f|I holds fI is with_eigenvalues & not L1 is eigenvalue of fI & L2 is eigenvalue of fI & UnionKers (f+(-L2)*id V1) is Subspace of I proof let L1,L2 be Scalar of K such that A1: f is with_eigenvalues and A2: L1 <> L2 and L1 is eigenvalue of f and A3: L2 is eigenvalue of f; set V=V1; set f1=(f+(-L1)*id V); set f2=(f+(-L2)*id V); set U=UnionKers f1; let I be Linear_Compl of U; let fI be linear-transformation of I,I such that A4: fI = f|I; reconsider fU=f|U as linear-transformation of U,U by Th31; A5: now let v be Vector of V such that A6: v in UnionKers f2; set v1=v|--(I,U); set i1=v1`1; set u1=v1`2; A7: V is_the_direct_sum_of I,U by VECTSP_5:def 5; then A8: v=i1 + u1 & i1 in I & u1 in U by VECTSP_5:def 6; consider n such that A9: (f1|^n).u1 =0.V by A8,Th24; assume A10: not v is Vector of I; A11: u1 <>0.V proof assume u1=0.V; then v =i1 by A8,RLVECT_1:def 7; hence thesis by A8,A10,STRUCT_0:def 5; end; set L21=L2-L1; set f21=f2+L21*id V; n<>0 proof assume n=0; then 0.V = (id V).u1 by A9,Th18 .= u1 by FUNCT_1:35; hence thesis by A11; end; then consider h be linear-transformation of V,V such that A12: f21 |^ n = f2 * h + ((L21*id V) |^ n) and A13: for i holds (f2 |^ i) * h = h * (f2 |^ i) by Th38,NAT_1:14; consider m such that A14: (f2|^m).v =0.V by A6,Th24; defpred Q[Nat] means for W be Subspace of V st W=I or W=U for w be Vector of V st w in W holds (f2|^$1).w in W; A15: Q[0] proof let W be Subspace of V such that W=I or W=U; let w be Vector of V such that A16: w in W; (f2|^0).w = (id V).w by Th18 .= w by FUNCT_1:35; hence thesis by A16; end; A17: for n st Q[n] holds Q[n+1] proof let n such that A18: Q[n]; let W be Subspace of V such that A19: W=I or W=U; let w be Vector of V such that A20: w in W; A21: dom (f2|^n) = [#]V by FUNCT_2:def 1; set fnw=(f2|^n).w; A22: fnw in W by A18,A19,A20; A23: now per cases by A19; suppose A24: W=I; then reconsider F=fnw as Vector of I by A22,STRUCT_0:def 5; f.fnw = fI.F by A4,FUNCT_1:72; hence f.fnw in W by A24,STRUCT_0:def 5; end; suppose A25: W=U; then reconsider F=fnw as Vector of U by A22,STRUCT_0:def 5; f.fnw = fU.F by FUNCT_1:72; hence f.fnw in W by A25,STRUCT_0:def 5; end; end; ((-L2)*id V).fnw = (-L2)*((id V).fnw) by MATRLIN:def 6 .= (-L2)*fnw by FUNCT_1:35; then A26: ((-L2)*id V).fnw in W by A22,VECTSP_4:29; (f2|^(n+1)).w = ((f2|^1)*(f2|^n)).w by Th20 .= (f2|^1).fnw by A21,FUNCT_1:23 .= (f+(-L2)*id V).fnw by Th19 .= f.fnw+((-L2)*id V).fnw by MATRLIN:def 5; hence thesis by A23,A26,VECTSP_4:28; end; A27: for n holds Q[n] from NAT_1:sch 2(A15,A17); defpred P[Nat] means (f2|^$1).u1 = 0.V; A28: (f2|^m).i1 in I & (f2|^m).u1 in U & 0.V in I & 0.V in U by VECTSP_4:25,A8,A27; 0.V+0.V = 0.V by RLVECT_1:def 7 .= (f2|^m).i1 +(f2|^m).u1 by A8,A14,MOD_2:def 5; then (f2|^m).u1=0.V by A7,A28,VECTSP_5:58; then A29: ex m st P[m]; consider MIN be Nat such that A30: P[MIN] and A31: for n st P[n] holds MIN <= n from NAT_1:sch 5(A29); MIN <>0 proof assume MIN=0; then 0.V = (id V).u1 by A30,Th18 .= u1 by FUNCT_1:35; hence thesis by A11; end; then reconsider M1=MIN-1 as Element of NAT by NAT_1:20; A32: (f2|^M1)*(f2 * h) = (f2|^M1)*f2 * h by RELAT_1:55 .= (f2|^M1)*(f2|^1)*h by Th19 .= (f2|^(M1+1))*h by Th20 .= h*(f2|^MIN) by A13; dom (f2|^MIN) =[#]V by FUNCT_2:def 1; then A33: (h*(f2|^MIN)).u1 = h.((f2|^MIN).u1) by FUNCT_1:23 .= 0.V by A30,RANKNULL:9; A34: dom((L21*id V) |^ n)=[#]V by FUNCT_2:def 1; A35: ((f2|^M1) * ((L21*id V) |^ n)).u1 = (f2|^M1).(((L21*id V) |^ n).u1) by A34,FUNCT_1:23 .= (f2|^M1).(((power K).(L21,n) * id V).u1) by Lm9 .= (f2|^M1).((power K).(L21,n)*((id V).u1)) by MATRLIN:def 6 .= (f2|^M1).( (power K).(L21,n)*u1) by FUNCT_1:35 .= (power K).(L21,n) * ((f2|^M1).u1) by MOD_2:def 5; A36: dom (f21|^n)=[#]V by FUNCT_2:def 1; f21 = f+((-L2)*id V + (L21*id V)) by Lm8 .= f+((-L2+L21)*id V) by Lm10 .= f+((-L2+L2-L1)*id V) by RLVECT_1:def 6 .= f+((0.K+-L1)*id V) by VECTSP_1:66 .= f1 by RLVECT_1:def 7; then A37: 0.V =(f2|^M1).((f21|^n).u1) by A9,RANKNULL:9 .= ((f2|^M1)*(f2 * h + ((L21*id V) |^ n))).u1 by A12,A36,FUNCT_1:23 .= (h*(f2|^MIN) + (f2|^M1) * ((L21*id V) |^ n)).u1 by A32,Lm7 .= 0.V + (power K).(L21,n) * ((f2|^M1).u1) by A33,A35,MATRLIN:def 5 .= (power K).(L21,n) * ((f2|^M1).u1) by RLVECT_1:def 7; (power K).(L21,n) <>0.K proof assume 0.K=(power K).(L21,n); then 0.K = Product (n|->L21) by MATRIXJ1:5; then consider k be Element of NAT such that A38: k in dom (n|->L21) & (n|->L21).k=0.K by FVSUM_1:107; dom (n|->L21)=Seg n by FINSEQ_2:144; then L21=0.K by A38,FINSEQ_1:4,FINSEQ_2:71; hence thesis by A2,VECTSP_1:66; end; then (f2|^M1).u1 = 0.V by A37,VECTSP_1:60; then M1+1<=M1 by A31; hence contradiction by NAT_1:13; end; consider v be Vector of V such that A39: v <> 0.V & f.v = L2 * v by A1,A3,Def2; v is eigenvector of f,L2 by A1,A3,A39,Def3; then v in ker(f2) by A1,A3,Th17; then 0.V = f2.v by RANKNULL:10 .= (f2|^1).v by Th19; then v in UnionKers f2 by Th24; then reconsider vI=v as Vector of I by A5; A40: 0.V = 0.I & L2*v=L2*vI & f.v=fI.vI by A4,VECTSP_4:19,22,FUNCT_1:72; hence A41: fI is with_eigenvalues by A39,Def1; not L1 is eigenvalue of fI proof assume L1 is eigenvalue of fI; then consider w be Vector of I such that A42: w<>0.I & fI.w = L1 * w by A41,Def2; w=0.V by A4,A42,Th37; hence thesis by A42,VECTSP_4:19; end; hence not L1 is eigenvalue of fI & L2 is eigenvalue of fI by A39,A40,A41,Def2; the carrier of UnionKers f2 c= the carrier of I proof let x such that A43: x in the carrier of UnionKers f2; A44: x in UnionKers f2 by A43,STRUCT_0:def 5; then x in V by VECTSP_4:17; then reconsider v=x as Vector of V by STRUCT_0:def 5; v is Vector of I by A5,A44; hence thesis; end; hence thesis by VECTSP_4:35; end; :: Main Lemmas for Expansion of Matrices of Nilpotent Linear Transformations theorem for U be finite Subset of V1 st U is linearly-independent for u be Vector of V1 st u in U for L be Linear_Combination of U\{u} holds Card U=Card (U\{u}\/{u+Sum(L)}) & U\{u}\/{u+Sum(L)} is linearly-independent proof set V=V1; let U be finite Subset of V1 such that A1:U is linearly-independent; let u be Vector of V such that A2:u in U; defpred P[Nat] means for L be Linear_Combination of U\{u} st Card Carrier(L)=$1 holds Card U=Card (U\{u}\/{u+Sum(L)}) & U\{u}\/{u+Sum(L)} is linearly-independent; A3:P[0] proof let L be Linear_Combination of U\{u} such that A4: Card Carrier(L)=0; Carrier L = {} by A4; then u+Sum L = u+0.V by VECTSP_6:45 .= u by RLVECT_1:def 7; hence thesis by A1,A2,ZFMISC_1:140; end; A5:for n st P[n] holds P[n+1] proof let n such that A6: P[n]; set n1=n+1; let L be Linear_Combination of U\{u} such that A7: card Carrier(L)=n1; consider x such that A8: x in Carrier L by XBOOLE_0:def 1,A7,CARD_1:47; A9: Carrier L c= U\{u} by VECTSP_6:def 7; then x in U by A8,XBOOLE_0:def 4; then A10: x<>0.V by A1,VECTSP_7:3; reconsider x as Vector of V by A8; x in {x} by TARSKI:def 1; then x in Lin({x}) by VECTSP_7:13; then consider X be Linear_Combination of {x} such that A11: x=Sum(X) by VECTSP_7:12; X.x * x = x by A11,VECTSP_6:43 .= 1_K*x by VECTSP_1:def 26; then A12: X.x=1_K by A10,VECTSP10:5; set Lx=L.x; set LxX=Lx*X; Carrier LxX c= Carrier X & Carrier X c= {x} by VECTSP_6:58,def 7; then A13: Carrier LxX c= {x} by XBOOLE_1:1; then Carrier (L-LxX) c= Carrier L \/ Carrier LxX & Carrier L \/ Carrier LxX c= Carrier L \/ {x} by XBOOLE_1:9,VECTSP_6:74; then Carrier (L-LxX) c= Carrier L \/{x} by XBOOLE_1:1; then A14: Carrier (L-LxX) c= Carrier L by A8,ZFMISC_1:46; then Carrier (L-LxX) c= U\{u} by A9,XBOOLE_1:1; then reconsider LLxX=L-LxX as Linear_Combination of U\{u} by VECTSP_6:def 7; (L-LxX).x = Lx - LxX.x by VECTSP_6:73 .= Lx-Lx * 1_K by A12,VECTSP_6:def 12 .= Lx-Lx by VECTSP_1:def 13 .= 0.K by RLVECT_1:16; then not x in Carrier (L-LxX) by VECTSP_6:20; then A15: Carrier (L-LxX) c= Carrier L\{x} by A14,ZFMISC_1:40; Carrier L\{x} c= Carrier(L-LxX) proof let y such that A16: y in Carrier L\{x}; y in Carrier L by A16,XBOOLE_0:def 4; then consider Y be Vector of V such that A17: y = Y & L.Y <> 0.K; not Y in Carrier LxX by A13,A17,A16,XBOOLE_0:def 4; then LxX.Y =0.K; then (L-LxX).Y = L.Y - 0.K by VECTSP_6:73 .= L.Y by RLVECT_1:26; hence thesis by A17; end; then A18: Carrier (L-LxX) = Carrier L\{x} by A15,XBOOLE_0:def 10; {x} c= Carrier L by A8,ZFMISC_1:37; then card Carrier (L-LxX) = n1 - card {x} by A7,A18,CARD_2:63 .= n1-1 by CARD_1:50 .= n; then A19: (U\{u})\/{u+Sum(LLxX)} is linearly-independent by A6; Sum L = 0.V+Sum (L) by RLVECT_1:def 7 .= Sum LxX +(-Sum LxX) +Sum L by RLVECT_1:16 .= Sum LxX +(Sum L-Sum LxX)by RLVECT_1:def 6 .= Sum LxX + Sum LLxX by VECTSP_6:80 .= Lx*x + Sum LLxX by A11,VECTSP_6:78; then A20: u+Sum(LLxX)+Lx*x = u +Sum L by RLVECT_1:def 6; A21: not u+Sum(LLxX) in U\{u} proof assume u+Sum(LLxX) in U\{u}; then A22: u+Sum(LLxX) in Lin(U\{u}) & Sum (LLxX) in Lin(U\{u}) by VECTSP_7:13,VECTSP_7:12; (u+Sum(LLxX))-Sum(LLxX) = u+(Sum(LLxX)-Sum(LLxX)) by RLVECT_1:def 6 .= u+0.V by RLVECT_1:16 .= u by RLVECT_1:def 7; hence thesis by A1,A2,A22,VECTSP_9:18,VECTSP_4:31; end; then A23: ((U\{u})\/{u+Sum(LLxX)}) \ {u+Sum(LLxX)} = U\{u} by ZFMISC_1:141; u+Sum(LLxX) in {u+Sum(LLxX)} by TARSKI:def 1; then A24: u+Sum(LLxX) in (U\{u})\/{u+Sum(LLxX)} & x in (U\{u})\/{u+Sum(LLxX)} & u+Sum(LLxX)<>x by A21,A9,A8,XBOOLE_0:def 2; Card U<>0 by A2; then reconsider C=card U-1 as Element of NAT by NAT_1:20; A25: not u+Sum(L) in U\{u} proof assume u+Sum(L) in U\{u}; then A26: u+Sum(L) in Lin(U\{u}) & Sum (L) in Lin(U\{u}) by VECTSP_7:13,VECTSP_7:12; (u+Sum(L))-Sum(L) = u+(Sum(L)-Sum(L)) by RLVECT_1:def 6 .= u+0.V by RLVECT_1:16 .= u by RLVECT_1:def 7; hence thesis by A1,A2,A26,VECTSP_9:18,VECTSP_4:31; end; card U=C+1; then card (U\{u})= C by A2,STIRL2_1:65; then card ((U\{u})\/{ u+Sum L}) =C+1 by CARD_2:54,A25; hence thesis by A23,A24,A19,A20,MATRIX13:115; end; A27: for n holds P[n] from NAT_1:sch 2(A3,A5); let L be Linear_Combination of U\{u}; P[card Carrier L] by A27; hence thesis; end; theorem Th41: for A be Subset of V1 for L be Linear_Combination of V2, f be linear-transformation of V1,V2 st Carrier L c= f.:A ex M be Linear_Combination of A st f.(Sum M)=Sum L proof let A be Subset of V1; let L be Linear_Combination of V2, f be linear-transformation of V1,V2 such that A1: Carrier L c= f.:A; consider F be FinSequence of the carrier of V2 such that A2: F is one-to-one & rng F = Carrier(L) & Sum L = Sum(L (#) F) by VECTSP_6:def 9; set C=Carrier L; set D=dom F; defpred P[set,set] means $2 in A & f.$2=F.$1; A3: dom f=[#]V1 by FUNCT_2:def 1; A4: for x st x in D ex y st y in the carrier of V1 & P[x,y] proof let x;assume x in D; then F.x in rng F by FUNCT_1:def 5; then consider y such that A5: y in dom f & y in A & f.y=F.x by A1,A2,FUNCT_1:def 12; take y; thus thesis by A5; end; consider p be Function of D,the carrier of V1 such that A6: for x st x in D holds P[x,p.x] from FUNCT_2:sch 1(A4); A7: dom p=D & D=Seg len F & rng p c= the carrier of V1 by FUNCT_2:def 1,RELSET_1:12,FINSEQ_1:def 3; then reconsider p as FinSequence by FINSEQ_1:def 2; reconsider p as FinSequence of V1 by A7,FINSEQ_1:def 4; reconsider RNG=rng p as finite Subset of V1 by RELSET_1:12; A8: now let x1,x2 be set such that A9: x1 in dom p & x2 in dom p & p.x1=p.x2; f.(p.x1)=F.x1 & f.(p.x2)=F.x2 by A6,A7,A9; hence x1=x2 by A2,A7,A9,FUNCT_1:def 8; end; then A10: p is one-to-one by FUNCT_1:def 8; defpred Q[set,set] means ( $1 in rng p implies for x st x in D & p.x=$1 holds $2=L.(F.x)) & ( not $1 in rng p implies $2=0.K); A11: for x st x in the carrier of V1 ex y st y in the carrier of K & Q[x,y] proof let x;assume x in the carrier of V1; then reconsider v1=x as Vector of V1; per cases; suppose A12: not v1 in rng p; take 0.K; thus thesis by A12; end; suppose A13: v1 in rng p; then consider y such that A14: y in dom p & p.y=v1 by FUNCT_1:def 5; take L.(F.y); F.y=F/.y & L.(F/.y) in the carrier of K by A7,A14,PARTFUN1:def 8; hence thesis by A7,A8,A14,A13; end; end; consider M be Function of V1,K such that A15: for x st x in the carrier of V1 holds Q[x,M.x] from FUNCT_2:sch 1(A11); reconsider M as Element of Funcs(the carrier of V1, the carrier of K) by FUNCT_2:11; for v1 be Element of V1 st not v1 in RNG holds M.v1 = 0.K by A15; then reconsider M as Linear_Combination of V1 by VECTSP_6:def 4; A16: Carrier M= RNG proof thus Carrier M c= RNG proof let x such that A17: x in Carrier M; reconsider v1=x as Vector of V1 by A17; M.v1 <>0.K by A17,VECTSP_6:20; hence thesis by A15; end; let y such that A18: y in RNG; reconsider v1=y as Vector of V1 by A18; consider x such that A19: x in D & p.x=v1 by A7,A18,FUNCT_1:def 5; F.x in C by A2,A19,FUNCT_1:def 5; then L.(F.x)<>0.K & M.v1= L.(F.x) by A18,A19,A15,VECTSP_6:20; hence thesis; end; RNG c= A proof let y such that A20: y in RNG; ex x st x in D & p.x=y by A7,A20,FUNCT_1:def 5; hence thesis by A6; end; then reconsider M as Linear_Combination of A by A16,VECTSP_6:def 7; take M; len (L(#)F) =len F & len (M(#)p)=len p & rng (M(#)p) c= [#]V1 by VECTSP_6:def 8,RELSET_1:12; then A21: dom (L(#)F) = D & dom (M(#)p)=D & dom(f*(M(#)p))=dom(M(#)p) by A3,A7,FINSEQ_3:31,RELAT_1:46; now let x such that A22: x in D; reconsider i=x as Element of NAT by A22; A23: p/.i=p.i & f.(p.i)=F.i & F.i=F/.i & p.i in RNG by A6,A7,A22,PARTFUN1:def 8,FUNCT_1:def 5; then A24: M.(p.i)=L.(F.i) by A22,A15; thus (f*(M(#)p)).x = f.((M(#)p).i) by A21,A22,FUNCT_1:23 .= f.(M.(p/.i)*p/.i) by A21,A22,VECTSP_6:def 8 .= L.(F/.i) *F/.i by A23,A24,MOD_2:def 5 .= (L(#)F).x by A21,A22,VECTSP_6:def 8; end; then f*(M(#)p) = L(#)F by A21,FUNCT_1:9; hence Sum L = f.(Sum(M(#)p)) by A2,MATRLIN:20 .= f.(Sum M) by A16,A10,VECTSP_6:def 9; end; theorem for f be linear-transformation of V1,V2 for A be Subset of V1,B be Subset of V2 st f.:A = B holds f.:(the carrier of Lin A) = the carrier of Lin B proof let f be linear-transformation of V1,V2; let A be Subset of V1,B be Subset of V2 such that A1: f.:A = B; thus f.:(the carrier of Lin A) c= the carrier of Lin B proof let y;assume y in f.:(the carrier of Lin A); then consider x such that A2: x in dom f & x in the carrier of Lin A & f.x=y by FUNCT_1:def 12; x in Lin A by A2,STRUCT_0:def 5; then consider L be Linear_Combination of A such that A3: x=Sum L by VECTSP_7:12; consider F be FinSequence of V1 such that A4: F is one-to-one & rng F=Carrier L & x= Sum(L (#) F) by A3,VECTSP_6:def 9; set LF=L(#)F; A5: len LF=len F by VECTSP_6:def 8; then A6: dom LF=dom F by FINSEQ_3:31; consider g be Function of NAT,the carrier of V1 such that A7: x = g.(len LF) and A8: g.0 = 0.V1 and A9: for j be Element of NAT, v be Vector of V1 st j < len LF & v = LF.(j+1) holds g.(j+1) = g.j + v by A4,RLVECT_1:def 13; defpred P[Nat] means $1 <= len F implies f.(g.$1) in Lin B; f.(0.V1)=0.V2 & 0.V2 in Lin B by RANKNULL:9,VECTSP_4:25; then A10: P[0] by A8; A11: for n st P[n] holds P[n+1] proof let n such that A12: P[n]; reconsider N=n as Element of NAT by ORDINAL1:def 13; reconsider gn=g.N as Vector of V1; set N1=N+1; assume A13: n+1<=len F; then A14: N0.K by A9,VECTSP_6:20; hence thesis by A7; end; f.:(C/\ R) c= Carrier Lf proof let y such that A10: y in f.:(C/\R); consider v1 be set such that A11: v1 in dom f & v1 in C/\R & f.v1=y by A10,FUNCT_1:def 12; reconsider v1 as Vector of V1 by A11; reconsider v2=y as Vector of V2 by A10; v1 in C by A11,XBOOLE_0:def 3; then Lf.v2 = L.v1 & L.v1 <> 0.K by A7,A10,A11,VECTSP_6:20; hence thesis; end; hence Carrier Lf = f.:(C/\ R) by A8,XBOOLE_0:def 10; A12: dom f = [#]V1 & rng F c= [#]V1 & rng (L(#)F) c= [#]V1 & len (L(#)F)=len F & len (Lf(#)(f*F)) =len (f*F) by FUNCT_2:def 1,RELSET_1:12,VECTSP_6:def 8; then A13: dom (f*(L(#)F))= dom (L(#)F) & dom (L(#)F) =dom F & dom (Lf(#)(f*F)) =dom (f*F) & dom (f*F)=dom F by FINSEQ_3:31,RELAT_1:46; now let x such that A14: x in dom F; reconsider k=x as Nat by A14; A15: F/.k=F.k by A14,PARTFUN1:def 8; then A16: (f*F).k=f.(F/.k) & (f*F).k=(f*F)/.k & F.k in R by A13,A14,FUNCT_1:def 5,22,PARTFUN1:def 8; then A17: F.k in C/\R by A1,XBOOLE_0:def 3; then (f*F)/.k in f.:(C/\R) by A12,A15,A16,FUNCT_1:def 12; then A18: L.(F/.k)=Lf.((f*F)/.k) by A7,A15,A16,A17; thus (f*(L(#)F)).x = f.((L(#)F).k) by A13,A14,FUNCT_1:23 .= f.(L.(F/.k)* F/.k) by A13,A14,VECTSP_6:def 8 .= Lf.((f*F)/.k) * (f*F)/.k by A16,A18,MOD_2:def 5 .= (Lf(#)(f*F)).x by A13,A14,VECTSP_6:def 8; end; hence f*(L(#)F) = Lf(#)(f*F) by A13,FUNCT_1:9; let v1 be Vector of V1 such that A19: v1 in C /\ R; f.v1 in f.:(C/\R) by A12,A19,FUNCT_1:def 12; hence thesis by A7,A19; end; theorem for A,B be Subset of V1 for L be Linear_Combination of V1 st Carrier L c= A\/B & Sum L = 0.V1 for f be linear Function of V1,V2 st f|B is one-to-one & f.:B is linearly-independent Subset of V2 & f.:A c= {0.V2} holds Carrier L c= A proof let A,B be Subset of V1; let L be Linear_Combination of V1 such that A1: Carrier L c= A\/B & Sum L = 0.V1; let f be linear Function of V1,V2 such that A2: f|B is one-to-one and A3: f.:B is linearly-independent Subset of V2 and A4: f.:A c= {0.V2}; consider F be FinSequence of V1 such that A5: F is one-to-one and A6: rng F = Carrier L & 0.V1 = Sum(L (#) F) by A1,VECTSP_6:def 9; per cases; suppose dom F={}; then rng F={} by RELAT_1:65; hence thesis by A6,XBOOLE_1:2; end; suppose dom F<>{}; then reconsider D=dom F as non empty finite set; set C=Carrier L; set FA=F"(C/\A); set FB=F"(C/\B); (C/\A) \/ (C/\B) = C /\ (A\/B) by XBOOLE_1:23 .= C by A1,XBOOLE_1:28; then A7: FA\/FB = F"C by RELAT_1:175 .= dom F by A6,RELAT_1:169; A8: D=Seg len F by FINSEQ_1:def 3; A misses B proof assume A meets B; then consider x such that A9: x in A & x in B by XBOOLE_0:3; reconsider x as Vector of V1 by A9; dom f = the carrier of V1 by FUNCT_2:def 1; then f.x in f.:A & f.x in f.:B by A9, FUNCT_1:def 12; then 0.V2 in f.:B by A4,TARSKI:def 1; hence thesis by A3,VECTSP_7:3; end; then A10: C/\A misses C/\B by XBOOLE_1:76; then A11: FA misses FB by FUNCT_1:141; A12: card FA +card FB = card (Seg len F) by A7,A8,A10,CARD_2:53,FUNCT_1:141 .= len F by FINSEQ_1:78; set SS=(Sgm FB)^(Sgm FA); A13: FA c= D & FB c= D by RELAT_1:167; then A14: Sgm FA is one-to-one & rng Sgm FA =FA & len Sgm FA = card FA & Sgm FB is one-to-one & rng Sgm FB = FB & len Sgm FB = card FB by A8,FINSEQ_1:def 13,FINSEQ_3:44,99; then A15: SS is one-to-one & len SS = len F by A12,A11,FINSEQ_1:35,FINSEQ_3:98; then A16: dom SS = D by FINSEQ_3:31; A17: card D=card D; rng SS = D by A7,A14,FINSEQ_1:44; then reconsider SS as Function of D,D by A16,FUNCT_2:3; SS is onto by A15,A17,STIRL2_1:70; then reconsider SS as Permutation of D by A15; reconsider SA=Sgm FA,SB=Sgm FB as FinSequence of D by A13,A14,FINSEQ_1:def 4; rng F c= the carrier of V1 by RELSET_1:12; then reconsider F'=F as Function of D,the carrier of V1 by FUNCT_2:4; reconsider FS=F'*SS,FSA=F'*SA,FSB=F'*SB as FinSequence of V1 by FINSEQ_2:51; FS=FSB^FSA by FINSEQOP:10; then L(#)FS = (L(#)FSB) ^(L(#)FSA) by VECTSP_6:37; then A18: f * (L(#)FS) = (f*(L(#)FSB)) ^(f*(L(#)FSA)) by FINSEQOP:10; A19: len (f*(L(#)FSA))=len (f*(L(#)FSA)); now let k be Element of NAT,v be Element of V2 such that A20: k in dom (f*(L(#)FSA)) & v = (f*(L(#)FSA)).k; rng (L(#)FSA) c= [#]V1 & dom f = [#]V1 & len (L(#)FSA) =len FSA by RELSET_1:12,FUNCT_2:def 1,VECTSP_6:def 8; then A21: dom (f*(L(#)FSA))=dom (L(#)FSA) & dom FSA=dom SA & dom (L(#)FSA) =dom FSA by A13,A14,FINSEQ_3:31,RELAT_1:46; A22: FSA/.k = FSA.k by A20,A21,PARTFUN1:def 8 .= F.(SA.k) by A20,A21,FUNCT_1:22; SA.k in F"(C/\A) by A14,A20,A21,FUNCT_1:def 5; then F.(SA.k) in C/\A by FUNCT_1:def 13; then FSA/.k in A & dom f=[#]V1 by A22,XBOOLE_0:def 3,FUNCT_2:def 1; then f.(FSA/.k) in f.:A by FUNCT_1:def 12; then A23: f.(FSA/.k)=0.V2 by A4,TARSKI:def 1; thus (f*(L(#)FSA)).k = f.((L(#)FSA).k) by A20,FUNCT_1:22 .= f.(L.(FSA/.k)*(FSA/.k)) by A20,A21,VECTSP_6:def 8 .= L.(FSA/.k) * 0.V2 by A23,MOD_2:def 5 .= 0.V2 by VECTSP_1:59 .= 0.K*v by VECTSP_1:59; end; then A24: Sum(f*(L(#)FSA)) =0.K * Sum(f*(L(#)FSA)) by A19,VECTSP_3:9; A25: rng FSB c= C/\B proof let y such that A26: y in rng FSB; consider x such that A27: x in dom FSB & FSB.x=y by A26,FUNCT_1:def 5; A28: FSB.x =F.(SB.x) & x in dom SB by A27,FUNCT_1:21,22; then SB.x in F"(C/\B) by A14,FUNCT_1:def 5; hence thesis by A27,A28,FUNCT_1:def 13; end; C/\B c= rng FSB proof let y such that A29: y in C/\B; y in rng F by A6,A29,XBOOLE_0:def 3; then consider x such that A30: x in dom F & y=F.x by FUNCT_1:def 5; x in FB by A29,A30,FUNCT_1:def 13; then consider z be set such that A31: z in dom SB & SB.z=x by A14, FUNCT_1:def 5; FSB.z = y & z in dom FSB by A30,A31,FUNCT_1:21,23; hence thesis by FUNCT_1:def 5; end; then A32: C/\B = rng FSB by A25,XBOOLE_0:def 10; A34: C/\(C/\B) = C/\B by XBOOLE_1:18,28; (f|B)|(C/\B)= f|(C/\B) by XBOOLE_1:18,RELAT_1:103; then A35: f|(C/\B) is one-to-one & FSB is one-to-one by A2,A5,FUNCT_1:84,A14; consider Lf be Linear_Combination of V2 such that A36: Carrier Lf = f.:(C /\ rng FSB) and A37: f*(L(#)FSB) = Lf(#) (f*FSB) and A38: for v1 be Vector of V1 st v1 in C /\ rng FSB holds L.v1=Lf.(f.v1) by A35,A32,XBOOLE_1:18,A34,Th43; Carrier Lf c= f.:B by XBOOLE_1:18,A34,A32,A36,RELAT_1:156; then A39: Lf is Linear_Combination of f.:B by VECTSP_6:def 7; A40: Carrier Lf=rng (f*FSB) by RELAT_1:160,A36,A34,A32; aa: f*FSB = f*((id rng FSB)*FSB) by RELAT_1:79 .= f*(id rng FSB)*FSB by RELAT_1:55 .= (f|(C/\B)) *FSB by A32,RELAT_1:94; f.(0.V1)=0.V2 by RANKNULL:9; then A42: 0.V2 = f.Sum (L(#)FS) by A6,VECTSP_9:5 .= Sum (f * (L(#)FS)) by MATRLIN:20 .= Sum(f*(L(#)FSB)) +Sum(f*(L(#)FSA)) by A18,RLVECT_1:58 .= Sum(f*(L(#)FSB)) + 0.V2 by A24,VECTSP_1:59 .= Sum(Lf(#) (f*FSB)) by A37,RLVECT_1:def 7 .= Sum(Lf) by A40,aa,A35,VECTSP_6:def 9; thus C c= A proof let x such that A43: x in C; reconsider v1=x as Vector of V1 by A43; A44: x in A or x in B by A1,A43,XBOOLE_0:def 2; assume not x in A; then v1 in C/\rng FSB by A34,A43,A44,A32,XBOOLE_0:def 3; then L.v1 = Lf.(f.v1) & not (f.v1) in Carrier Lf by A38,A42,A3,A39,VECTSP_7:def 1; then L.v1=0.K; hence contradiction by A43,VECTSP_6:20; end; end; end;