:: Eigenvalues of a Linear Transformation
:: by Karol P\c{a}k
::
:: Received July 11, 2008
:: Copyright (c) 2008-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, NAT_1, VECTSP_1, SUBSET_1, MATRIX_1, FINSEQ_2,
ZFMISC_1, RELAT_1, TARSKI, CARD_1, ARYTM_3, FUNCT_1, FREEALG,
FINSET_1, FINSEQ_1, MESFUNC1, GROUP_1, SUPINF_2, LAPLACE,
XBOOLE_0, ARYTM_1, XXREAL_0, POLYNOM1, POLYNOM2, MATRIX_3, CARD_3,
AFINSQ_1, ORDINAL4, POLYNOM3, STRUCT_0, PARTFUN1, RANKNULL,
RLSUB_1, RLVECT_5, PRVECT_1, RLVECT_3, ALGSTR_0, VECTSP10,
MATRLIN, MATRLIN2, POLYNOM5, NEWTON, MONOID_0, BINOP_1, RLVECT_1,
LATTICES, RLSUB_2, FINSEQ_4, MCART_1, RLVECT_2, VALUED_1, FUNCT_2,
VECTSP11, MSSUBFAM, UNIALG_1, NUMBER09;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS,
CARD_1, XCMPLX_0, ALGSTR_0, XXREAL_0, FINSET_1, RELAT_1, FUNCT_1,
PARTFUN1, FUNCT_2, NAT_1, FINSEQ_1, BINOP_1, STRUCT_0, RLVECT_1,
GROUP_1, VECTSP_1, FINSEQ_2, MATRIX_0, MATRIX_1, NAT_D, GROUP_4,
MATRIX_3, DOMAIN_1, MEASURE6, PRVECT_1, VECTSP_2, VECTSP_4,
VECTSP_5, VECTSP_6, VECTSP_7, VECTSP_9, FINSEQOP, MATRIX13,
MATRLIN, LAPLACE, MOD_2, RANKNULL, POLYNOM3, MONOID_0, ALGSEQ_1,
POLYNOM4, POLYNOM5, MATRLIN2;
constructors FINSOP_1, GROUP_4, VECTSP_7, VECTSP_9, MATRIX13, REALSET1,
VECTSP_2, LAPLACE, VECTSP_5, RANKNULL, MONOID_0, POLYNOM4,
POLYNOM5, MATRLIN2, BINOP_2, RELSET_1, MATRIX_1, ALGSEQ_1,
MATRIX_3;
registrations XBOOLE_0, FUNCT_1, FINSET_1, STRUCT_0, VECTSP_1, FUNCT_2,
ORDINAL1, XXREAL_0, NAT_1, FINSEQ_1, FINSEQ_2, SEQM_3, MATRIX13, XREAL_0,
VECTSP_9, RANKNULL, POLYNOM3, POLYNOM5, MONOID_0, CARD_1, RELSET_1,
MOD_2, GRCAT_1, PRVECT_1, MATRLIN2, MATRIX_1, MATRIX_3, VECTSP_2;
requirements ARITHM, NUMERALS, REAL, BOOLE, SUBSET;
definitions TARSKI, XBOOLE_0;
equalities STRUCT_0, RLVECT_1, FINSEQ_1, VECTSP_4, FVSUM_1, LAPLACE, MATRIX13,
RANKNULL, VECTSP_6, MATRLIN2, MATRIX_1;
expansions STRUCT_0, TARSKI, XBOOLE_0, VECTSP_4;
theorems ZFMISC_1, RLVECT_1, MATRIX_0, MATRIX_3, VECTSP_1, NAT_1, FINSEQ_1,
FINSEQ_3, FINSEQ_2, CARD_1, CARD_2, FINSEQOP, FINSOP_1, FUNCT_1, FUNCT_2,
FVSUM_1, GROUP_1, LAPLACE, MATRIX13, MATRIXR2, MATRLIN, ORDINAL1,
PARTFUN1, RELAT_1, STIRL2_1, STRUCT_0, TARSKI, VECTSP_4, VECTSP_5,
VECTSP_6, VECTSP_7, VECTSP_9, VECTSP10, XBOOLE_0, XBOOLE_1, XREAL_1,
XXREAL_0, MOD_2, RANKNULL, MONOID_0, GROUP_4, SYSREL, SUBSET_1, FINSEQ_5,
ALGSEQ_1, POLYNOM4, POLYNOM5, HILBASIS, MATRIXJ1, MATRLIN2, VALUED_0,
NAT_D, RLVECT_2, MATRIX_1, FINSEQ_4;
schemes NAT_1, FUNCT_2;
begin :: Preliminaries
reserve i,j,m,n,k for Nat,
x,y for set,
K for Field,
a 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
A2: Indices Segm(A,nt,mt) = Indices Segm(B,nt,mt) by MATRIX_0:26;
let i,j such that
A3: [i,j] in Indices Segm(A+B,nt,mt);
reconsider nti = nt.i, mtj = mt.j as Nat by VALUED_0:12;
A4: Indices Segm(A+B,nt,mt) = Indices Segm(A,nt,mt) by MATRIX_0:26;
then
A5: [nt.i,mt.j] in Indices A by A1,A3,MATRIX13:17;
thus Segm(A+B,nt,mt)*(i,j) = (A+B)*(nti,mtj) by A3,MATRIX13:def 1
.= A*(nti,mtj)+B*(nti,mtj) by A5,MATRIX_1:def 6
.= Segm(A,nt,mt)*(i,j) + B*(nti,mtj) by A3,A4,MATRIX13:def 1
.= Segm(A,nt,mt)*(i,j) + Segm(B,nt,mt)*(i,j) by A3,A4,A2,MATRIX13:def 1
.= (Segm(A,nt,mt) + Segm(B,nt,mt))*(i,j) by A3,A4,MATRIX_1:def 6;
end;
hence thesis by MATRIX_0:27;
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
set SP=Sgm P;
let i,j such that
A2: [i,j] in Indices 1.(K,card P);
A3: SP is one-to-one by FINSEQ_3:92;
A4: rng SP = P by FINSEQ_1:def 14;
reconsider Spi = SP.i, Spj = SP.j as Nat by VALUED_0:12;
A5: Indices 1.(K,card P) = Indices S by MATRIX_0:26;
then
A6: S*(i,j) = 1.(K,n)*(Spi,Spj) by A2,MATRIX13:def 1;
Indices 1.(K,n) = [:Seg n,Seg n:] & [:P,P:] c= [:Seg n,Seg n:] by A1,
MATRIX_0:24,ZFMISC_1:96;
then
A7: [SP.i,SP.j] in Indices 1.(K,n) by A2,A5,A4,MATRIX13:17;
Indices S=[:Seg card P,Seg card P:] & dom SP=Seg card P by FINSEQ_3:40
,MATRIX_0:24;
then
A8: i in dom SP & j in dom SP by A2,A5,ZFMISC_1:87;
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,A7,A8,A6,FUNCT_1:def 4,MATRIX_1:def 3;
hence 1.(K,card P)*(i,j)=S*(i,j) by A7,A6,MATRIX_1:def 3;
end;
hence thesis by MATRIX_0:27;
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;
rng (Sgm Q)=Q & rng (Sgm P)=P by FINSEQ_1:def 14;
hence thesis by 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:] by ZFMISC_1:96;
A3: Indices A = [:Seg n,Seg n:] by MATRIX_0:24;
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,A3,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:] by ZFMISC_1:96;
A3: Indices A = [:Seg n,Seg n:] by MATRIX_0:24;
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,A3,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 <> 0;
then n >= 1 by NAT_1:14;
then n-'1=n-1 by XREAL_1:233;
then card Seg n=n-'1+1 by FINSEQ_1:57;
then
A2: card (Seg n\{i})=n-'1 by A1,STIRL2_1:55;
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 A2,Th2,XBOOLE_1:36;
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: for n st P[n] holds P[n+1]
proof
let n such that
A2: P[n];
set n1=n+1;
let A,B be Matrix of n1,K;
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);
A3: n1 in Seg n1 by FINSEQ_1:4;
A4: for m st Q[m] holds Q[m+1]
proof
let m such that
A5: Q[m];
set m1=m+1;
assume
A6: m1 <= n1;
then consider P be Polynomial of K such that
A7: len P <= n1+1 and
A8: for x be Element of K holds eval(P,x) = Sum (LaplaceExpL(A+x*B,
n1)|m) by A5,NAT_1:13;
1<=m1 by NAT_1:11;
then
A9: m1 in Seg n1 by A6;
then
A10: [n1,m1] in [:Seg n1,Seg n1:] by A3,ZFMISC_1:87;
set pow=power(K).(-1_K,m1+n1);
set DB=Delete(B,n1,m1);
set DA=Delete(A,n1,m1);
set P2=<% A*(n1,m1)*pow,B*(n1,m1)*pow %>;
A11: Indices B=[:Seg n1,Seg n1:] by MATRIX_0:24;
n1-'1=n by NAT_D:34;
then consider P1 be Polynomial of K such that
A12: len P1 <= n+1 and
A13: for x be Element of K holds eval(P1,x) = Det(DA+x*DB) by A2;
take PP=P+(P1*'P2);
len P2 <= 2 by POLYNOM5:39;
then (len P1)+(len P2) <= n1+2 by A12,XREAL_1:7;
then
A14: (len P1)+(len P2)-'1 <=n1+2-'1 by NAT_D:42;
n+2+1-'1=n+2 & len (P1*'P2) <= (len P1)+(len P2)-'1 by HILBASIS:21
,NAT_D:34;
then len (P1*'P2) <= n1+1 by A14,XXREAL_0:2;
hence len PP<=n1+1 by A7,POLYNOM4:6;
let x be Element of K;
set L=LaplaceExpL(A+x*B,n1);
A15: Indices A=[:Seg n1,Seg n1:] by MATRIX_0:24;
A16: A*(n1,m1)*pow+B*(n1,m1)*pow*x = A*(n1,m1)*pow+B*(n1,m1)*x*pow by
GROUP_1:def 3
.= (A*(n1,m1)+B*(n1,m1)*x)*pow by VECTSP_1:def 2
.= (A*(n1,m1)+(x*B)*(n1,m1))*pow by A10,A11,MATRIX_3:def 5
.= (A+x*B)*(n1,m1)*pow by A10,A15,MATRIX_1:def 6;
n1=len L by LAPLACE:def 7;
then
A17: dom L=Seg n1 by FINSEQ_1:def 3;
then
A18: L|m1 = (L|m)^<*L.m1*> by A9,FINSEQ_5:10;
A19: DA+x*DB = DA+Delete(x*B,n1,m1) by A3,A9,Th5
.= Delete(A+x*B,n1,m1) by A3,A9,Th4;
eval(P1*'P2,x) = eval(P1,x)*eval(P2,x) by POLYNOM4:24
.= Det(DA+x*DB) * eval(P2,x) by A13
.= Minor(A+x*B,n1,m1)*((A+x*B)*(n1,m1)*pow) by A16,A19,POLYNOM5:44
.=(A+x*B)*(n1,m1)*Cofactor(A+x*B,n1,m1) by GROUP_1:def 3
.= L.m1 by A9,A17,LAPLACE:def 7;
hence Sum (L|m1) = Sum (L|m) + eval(P1*'P2,x) by A18,FVSUM_1:71
.= eval(P,x)+eval(P1*'P2,x) by A8
.= eval(PP,x) by POLYNOM4:19;
end;
A20: Q[0]
proof
assume 0<=n1;
take P=0_.(K);
thus len P <=n1+1 by POLYNOM4:3;
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:43
.= eval(P,x) by POLYNOM4:17;
end;
for m holds Q[m] from NAT_1:sch 2(A20,A4);
then consider P be Polynomial of K such that
A21: len P <= n1+1 and
A22: 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 A21;
let x be Element of K;
A23: len LaplaceExpL(A+x*B,n1)=n1 by LAPLACE:def 7;
thus eval(P,x) = Sum (LaplaceExpL(A+x*B,n1)|n1) by A22
.= Sum LaplaceExpL(A+x*B,n1) by A23,FINSEQ_1:58
.= Det (A+x*B) by A3,LAPLACE:25;
end;
A24: P[0]
proof
let A,B be Matrix of 0,K;
take P=1_.(K);
thus len P <=0+1 by POLYNOM4:4;
let x be Element of K;
thus Det(A+x*B) = 1_K by MATRIXR2:41
.= eval(P,x) by POLYNOM4:18;
end;
for n holds P[n] from NAT_1:sch 2(A24,A1);
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: for n st P[n] holds P[n+1]
proof
let n such that
A2: P[n];
set n1=n+1;
let A be Matrix of n1,K;
set ONE=1.(K,n1);
A3: Indices ONE=Indices A by MATRIX_0:26;
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);
A4: n1-'1=n by NAT_D:34;
A5: 1<=n1 by NAT_1:11;
then
A6: 1 in Seg n1;
A7: Indices A=[:Seg n1,Seg n1:] by MATRIX_0:24;
A8: for k st Q[k] holds Q[k+1]
proof
let k such that
A9: Q[k];
set k1=k+1;
assume that
A10: 1<=k1 and
A11: k1<=n1;
set pow=power(K).(-1_K,k1+1);
set P2=<% A*(1,k1)*pow,ONE*(1,k1)*pow %>;
A12: k1 in Seg n1 by A10,A11;
then
A13: [1,k1] in Indices A by A7,A6,ZFMISC_1:87;
per cases by NAT_1:14;
suppose
A14: k=0;
then pow = (-1_K) * (-1_K) by GROUP_1:51
.= 1_K * 1_K by VECTSP_1:10
.= 1_K;
then
A15: ONE*(1,k1)*pow = 1_K*1_K by A3,A13,A14,MATRIX_1:def 3
.= 1_K;
then
A16: 2-'1=2-1 & P2.1 <>0.K by POLYNOM5:38,XREAL_1:233;
ONE*(1,k1)*pow<>0.K by A15;
then
A17: len P2=2 by POLYNOM5:40;
consider P be Polynomial of K such that
A18: len P = n1 and
A19: for x be Element of K holds eval(P,x) = Det(Delete(A,1,1)+x*
1.(K,n)) by A2,A4;
take PP=P2*'P;
P.n <> 0.K by A18,ALGSEQ_1:10;
then P2.(len P2-'1)*P.(len P-'1) <>0.K by A4,A18,A17,A16,VECTSP_1:12;
hence len PP = n1+2-1 by A18,A17,POLYNOM4:10
.= n1+1;
let x be Element of K;
A20: Delete(A,1,1)+x*1.(K,n) = Delete(A,1,1)+x*Delete(ONE,1,1) by A6,A4,Th6
.= Delete(A,1,1)+Delete(x*ONE,1,1) by A12,A14,Th5
.= Delete(A+x*ONE,1,1) by A6,Th4;
A21: A*(1,k1)*pow+ONE*(1,k1)*pow*x = A*(1,k1)*pow+ONE*(1,k1)*x*pow by
GROUP_1:def 3
.= (A*(1,k1)+ONE*(1,k1)*x)*pow by VECTSP_1:def 2
.= (A*(1,k1)+(x*ONE)*(1,k1))*pow by A3,A13,MATRIX_3:def 5
.= (A+x*ONE)*(1,k1)*pow by A13,MATRIX_1:def 6;
set L=LaplaceExpL(A+x*ONE,1);
A22: dom L=Seg len L by FINSEQ_1:def 3;
A23: len L=n1 by LAPLACE:def 7;
A24: eval(P2*'P,x) = eval(P2,x)*eval(P,x) by POLYNOM4:24
.= eval(P2,x) * Det(Delete(A,1,1)+x*1.(K,n)) by A19
.= Minor(A+x*ONE,1,1)*((A+x*ONE)*(1,1)*pow) by A14,A21,A20,
POLYNOM5:44
.= (A+x*ONE)*(1,1) * Cofactor(A+x*ONE,1,1) by A14,GROUP_1:def 3
.= L.1 by A6,A22,A23,LAPLACE:def 7;
1 <= n1 by A10,A11,XXREAL_0:2; then
1 <= len L by A23; then
1 in dom L by FINSEQ_3:25; then
L.1 = L/.1 by PARTFUN1:def 6;
hence Sum (L|k1) = Sum <*L/.1*> by A14,A23,CARD_1:27,FINSEQ_5:20
.= Sum <* eval(P2*'P,x) *> by A6,A22,A23,A24,PARTFUN1:def 6
.= eval(PP,x) by FINSOP_1:11;
end;
suppose
A25: k>=1;
consider P1 be Polynomial of K such that
A26: len P1 <= n+1 and
A27: for x be Element of K holds eval(P1,x)=Det(Delete(A,1,k1)+x*
Delete(ONE,1,k1))by A4,Th7;
consider P be Polynomial of K such that
A28: len P = n1+1 and
A29: for x be Element of K holds eval(P,x) = Sum (LaplaceExpL(A+x*
1.(K,n1),1)|k) by A9,A11,A25,NAT_1:13;
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 A26,POLYNOM5:24,25;
then
A30: len ((A*(1,k1)*pow)*P1) < len P by A28,NAT_1:13;
hence len PP = max(len ((A*(1,k1)*pow)*P1),len P) by POLYNOM4:7
.= n1+1 by A28,A30,XXREAL_0:def 10;
let x be Element of K;
set L=LaplaceExpL(A+x*ONE,1);
A31: dom L=Seg len L & len L=n1 by FINSEQ_1:def 3,LAPLACE:def 7;
then
A32: L|k1 = (L|k)^<*L.k1*> by A12,FINSEQ_5:10;
A33: k1<>1 by A25,NAT_1:13;
A34: A*(1,k1)*pow = (A*(1,k1)+0.K)*pow by RLVECT_1:def 4
.= (A*(1,k1)+x*0.K)*pow
.= (A*(1,k1)+x*(ONE*(1,k1)))*pow by A3,A13,A33,MATRIX_1:def 3
.= (A*(1,k1)+(x*ONE)*(1,k1))*pow by A3,A13,MATRIX_3:def 5
.= (A+x*ONE)*(1,k1)*pow by A13,MATRIX_1:def 6;
A35: Delete(A,1,k1)+x*Delete(ONE,1,k1) = Delete(A,1,k1)+Delete(x*ONE,1
,k1) by A6,A12,Th5
.= Delete(A+x*ONE,1,k1) by A6,A12,Th4;
eval((A*(1,k1)*pow)*P1,x) = (A*(1,k1)*pow)*eval(P1,x) by POLYNOM5:30
.= Minor(A+x*ONE,1,k1)*((A+x*ONE)*(1,k1)*pow) by A27,A34,A35
.= (A+x*ONE)*(1,k1)*Cofactor(A+x*ONE,1,k1) by GROUP_1:def 3
.= L.k1 by A12,A31,LAPLACE:def 7;
hence Sum (L|k1) = Sum (L|k) + eval((A*(1,k1)*pow)*P1,x) by A32,
FVSUM_1:71
.= eval(P,x)+eval((A*(1,k1)*pow)*P1,x) by A29
.= eval(PP,x) by POLYNOM4:19;
end;
end;
A36: Q[0];
for k holds Q[k] from NAT_1:sch 2(A36,A8);
then consider P be Polynomial of K such that
A37: len P = n1+1 and
A38: 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 A37;
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 A38
.= Sum L by FINSEQ_1:58
.= Det (A+x*1.(K,n1)) by A6,LAPLACE:25;
end;
A39: P[0]
proof
let A be Matrix of 0,K;
take P=1_.(K);
thus len P =0+1 by POLYNOM4:4;
let x be Element of K;
thus Det(A+x*1.(K,0)) = 1_K by MATRIXR2:41
.= eval(P,x) by POLYNOM4:18;
end;
for n holds P[n] from NAT_1:sch 2(A39,A1);
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 a be Scalar of K,w be Vector of W1;
thus F.(a*w) = a*(f|W1).w by A1,MOD_2:def 2
.= a*(F.w) by A1,VECTSP_4:14;
end;
now
let w1,w2 be Vector of W1;
thus F.(w1+w2) = (f|W1).w1+(f|W1).w2 by A1,VECTSP_1:def 20
.= F.w1+F.w2 by A1,VECTSP_4:13;
end;
then F is additive homogeneous by A2,MOD_2:def 2,VECTSP_1:def 20;
hence thesis;
end;
registration
let K;
cluster non trivial finite-dimensional for 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:30;
hence thesis;
end;
end;
begin :: Maps with Eigenvalues
definition
let R be non empty doubleLoopStr;
let V be non empty ModuleStr over R;
let IT be Function of V,V;
attr IT is with_eigenvalues means
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 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 STRUCT_0:def 18;
id V.v = v
.= 1_K*v;
hence thesis by A1;
end;
registration
let K,V;
cluster with_eigenvalues for linear-transformation of V,V;
existence
proof
take id V;
thus thesis by Lm2;
end;
end;
definition
let R be non empty doubleLoopStr;
let V be non empty ModuleStr 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
by A1;
end;
definition
let R be non empty doubleLoopStr;
let V be non empty ModuleStr 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 and
A3: f.v = L * v by Def2;
A4: (a*f).v = a*(L*v) by A3,MATRLIN:def 4
.= (a*L)*v by VECTSP_1:def 16;
hence
A5: a*f is with_eigenvalues by A2;
hence
A6: a*L is eigenvalue of a*f by A2,A4,Def2;
hereby
assume
A7: w is eigenvector of f,L;
(a*f).w = a*(f.w) by MATRLIN:def 4
.= a*(L*w) by A7,Def3
.= (a*L)*w by VECTSP_1:def 16;
hence w is eigenvector of a*f,a*L by A5,A6,Def3;
end;
assume
A8: w is eigenvector of a*f,a*L;
a*f.w = (a*f).w by MATRLIN:def 4
.= (a*L)*w by A5,A6,A8,Def3
.= a*(L*w) by VECTSP_1:def 16;
then 0.V = a*f.w+-a*(L*w) by VECTSP_1:16
.= a*f.w+a*(-(L*w)) by VECTSP_1:22
.= a*(f.w-(L*w)) by VECTSP_1:def 14;
then f.w-(L*w)=0.V by A1,VECTSP_1:15;
then -f.w=-(L*w) by VECTSP_1:16;
then f.w=L*w by RLVECT_1:18;
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 that
A1: L1 is eigenvalue of f1 and
A2: L2 is eigenvalue of f2;
given v such that
A3: v is eigenvector of f1,L1 and
A4: v is eigenvector of f2,L2 and
A5: v<>0.V;
A6: g.v = f1.v+f2.v by MATRLIN:def 3
.= L1*v+f2.v by A1,A3,Def3
.= L1*v+L2*v by A2,A4,Def3
.= (L1+L2)*v by VECTSP_1:def 15;
hence
A7: g is with_eigenvalues by A5;
hence
A8: L1+L2 is eigenvalue of g by A5,A6,Def2;
let w such that
A9: w is eigenvector of f1,L1 and
A10: w is eigenvector of f2,L2;
g.w = f1.w+f2.w by MATRLIN:def 3
.= L1*w+f2.w by A1,A9,Def3
.= L1*w+L2*w by A2,A10,Def3
.= (L1+L2)*w by VECTSP_1:def 15;
hence thesis by A7,A8,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;
ex v st v<>0.V & id V.v=1_K*v by Lm2;
hence
A2: 1_K is eigenvalue of id V by A1,Def2;
let w;
id V.w = w
.= 1_K*w;
hence thesis by A1,A2,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 and
A2: id V.v = L*v by Def2;
L*v = v by A2
.= 1_K*v;
hence thesis by A1,VECTSP10:4;
end;
theorem
ker f is non trivial implies f is with_eigenvalues & 0.K is eigenvalue of f
proof
assume ker f is non trivial;
then consider v be Vector of ker f such that
A1: v<>0.ker f;
reconsider v as Vector of V1 by VECTSP_4:10;
A2: f.v = 0.V1 by RANKNULL:14
.= 0.K*v by VECTSP_1:14;
A3: v<>0.V1 by A1,VECTSP_4:11;
then f is with_eigenvalues by A2;
hence thesis by A3,A2,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 and
A2: f.v1=L*v1 by Def2;
(f+(-L)*id V1).v1 = f.v1+((-L)*id V1).v1 by MATRLIN:def 3
.= f.v1+(-L)*(id V1.v1) by MATRLIN:def 4
.= f.v1+(-L)*v1
.= (L+-L)*v1 by A2,VECTSP_1:def 15
.= 0.K*v1 by VECTSP_1:19
.= 0.V1 by VECTSP_1:15;
then v1 in ker (f+(-L)*id V1) by RANKNULL:10;
then
A3: v1 is Element of ker (f+(-L)*id V1);
v1<>0.ker (f+(-L)*id V1) by A1,VECTSP_4:11;
hence ker (f+(-L)*id V1) is non trivial by A3;
end;
assume ker (f+(-L)*id V1) is non trivial;
then consider v be Vector of ker (f+(-L)*id V1) such that
A4: v<>0.ker (f+(-L)*id V1);
A5: v in ker (f+(-L)*id V1);
reconsider v as Vector of V1 by VECTSP_4:10;
0.V1 = (f+(-L)*id V1).v by A5,RANKNULL:10
.= f.v+((-L)*id V1).v by MATRLIN:def 3
.= f.v+(-L)*(id V1.v) by MATRLIN:def 4
.= f.v+(-L)*v;
then
A6: f.v = -(-L)*v by VECTSP_1:16
.= (--L)*v by VECTSP_1:21
.= L*v by RLVECT_1:17;
A7: v<>0.V1 by A4,VECTSP_4:11;
then f is with_eigenvalues by A6;
hence thesis by A6,A7,Def2;
end;
theorem Th15:
for V1 be finite-dimensional VectSp of K, b1,b19 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,b19) =0.K
proof
let V1 be finite-dimensional VectSp of K, b1,b19 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,b19) =0.K by A1,MATRLIN2:50;
end;
assume Det AutEqMt(f+(-L)*id V1,b1,b19) =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;
set b1 = the 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:8;
then P is with_roots by POLYNOM5:def 9;
then consider L be Element of K such that
A3: L is_a_root_of P by POLYNOM5:def 8;
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 7
.= 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:42
.= Det(AutMt(f+(-(-L))*id V1,b1,b1)) by RLVECT_1:17
.= 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 3
.= f.v1+(-L)*(id V1.v1) by MATRLIN:def 4
.= f.v1+(-L)*v1
.= (L+-L)*v1 by A2,VECTSP_1:def 15
.= 0.K*v1 by VECTSP_1:19
.= 0.V1 by VECTSP_1:15;
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 3
.= f.v1+(-L)*(id V1.v1) by MATRLIN:def 4
.= f.v1+(-L)*v1;
then f.v1 = -(-L)*v1 by VECTSP_1:16
.= (--L)*v1 by VECTSP_1:21
.= L*v1 by RLVECT_1:17;
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 F9 be Element of GFuncs the
carrier of S st F9=F holds it = Product(n|-> F9);
existence
proof
reconsider F9=F as Element of GFuncs the carrier of S by MONOID_0:73;
reconsider P=Product(n|-> F9) as Function of S,S by MONOID_0:73;
take P;
thus thesis;
end;
uniqueness
proof
reconsider F9=F as Element of GFuncs the carrier of S by MONOID_0:73;
let F1,F2 be Function of S,S such that
A1: for F9 be Element of GFuncs the carrier of S st F9=F holds F1 =
Product(n|-> F9) and
A2: for F9 be Element of GFuncs the carrier of S st F9=F holds F2 =
Product(n|-> F9);
thus F1 = Product(n|-> F9) 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 F9=F as Element of G by MONOID_0:73;
0|->F9=<*>the carrier of G;
then Product(0|->F9) = 1_G by GROUP_4:8
.= the_unity_wrt the multF of G by GROUP_1:22
.= id S by MONOID_0:75;
hence thesis by Def4;
end;
theorem Th19:
F |^ 1 = F
proof
set G=GFuncs the carrier of S;
reconsider F9=F as Element of G by MONOID_0:73;
Product(1|->F9) = Product<*F9*> by FINSEQ_2:59
.= F9 by GROUP_4:9;
hence thesis by Def4;
end;
theorem Th20:
F |^(i+j) = (F |^ j) * (F |^ i)
proof
set G=GFuncs the carrier of S;
reconsider Fg=F as Element of G by MONOID_0:73;
reconsider G as associative unital non empty multMagma;
reconsider F9=F as Element of G by MONOID_0:73;
Product((i+j)|->F9) = Product((i|->F9)^(j|->F9)) by FINSEQ_2:123
.= (Product(i|->F9))*(Product(j|->F9)) by GROUP_4:5
.= Product(j|->Fg)(*)Product(i|->Fg) by MONOID_0:70
.= (F|^j)(*)Product(i|->Fg) by Def4
.= (F|^j)(*)(F|^i) 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 and
A2: (F|^n).s2 = s2;
defpred P[Nat] means (F|^(m+$1*n)).s1 = s2;
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:52;
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 A2,A4,A5,A6,FUNCT_1:13;
end;
suppose
the carrier of S={};
then ( not s1 in dom (F|^(m+(i+1)*n)))& s2={} by SUBSET_1:def 1;
hence (F|^(m+(i+1)*n)).s1=s2 by FUNCT_1:def 2;
end;
end;
A7: P[0] by A1;
for i holds P[i] from NAT_1:sch 2(A7,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 vector-distributive
scalar-distributive scalar-associative scalar-unital
non empty
ModuleStr 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 vector-distributive
scalar-distributive scalar-associative scalar-unital
non empty
ModuleStr 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: for n st P[n] holds P[n+1]
proof
let n such that
A3: P[n];
A4: rng (fW|^n) c= [#]W by RELAT_1:def 19;
thus (f|^(n+1))|W = ((f|^1)*(f|^n))|W by Th20
.= (f|^1)*((f|^n)|W) by RELAT_1:83
.= (f|^1)*((id W)*(fW|^n)) by A3,A4,RELAT_1:53
.= ((f|^1)*(id W))*(fW|^n) by RELAT_1:36
.=(f*id W)*(fW|^n) by Th19
.= fW*(fW|^n) by A1,RELAT_1:65
.= (fW|^1)*(fW|^n) by Th19
.=fW|^(n+1) by Th20;
end;
[#]W c= [#]V1 by VECTSP_4:def 2;
then
A5: [#]W=[#]V1/\[#]W by XBOOLE_1:28;
(f|^0)|W = (id V1)|W by Th18
.= (id V1)*id W by RELAT_1:65
.= id W by A5,FUNCT_1:22
.= fW|^0 by Th18;
then
A6: P[0];
for n holds P[n] from NAT_1:sch 2(A6,A2);
hence thesis;
end;
registration
let K,V1;
let f be linear-transformation of V1,V1;
let n be Nat;
cluster f |^ n -> homogeneous additive;
coherence
proof
defpred P[Nat] means f|^ $1 is linear-transformation of V1,V1;
A1: 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;
f|^0=id V1 by Th18;
then
A2: P[0];
for k holds P[k] from NAT_1:sch 2(A2,A1);
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:13
.=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 be object;
assume x in S;
then ex v be Vector of V1 st x=v & ex n st (f|^n).v=0.V1;
hence thesis;
end;
then reconsider S as Subset of V1;
(f|^0).(0.V1) = (id V1).0.V1 by Th18
.= 0.V1;
then
A1: 0.V1 in S;
A2: now
let v,u be Element of V1 such that
A3: v in S and
A4: u in S;
ex v9 be Vector of V1 st v9=v & ex n st (f|^n).v9=0.V1 by A3;
then consider n such that
A5: (f|^n).v=0.V1;
ex u9 be Vector of V1 st u9=u & ex m st (f|^m).u9=0.V1 by A4;
then consider m such that
A6: (f|^m).u=0.V1;
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 VECTSP_1:def 20
.= 0.V1+0.V1 by A5,A6,Th23
.= 0.V1 by RLVECT_1:def 4;
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 VECTSP_1:def 20
.= 0.V1+0.V1 by A5,A6,Th23
.= 0.V1 by RLVECT_1:def 4;
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;
assume v in S;
then ex v9 be Vector of V1 st v9=v & ex n st (f|^n).v9=0.V1;
then consider n such that
A7: (f|^n).v=0.V1;
(f|^n).(a*v) = a*0.V1 by A7,MOD_2:def 2
.= 0.V1 by VECTSP_1:14;
hence a * v in S;
end;
then S is linearly-closed by A2;
hence thesis by A1,VECTSP_4:34;
end;
uniqueness by VECTSP_4:29;
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;
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;
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 be object;
assume x in the carrier of ker (f|^i);
then reconsider v=x as Element of ker (f|^i);
(f|^i).v=0.V1 & v is Vector of V1 by RANKNULL:14,VECTSP_4:10;
then x in UnionKers f by Th24;
hence thesis;
end;
hence thesis by VECTSP_4:27;
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 be object such that
A1: x in the carrier of ker(f|^i);
reconsider v = x as Vector of V1 by A1,VECTSP_4:10;
(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;
end;
hence thesis by VECTSP_4:27;
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:25;
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] and
A3: for n st P[n] holds k<=n;
ex m st dim ker(f|^m)=k
proof
assume
A4: for m holds dim ker(f|^m)<>k;
dim ker (f|^0)<=k by A2;
then dim ker(f|^0)<k by A4,XXREAL_0:1;
then reconsider k1=k-1 as Element of NAT by NAT_1:20;
now
let n;
dim ker (f|^n)<=k by A2;
then dim ker(f|^n)<k1+1 by A4,XXREAL_0:1;
hence dim ker(f|^n)<=k1 by NAT_1:13;
end;
then k1+1<=k1 by A3;
hence thesis by NAT_1:16;
end;
then consider m such that
A5: dim ker(f|^m)=k;
take m;
assume
A6: UnionKers f<>ker (f|^m);
ker (f|^m) is Subspace of UnionKers f by Th25;
then consider v be Element of UnionKers f such that
A7: not v in ker (f|^m) by A6,VECTSP_4:32;
A8: v in UnionKers f;
reconsider v as Vector of V by VECTSP_4:10;
consider i such that
A9: (f|^i).v=0.V by A8,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 A9,Th23;
hence thesis by A7,RANKNULL:10;
end;
then reconsider j=i-m as Element of NAT by NAT_1:21;
A10: ker (f|^m) is Subspace of ker (f|^(m+j)) by Th26;
then
A11: k<=dim ker(f|^i) by A5,VECTSP_9:25;
(Omega).(ker (f|^m))<>(Omega).(ker(f|^i)) by A7,A9,RANKNULL:10;
then k <> dim ker (f|^i) by A5,A10,VECTSP_9:28;
then k < dim ker (f|^i) by A11,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 be object;
assume y in rng (f|KER);
then consider x being object such that
A1: x in dom (f|KER) and
A2: (f|KER).x=y by FUNCT_1:def 3;
x in the carrier of KER by A1,FUNCT_2:def 1;
then
A3: x in KER;
then x in V1 by VECTSP_4:9;
then reconsider v=x as Vector of V1;
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:13;
then
A5: f.v in KER by RANKNULL:10;
y=f.v by A1,A2,FUNCT_1:47;
hence thesis by A5;
end;
hence thesis by Lm1,FUNCT_2:6;
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 be object;
assume y in rng (f|KER);
then consider x being object such that
A1: x in dom (f|KER) and
A2: (f|KER).x=y by FUNCT_1:def 3;
A3: x in the carrier of KER by A1,FUNCT_2:def 1;
then
A4: x in KER;
then x in V1 by VECTSP_4:9;
then reconsider v=x as Vector of V1;
A5: (f|KER).v =f.v by A1,FUNCT_1:47;
dom fidK=the carrier of KER by FUNCT_2:def 1;
then fidK.v = fid.v & fidK/.v=fidK.v by A3,FUNCT_1:47,PARTFUN1:def 6;
then
A6: fid.v in KER;
fid.v = f.v+(L*id V1).v by MATRLIN:def 3
.= f.v +L*((id V1).v) by MATRLIN:def 4
.= f.v +L*v;
then
A7: fid.v + (-L)*v = f.v + (L*v+ (-L)*v) by RLVECT_1:def 3
.= f.v+((L+(-L))*v) by VECTSP_1:def 15
.= f.v+(0.K *v) by VECTSP_1:16
.= f.v+0.V1 by VECTSP_1:14
.= f.v by RLVECT_1:def 4;
(-L)*v in KER by A4,VECTSP_4:21;
then f.v in KER by A7,A6,VECTSP_4:20;
hence thesis by A2,A5;
end;
hence thesis by Lm1,FUNCT_2:6;
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 be object;
assume y in rng (f|U);
then consider x being object such that
A1: x in dom (f|U) and
A2: (f|U).x=y by FUNCT_1:def 3;
x in the carrier of U by A1,FUNCT_2:def 1;
then
A3: x in U;
then x in V1 by VECTSP_4:9;
then reconsider v=x as Vector of V1;
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:13;
then
A6: f.v in U by Th24;
y=f.v by A1,A2,FUNCT_1:47;
hence thesis by A6;
end;
hence thesis by Lm1,FUNCT_2:6;
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 be object;
assume y in rng (f|U);
then consider x being object such that
A1: x in dom (f|U) and
A2: (f|U).x=y by FUNCT_1:def 3;
A3: x in the carrier of U by A1,FUNCT_2:def 1;
then
A4: x in U;
then x in V1 by VECTSP_4:9;
then reconsider v=x as Vector of V1;
A5: (f|U).v =f.v by A1,FUNCT_1:47;
dom fidU=the carrier of U by FUNCT_2:def 1;
then fidU.v=fid.v & fidU/.v=fidU.v by A3,FUNCT_1:47,PARTFUN1:def 6;
then
A6: fid.v in U;
fid.v = f.v+(L*id V1).v by MATRLIN:def 3
.= f.v +L*((id V1).v) by MATRLIN:def 4
.= f.v +L*v;
then
A7: fid.v + (-L)*v = f.v + (L*v+ (-L)*v) by RLVECT_1:def 3
.= f.v+((L+(-L))*v) by VECTSP_1:def 15
.= f.v+(0.K *v) by VECTSP_1:16
.= f.v+0.V1 by VECTSP_1:14
.= f.v by RLVECT_1:def 4;
(-L)*v in U by A4,VECTSP_4:21;
then f.v in U by A7,A6,VECTSP_4:20;
hence thesis by A2,A5;
end;
hence thesis by Lm1,FUNCT_2:6;
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 be object;
assume y in rng (f|IM);
then consider x being object such that
A1: x in dom (f|IM) and
A2: (f|IM).x=y by FUNCT_1:def 3;
x in the carrier of IM by A1,FUNCT_2:def 1;
then
A3: x in IM;
then x in V1 by VECTSP_4:9;
then reconsider v=x as Vector of V1;
consider w be Vector of V1 such that
A4: (f|^n).w=v by A3,RANKNULL:13;
A5: the carrier of V1 = dom (f|^1) by FUNCT_2:def 1;
A6: the carrier of V1=dom (f|^n) by FUNCT_2:def 1;
y = f.x by A1,A2,FUNCT_1:47
.= (f*(f|^n)).w by A4,A6,FUNCT_1:13
.= ((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:13;
then y in IM by RANKNULL:13;
hence thesis;
end;
hence thesis by Lm1,FUNCT_2:6;
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 be object;
assume y in rng (f|IM);
then consider x being object such that
A1: x in dom (f|IM) and
A2: (f|IM).x=y by FUNCT_1:def 3;
A3: x in the carrier of IM by A1,FUNCT_2:def 1;
then
A4: x in IM;
then x in V1 by VECTSP_4:9;
then reconsider v=x as Vector of V1;
A5: (f|IM).v =f.v by A1,FUNCT_1:47;
dom fidI=the carrier of IM by FUNCT_2:def 1;
then fidI.v=fid.v & fidI/.v=fidI.v by A3,FUNCT_1:47,PARTFUN1:def 6;
then
A6: fid.v in IM;
fid.v = f.v+(L*id V1).v by MATRLIN:def 3
.= f.v +L*((id V1).v) by MATRLIN:def 4
.= f.v +L*v;
then
A7: fid.v + (-L)*v = f.v + (L*v+ (-L)*v) by RLVECT_1:def 3
.= f.v+((L+(-L))*v) by VECTSP_1:def 15
.= f.v+(0.K *v) by VECTSP_1:16
.= f.v+0.V1 by VECTSP_1:14
.= f.v by RLVECT_1:def 4;
(-L)*v in IM by A4,VECTSP_4:21;
then f.v in IM by A7,A6,VECTSP_4:20;
hence thesis by A2,A5;
end;
hence thesis by Lm1,FUNCT_2:6;
end;
theorem Th34:
UnionKers f = ker (f|^n) implies ker (f|^n) /\ im (f|^n) = (0). V1
proof
set KER=ker (f|^n);
set IM = im (f|^n);
assume
A1: UnionKers f = ker (f|^n);
the carrier of KER /\ IM c= {0.V1}
proof
let x be object;
assume x in the carrier of KER/\IM;
then
A2: x in KER/\IM;
then x in V1 by VECTSP_4:9;
then reconsider v=x as Vector of V1;
v in IM by A2,VECTSP_5:3;
then consider w be Element of V1 such that
A3: (f|^n).w=v by RANKNULL:13;
A4: dom (f|^n) = the carrier of V1 by FUNCT_2:def 1;
v in KER by A2,VECTSP_5:3;
then 0.V1 = (f|^n).((f|^n).w) by A3,RANKNULL:10
.= ((f|^n)*(f|^n)).w by A4,FUNCT_1:13
.= (f|^(n+n)).w by Th20;
then w in ker(f|^n) by A1,Th24;
then v=0.V1 by A3,RANKNULL:10;
hence thesis by TARSKI:def 1;
end;
then the carrier of KER/\IM = {0.V1} by ZFMISC_1:33
.= the carrier of (0).V1 by VECTSP_4:def 3;
hence thesis by VECTSP_4:29;
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;
set KER=ker (f|^n);
set IM=im (f|^n);
A1: dim V = rank (f|^n)+nullity (f|^n) by RANKNULL:44
.= dim (IM+KER)+dim (IM/\KER) by VECTSP_9:32;
assume
A2: UnionKers f = ker (f|^n);
then (Omega).(IM/\KER) = (0).V by Th34
.= (0).(IM/\KER) by VECTSP_4:36;
then dim (IM/\KER)=0 by VECTSP_9:29;
then (Omega).V=(Omega).(IM+KER) by A1,VECTSP_9:28;
then
A3: KER + IM = (Omega).V by VECTSP_5:5;
KER/\IM=(0).V by A2,Th34;
hence thesis by A3,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;
the carrier of ker fI c= {0.I}
proof
let x be object;
assume x in the carrier of ker fI;
then
A1: x in ker fI;
then
A2: x in I by VECTSP_4:9;
then reconsider v=x as Vector of I;
reconsider w=v as Vector of V1 by VECTSP_4:10;
0.I = 0.V1 by VECTSP_4:11
.= (f|I).v by A1,RANKNULL:10
.= f.v by FUNCT_1:49;
then (f|^1).w = 0.I by Th19
.= 0.V1 by VECTSP_4:11;
then v in U by Th24;
then U/\I = (0).V1 & v in U/\I by A2,VECTSP_5:3,40;
then v in the carrier of (0).V1;
then v in {0.V1} by VECTSP_4:def 3;
then v = 0.V1 by TARSKI:def 1
.= 0.I by VECTSP_4:11;
hence thesis by TARSKI:def 1;
end;
then the carrier of ker fI = {0.I} by ZFMISC_1:33
.= the carrier of (0).I by VECTSP_4:def 3;
then ker fI = (0).I by VECTSP_4:29;
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;
let v be Vector of I such that
A2: fI.v = L * v;
reconsider v1=v as Vector of V by VECTSP_4:10;
A3: f.v = fI.v by A1,FUNCT_1:49
.= L*v1 by A2,VECTSP_4:14;
(fi|I).v1 = fi.v1 by FUNCT_1:49
.= f.v1+((-L)*id V).v1 by MATRLIN:def 3
.= f.v1 +(-L)*(id V.v1) by MATRLIN:def 4
.= L*v1 +(-L)*v1 by A3
.= (L+(-L))*v1 by VECTSP_1:def 15
.= 0.K*v1 by VECTSP_1:19
.= 0.V by VECTSP_1:14;
then
A4: v1 in ker (fi|I) by RANKNULL:10;
fi|I is one-to-one by Th36;
then ker (fi|I)=(0).I by MATRLIN2:43;
hence v = 0.I by A4,VECTSP_4:35
.= 0.V by VECTSP_4:11;
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: now
let x be object;
assume x in dom ((a*b)*f);
then reconsider v=x as Element of V1 by FUNCT_2:def 1;
thus ((a*b)*f).x = (a*b)*(f.v) by MATRLIN:def 4
.= a*(b*f.v) by VECTSP_1:def 16
.= a*(b*f).v by MATRLIN:def 4
.= (a*(b*f)).x by MATRLIN:def 4;
end;
dom ((a*b)*f)=[#]V1 & dom (a*(b*f))=[#]V1 by FUNCT_2:def 1;
hence thesis by A1,FUNCT_1:2;
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 by FUNCT_2:def 1;
A2: dom g=[#]V1 by FUNCT_2:def 1;
A3: now
let x be object;
assume x in dom (L*(f*g));
then reconsider v=x as Element of V1 by FUNCT_2:def 1;
thus (L*(f*g)).x = L* (f*g).v by MATRLIN:def 4
.= L*(f.(g.v)) by A2,FUNCT_1:13
.= (L*f).(g.v) by MATRLIN:def 4
.= ((L*f)*g).x by A1,FUNCT_1:12;
end;
dom (L*(f*g))=[#]V1 by FUNCT_2:def 1;
hence thesis by A1,A3,FUNCT_1:2;
end;
Lm5: for f,g be Function of V1,V1 st f is additive homogeneous
holds L*(f*g)=f*(L*g)
proof
let f,g be Function of V1,V1 such that
A1: f is additive homogeneous;
A2: dom (f*(L*g))=[#]V1 by FUNCT_2:def 1;
A3: dom g=[#]V1 by FUNCT_2:def 1;
A4: now
let x be object;
assume x in dom (L*(f*g));
then reconsider v=x as Element of V1 by FUNCT_2:def 1;
thus (L*(f*g)).x = L* (f*g).v by MATRLIN:def 4
.= L*(f.(g.v)) by A3,FUNCT_1:13
.= f.(L*(g.v)) by A1,MOD_2:def 2
.= f.((L*g).v) by MATRLIN:def 4
.= (f*(L*g)).x by A2,FUNCT_1:12;
end;
dom (L*(f*g))=[#]V1 by FUNCT_2:def 1;
hence thesis by A2,A4,FUNCT_1:2;
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 g=[#]V1 by FUNCT_2:def 1;
A2: dom ((f1+f2)*g)=[#]V1 by FUNCT_2:def 1;
A3: now
let x be object;
assume x in dom g;
then reconsider v=x as Element of V1 by FUNCT_2:def 1;
thus ((f1+f2)*g).x = (f1+f2).(g.v) by A2,FUNCT_1:12
.= f1.(g.v)+f2.(g.v) by MATRLIN:def 3
.= (f1*g).v+f2.(g.v) by A1,FUNCT_1:13
.= (f1*g).v+(f2*g).v by A1,FUNCT_1:13
.= ((f1*g)+(f2*g)).x by MATRLIN:def 3;
end;
dom ((f1*g)+(f2*g))=[#]V1 by FUNCT_2:def 1;
hence thesis by A2,A1,A3,FUNCT_1:2;
end;
Lm7: for f1,f2,g be Function of V1,V1 st g is additive homogeneous
holds g*(f1+f2)=(g*f1)+(g*
f2)
proof
let f1,f2,g be Function of V1,V1 such that
A1: g is additive homogeneous;
A2: dom (g*(f1+f2))=[#]V1 by FUNCT_2:def 1;
A3: dom f2 = [#]V1 by FUNCT_2:def 1;
A4: dom f1 = [#]V1 by FUNCT_2:def 1;
A5: now
let x be object;
assume x in dom (g*(f1+f2));
then reconsider v=x as Element of V1 by FUNCT_2:def 1;
thus (g*(f1+f2)).x = g.((f1+f2).v) by A2,FUNCT_1:12
.= g.(f1.v+f2.v) by MATRLIN:def 3
.= g.(f1.v)+g.(f2.v) by A1,VECTSP_1:def 20
.= (g*f1).v+g.(f2.v) by A4,FUNCT_1:13
.= (g*f1).v+(g*f2).v by A3,FUNCT_1:13
.= ((g*f1)+(g*f2)).x by MATRLIN:def 3;
end;
dom ((g*f1)+(g*f2))=[#]V1 by FUNCT_2:def 1;
hence thesis by A2,A5,FUNCT_1:2;
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: now
let x be object;
assume x in dom (f1+f2+f3);
then reconsider v=x as Element of V1 by FUNCT_2:def 1;
thus (f1+f2+f3).x = (f1+f2).v+f3.v by MATRLIN:def 3
.= (f1.v+f2.v)+f3.v by MATRLIN:def 3
.= f1.v+(f2.v+f3.v) by RLVECT_1:def 3
.= f1.v+(f2+f3).v by MATRLIN:def 3
.= (f1+(f2+f3)).x by MATRLIN:def 3;
end;
dom (f1+f2+f3)=[#]V1 & dom (f1+(f2+f3))=[#]V1 by FUNCT_2:def 1;
hence thesis by A1,FUNCT_1:2;
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: dom id V1 = [#]V1 & dom (1_K*id V1)=[#]V1 by FUNCT_2:def 1;
A2: now
let x be object;
assume x in [#]V1;
then reconsider v=x as Vector of V1;
(id V1).x=v & 1_K*v=v;
hence (id V1).x=(1_K*id V1).x by MATRLIN:def 4;
end;
A3: for n st P[n] holds P[n+1]
proof
let n such that
A4: P[n];
thus (L*id V1) |^ (n+1) = ((L*id V1) |^ 1)*((power K).(L,n)*id V1) by A4
,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:12
.= ((power K).(L,n)*L)*id V1 by Lm3
.=(power K).(L,n+1)*id V1 by GROUP_1:def 7;
end;
(L*id V1) |^ 0 = id V1 & (power K).(L,0)=1_K by Th18,GROUP_1:def 7;
then
A5: P[0] by A1,A2,FUNCT_1:2;
for n holds P[n] from NAT_1:sch 2(A5,A3);
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: now
let x be object;
assume x in dom ((a+b)*f);
then reconsider v=x as Element of V1 by FUNCT_2:def 1;
thus ((a+b)*f).x = (a+b)*(f.v) by MATRLIN:def 4
.= a*f.v+b*f.v by VECTSP_1:def 15
.= (a*f).v+b*f.v by MATRLIN:def 4
.= (a*f).v+(b*f).v by MATRLIN:def 4
.=(a*f + b*f).x by MATRLIN:def 3;
end;
dom ((a+b)*f)=[#]V1 & dom (a*f + b*f)=[#]V1 by FUNCT_2:def 1;
hence thesis by A1,FUNCT_1:2;
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: 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
A2: (f+g)|^n = f * h + (g|^n) and
A3: for i holds (f |^i) * h = h * (f|^i);
take H=f*h+(g|^n)+L*h;
A4: rng (f * h) c= [#] V1 by RELAT_1:def 19;
thus (f+g)|^(n+1) = ((f+g)|^1)*((f+g)|^n) by Th20
.= (f+g)*(f * h + (g|^n)) by A2,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 A4,RELAT_1:53
.= (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;
A5: (f |^i) *(f*h) = (f |^i) *f*h by RELAT_1:36
.= ((f |^i) *(f|^1))*h by Th19
.= (f |^(i+1))*h by Th20
.= h*(f |^(i+1)) by A3
.= h*((f |^1)* (f |^i)) by Th20
.= (h*(f|^1))* (f |^i) by RELAT_1:36
.= ((f|^1)*h)* (f |^i) by A3
.= (f*h)* (f |^i) by Th19;
A6: (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;
(f |^i)*(L*h) = L*((f |^i)*h) by Lm5
.= L*(h*(f|^i)) by A3
.= (L*h)*(f|^i) by Lm4;
hence (f |^i) * H = ((f |^i) *(f*h+(g|^n)))+(L*h)*(f|^i) by Lm7
.= ((f*h)* (f |^i))+ ((g|^n) * (f|^i))+(L*h)*(f|^i) by A5,A6,Lm7
.= (((f*h)+(g|^n)) * (f|^i))+(L*h)*(f|^i) by Lm6
.= H*(f|^i) by Lm6;
end;
A7: 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;
for n st 1<=n holds P[n] from NAT_1:sch 8(A7,A1);
hence thesis;
end;
theorem
for L1,L2 be Scalar of K st f is with_eigenvalues & L1 <> L2 & 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
A3: L2 is eigenvalue of f;
set V=V1;
consider v be Vector of V such that
A4: v <> 0.V and
A5: f.v = L2 * v by A1,A3,Def2;
set f1=(f+(-L1)*id V);
set U=UnionKers f1;
reconsider fU=f|U as linear-transformation of U,U by Th31;
set f2=(f+(-L2)*id V);
let I be Linear_Compl of U;
let fI be linear-transformation of I,I such that
A6: fI = f|I;
A7: now
let v be Vector of V;
assume v in UnionKers f2;
then consider m such that
A8: (f2|^m).v =0.V by Th24;
set v1=v|--(I,U);
set i1=v1`1;
set u1=v1`2;
A9: V is_the_direct_sum_of I,U by VECTSP_5:def 5;
then
A10: v=i1 + u1 by VECTSP_5:def 6;
defpred P[Nat] means (f2|^$1).u1 = 0.V;
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;
set L21=L2-L1;
set f21=f2+L21*id V;
A11: 0.V in I & 0.V in U by VECTSP_4:17;
A12: for n st Q[n] holds Q[n+1]
proof
let n such that
A13: Q[n];
let W be Subspace of V such that
A14: W=I or W=U;
let w be Vector of V such that
A15: w in W;
set fnw=(f2|^n).w;
A16: fnw in W by A13,A14,A15;
A17: now
per cases by A14;
suppose
A18: W=I;
then reconsider F=fnw as Vector of I by A16;
f.fnw = fI.F by A6,FUNCT_1:49;
hence f.fnw in W by A18;
end;
suppose
A19: W=U;
then reconsider F=fnw as Vector of U by A16;
f.fnw = fU.F by FUNCT_1:49;
hence f.fnw in W by A19;
end;
end;
((-L2)*id V).fnw = (-L2)*((id V).fnw) by MATRLIN:def 4
.= (-L2)*fnw;
then
A20: ((-L2)*id V).fnw in W by A16,VECTSP_4:21;
A21: dom (f2|^n) = [#]V by FUNCT_2:def 1;
(f2|^(n+1)).w = ((f2|^1)*(f2|^n)).w by Th20
.= (f2|^1).fnw by A21,FUNCT_1:13
.= (f+(-L2)*id V).fnw by Th19
.= f.fnw+((-L2)*id V).fnw by MATRLIN:def 3;
hence thesis by A17,A20,VECTSP_4:20;
end;
A22: 0.V+0.V = 0.V by RLVECT_1:def 4
.= (f2|^m).i1 +(f2|^m).u1 by A10,A8,VECTSP_1:def 20;
A23: u1 in U by A9,VECTSP_5:def 6;
then consider n such that
A24: (f1|^n).u1 =0.V by Th24;
A25: Q[0]
proof
let W be Subspace of V such that
W=I or W=U;
let w be Vector of V such that
A26: w in W;
(f2|^0).w = (id V).w by Th18
.= w;
hence thesis by A26;
end;
A27: for n holds Q[n] from NAT_1:sch 2(A25,A12);
then
A28: (f2|^m).u1 in U by A23;
A29: i1 in I by A9,VECTSP_5:def 6;
then (f2|^m).i1 in I by A27;
then (f2|^m).u1=0.V by A9,A28,A11,A22,VECTSP_5:48;
then
A30: ex m st P[m];
consider MIN be Nat such that
A31: P[MIN] and
A32: for n st P[n] holds MIN <= n from NAT_1:sch 5(A30);
assume
A33: not v is Vector of I;
A34: u1 <>0.V
by A10,A29,A33,RLVECT_1:def 4;
n<>0
proof
assume n=0;
then 0.V = (id V).u1 by A24,Th18
.= u1;
hence thesis by A34;
end;
then consider h be linear-transformation of V,V such that
A35: f21 |^ n = f2 * h + ((L21*id V) |^ n) and
A36: for i holds (f2 |^ i) * h = h * (f2 |^ i) by Th38,NAT_1:14;
A37: dom (f21|^n)=[#]V by FUNCT_2:def 1;
MIN <>0
proof
assume MIN=0;
then 0.V = (id V).u1 by A31,Th18
.= u1;
hence thesis by A34;
end;
then reconsider M1=MIN-1 as Element of NAT by NAT_1:20;
A38: (f2|^M1)*(f2 * h) = (f2|^M1)*f2 * h by RELAT_1:36
.= (f2|^M1)*(f2|^1)*h by Th19
.= (f2|^(M1+1))*h by Th20
.= h*(f2|^MIN) by A36;
dom((L21*id V) |^ n)=[#]V by FUNCT_2:def 1;
then
A39: ((f2|^M1) * ((L21*id V) |^ n)).u1 = (f2|^M1).(((L21*id V) |^ n).u1)
by FUNCT_1:13
.= (f2|^M1).(((power K).(L21,n) * id V).u1) by Lm9
.= (f2|^M1).((power K).(L21,n)*((id V).u1)) by MATRLIN:def 4
.= (f2|^M1).( (power K).(L21,n)*u1)
.= (power K).(L21,n) * ((f2|^M1).u1) by MOD_2:def 2;
A40: (power K).(L21,n) <>0.K
proof
assume 0.K=(power K).(L21,n);
then 0.K = Product (n|->L21) by MATRIXJ1:5;
then
A41: ex k be Nat st k in dom (n|->L21) & (n|->L21) .k=0.K by FVSUM_1:82;
dom (n|->L21)=Seg n by FINSEQ_2:124;
then L21=0.K by A41,FINSEQ_2:57;
hence thesis by A2,VECTSP_1:19;
end;
dom (f2|^MIN) =[#]V by FUNCT_2:def 1;
then
A42: (h*(f2|^MIN)).u1 = h.((f2|^MIN).u1) by FUNCT_1:13
.= 0.V by A31,RANKNULL:9;
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 3
.= f+((0.K+-L1)*id V) by VECTSP_1:19
.= f1 by RLVECT_1:def 4;
then 0.V =(f2|^M1).((f21|^n).u1) by A24,RANKNULL:9
.= ((f2|^M1)*(f2 * h + ((L21*id V) |^ n))).u1 by A35,A37,FUNCT_1:13
.= (h*(f2|^MIN) + (f2|^M1) * ((L21*id V) |^ n)).u1 by A38,Lm7
.= 0.V + (power K).(L21,n) * ((f2|^M1).u1) by A42,A39,MATRLIN:def 3
.= (power K).(L21,n) * ((f2|^M1).u1) by RLVECT_1:def 4;
then (f2|^M1).u1 = 0.V by A40,VECTSP_1:15;
then M1+1<=M1 by A32;
hence contradiction by NAT_1:13;
end;
v is eigenvector of f,L2 by A1,A3,A5,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 A7;
A43: 0.V = 0.I & L2*v=L2*vI by VECTSP_4:11,14;
A44: f.v=fI.vI by A6,FUNCT_1:49;
hence
A45: fI is with_eigenvalues by A4,A5,A43;
not L1 is eigenvalue of fI
proof
assume L1 is eigenvalue of fI;
then consider w be Vector of I such that
A46: w<>0.I and
A47: fI.w = L1 * w by A45,Def2;
w=0.V by A6,A47,Th37;
hence thesis by A46,VECTSP_4:11;
end;
hence
not L1 is eigenvalue of fI & L2 is eigenvalue of fI by A4,A5,A43,A44,A45,Def2
;
the carrier of UnionKers f2 c= the carrier of I
proof
let x be object;
assume x in the carrier of UnionKers f2;
then
A48: x in UnionKers f2;
then x in V by VECTSP_4:9;
then reconsider v=x as Vector of V;
v is Vector of I by A7,A48;
hence thesis;
end;
hence thesis by VECTSP_4:27;
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: for n st P[n] holds P[n+1]
proof
card U<>0 by A2;
then reconsider C=card U-1 as Element of NAT by NAT_1:20;
let n such that
A4: P[n];
set n1=n+1;
let L be Linear_Combination of U\{u} such that
A5: card Carrier(L)=n1;
consider x being object such that
A6: x in Carrier L by A5,CARD_1:27,XBOOLE_0:def 1;
A7: Carrier L c= U\{u} by VECTSP_6:def 4;
then x in U by A6,XBOOLE_0:def 5;
then
A8: x<>0.V by A1,VECTSP_7:2;
reconsider x as Vector of V by A6;
x in {x} by TARSKI:def 1;
then x in Lin({x}) by VECTSP_7:8;
then consider X be Linear_Combination of {x} such that
A9: x=Sum(X) by VECTSP_7:7;
set Lx=L.x;
set LxX=Lx*X;
Carrier LxX c= Carrier X & Carrier X c= {x} by VECTSP_6:28,def 4;
then
A10: Carrier LxX c= {x};
then Carrier (L-LxX) c= Carrier L \/ Carrier LxX & Carrier L \/ Carrier
LxX c= Carrier L \/ {x} by VECTSP_6:41,XBOOLE_1:9;
then Carrier (L-LxX) c= Carrier L \/{x};
then
A11: Carrier (L-LxX) c= Carrier L by A6,ZFMISC_1:40;
then Carrier (L-LxX) c= U\{u} by A7;
then reconsider LLxX=L-LxX as Linear_Combination of U\{u} by VECTSP_6:def 4
;
A12: x in (U\{u})\/{u+Sum(LLxX)} by A6,A7,XBOOLE_0:def 3;
A13: Carrier L\{x} c= Carrier(L-LxX)
proof
let y be object such that
A14: y in Carrier L\{x};
y in Carrier L by A14,XBOOLE_0:def 5;
then consider Y be Vector of V such that
A15: y = Y and
A16: L.Y <> 0.K;
not Y in Carrier LxX by A10,A14,A15,XBOOLE_0:def 5;
then LxX.Y =0.K;
then (L-LxX).Y = L.Y - 0.K by VECTSP_6:40
.= L.Y by RLVECT_1:13;
hence thesis by A15,A16;
end;
X.x * x = x by A9,VECTSP_6:17
.= 1_K*x;
then
A17: X.x=1_K by A8,VECTSP10:4;
(L-LxX).x = Lx - LxX.x by VECTSP_6:40
.= Lx-Lx * 1_K by A17,VECTSP_6:def 9
.= Lx-Lx
.= 0.K by RLVECT_1:5;
then not x in Carrier (L-LxX) by VECTSP_6:2;
then Carrier (L-LxX) c= Carrier L\{x} by A11,ZFMISC_1:34;
then
A18: Carrier (L-LxX) = Carrier L\{x} by A13;
{x} c= Carrier L by A6,ZFMISC_1:31;
then card Carrier (L-LxX) = n1 - card {x} by A5,A18,CARD_2:44
.= n1-1 by CARD_1:30
.= n;
then
A19: (U\{u})\/{u+Sum(LLxX)} is linearly-independent by A4;
u+Sum(LLxX) in {u+Sum(LLxX)} by TARSKI:def 1;
then
A20: u+Sum(LLxX) in (U\{u})\/{u+Sum(LLxX)} by XBOOLE_0:def 3;
A21: not u+Sum(L) in U\{u}
proof
assume u+Sum(L) in U\{u};
then
A22: u+Sum(L) in Lin(U\{u}) by VECTSP_7:8;
A23: (u+Sum(L))-Sum(L) = u+(Sum(L)-Sum(L)) by RLVECT_1:def 3
.= u+0.V by RLVECT_1:5
.= u by RLVECT_1:def 4;
Sum (L) in Lin(U\{u}) by VECTSP_7:7;
hence thesis by A1,A2,A22,A23,VECTSP_4:23,VECTSP_9:14;
end;
card U=C+1;
then card (U\{u})= C by A2,STIRL2_1:55;
then
A24: card ((U\{u})\/{ u+Sum L}) =C+1 by A21,CARD_2:41;
Sum L = 0.V+Sum (L) by RLVECT_1:def 4
.= Sum LxX +(-Sum LxX) +Sum L by RLVECT_1:5
.= Sum LxX +(Sum L-Sum LxX)by RLVECT_1:def 3
.= Sum LxX + Sum LLxX by VECTSP_6:47
.= Lx*x + Sum LLxX by A9,VECTSP_6:45;
then
A25: u+Sum(LLxX)+Lx*x = u +Sum L by RLVECT_1:def 3;
A26: not u+Sum(LLxX) in U\{u}
proof
assume u+Sum(LLxX) in U\{u};
then
A27: u+Sum(LLxX) in Lin(U\{u}) by VECTSP_7:8;
A28: (u+Sum(LLxX))-Sum(LLxX) = u+(Sum(LLxX)-Sum(LLxX)) by RLVECT_1:def 3
.= u+0.V by RLVECT_1:5
.= u by RLVECT_1:def 4;
Sum (LLxX) in Lin(U\{u}) by VECTSP_7:7;
hence thesis by A1,A2,A27,A28,VECTSP_4:23,VECTSP_9:14;
end;
then
A29: ((U\{u})\/{u+Sum(LLxX)}) \ {u+Sum(LLxX)} = U\{u} by ZFMISC_1:117;
u+Sum(LLxX)<>x by A6,A7,A26;
hence thesis by A19,A25,A29,A20,A12,A24,MATRIX13:115;
end;
let L be Linear_Combination of U\{u};
A30: P[0]
proof
let L be Linear_Combination of U\{u};
assume card Carrier(L)=0;
then Carrier L = {};
then u+Sum L = u+0.V by VECTSP_6:19
.= u by RLVECT_1:def 4;
hence thesis by A1,A2,ZFMISC_1:116;
end;
for n holds P[n] from NAT_1:sch 2(A30,A3);
then P[card Carrier L];
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;
set C=Carrier L;
consider F be FinSequence of the carrier of V2 such that
A2: F is one-to-one and
A3: rng F = Carrier(L) and
A4: Sum L = Sum(L (#) F) by VECTSP_6:def 6;
defpred P[object,object] means $2 in A & f.$2=F.$1;
:: obciecie funkcji ??? !!!
set D=dom F;
A5: for x being object st x in D
ex y being object st y in the carrier of V1 & P[x,y]
proof
let x be object;
assume x in D;
then F.x in rng F by FUNCT_1:def 3;
then consider y being object such that
y in dom f and
A6: y in A & f.y=F.x by A1,A3,FUNCT_1:def 6;
take y;
thus thesis by A6;
end;
consider p be Function of D,the carrier of V1 such that
A7: for x being object st x in D holds P[x,p.x] from FUNCT_2:sch 1(A5);
A8: rng p c= the carrier of V1 by RELAT_1:def 19;
A9: dom p=D by FUNCT_2:def 1;
D=Seg len F by FINSEQ_1:def 3;
then reconsider p as FinSequence by A9,FINSEQ_1:def 2;
reconsider p as FinSequence of V1 by A8,FINSEQ_1:def 4;
A10: now
let x1,x2 be object such that
A11: x1 in dom p & x2 in dom p and
A12: p.x1=p.x2;
f.(p.x1)=F.x1 & f.(p.x2)=F.x2 by A7,A9,A11;
hence x1=x2 by A2,A9,A11,A12,FUNCT_1:def 4;
end;
then
A13: p is one-to-one by FUNCT_1:def 4;
reconsider RNG=rng p as finite Subset of V1 by RELAT_1:def 19;
defpred Q[object,object] 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);
A14: for x being object st x in the carrier of V1
ex y being object st y in the carrier of K & Q[x,y]
proof
let x be object;
assume x in the carrier of V1;
then reconsider v1=x as Vector of V1;
per cases;
suppose
A15: not v1 in rng p;
take 0.K;
thus thesis by A15;
end;
suppose
A16: v1 in rng p;
then consider y being object such that
A17: y in dom p & p.y=v1 by FUNCT_1:def 3;
take L.(F.y);
L.(F/.y) in the carrier of K;
hence thesis by A9,A10,A16,A17,PARTFUN1:def 6;
end;
end;
consider M be Function of V1,K such that
A18: for x being object st x in the carrier of V1 holds Q[x,M.x]
from FUNCT_2:sch 1(
A14 );
reconsider M as Element of Funcs(the carrier of V1, the carrier of K) by
FUNCT_2:8;
for v1 be Element of V1 st not v1 in RNG holds M.v1 = 0.K by A18;
then reconsider M as Linear_Combination of V1 by VECTSP_6:def 1;
A19: Carrier M= RNG
proof
thus Carrier M c= RNG
proof
let x be object such that
A20: x in Carrier M;
reconsider v1=x as Vector of V1 by A20;
M.v1 <>0.K by A20,VECTSP_6:2;
hence thesis by A18;
end;
let y be object such that
A21: y in RNG;
reconsider v1=y as Vector of V1 by A21;
consider x being object such that
A22: x in D and
A23: p.x=v1 by A9,A21,FUNCT_1:def 3;
F.x in C by A3,A22,FUNCT_1:def 3;
then
A24: L.(F.x)<>0.K by VECTSP_6:2;
M.v1= L.(F.x) by A18,A21,A22,A23;
hence thesis by A24;
end;
RNG c= A
proof
let y be object;
assume y in RNG;
then ex x being object st x in D & p.x=y by A9,FUNCT_1:def 3;
hence thesis by A7;
end;
then reconsider M as Linear_Combination of A by A19,VECTSP_6:def 4;
len (M(#)p)=len p by VECTSP_6:def 5;
then
A25: dom (M(#)p)=D by A9,FINSEQ_3:29;
len (L(#)F) =len F by VECTSP_6:def 5;
then
A26: dom (L(#)F) = D by FINSEQ_3:29;
A27: now
let x be object such that
A28: x in D;
reconsider i=x as Element of NAT by A28;
A29: F.i=F/.i by A28,PARTFUN1:def 6;
p.i in RNG by A9,A28,FUNCT_1:def 3;
then
A30: M.(p.i)=L.(F.i) by A18,A28;
A31: p/.i=p.i & f.(p.i)=F.i by A7,A9,A28,PARTFUN1:def 6;
thus (f*(M(#)p)).x = f.((M(#)p).i) by A25,A28,FUNCT_1:13
.= f.(M.(p/.i)*p/.i) by A25,A28,VECTSP_6:def 5
.= L.(F/.i) *F/.i by A31,A29,A30,MOD_2:def 2
.= (L(#)F).x by A26,A28,VECTSP_6:def 5;
end;
take M;
dom f=[#]V1 & rng (M(#)p) c= [#]V1 by FUNCT_2:def 1,RELAT_1:def 19;
then dom(f*(M(#)p))=dom(M(#)p) by RELAT_1:27;
then f*(M(#)p) = L(#)F by A26,A25,A27,FUNCT_1:2;
hence Sum L = f.(Sum(M(#)p)) by A4,MATRLIN:16
.= f.(Sum M) by A13,A19,VECTSP_6:def 6;
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;
A1: dom f=[#]V1 by FUNCT_2:def 1;
let A be Subset of V1,B be Subset of V2 such that
A2: f.:A = B;
thus f.:(the carrier of Lin A) c= the carrier of Lin B
proof
let y be object;
assume y in f.:(the carrier of Lin A);
then consider x being object such that
x in dom f and
A3: x in the carrier of Lin A and
A4: f.x=y by FUNCT_1:def 6;
x in Lin A by A3;
then consider L be Linear_Combination of A such that
A5: x=Sum L by VECTSP_7:7;
consider F be FinSequence of V1 such that
F is one-to-one and
A6: rng F=Carrier L and
A7: x= Sum(L (#) F) by A5,VECTSP_6:def 6;
set LF=L(#)F;
consider g be sequence of the carrier of V1 such that
A8: x = g.(len LF) and
A9: g.0 = 0.V1 and
A10: for j be Nat, v be Vector of V1 st j < len LF & v = LF
.(j+1) holds g.(j+1) = g.j + v by A7,RLVECT_1:def 12;
defpred P[Nat] means $1 <= len F implies f.(g.$1) in Lin B;
A11: len LF=len F by VECTSP_6:def 5;
then
A12: dom LF=dom F by FINSEQ_3:29;
A13: for n st P[n] holds P[n+1]
proof
let n such that
A14: P[n];
reconsider N=n as Element of NAT by ORDINAL1:def 12;
reconsider gn=g.N as Vector of V1;
set N1=N+1;
assume
A15: n+1<=len F;
then
A16: N<len F by NAT_1:13;
A17: Carrier L c= A & dom f=[#]V1 by FUNCT_2:def 1,VECTSP_6:def 4;
1<=n+1 by NAT_1:14;
then
A18: n+1 in dom F by A15,FINSEQ_3:25;
then F/.N1= F.N1 & F.N1 in Carrier L by A6,FUNCT_1:def 3,PARTFUN1:def 6;
then f.(F/.N1) in B by A2,A17,FUNCT_1:def 6;
then
A19: L.(F/.N1)*f.(F/.N1) in Lin B by VECTSP_4:21,VECTSP_7:8;
LF.N1=L.(F/.N1)*(F/.N1) by A12,A18,VECTSP_6:def 5;
then g.N1=gn+L.(F/.N1)*(F/.N1) by A11,A10,A16;
then f.(g.(n+1)) = f.(gn)+f.(L.(F/.N1)*(F/.N1))
by VECTSP_1:def 20
.= f.(gn)+L.(F/.N1)*f.(F/.N1) by MOD_2:def 2;
hence thesis by A14,A15,A19,NAT_1:13,VECTSP_4:20;
end;
f.(0.V1)=0.V2 by RANKNULL:9;
then
A20: P[0] by A9,VECTSP_4:17;
for n holds P[n] from NAT_1:sch 2(A20,A13);
then P[len F];
hence thesis by A4,A11,A8,STRUCT_0:def 5;
end;
let x be object;
assume x in the carrier of Lin B;
then x in Lin B;
then consider L be Linear_Combination of B such that
A21: x=Sum L by VECTSP_7:7;
Carrier L c= B by VECTSP_6:def 4;
then consider M be Linear_Combination of A such that
A22: f.(Sum M)=Sum L by A2,Th41;
Sum M in Lin A by VECTSP_7:7;
then Sum M in the carrier of Lin A;
hence thesis by A21,A22,A1,FUNCT_1:def 6;
end;
theorem Th43:
for L be Linear_Combination of V1, F be FinSequence of V1, f be
linear-transformation of V1,V2 st f|(Carrier L /\ rng F) is one-to-one & rng F
c= Carrier L ex Lf be Linear_Combination of V2 st Carrier Lf = f.:(Carrier L /\
rng F) & f*(L(#)F) = Lf(#)(f*F) & for v1 st v1 in Carrier L /\ rng F holds L.v1
=Lf.(f.v1)
proof
let L be Linear_Combination of V1, F be FinSequence of V1, f be
linear-transformation of V1,V2 such that
A1: f|((Carrier L) /\ (rng F)) is one-to-one and
A2: rng F c= Carrier L;
set R=rng F;
set C=Carrier L;
defpred P[object,object] means
(not $1 in f.:(C/\R) implies $2=0.K) & ($1 in f.:(C
/\R) implies for v1 be Vector of V1 st v1 in C/\R & f.v1=$1 holds $2=L.v1);
A3: for x being object st x in the carrier of V2
ex y being object st y in the carrier of K & P[x,y]
proof
let x being object such that
x in the carrier of V2;
per cases;
suppose
A4: not x in f.:(C/\R);
take 0.K;
thus thesis by A4;
end;
suppose
A5: x in f.:(C/\R);
then consider y being object such that
y in dom f and
A6: y in C/\R and
A7: x=f.y by FUNCT_1:def 6;
reconsider y as Vector of V1 by A6;
take L.y;
now
A8: dom f=[#]V1 by FUNCT_2:def 1;
then
A9: y in dom(f|(C/\R)) by A6,RELAT_1:57;
A10: (f|(C/\R)).y=x by A6,A7,FUNCT_1:49;
let v1 be Vector of V1 such that
A11: v1 in C/\R and
A12: f.v1=x;
A13: (f|(C/\R)).v1=x by A11,A12,FUNCT_1:49;
v1 in dom(f|(C/\R)) by A11,A8,RELAT_1:57;
hence L.y=L.v1 by A1,A9,A13,A10,FUNCT_1:def 4;
end;
hence thesis by A5;
end;
end;
consider Lf be Function of V2,K such that
A14: for x being object st x in the carrier of V2 holds P[x,Lf.x]
from FUNCT_2:sch 1(
A3 );
reconsider Lf as Element of Funcs(the carrier of V2, the carrier of K) by
FUNCT_2:8;
for v2 be Element of V2 st not v2 in f.:(C/\R) holds Lf.v2 = 0.K by A14;
then reconsider Lf as Linear_Combination of V2 by VECTSP_6:def 1;
A15: dom f = [#]V1 by FUNCT_2:def 1;
take Lf;
A16: f.:(C/\ R) c= Carrier Lf
proof
let y be object such that
A17: y in f.:(C/\R);
consider v1 be object such that
v1 in dom f and
A18: v1 in C/\R and
A19: f.v1=y by A17,FUNCT_1:def 6;
reconsider v1 as Vector of V1 by A18;
v1 in C by A18,XBOOLE_0:def 4;
then
A20: L.v1 <> 0.K by VECTSP_6:2;
reconsider v2=y as Vector of V2 by A17;
Lf.v2 = L.v1 by A14,A17,A18,A19;
hence thesis by A20;
end;
Carrier Lf c= f.:(C/\ R)
proof
let x be object such that
A21: x in Carrier Lf;
reconsider v2=x as Vector of V2 by A21;
Lf.v2<>0.K by A21,VECTSP_6:2;
hence thesis by A14;
end;
hence Carrier Lf = f.:(C/\ R) by A16;
len (L(#)F)=len F by VECTSP_6:def 5;
then
A22: dom (L(#)F) =dom F by FINSEQ_3:29;
rng F c= [#]V1 by RELAT_1:def 19;
then
A23: dom (f*F)=dom F by A15,RELAT_1:27;
len (Lf(#)(f*F)) =len (f*F) by VECTSP_6:def 5;
then
A24: dom (Lf(#)(f*F)) =dom (f*F) by FINSEQ_3:29;
A25: now
let x be object such that
A26: x in dom F;
reconsider k=x as Nat by A26;
A27: (f*F).k=(f*F)/.k by A23,A26,PARTFUN1:def 6;
A28: F/.k=F.k by A26,PARTFUN1:def 6;
then
A29: (f*F).k=f.(F/.k) by A23,A26,FUNCT_1:12;
F.k in R by A26,FUNCT_1:def 3;
then
A30: F.k in C/\R by A2,XBOOLE_0:def 4;
then (f*F)/.k in f.:(C/\R) by A15,A28,A29,A27,FUNCT_1:def 6;
then
A31: L.(F/.k)=Lf.((f*F)/.k) by A14,A28,A29,A27,A30;
thus (f*(L(#)F)).x = f.((L(#)F).k) by A22,A26,FUNCT_1:13
.= f.(L.(F/.k)* F/.k) by A22,A26,VECTSP_6:def 5
.= Lf.((f*F)/.k) * (f*F)/.k by A29,A27,A31,MOD_2:def 2
.= (Lf(#)(f*F)).x by A24,A23,A26,VECTSP_6:def 5;
end;
rng (L(#)F) c= [#]V1 by RELAT_1:def 19;
then dom (f*(L(#)F))= dom (L(#)F) by A15,RELAT_1:27;
hence f*(L(#)F) = Lf(#)(f*F) by A22,A24,A23,A25,FUNCT_1:2;
let v1 be Vector of V1 such that
A32: v1 in C /\ R;
f.v1 in f.:(C/\R) by A15,A32,FUNCT_1:def 6;
hence thesis by A14,A32;
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 additive homogeneous 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 and
A2: Sum L = 0.V1;
consider F be FinSequence of V1 such that
A3: F is one-to-one and
A4: rng F = Carrier L and
A5: 0.V1 = Sum(L (#) F) by A2,VECTSP_6:def 6;
let f be additive homogeneous Function of V1,V2 such that
A6: f|B is one-to-one and
A7: f.:B is linearly-independent Subset of V2 and
A8: f.:A c= {0.V2};
per cases;
suppose
dom F={};
then rng F={} by RELAT_1:42;
hence thesis by A4;
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);
set SS=(Sgm FB)^(Sgm FA);
A9: C/\(C/\B) = C/\B by XBOOLE_1:18,28;
rng F c= the carrier of V1 by RELAT_1:def 19;
then reconsider F9=F as Function of D,the carrier of V1 by FUNCT_2:2;
A10: D=Seg len F by FINSEQ_1:def 3;
A16: FA c= D by RELAT_1:132;
then
a10: FA is included_in_Seg by A10,FINSEQ_1:def 13;
then
A11: Sgm FA is one-to-one by FINSEQ_3:92;
A14: FB c= D by RELAT_1:132;
then
a11: FB is included_in_Seg by A10,FINSEQ_1:def 13;
then
A12: len Sgm FA = card FA & len Sgm FB = card FB
by a10,FINSEQ_3:39;
A13: Sgm FB is one-to-one by a11,FINSEQ_3:92;
FB is included_in_Seg by A10,A14,FINSEQ_1:def 13;
then
A15: rng Sgm FB = FB by FINSEQ_1:def 14;
A17: rng Sgm FA =FA by a10,FINSEQ_1:def 14;
then reconsider SA=Sgm FA,SB=Sgm FB as FinSequence of D
by A16,A14,A15,FINSEQ_1:def 4;
A misses B
proof
assume A meets B;
then consider x being object such that
A18: x in A and
A19: x in B by XBOOLE_0:3;
reconsider x as Vector of V1 by A18;
dom f = the carrier of V1 by FUNCT_2:def 1;
then f.x in f.:A & f.x in f.:B by A18,A19,FUNCT_1:def 6;
then 0.V2 in f.:B by A8,TARSKI:def 1;
hence thesis by A7,VECTSP_7:2;
end;
then
A20: C/\A misses C/\B by XBOOLE_1:76;
then FA misses FB by FUNCT_1:71;
then
A21: SS is one-to-one by A11,A17,A13,A15,FINSEQ_3:91;
(C/\A) \/ (C/\B) = C /\ (A\/B) by XBOOLE_1:23
.= C by A1,XBOOLE_1:28;
then
A22: FA\/FB = F"C by RELAT_1:140
.= dom F by A4,RELAT_1:134;
then card FA +card FB = card (Seg len F) by A10,A20,CARD_2:40,FUNCT_1:71
.= len F by FINSEQ_1:57;
then len SS = len F by A12,FINSEQ_1:22;
then
A23: dom SS = D by FINSEQ_3:29;
rng SS = D by A22,A17,A15,FINSEQ_1:31;
then reconsider SS as Function of D,D by A23,FUNCT_2:1;
card D=card D;
then SS is onto by A21,FINSEQ_4:63;
then reconsider SS as Permutation of D by A21;
reconsider FS=F9*SS,FSA=F9*SA,FSB=F9*SB as FinSequence of V1 by FINSEQ_2:47
;
A24: C/\B c= rng FSB
proof
let y be object such that
A25: y in C/\B;
y in rng F by A4,A25,XBOOLE_0:def 4;
then consider x being object such that
A26: x in dom F & y=F.x by FUNCT_1:def 3;
x in FB by A25,A26,FUNCT_1:def 7;
then consider z be object such that
A27: z in dom SB & SB.z=x by A15,FUNCT_1:def 3;
FSB.z = y & z in dom FSB by A26,A27,FUNCT_1:11,13;
hence thesis by FUNCT_1:def 3;
end;
rng FSB c= C/\B
proof
let y be object;
assume y in rng FSB;
then consider x being object such that
A28: x in dom FSB and
A29: FSB.x=y by FUNCT_1:def 3;
x in dom SB by A28,FUNCT_1:11;
then
A30: SB.x in F"(C/\B) by A15,FUNCT_1:def 3;
FSB.x =F.(SB.x) by A28,FUNCT_1:12;
hence thesis by A29,A30,FUNCT_1:def 7;
end;
then
A31: C/\B = rng FSB by A24;
A32: now
len (L(#)FSA) =len FSA by VECTSP_6:def 5;
then
A33: dom (L(#)FSA) =dom FSA by FINSEQ_3:29;
A34: dom f=[#]V1 by FUNCT_2:def 1;
rng (L(#)FSA) c= [#]V1 & dom f = [#]V1 by FUNCT_2:def 1,RELAT_1:def 19;
then
A35: dom (f*(L(#)FSA))=dom (L(#)FSA) by RELAT_1:27;
let k be Nat,v be Element of V2 such that
A36: k in dom (f*(L(#)FSA)) and
v = (f*(L(#)FSA)).k;
dom FSA=dom SA by A17,RELAT_1:27,132;
then SA.k in F"(C/\A) by A17,A36,A35,A33,FUNCT_1:def 3;
then
A37: F.(SA.k) in C/\A by FUNCT_1:def 7;
FSA/.k = FSA.k by A36,A35,A33,PARTFUN1:def 6
.= F.(SA.k) by A36,A35,A33,FUNCT_1:12;
then FSA/.k in A by A37,XBOOLE_0:def 4;
then f.(FSA/.k) in f.:A by A34,FUNCT_1:def 6;
then
A38: f.(FSA/.k)=0.V2 by A8,TARSKI:def 1;
thus (f*(L(#)FSA)).k = f.((L(#)FSA).k) by A36,FUNCT_1:12
.= f.(L.(FSA/.k)*(FSA/.k)) by A36,A35,VECTSP_6:def 5
.= L.(FSA/.k) * 0.V2 by A38,MOD_2:def 2
.= 0.V2 by VECTSP_1:14
.= 0.K*v by VECTSP_1:14;
end;
len (f*(L(#)FSA))=len (f*(L(#)FSA));
then
A39: Sum(f*(L(#)FSA)) =0.K * Sum(f*(L(#)FSA)) by A32,RLVECT_2:66;
FS=FSB^FSA by FINSEQOP:9;
then L(#)FS = (L(#)FSB) ^(L(#)FSA) by VECTSP_6:13;
then
A40: f * (L(#)FS) = (f*(L(#)FSB)) ^(f*(L(#)FSA)) by FINSEQOP:9;
(f|B)|(C/\B)= f|(C/\B) by RELAT_1:74,XBOOLE_1:18;
then
A41: f|(C/\B) is one-to-one by A6,FUNCT_1:52;
then consider Lf be Linear_Combination of V2 such that
A42: Carrier Lf = f.:(C /\ rng FSB) and
A43: f*(L(#)FSB) = Lf(#) (f*FSB) and
A44: for v1 be Vector of V1 st v1 in C /\ rng FSB holds L.v1=Lf.(f.v1)
by A31,A9,Th43,XBOOLE_1:18;
A45: Carrier Lf=rng (f*FSB) by A31,A9,A42,RELAT_1:127;
A46: f*FSB = f*((id rng FSB)*FSB) by RELAT_1:53
.= f*(id rng FSB)*FSB by RELAT_1:36
.= (f|(C/\B)) *FSB by A31,RELAT_1:65;
Carrier Lf c= f.:B by A31,A9,A42,RELAT_1:123,XBOOLE_1:18;
then
A47: Lf is Linear_Combination of f.:B by VECTSP_6:def 4;
f.(0.V1)=0.V2 by RANKNULL:9;
then
A48: 0.V2 = f.Sum (L(#)FS) by A5,VECTSP_9:1
.= Sum (f * (L(#)FS)) by MATRLIN:16
.= Sum(f*(L(#)FSB)) +Sum(f*(L(#)FSA)) by A40,RLVECT_1:41
.= Sum(f*(L(#)FSB)) + 0.V2 by A39,VECTSP_1:14
.= Sum(Lf(#) (f*FSB)) by A43,RLVECT_1:def 4
.= Sum(Lf) by A3,A13,A41,A45,A46,VECTSP_6:def 6;
thus C c= A
proof
let x be object such that
A49: x in C;
reconsider v1=x as Vector of V1 by A49;
assume
A50: not x in A;
x in A or x in B by A1,A49,XBOOLE_0:def 3;
then v1 in C/\rng FSB by A31,A9,A49,A50,XBOOLE_0:def 4;
then
A51: L.v1 = Lf.(f.v1) by A44;
not (f.v1) in Carrier Lf by A7,A47,A48,VECTSP_7:def 1;
then L.v1=0.K by A51;
hence contradiction by A49,VECTSP_6:2;
end;
end;
end;