:: Associated Matrix of Linear Map :: by Robert Milewski :: :: Received June 30, 1995 :: Copyright (c) 1995-2021 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, XBOOLE_0, MATRIX_1, FINSEQ_3, RELAT_1, FINSEQ_1, TARSKI, ARYTM_3, XXREAL_0, CARD_1, TREES_1, FUNCT_1, INCSP_1, ORDINAL4, SUBSET_1, VECTSP_1, RLVECT_2, RLVECT_3, CARD_3, ARYTM_1, SUPINF_2, RLVECT_5, FINSET_1, STRUCT_0, RLSUB_1, ALGSTR_0, PARTFUN1, RLVECT_1, ZFMISC_1, QC_LANG1, FUNCT_2, VALUED_1, PRE_POLY, FINSEQ_2, RVSUM_1, FINSEQ_4, FVSUM_1, MATRLIN, MSSUBFAM, UNIALG_1; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, NAT_1, MOD_2, FINSEQ_1, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, FUNCT_3, MATRIX_0, STRUCT_0, ALGSTR_0, MATRIX_1, MATRIX_3, FVSUM_1, RLVECT_1, VECTSP_1, VECTSP_4, VECTSP_6, VECTSP_7, FINSET_1, FINSEQ_3, FINSEQ_2, FINSEQOP, BINOP_1, XXREAL_0, PRE_POLY, GRCAT_1; constructors PARTFUN1, BINOP_1, FUNCT_3, SQUARE_1, NAT_1, VECTSP_6, VECTSP_7, MOD_2, FVSUM_1, MATRIX_3, RELSET_1, PRE_POLY, GRCAT_1, MATRIX_1; registrations XBOOLE_0, SUBSET_1, ORDINAL1, RELSET_1, FUNCT_2, FINSET_1, XXREAL_0, XREAL_0, NAT_1, FINSEQ_1, STRUCT_0, VECTSP_1, CARD_1, VECTSP_7, PRE_POLY, RELAT_1, FUNCT_1, MATRIX_0; requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM; begin :: Preliminaries reserve k,t,i,j,m,n for Nat, x,y,y1,y2 for object, D for non empty set; definition let D be non empty set; let k; let M be Matrix of D; redefine func Del(M,k) -> Matrix of D; end; ::$CT theorem :: MATRLIN:2 for M be Matrix of n+1,m,D for M1 be Matrix of D holds ( n > 0 implies width M = width Del(M,n+1) ) & ( M1 = <*M.(n+1)*> implies width M = width M1 ); theorem :: MATRLIN:3 for M be Matrix of n+1,m,D holds Del(M,n+1) is Matrix of n,m,D; ::$CT definition let D; let P be FinSequence of D; redefine func <*P*> -> Matrix of 1,len P,D; end; begin :: More on Finite Sequences begin :: Sequences and Matrices Concerning Linear Transformations reserve K for Field, V for VectSp of K, a for Element of K, W for Element of V; reserve KL1,KL2,KL3 for Linear_Combination of V, X for Subset of V; theorem :: MATRLIN:5 X is linearly-independent & Carrier KL1 c= X & Carrier KL2 c= X & Sum KL1 = Sum KL2 implies KL1 = KL2; theorem :: MATRLIN:6 X is linearly-independent & Carrier KL1 c= X & Carrier KL2 c= X & Carrier KL3 c= X & Sum KL1 = Sum KL2 + Sum KL3 implies KL1 = KL2 + KL3; theorem :: MATRLIN:7 X is linearly-independent & Carrier KL1 c= X & Carrier KL2 c= X & a <> 0.K & Sum KL1 = a * Sum KL2 implies KL1 = a * KL2; theorem :: MATRLIN:8 for b2 be Basis of V ex KL be Linear_Combination of V st W = Sum KL & Carrier KL c= b2; definition let K be Field; let V be VectSp of K; attr V is finite-dimensional means :: MATRLIN:def 1 ex A being finite Subset of V st A is Basis of V; end; registration let K be Field; cluster strict finite-dimensional for VectSp of K; end; definition let K be Field; let V be finite-dimensional VectSp of K; mode OrdBasis of V -> FinSequence of V means :: MATRLIN:def 2 it is one-to-one & rng it is Basis of V; end; reserve s for FinSequence, V1,V2,V3 for finite-dimensional VectSp of K, f,f1,f2 for Function of V1,V2, g for Function of V2,V3, b1 for OrdBasis of V1, b2 for OrdBasis of V2, b3 for OrdBasis of V3, v1,v2 for Vector of V2, v,w for Element of V1; reserve p2,F for FinSequence of V1, p1,d for FinSequence of K, KL for Linear_Combination of V1; definition let K be non empty doubleLoopStr; let V1,V2 be non empty ModuleStr over K; let f1,f2 be Function of V1, V2; func f1+f2 -> Function of V1,V2 means :: MATRLIN:def 3 for v be Element of V1 holds it .v = f1.v + f2.v; end; definition let K be non empty doubleLoopStr; let V1,V2 be non empty ModuleStr over K; let f be Function of V1,V2; let a be Element of K; func a*f -> Function of V1,V2 means :: MATRLIN:def 4 for v be Element of V1 holds it.v = a * (f.v); end; theorem :: MATRLIN:9 for a being Element of V1 for F being FinSequence of V1 for G being FinSequence of K st len F = len G & for k for v being Element of K st k in dom F & v = G.k holds F.k = v * a holds Sum(F) = Sum(G) * a; theorem :: MATRLIN:10 for a be Element of V1 for F being FinSequence of K for G being FinSequence of V1 st len F = len G & for k st k in dom F holds G.k = (F/.k) * a holds Sum(G) = Sum(F) * a; theorem :: MATRLIN:11 for V1 being add-associative right_zeroed right_complementable non empty addLoopStr for F being FinSequence of V1 st for k st k in dom F holds F/.k = 0.V1 holds Sum(F) = 0.V1; definition let K, V1, p1,p2; func lmlt(p1,p2) -> FinSequence of V1 equals :: MATRLIN:def 5 (the lmult of V1).:(p1,p2); end; theorem :: MATRLIN:12 dom p1 = dom p2 implies dom lmlt(p1,p2) = dom p1; definition let V1 be non empty addLoopStr, M be FinSequence of (the carrier of V1)*; func Sum M -> FinSequence of V1 means :: MATRLIN:def 6 len it = len M & for k st k in dom it holds it/.k = Sum (M/.k); end; theorem :: MATRLIN:13 for M be Matrix of the carrier of V1 st len M = 0 holds Sum Sum M = 0.V1; theorem :: MATRLIN:14 for M be Matrix of m+1,0,the carrier of V1 holds Sum Sum M = 0.V1; theorem :: MATRLIN:15 for x be Element of D holds <*<*x*>*> = <*<*x*>*>@; theorem :: MATRLIN:16 for V1,V2 being VectSp of K, f being Function of V1,V2, p being FinSequence of V1 st f is additive homogeneous holds f.Sum p = Sum(f*p); theorem :: MATRLIN:17 for a be FinSequence of K, p being FinSequence of V1 st len p = len a holds f is additive homogeneous implies f*lmlt(a,p) = lmlt(a,f*p); theorem :: MATRLIN:18 for a be FinSequence of K st len a = len b2 & g is additive homogeneous holds g.Sum(lmlt(a,b2)) = Sum(lmlt(a,g*b2)); theorem :: MATRLIN:19 for F, F1 being FinSequence of V1, KL being Linear_Combination of V1, p being Permutation of dom F st F1 = F * p holds KL (#) F1 = (KL (#) F) * p; theorem :: MATRLIN:20 F is one-to-one & Carrier KL c= rng F implies Sum(KL (#) F) = Sum KL; theorem :: MATRLIN:21 for A be set for p be FinSequence of V1 st rng p c= A holds f1 is additive homogeneous & f2 is additive homogeneous & (for v st v in A holds f1.v = f2.v) implies f1.Sum p = f2.Sum p; theorem :: MATRLIN:22 f1 is additive homogeneous & f2 is additive homogeneous implies for b1 being OrdBasis of V1 st len b1 > 0 holds f1*b1 = f2*b1 implies f1 = f2; registration let D be non empty set; cluster -> FinSequence-yielding for Matrix of D; end; definition let D be non empty set; let F,G be Matrix of D; redefine func F^^G -> Matrix of D; end; definition let D be non empty set; let n,m,k; let M1 be Matrix of n,k,D, M2 be Matrix of m,k,D; redefine func M1^M2 -> Matrix of n+m,k,D; end; theorem :: MATRLIN:23 for M1 be Matrix of n,k,D, M2 be Matrix of m,k,D st i in dom M1 holds Line(M1^M2,i) = Line(M1,i); theorem :: MATRLIN:24 for M1 be Matrix of n,k,D, M2 be Matrix of m,k,D st width M1 = width M2 holds width (M1^M2) = width M1; theorem :: MATRLIN:25 for M1 be Matrix of t,k,D, M2 be Matrix of m,k,D st n in dom M2 & i = len M1 + n holds Line(M1^M2,i) = Line(M2,n); theorem :: MATRLIN:26 for M1 be Matrix of n,k,D, M2 be Matrix of m,k,D st width M1 = width M2 for i st i in Seg width M1 holds Col(M1^M2,i) = Col(M1,i)^Col(M2,i); theorem :: MATRLIN:27 for M1 be Matrix of n,k,the carrier of V, M2 be Matrix of m,k, the carrier of V holds Sum(M1^M2) = (Sum M1)^(Sum M2); theorem :: MATRLIN:28 for M1 be Matrix of n,k,D, M2 be Matrix of m,k,D st width M1 = width M2 holds (M1^M2)@ = M1@ ^^ M2@; theorem :: MATRLIN:29 for M1,M2 be Matrix of the carrier of V1 holds Sum M1 + Sum M2 = Sum(M1 ^^ M2); theorem :: MATRLIN:30 for P1,P2 be FinSequence of V1 st len P1 = len P2 holds Sum(P1 + P2) = (Sum P1) + (Sum P2); theorem :: MATRLIN:31 for M1,M2 be Matrix of the carrier of V1 st len M1 = len M2 holds Sum Sum M1 + Sum Sum M2 = Sum Sum(M1 ^^ M2); theorem :: MATRLIN:32 for M be Matrix of the carrier of V1 holds Sum Sum M = Sum Sum (M@); theorem :: MATRLIN:33 for M being Matrix of n,m,the carrier of K st n > 0 & m > 0 for p,d being FinSequence of K st len p = n & len d = m & for j st j in dom d holds d/.j = Sum mlt(p,Col(M,j)) for b,c being FinSequence of V1 st len b = m & len c = n & for i st i in dom c holds c/.i = Sum lmlt(Line(M,i),b) holds Sum lmlt(p,c) = Sum lmlt(d,b); begin :: Decomposition of a Vector in Basis definition let K be Field; let V be finite-dimensional VectSp of K; let b1 be OrdBasis of V; let W be Element of V; func W|--b1 -> FinSequence of K means :: MATRLIN:def 7 len it = len b1 & ex KL be Linear_Combination of V st W = Sum(KL) & Carrier KL c= rng b1 & for k st 1<=k & k<=len it holds it/.k=KL.(b1/.k); end; theorem :: MATRLIN:34 v1|--b2 = v2|--b2 implies v1 = v2; theorem :: MATRLIN:35 v = Sum lmlt(v|--b1,b1); theorem :: MATRLIN:36 len d = len b1 implies d = Sum(lmlt(d,b1)) |-- b1; theorem :: MATRLIN:37 for a,d be FinSequence of K st len a = len b1 for j be Nat st j in dom b2 & len d = len b1 & for k st k in dom b1 holds d.k = (f.((b1/.k)) |-- b2)/.j holds len b1 > 0 implies (Sum(lmlt(a,f*b1)) |-- b2)/.j = Sum(mlt(a,d)); begin :: Matrices of Linear Transformations definition let K be Field; let V1,V2 be finite-dimensional VectSp of K; let f be Function of V1, V2; let b1 be FinSequence of V1; let b2 be OrdBasis of V2; func AutMt(f,b1,b2) -> Matrix of K means :: MATRLIN:def 8 len it = len b1 & for k st k in dom b1 holds it/.k = f.(b1/.k) |-- b2; end; theorem :: MATRLIN:38 len b1 = 0 implies AutMt(f,b1,b2) = {}; theorem :: MATRLIN:39 len b1 > 0 implies width AutMt(f,b1,b2) = len b2; theorem :: MATRLIN:40 f1 is additive homogeneous & f2 is additive homogeneous & AutMt(f1,b1,b2) = AutMt(f2,b1,b2) & len b1 > 0 implies f1 = f2; theorem :: MATRLIN:41 g is additive homogeneous & len b1 > 0 & len b2 > 0 implies AutMt(g*f,b1,b3) = AutMt(f,b1,b2) * AutMt(g,b2,b3); theorem :: MATRLIN:42 AutMt(f1+f2,b1,b2) = AutMt(f1,b1,b2) + AutMt(f2,b1,b2); theorem :: MATRLIN:43 a <> 0.K implies AutMt(a*f,b1,b2) = a * AutMt(f,b1,b2);