:: Some Properties of Line and Column Operations on Matrices :: by Xiquan Liang , Tao Sun and Dahai Hu :: :: Received August 13, 2007 :: Copyright (c) 2007-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, MATRIX_1, FINSEQ_1, TREES_1, INCSP_1, MATRIX11, RELAT_1, FUNCT_1, XXREAL_0, CARD_1, ARYTM_3, FINSEQ_2, STRUCT_0, ALGSTR_0, MESFUNC1, ZFMISC_1, GROUP_1, SUPINF_2, FVSUM_1, CARD_3, RVSUM_1, MATRIX_6, ARYTM_1, QC_LANG1, MATRIX12; notations MATRIX_0, XXREAL_0, MATRIX11, TARSKI, ORDINAL1, NUMBERS, FUNCT_1, FINSEQ_1, ZFMISC_1, BINOP_1, STRUCT_0, ALGSTR_0, GROUP_1, VECTSP_1, FVSUM_1, FINSEQ_2, MATRIX_1, MATRIX_3, MATRIX_6; constructors MATRIX_6, MATRIX11, CAT_2, ALGSTR_1, FVSUM_1, RELSET_1, MATRIX_1, MATRIX_3, XXREAL_0; registrations RELSET_1, STRUCT_0, FVSUM_1, VECTSP_1, ORDINAL1, XXREAL_0, NAT_1, FINSEQ_2, MATRIX_6, MATRIX_0; requirements NUMERALS, REAL, SUBSET; begin reserve j, k, l, n, m, t,i for Nat, K for Field, a for Element of K, M,M1,M2 for Matrix of n,m,K, pK,qK for FinSequence of K, A for Matrix of n,K; definition let n,m; let K; let M be Matrix of n,m,K; let l,k be Nat; func InterchangeLine(M,l,k) -> Matrix of n,m,K means :: MATRIX12:def 1 len it = len M & for i,j st i in dom M & j in Seg width M holds (i = l implies it*(i,j) = M*(k,j )) & (i = k implies it*(i,j) = M*(l,j)) & (i <> l & i <> k implies it*(i,j) = M *(i,j)); end; theorem :: MATRIX12:1 for M1,M2 being Matrix of n,m,K holds width M1 = width M2; theorem :: MATRIX12:2 for M,M1,i st l in dom M & k in dom M & i in dom M & M1 = InterchangeLine(M,l,k) holds (i = l implies Line(M1,i) = Line(M,k)) & (i = k implies Line(M1,i) = Line(M,l)) & (i <> l & i <> k implies Line(M1,i) = Line(M, i)); theorem :: MATRIX12:3 for a,i,j,M st i in dom M & j in Seg width M holds (a*Line(M,i)). j = a*(M*(i,j)); definition let n,m; let K; let M be Matrix of n,m,K; let l be Nat; let a be Element of K; func ScalarXLine(M,l,a) -> Matrix of n,m,K means :: MATRIX12:def 2 len it = len M & for i,j st i in dom M & j in Seg width M holds (i = l implies it*(i,j) = a*(M*(l,j) )) & (i <> l implies it*(i,j) = M*(i,j)); end; theorem :: MATRIX12:4 l in dom M & i in dom M & M1 = ScalarXLine(M,l,a) implies (i = l implies Line(M1,i) = a*Line(M,l)) & (i <> l implies Line(M1,i) = Line(M,i)); definition let n,m; let K; let M be Matrix of n,m,K; let l,k be Nat; let a be Element of K; assume k in dom M; func RlineXScalar(M,l,k,a) -> Matrix of n,m,K means :: MATRIX12:def 3 len it = len M & for i,j st i in dom M & j in Seg width M holds (i = l implies it*(i,j) = a*(M*( k,j))+(M*(l,j))) & (i <> l implies it*(i,j) = M*(i,j)); end; theorem :: MATRIX12:5 l in dom M & k in dom M & i in dom M & M1 = RlineXScalar(M,l,k,a) implies (i = l implies Line(M1,i) = a*Line(M,k) + Line(M,l)) & (i <> l implies Line(M1,i) = Line(M,i)); notation let n,m; let K; let M be Matrix of n,m,K; let l,k be Nat; synonym ILine(M,l,k) for InterchangeLine(M,l,k); end; notation let n,m; let K; let M be Matrix of n,m,K; let l be Nat; let a be Element of K; synonym SXLine(M,l,a) for ScalarXLine(M,l,a); end; notation let n,m; let K; let M be Matrix of n,m,K; let l,k be Nat; let a be Element of K; synonym RLineXS(M,l,k,a) for RlineXScalar(M,l,k,a); end; theorem :: MATRIX12:6 l in dom (1.(K,n)) & k in dom (1.(K,n)) implies ILine((1.(K,n)),l ,k) * A = ILine(A,l,k); theorem :: MATRIX12:7 for l,a,A st l in dom (1.(K,n)) holds SXLine((1.(K,n)),l,a) * A = SXLine(A,l,a); theorem :: MATRIX12:8 l in dom (1.(K,n)) & k in dom (1.(K,n)) implies RLineXS((1.(K,n)) ,l,k,a) * A = RLineXS(A,l,k,a); theorem :: MATRIX12:9 ILine(M,k,k) = M; theorem :: MATRIX12:10 ILine(M,l,k) = ILine(M,k,l); theorem :: MATRIX12:11 l in dom M & k in dom M implies ILine(ILine(M,l,k),l,k) = M; theorem :: MATRIX12:12 l in dom (1.(K,n)) & k in dom (1.(K,n)) implies ILine((1.(K,n)), l,k) is invertible & (ILine((1.(K,n)),l,k))~ = ILine((1.(K,n)),l,k); theorem :: MATRIX12:13 l in dom (1.(K,n)) & k in dom (1.(K,n)) & k<>l implies RLineXS(( 1.(K,n)),l,k,a) is invertible & (RLineXS((1.(K,n)),l,k,a))~ = RLineXS((1.(K,n)) ,l,k,-a); theorem :: MATRIX12:14 l in dom (1.(K,n)) & a <> 0.K implies SXLine((1.(K,n)),l,a) is invertible & (SXLine((1.(K,n)),l,a))~ = SXLine((1.(K,n)),l,a"); definition let n,m; let K; let M be Matrix of n,m,K; let l,k be Nat; assume that l in Seg width M and k in Seg width M and n>0 and m>0; func InterchangeCol(M,l,k) -> Matrix of n,m,K means :: MATRIX12:def 4 len it = len M & for i,j st i in dom M & j in Seg width M holds (j = l implies it*(i,j) = M*(i,k )) & (j = k implies it*(i,j) = M*(i,l)) & (j <> l & j <> k implies it*(i,j) = M *(i,j)); end; definition let n,m; let K; let M be Matrix of n,m,K; let l be Nat; let a be Element of K; assume that l in Seg width M and n>0 and m>0; func ScalarXCol(M,l,a) -> Matrix of n,m,K means :: MATRIX12:def 5 len it = len M & for i,j st i in dom M & j in Seg width M holds (j = l implies it*(i,j) = a*(M*(i,l) )) & (j <> l implies it*(i,j) = M*(i,j)); end; definition let n,m; let K; let M be Matrix of n,m,K; let l,k be Nat; let a be Element of K; assume that l in Seg width M and k in Seg width M and n>0 and m>0; func RcolXScalar(M,l,k,a) -> Matrix of n,m,K means :: MATRIX12:def 6 len it = len M & for i,j st i in dom M & j in Seg width M holds (j = l implies it*(i,j) = a*(M*( i,k))+(M*(i,l))) & (j <> l implies it*(i,j) = M*(i,j)); end; notation let n,m; let K; let M be Matrix of n,m,K; let l,k be Nat; synonym ICol(M,l,k) for InterchangeCol(M,l,k); end; notation let n,m; let K; let M be Matrix of n,m,K; let l be Nat; let a be Element of K; synonym SXCol(M,l,a) for ScalarXCol(M,l,a); end; notation let n,m; let K; let M be Matrix of n,m,K; let l,k be Nat; let a be Element of K; synonym RColXS(M,l,k,a) for RcolXScalar(M,l,k,a); end; theorem :: MATRIX12:15 l in Seg width M & k in Seg width M & n>0 & m>0 & M1 = M@ implies (ILine(M1,l,k))@ = ICol(M,l,k); theorem :: MATRIX12:16 l in Seg width M & n>0 & m>0 & M1 = M@ implies (SXLine(M1,l,a))@ = SXCol(M,l,a); theorem :: MATRIX12:17 l in Seg width M & k in Seg width M & n>0 & m>0 & M1 = M@ implies (RLineXS(M1,l,k,a))@ = RColXS(M,l,k,a); theorem :: MATRIX12:18 l in dom (1.(K,n)) & k in dom (1.(K,n)) & n>0 implies A * ICol((1.(K,n )),l,k) = ICol(A,l,k); theorem :: MATRIX12:19 l in dom (1.(K,n)) & n>0 implies A * SXCol((1.(K,n)),l,a) = SXCol(A,l, a); theorem :: MATRIX12:20 l in dom (1.(K,n)) & k in dom (1.(K,n)) & n>0 implies A * RColXS((1.(K ,n)),l,k,a) = RColXS(A,l,k,a); theorem :: MATRIX12:21 l in dom (1.(K,n)) & k in dom (1.(K,n)) & n>0 implies (ICol((1.(K,n)), l,k))~ = ICol((1.(K,n)),l,k); theorem :: MATRIX12:22 l in dom (1.(K,n)) & k in dom (1.(K,n)) & k<>l & n>0 implies (RColXS(( 1.(K,n)),l,k,a))~ = RColXS((1.(K,n)),l,k,-a); theorem :: MATRIX12:23 l in dom (1.(K,n)) & a <> 0.K & n>0 implies (SXCol((1.(K,n)),l,a))~ = SXCol((1.(K,n)),l,a");