:: Linear Map of Matrices :: by Karol P\c{a}k :: :: Received May 13, 2008 :: Copyright (c) 2008-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, VECTSP_1, SUBSET_1, RLSUB_1, XBOOLE_0, ARYTM_3, STRUCT_0, TARSKI, RLVECT_3, RLVECT_2, CARD_3, SUPINF_2, FINSET_1, FUNCT_1, RLSUB_2, FUNCT_2, RLVECT_5, MATRLIN, RELAT_1, CARD_1, XXREAL_0, FINSEQ_1, ZFMISC_1, ALGSTR_0, PARTFUN1, ORDINAL4, FINSEQ_2, INCSP_1, MESFUNC1, TREES_1, MATRIX_1, GROUP_1, ARYTM_1, FINSEQ_4, RFINSEQ, RANKNULL, MATRIXJ1, MATRIX_3, MATRIX_6, FVSUM_1, RVSUM_1, MATRIXR1, VECTSP10, MATRIX15, QC_LANG1, CLASSES1, PRVECT_1, MATRIX13, LMOD_7, VALUED_1, RLVECT_1, BINOP_1, LATTICES, MATRLIN2, UNIALG_1, MSSUBFAM; 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, FVSUM_1, MATRIX_3, MATRIX_6, DOMAIN_1, VECTSP_4, VECTSP_6, VECTSP_7, VECTSP_9, FINSEQOP, PRVECT_1, MATRIX13, MATRLIN, MATRIX15, RFINSEQ, WSIERP_1, MOD_2, VECTSP_5, RANKNULL, MATRIXJ1; constructors FVSUM_1, VECTSP_9, MATRIX_6, LAPLACE, MATRIX15, VECTSP_2, RANKNULL, VECTSP10, MATRIXJ1, REALSET1, RELSET_1, MATRIX13, MATRIX_1; registrations XBOOLE_0, FUNCT_1, FINSET_1, STRUCT_0, VECTSP_1, FUNCT_2, ORDINAL1, XXREAL_0, NAT_1, FINSEQ_1, RELAT_1, FINSEQ_2, MATRLIN, VECTSP_2, MATRIX13, XREAL_0, VECTSP_9, CARD_1, MOD_2, PRVECT_1, GRCAT_1, MATRIX_6; requirements ARITHM, NUMERALS, REAL, BOOLE, SUBSET; begin :: Preliminaries reserve i, j, m, n, k for Nat, x, y for set, K for Field, a,a1 for Element of K; theorem :: MATRLIN2:1 for V be VectSp of K for W1,W2,W12 be Subspace of V for U1,U2 be Subspace of W12 st U1 = W1 & U2 = W2 holds W1 /\ W2 = U1 /\ U2 & W1 + W2 = U1 + U2; theorem :: MATRLIN2:2 for V be VectSp of K for W1,W2 be Subspace of V st W1/\W2=(0).V for B1 be linearly-independent Subset of W1, B2 be linearly-independent Subset of W2 holds B1\/B2 is linearly-independent Subset of W1+W2; theorem :: MATRLIN2:3 for V be VectSp of K for W1,W2 be Subspace of V st W1/\W2 = (0).V for B1 be Basis of W1,B2 be Basis of W2 holds B1\/B2 is Basis of W1+W2; theorem :: MATRLIN2:4 for V be finite-dimensional VectSp of K, B be OrdBasis of (Omega).V holds B is OrdBasis of V; theorem :: MATRLIN2:5 for V1 be VectSp of K for A be finite Subset of V1 st dim Lin(A) = card A holds A is linearly-independent; theorem :: MATRLIN2:6 for V be VectSp of K for A be finite Subset of V holds dim Lin A <= card A; begin :: More on the Product of Finite Sequence of Scalars and Vectors reserve V1,V2,V3 for finite-dimensional VectSp of K, f for Function of V1,V2, b1,b19 for OrdBasis of V1, B1 for FinSequence of V1, b2 for OrdBasis of V2, B2 for FinSequence of V2, B3 for FinSequence of V3, v1,w1 for Element of V1, R,R1,R2 for FinSequence of V1, p,p1,p2 for FinSequence of K; theorem :: MATRLIN2:7 lmlt(p1 + p2,R) = lmlt(p1,R) + lmlt(p2,R); theorem :: MATRLIN2:8 lmlt(p,R1 + R2) = lmlt(p,R1) + lmlt(p,R2); theorem :: MATRLIN2:9 len p1 = len R1 & len p2 = len R2 implies lmlt(p1^p2,R1^R2) = lmlt(p1,R1)^lmlt(p2,R2); theorem :: MATRLIN2:10 len R1 = len R2 implies Sum (R1+R2)=Sum R1 + Sum R2; theorem :: MATRLIN2:11 Sum lmlt(len R|->a,R) = a * Sum R; theorem :: MATRLIN2:12 Sum lmlt(p,len p|->v1) = (Sum p) * v1; theorem :: MATRLIN2:13 Sum lmlt(a*p,R) = a * Sum lmlt(p,R); theorem :: MATRLIN2:14 for B1 be FinSequence of V1,W1 be Subspace of V1, B2 be FinSequence of W1 st B1 = B2 holds lmlt(p,B1) = lmlt(p,B2); theorem :: MATRLIN2:15 for B1 be FinSequence of V1,W1 be Subspace of V1, B2 be FinSequence of W1 st B1 = B2 holds Sum B1 = Sum B2; theorem :: MATRLIN2:16 i in dom R implies Sum lmlt(Line(1.(K,len R),i),R) = R/.i; begin :: More on the Decomposition of a Vector in a Basis theorem :: MATRLIN2:17 v1 + w1 |-- b1 = (v1 |-- b1) + (w1 |-- b1); theorem :: MATRLIN2:18 a * v1 |-- b1 = a * (v1 |-- b1); theorem :: MATRLIN2:19 i in dom b1 implies b1/.i|-- b1 = Line(1.(K,len b1),i); theorem :: MATRLIN2:20 0.V1|-- b1 = len b1 |-> 0.K; theorem :: MATRLIN2:21 len b1 = dim V1; theorem :: MATRLIN2:22 rng(b1|m) is linearly-independent Subset of V1 & for A be Subset of V1 st A = rng(b1|m) holds b1|m is OrdBasis of Lin A; theorem :: MATRLIN2:23 rng(b1/^m) is linearly-independent Subset of V1 & for A be Subset of V1 st A = rng(b1/^m) holds b1/^m is OrdBasis of Lin A; theorem :: MATRLIN2:24 for W1,W2 be Subspace of V1 st W1/\W2=(0).V1 for b1 be OrdBasis of W1,b2 be OrdBasis of W2,b be OrdBasis of W1+W2 st b=b1^b2 for v,v1,v2 be Vector of W1+W2, w1 be Vector of W1,w2 be Vector of W2 st v = v1+v2 & v1=w1 & v2=w2 holds v|-- b = (w1|--b1)^(w2|-- b2); theorem :: MATRLIN2:25 for W1 be Subspace of V1 st W1 = (Omega).V1 for w be Vector of W1, v be Vector of V1,w1 be OrdBasis of W1 st v = w & b1 = w1 holds v|--b1 = w |-- w1; theorem :: MATRLIN2:26 for W1,W2 be Subspace of V1 st W1/\W2=(0).V1 for w1 be OrdBasis of W1,w2 be OrdBasis of W2 holds w1^w2 is OrdBasis of W1+W2; begin :: Properties of Matrices of Linear Transformations definition let K,V1,V2,f,B1,b2; redefine func AutMt(f,B1,b2) -> Matrix of len B1,len b2,K; end; definition let S be 1-sorted; let R be Relation; func R|S -> set equals :: MATRLIN2:def 1 R | (the carrier of S); end; theorem :: MATRLIN2:27 for f be linear-transformation of V1,V2 for W1,W2 be Subspace of V1,U1 ,U2 be Subspace of V2 st ( dim W1 =0 implies dim U1 = 0 )& ( dim W2 =0 implies dim U2 = 0 )& V2 is_the_direct_sum_of U1,U2 for fW1 be linear-transformation of W1,U1, fW2 be linear-transformation of W2,U2 st fW1 = f | W1 & fW2 = f | W2 for w1 be OrdBasis of W1, w2 be OrdBasis of W2, u1 be OrdBasis of U1, u2 be OrdBasis of U2 st w1^w2 = b1 & u1^u2 = b2 holds AutMt(f,b1,b2) = block_diagonal (<*AutMt(fW1,w1,u1),AutMt(fW2,w2,u2)*>,0.K); definition let K,V1,V2; let f be Function of V1,V2; let B1 be FinSequence of V1; let b2 be OrdBasis of V2; assume len B1 = len b2; func AutEqMt(f,B1,b2) -> Matrix of len B1,len B1,K equals :: MATRLIN2:def 2 AutMt(f,B1, b2); end; theorem :: MATRLIN2:28 AutMt(id V1,b1,b1) = 1.(K,len b1); theorem :: MATRLIN2:29 AutEqMt(id V1,b1,b19) is invertible & AutEqMt(id V1,b19,b1) = AutEqMt( id V1,b1,b19)~; theorem :: MATRLIN2:30 len p1 = len p2 & len p1 = len B1 & len p1 > 0 & j in dom b1 & ( for i st i in dom p2 holds p2.i = (B1/.i|--b1).j) implies p1 "*" p2 = (Sum lmlt (p1,B1) |-- b1).j; theorem :: MATRLIN2:31 len b1>0 & f is additive homogeneous implies LineVec2Mx(v1|-- b1)*AutMt(f,b1, b2) = LineVec2Mx (f.v1 |-- b2); begin :: Linear Transformations of Matrices definition let K,V1,V2,b1,B2; let M be Matrix of len b1,len B2,K; func Mx2Tran(M,b1,B2) -> Function of V1, V2 means :: MATRLIN2:def 3 for v be Vector of V1 holds it.v = Sum lmlt (Line(LineVec2Mx(v|--b1) * M,1),B2); end; theorem :: MATRLIN2:32 for M be Matrix of len b1,len b2,K st len b1 > 0 holds LineVec2Mx(Mx2Tran(M,b1,b2).v1|--b2) = LineVec2Mx(v1|--b1) * M; theorem :: MATRLIN2:33 for M be Matrix of len b1,len B2,K st len b1 = 0 holds Mx2Tran(M ,b1,B2).v1 = 0.V2; registration let K,V1,V2,b1,B2; let M be Matrix of len b1,len B2,K; cluster Mx2Tran(M,b1,B2) -> homogeneous additive; end; theorem :: MATRLIN2:34 f is additive homogeneous implies Mx2Tran(AutMt(f,b1,b2),b1,b2) = f; theorem :: MATRLIN2:35 for A,B be Matrix of K st i in dom A & width A = len B holds LineVec2Mx(Line(A,i)) * B = LineVec2Mx(Line(A*B,i)); theorem :: MATRLIN2:36 for M be Matrix of len b1,len b2,K holds AutMt(Mx2Tran(M,b1,b2), b1,b2) = M; definition let n,m,K; let A be Matrix of n,m,K; let B be Matrix of K; redefine func A+B -> Matrix of n,m,K; end; theorem :: MATRLIN2:37 for A,B be Matrix of len b1,len B2,K holds Mx2Tran(A+B,b1,B2) = Mx2Tran(A,b1,B2) + Mx2Tran(B,b1,B2); theorem :: MATRLIN2:38 for A be Matrix of len b1,len B2,K holds a * Mx2Tran(A,b1,B2) = Mx2Tran(a * A,b1,B2); theorem :: MATRLIN2:39 for A,B be Matrix of len b1,len b2,K st Mx2Tran(A,b1,b2)=Mx2Tran(B,b1, b2) holds A = B; theorem :: MATRLIN2:40 for A be Matrix of len b1,len b2,K for B be Matrix of len b2,len B3,K st width A = len B for AB be Matrix of len b1,len B3,K st AB = A*B holds Mx2Tran(AB,b1,B3) = Mx2Tran(B,b2,B3) * Mx2Tran(A,b1,b2); theorem :: MATRLIN2:41 for A be Matrix of len b1,len b2,K st len b1>0 & len b2>0 holds v1 in ker Mx2Tran(A,b1,b2) iff v1|--b1 in Space_of_Solutions_of (A@); theorem :: MATRLIN2:42 V1 is trivial iff dim V1 = 0; theorem :: MATRLIN2:43 for V1,V2 be VectSp of K for f be linear-transformation of V1,V2 holds f is one-to-one iff ker f = (0).V1; registration let K; let V1,V2 be VectSp of K; let f,g be linear-transformation of V1,V2; cluster f+g -> homogeneous additive; end; registration let K; let V1,V2 be VectSp of K; let f be linear-transformation of V1,V2,a; cluster a*f -> homogeneous additive; end; definition let K; let V1,V2,V3 be VectSp of K; let f1 be linear-transformation of V1, V2; let f2 be linear-transformation of V2, V3; redefine func f2*f1 -> linear-transformation of V1,V3; end; theorem :: MATRLIN2:44 for A be Matrix of len b1,len b2,K st the_rank_of A = len b1 holds Mx2Tran(A,b1,b2) is one-to-one; theorem :: MATRLIN2:45 MX2FinS 1.(K,n) is OrdBasis of n-VectSp_over K; theorem :: MATRLIN2:46 for M be OrdBasis of (len b2)-VectSp_over K st M = MX2FinS 1.(K, len b2) for v1 be Vector of (len b2)-VectSp_over K holds v1|--M = v1; theorem :: MATRLIN2:47 for M be OrdBasis of (len b2)-VectSp_over K st M = MX2FinS 1.(K, len b2) for A be Matrix of len b1,len M,K st A = AutMt(f,b1,b2) & f is additive homogeneous holds Mx2Tran(A,b1,M).v1 = f.v1 |-- b2; definition let K be add-associative right_zeroed right_complementable Abelian associative well-unital distributive non empty doubleLoopStr, V1,V2 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; let f be Function of V1,V2; redefine func f|W -> Function of W,V2; end; definition let K be Field; let V1,V2 be VectSp of K; let W be Subspace of V1; let f be linear-transformation of V1, V2; redefine func f|W -> linear-transformation of W,V2; end; begin :: The Main Theorem theorem :: MATRLIN2:48 for f be linear-transformation of V1,V2 holds rank f = the_rank_of AutMt(f,b1,b2); theorem :: MATRLIN2:49 for M be Matrix of len b1,len b2,K holds rank Mx2Tran(M,b1,b2) = the_rank_of M; theorem :: MATRLIN2:50 for f be linear-transformation of V1,V2 st dim V1=dim V2 holds ker f is non trivial iff Det AutEqMt(f,b1,b2) = 0.K; theorem :: MATRLIN2:51 for f be linear-transformation of V1,V2, g be linear-transformation of V2,V3 st g|im f is one-to-one holds rank (g*f) = rank f & nullity (g*f) = nullity f;