:: Matrices. :: by Katarzyna Jankowska :: :: Received June 8, 1991 :: Copyright (c) 1991-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, FINSEQ_1, SUBSET_1, RELAT_1, CARD_1, FINSEQ_2, TARSKI, TREES_1, XXREAL_0, ZFMISC_1, FUNCT_1, QC_LANG1, INCSP_1, ARYTM_1, ARYTM_3, MATRIX_1, GOBRD13, CARD_3, FUNCT_6, FINSET_1, CARD_2, MATRIX_0, PARTFUN1, FUNCOP_1, FINSEQ_3; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, REAL_1, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0, COMPLEX1, NAT_1, VALUED_0, RELAT_1, CARD_1, CARD_2, FUNCT_1, INT_1, PARTFUN1, FUNCT_2, FUNCOP_1, FINSET_1, FINSEQ_1, FINSEQ_2, FINSEQ_3, FINSEQ_4, CARD_3, FUNCT_6, BINOP_1, FINSEQOP; constructors BINOP_1, XXREAL_0, FINSEQOP, RELSET_1, FINSEQ_3, INT_1, CARD_3, FUNCT_6, CARD_2, WELLORD2, NAT_1, PRE_POLY, FINSEQ_4, XCMPLX_0, DOMAIN_1, REAL_1; registrations XBOOLE_0, RELAT_1, FUNCT_1, XREAL_0, FINSEQ_1, FINSEQ_2, ORDINAL1, CARD_1, FINSET_1, PRE_POLY, XXREAL_0, NAT_1, INT_1; requirements NUMERALS, SUBSET, BOOLE, REAL, ARITHM; begin reserve x,y,z for object, i,j,n,m for Nat, D for non empty set, s,t for FinSequence, a,a1,a2,b1,b2,d for Element of D, p, p1,p2,q,r for FinSequence of D; definition let f be FinSequence; attr f is tabular means :: MATRIX_0:def 1 ex n being Nat st for x st x in rng f ex s being FinSequence st s=x & len s = n; end; registration cluster tabular for FinSequence; end; theorem :: MATRIX_0:1 <*<*d*>*> is tabular; theorem :: MATRIX_0:2 m |-> (n |-> x) is tabular; theorem :: MATRIX_0:3 <*s*> is tabular; theorem :: MATRIX_0:4 for s1,s2 be FinSequence st len s1 =n & len s2 = n holds <*s1,s2 *> is tabular; theorem :: MATRIX_0:5 {} is tabular; theorem :: MATRIX_0:6 <*{},{}*> is tabular; theorem :: MATRIX_0:7 <*<*a1*>,<*a2*>*> is tabular; theorem :: MATRIX_0:8 <*<*a1,a2*>,<*b1,b2*>*> is tabular; registration let D be set; cluster tabular for FinSequence of D*; end; definition let D be set; mode Matrix of D is tabular FinSequence of D*; end; registration let X be set; cluster -> Function-yielding for Matrix of X; end; registration let D be non empty set; cluster non empty-yielding for Matrix of D; end; theorem :: MATRIX_0:9 s is Matrix of D iff ex n st for x st x in rng s ex p st x = p & len p = n; definition let D; let m,n be Nat; let M be Matrix of D; attr M is (m,n)-size means :: MATRIX_0:def 2 len M = m & for p st p in rng M holds len p = n; end; registration let D; let m,n be Nat; cluster (m,n)-size for Matrix of D; end; definition let D; let m,n; mode Matrix of m,n,D is (m,n)-size Matrix of D; end; definition let D,n; mode Matrix of n,D is Matrix of n,n,D; end; theorem :: MATRIX_0:10 m |-> (n |-> a) is Matrix of m,n,D; theorem :: MATRIX_0:11 for p being FinSequence of D holds <*p*> is Matrix of 1,len p,D; theorem :: MATRIX_0:12 for p1,p2 st len p1 =n & len p2 = n holds <*p1,p2*> is Matrix of 2,n,D; theorem :: MATRIX_0:13 {} is Matrix of 0,m,D; theorem :: MATRIX_0:14 <*{}*> is Matrix of 1,0,D; theorem :: MATRIX_0:15 <*<*a*>*> is Matrix of 1,D; theorem :: MATRIX_0:16 <*{},{}*> is Matrix of 2,0,D; theorem :: MATRIX_0:17 <*<*a1,a2*>*> is Matrix of 1,2,D; theorem :: MATRIX_0:18 <*<*a1*>,<*a2*>*> is Matrix of 2,1,D; theorem :: MATRIX_0:19 <*<*a1,a2*>,<*b1,b2*>*> is Matrix of 2,D; reserve M,M1,M2 for Matrix of D; definition let M be tabular FinSequence; func width M -> Nat means :: MATRIX_0:def 3 ex s st s in rng M & len s = it if len M > 0 otherwise it = 0; end; theorem :: MATRIX_0:20 len M > 0 implies for n holds M is Matrix of len M, n, D iff n = width M; definition let M be tabular FinSequence; func Indices M -> set equals :: MATRIX_0:def 4 [:dom M,Seg width M:]; end; definition let D be set; let M be Matrix of D; let i,j; assume [i,j] in Indices M; func M*(i,j) -> Element of D means :: MATRIX_0:def 5 ex p being FinSequence of D st p = M.i & it = p.j; end; theorem :: MATRIX_0:21 len M1 = len M2 & width M1 = width M2 & (for i,j st [i,j] in Indices M1 holds M1*(i,j) = M2*(i,j)) implies M1 = M2; scheme :: MATRIX_0:sch 1 MatrixLambda { D() -> non empty set, n, m() -> Nat, f(set,set) -> Element of D()} : ex M being Matrix of n(),m(),D() st for i,j st [i,j] in Indices M holds M*(i,j) = f(i,j); scheme :: MATRIX_0:sch 2 MatrixEx { D() -> non empty set, n, m() -> Nat, P[object,object,object] }: ex M being Matrix of n(),m(),D() st for i,j st [i,j] in Indices M holds P[i,j ,M*(i,j)] provided for i,j st [i,j] in [:Seg n(), Seg m():] ex x being Element of D() st P[i,j,x]; theorem :: MATRIX_0:22 for M being Matrix of 0,m,D holds len M = 0 & width M = 0 & Indices M = {}; theorem :: MATRIX_0:23 n > 0 implies for M being Matrix of n,m,D holds len M = n & width M = m & Indices M = [:Seg n, Seg m:]; theorem :: MATRIX_0:24 for M being Matrix of n,D holds len M = n & width M = n & Indices M = [:Seg n, Seg n:]; theorem :: MATRIX_0:25 for M being Matrix of n,m,D holds len M = n & Indices M = [:Seg n,Seg width M:]; theorem :: MATRIX_0:26 for M1,M2 being Matrix of n,m,D holds Indices M1 = Indices M2; theorem :: MATRIX_0:27 for M1,M2 being Matrix of n,m,D st (for i,j st [i,j] in Indices M1 holds M1*(i,j) = M2*(i,j)) holds M1 = M2; theorem :: MATRIX_0:28 for M1 being Matrix of n,D holds for i,j st [i,j] in Indices M1 holds [j,i] in Indices M1; definition let D; let M be Matrix of D; func M@ -> Matrix of D means :: MATRIX_0:def 6 len it = width M & (for i,j holds [i,j] in Indices it iff [j,i] in Indices M) & for i,j st [j,i] in Indices M holds it* (i,j) = M*(j,i); end; theorem :: MATRIX_0:29 for M being Matrix of D st width M > 0 holds len (M@)=width M & width (M@)=len M; registration let n,D; let M be Matrix of n,D; cluster M@ -> (n,n)-size; end; definition let D,M,i; func Line(M,i) -> FinSequence of D means :: MATRIX_0:def 7 len it = width M & for j st j in Seg width M holds it.j = M*(i,j); func Col(M,i) -> FinSequence of D means :: MATRIX_0:def 8 len it = len M & for j st j in dom M holds it.j = M*(j,i); end; definition let D; let M be Matrix of D; let i; redefine func Line(M,i) -> Element of (width M)-tuples_on D; redefine func Col(M,i) -> Element of (len M)-tuples_on D; end; theorem :: MATRIX_0:30 for D being set for i,j for M being Matrix of D st 1 <= i & i <= len M & 1 <= j & j <= width M holds [i,j] in Indices M; theorem :: MATRIX_0:31 for M being Matrix of n,m,D st 1 <= i & i <= n & 1 <= j & j <= m holds [i,j] in Indices M; :: from GOBOARD5, 2008.03.08, A.T. theorem :: MATRIX_0:32 for M being tabular FinSequence, i,j st [i,j] in Indices M holds 1 <= i & i <= len M & 1 <= j & j <= width M; theorem :: MATRIX_0:33 for M being Matrix of n,m,D st [i,j] in Indices M holds 1 <= i & i <= n & 1 <= j & j <= m; :: from GOBRD13, 2011.07.26, A.T. definition let F be Function-yielding Function; func Values F -> set equals :: MATRIX_0:def 9 Union rngs F; end; theorem :: MATRIX_0:34 for M being FinSequence of D* holds M.i is FinSequence of D; theorem :: MATRIX_0:35 for M being FinSequence of D* holds Values M = union {rng f where f is Element of D*: f in rng M}; registration let D be non empty set, M be FinSequence of D*; cluster Values M -> finite; end; reserve f for FinSequence of D; theorem :: MATRIX_0:36 for M being Matrix of D st i in dom M & M.i = f holds len f = width M; theorem :: MATRIX_0:37 for M being Matrix of D st i in dom M & M.i = f & j in dom f holds [i,j] in Indices M; theorem :: MATRIX_0:38 for M being Matrix of D st [i,j] in Indices M & M.i = f holds len f = width M & j in dom f; theorem :: MATRIX_0:39 for M being Matrix of D holds Values M = { M*(i,j) where i is Nat, j is Nat: [i,j] in Indices M }; theorem :: MATRIX_0:40 for D being non empty set, M being Matrix of D holds card Values M <= (len M)*(width M); reserve i,j,i1,j1 for Nat; theorem :: MATRIX_0:41 for M being Matrix of D st 1 <= i & i <= len M & 1 <= j & j <= width M holds M*(i,j) in Values M; :: from GOBOARD1, 2012.02.25, A.T. theorem :: MATRIX_0:42 for D being non empty set,M being Matrix of D holds for i,j st j in dom M & i in Seg width M holds Col(M,i).j = Line(M,j).i; definition let D be non empty set; let M be Matrix of D; redefine attr M is empty-yielding means :: MATRIX_0:def 10 0 = len M or 0 = width M; end; reserve k for Nat, G for Matrix of D; theorem :: MATRIX_0:43 rng f misses rng Col(G,i) & f/.n = G*(m,k) & n in dom f & m in dom G implies i<>k; theorem :: MATRIX_0:44 for D being non empty set, M being Matrix of D holds M is non empty-yielding iff 0 < len M & 0 < width M; theorem :: MATRIX_0:45 for M1 being Matrix of 0, n, D, M2 being Matrix of 0, m, D holds M1 = M2; begin :: Some Examples of Matrices, from MATRIX_2, 2012.02.26, A.T. reserve x,y,x1,x2,y1,y2 for object, i,j,k,l,n,m for Nat, D for non empty set, s,s2 for FinSequence, a,b,c,d for Element of D, q,r for FinSequence of D, a9,b9 for Element of D; definition let n,m; let a be object; func (n,m) --> a -> tabular FinSequence equals :: MATRIX_0:def 11 n |-> (m |-> a); end; definition let D,n,m; let d; redefine func (n,m) --> d -> Matrix of n,m,D; end; theorem :: MATRIX_0:46 [i,j] in Indices ((n,m)-->a) implies ((n,m)-->a) * (i,j)=a; definition let a,b,c,d be object; func (a,b)][(c,d) ->tabular FinSequence equals :: MATRIX_0:def 12 <*<*a,b*>,<*c,d*>*>; end; theorem :: MATRIX_0:47 len (x1,x2)][(y1,y2)=2 & width (x1,x2)][(y1,y2)=2 & Indices (x1, x2)][(y1,y2)=[:Seg 2,Seg 2:]; theorem :: MATRIX_0:48 [1,1] in Indices (x1,x2)][(y1,y2) & [1,2] in Indices (x1,x2)][(y1 ,y2) & [2,1] in Indices (x1,x2)][(y1,y2) & [2,2] in Indices (x1,x2)][(y1,y2); definition let D; let a be Element of D; redefine func <*a*> -> Element of 1-tuples_on D; end; definition let D; let n; let p be Element of n-tuples_on D; redefine func <*p*> -> Matrix of 1,n,D; end; theorem :: MATRIX_0:49 [1,1] in Indices <*<*a*>*> & <*<*a*>*>*(1,1)=a; definition let D; let a,b,c,d be Element of D; redefine func (a,b)][(c,d) -> Matrix of 2,D; end; theorem :: MATRIX_0:50 (a,b)][(c,d)*(1,1)=a & (a,b)][(c,d)*(1,2)=b & (a,b)][(c,d)*(2,1)=c & ( a,b)][(c,d)*(2,2)=d; theorem :: MATRIX_0:51 for M being Matrix of D st len M=n holds M is Matrix of n,width M,D; begin :: Deleting of Rows and Columns in a Matrix theorem :: MATRIX_0:52 for M be Matrix of n,m,D holds for k st k in Seg n holds M.k= Line(M,k); definition let i, D; let M be Matrix of D; func DelCol(M,i) -> Matrix of D means :: MATRIX_0:def 13 len it=len M & for k st k in dom M holds it.k=Del(Line(M,k),i); end; theorem :: MATRIX_0:53 for M1,M2 being Matrix of D st M1@=M2@ & len M1=len M2 holds M1 = M2; theorem :: MATRIX_0:54 for M being Matrix of D st width M > 0 holds len (M@)=width M & width (M@)=len M; theorem :: MATRIX_0:55 for M1,M2 being Matrix of D st width M1>0 & width M2>0 & M1@=M2@ holds M1=M2; theorem :: MATRIX_0:56 for M1,M2 being Matrix of D st width M1>0 & width M2>0 holds M1=M2 iff M1@=M2@ & width M1 = width M2; theorem :: MATRIX_0:57 for M being Matrix of D st len M>0 & width M>0 holds (M@)@=M; theorem :: MATRIX_0:58 for M being Matrix of D holds for i st i in dom M holds Line(M,i )=Col(M@,i); theorem :: MATRIX_0:59 for M being Matrix of D holds for j st j in Seg width M holds Line(M@, j)=Col(M,j); theorem :: MATRIX_0:60 for M being Matrix of D holds for i st i in dom M holds M.i=Line(M,i); notation let D, i; let M be Matrix of D; synonym DelLine(M,i) for Del(M,i); end; registration let D, i; let M be Matrix of D; cluster DelLine(M,i) -> tabular; end; definition let D, i; let M be Matrix of D; redefine func DelLine(M,i) -> Matrix of D; end; definition let i,j,n,D; let M be Matrix of n,D; func Deleting(M,i,j) -> Matrix of D equals :: MATRIX_0:def 14 DelCol(DelLine(M,i),j); end; theorem :: MATRIX_0:61 not i in Seg width M implies DelCol(M,i) = M; :: from GOBOARD1, 2012.03.01, A.T. theorem :: MATRIX_0:62 k in dom G implies Line(DelCol(G,i),k) = Del(Line(G,k),i); theorem :: MATRIX_0:63 i in Seg width G & width G = m+1 implies width DelCol(G,i) = m; theorem :: MATRIX_0:64 i in Seg width G & width G > 0 implies width G = width DelCol(G,i) + 1; theorem :: MATRIX_0:65 width G > 1 & i in Seg width G implies DelCol(G,i) is not empty-yielding; theorem :: MATRIX_0:66 i in Seg width G & width G > 1 & n in dom G & m in Seg width DelCol(G,i) implies DelCol(G,i)*(n,m)=Del(Line(G,n),i).m; reserve m for Nat; theorem :: MATRIX_0:67 i in Seg width G & width G = m+1 & m>0 & 1<=k & k0 & i<=k & k<=m implies Col (DelCol(G,i),k) = Col(G,k+1) & k in Seg width DelCol(G,i) & k+1 in Seg width G; theorem :: MATRIX_0:69 i in Seg width G & width G = m+1 & m>0 & n in dom G & 1<=k & k0 & n in dom G & i<=k & k<= m implies DelCol(G,i)*(n,k) = G*(n,k+1) & k+1 in Seg width G; theorem :: MATRIX_0:71 width G = m+1 & m>0 & k in Seg m implies Col(DelCol(G,1),k) = Col(G,k+ 1) & k in Seg width DelCol(G,1) & k+1 in Seg width G; theorem :: MATRIX_0:72 width G = m+1 & m>0 & k in Seg m & n in dom G implies DelCol(G,1)*(n,k ) = G*(n,k+1) & 1 in Seg width G; theorem :: MATRIX_0:73 width G = m+1 & m>0 & k in Seg m implies Col(DelCol(G,width G),k) = Col(G,k) & k in Seg width DelCol(G,width G); theorem :: MATRIX_0:74 width G = m+1 & m>0 & k in Seg m & n in dom G implies k in Seg width G & DelCol(G,width G)*(n,k) = G*(n,k) & width G in Seg width G; reserve f for FinSequence of D, G for Matrix of D; theorem :: MATRIX_0:75 rng f misses rng Col(G,i) & f/.n in rng Line(G,m) & n in dom f & i in Seg width G & m in dom G & width G>1 implies f/.n in rng Line(DelCol(G,i),m);