:: The Product of Matrices of Elements of a Field and Determinants :: by Katarzyna Zawadzka :: :: Received May 17, 1993 :: Copyright (c) 1993-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, VECTSP_1, SUPINF_2, MATRIX_1, FINSEQ_2, ARYTM_1, FINSEQ_1, TREES_1, RELAT_1, ZFMISC_1, XXREAL_0, CARD_1, ARYTM_3, SUBSET_1, FUNCT_1, INCSP_1, FVSUM_1, RVSUM_1, ALGSTR_0, MESFUNC1, RLVECT_1, CARD_3, ORDINAL4, TARSKI, STRUCT_0, QC_LANG1, FINSUB_1, BINOP_1, SETWISEO, FUNCOP_1, PARTFUN1, FINSEQOP, FUNCT_5, FINSOP_1, ABIAN, MATRIX_3, FUNCSDOM, FUNCT_7, FINSET_1; notations TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, FINSEQ_1, FINSET_1, BINOP_1, FINSEQ_4, STRUCT_0, ALGSTR_0, FUNCT_3, FUNCOP_1, MATRIX_0, RLVECT_1, GROUP_1, VECTSP_1, SETWISEO, FINSOP_1, SETWOP_2, FINSEQ_2, FINSEQOP, MATRIX_1, FINSUB_1, NAT_1, FVSUM_1, TREES_1, FUNCT_5; constructors RELAT_2, PARTFUN1, SETWISEO, SQUARE_1, NAT_1, FINSEQOP, FINSOP_1, SETWOP_2, FUNCT_5, ALGSTR_1, FVSUM_1, RELSET_1, FINSEQ_4, FUNCT_3, BINOP_1, XTUPLE_0, MATRIX_0, MATRIX_1; registrations XBOOLE_0, SUBSET_1, FUNCT_1, ORDINAL1, RELSET_1, PARTFUN1, FUNCT_2, FINSET_1, FINSUB_1, XXREAL_0, XREAL_0, NAT_1, STRUCT_0, VECTSP_1, MATRIX_1, FVSUM_1, RELAT_1, CARD_1, FINSEQ_1, FINSEQ_2; requirements NUMERALS, REAL, BOOLE, SUBSET; begin reserve x,y,z,x1,x2,y1,y2,z1,z2 for object, i,j,k,l,n,m for Nat, D for non empty set, K for Ring; definition let K be Ring; let n,m be Nat; func 0.(K,n,m) -> Matrix of n,m,K equals :: MATRIX_3:def 1 n |-> (m |-> 0.K); end; definition let K be Ring; let A be Matrix of K; func -A -> Matrix of K means :: MATRIX_3:def 2 len it= len A & width it =width A & for i,j holds [i,j] in Indices A implies it*(i,j)= -(A*(i,j)); end; definition let K be Ring; let A,B be Matrix of K; func A+B -> Matrix of K means :: MATRIX_3:def 3 len it =len A & width it=width A & for i,j holds [i,j] in Indices A implies it*(i,j) = A*(i,j) + B*(i,j); end; theorem :: MATRIX_3:1 for i,j st [i,j] in Indices (0.(K,n,m)) holds (0.(K,n,m))*(i,j)= 0.K; theorem :: MATRIX_3:2 for A,B being Matrix of K st len A= len B & width A=width B holds A + B = B + A; theorem :: MATRIX_3:3 for A,B,C being Matrix of K st len A=len B & width A=width B holds (A + B) + C= A + (B + C); theorem :: MATRIX_3:4 for A being Matrix of n,m,K holds A + 0.(K,n,m)= A; theorem :: MATRIX_3:5 for A being Matrix of n,m,K holds A + (-A) = 0.(K,n,m); definition let K be Ring; let A,B be Matrix of K; assume width A=len B; func A*B -> Matrix of K means :: MATRIX_3:def 4 len it=len A & width it=width B & for i,j st [i,j] in Indices it holds it*(i,j)=Line(A,i) "*" Col(B,j); end; definition let n,k,m; let K be Ring; let A be Matrix of n,k,K; let B be Matrix of width A,m,K; redefine func A*B -> Matrix of len A,width B,K; end; definition let K be Ring; let M be Matrix of K; let a be Element of K; func a*M -> Matrix of K means :: MATRIX_3:def 5 len it=len M & width it =width M & for i,j st [i,j] in Indices M holds it*(i,j)=a*(M*(i,j)); end; definition let K be Ring; let M be Matrix of K; let a be Element of K; func M*a -> Matrix of K equals :: MATRIX_3:def 6 a*M; end; theorem :: MATRIX_3:6 for p,q being FinSequence of K st len p=len q holds len mlt(p,q)=len p & len mlt(p,q)=len q; theorem :: MATRIX_3:7 for i,l st [i,l] in Indices (1.(K,n)) & l=i holds (Line(1.(K,n),i)).l= 1.K; theorem :: MATRIX_3:8 for i,l st [i,l] in Indices (1.(K,n)) & l<>i holds (Line(1.(K,n),i)).l =0.K; theorem :: MATRIX_3:9 for l,j st [l,j] in Indices (1.(K,n)) & l=j holds (Col(1.(K,n),j)).l= 1.K; theorem :: MATRIX_3:10 for l,j st [l,j] in Indices (1.(K,n)) & l<>j holds (Col(1.(K,n),j)).l= 0.K; theorem :: MATRIX_3:11 for n being Element of NAT for K being add-associative right_zeroed right_complementable non empty addLoopStr holds Sum (n |-> 0.K) = 0.K; theorem :: MATRIX_3:12 for K being add-associative right_zeroed right_complementable non empty addLoopStr for p being FinSequence of K for i st i in dom p & for k st k in dom p & k<>i holds p.k=0.K holds Sum p=p.i; theorem :: MATRIX_3:13 for p,q being FinSequence of K holds len (mlt(p,q))=min(len p, len q); theorem :: MATRIX_3:14 for K being Ring for p,q being FinSequence of K for i st p.i=1.K & for k st k in dom p & k<>i holds p.k=0.K for j st j in dom (mlt(p,q)) holds (i=j implies mlt( p,q).j=(q.i)) & (i<>j implies mlt(p,q).j=0.K); theorem :: MATRIX_3:15 for i,j st [i,j] in Indices (1.(K,n)) holds (i=j implies (Line(( 1.(K,n)),i)).j=1.K) & (i<>j implies (Line((1.(K,n)),i)).j=0.K); theorem :: MATRIX_3:16 for i,j st [i,j] in Indices (1.(K,n)) holds (i=j implies (Col(( 1.(K,n)),j)).i=1.K) & (i<>j implies (Col((1.(K,n)),j)).i=0.K); theorem :: MATRIX_3:17 for K being Ring for p,q being FinSequence of K for i st i in dom p & i in dom q & p.i=1.K & for k st k in dom p & k<>i holds p.k=0.K holds Sum(mlt(p,q))=q.i; theorem :: MATRIX_3:18 for K being Ring for A being Matrix of n,K holds 1.(K,n)*A=A; theorem :: MATRIX_3:19 for K being commutative Ring for A being Matrix of n,K holds A*(1.(K,n))=A; theorem :: MATRIX_3:20 for K being Field for a,b being Element of K holds <*<*a*>*> * <*<*b*>*> =<*<*a*b*>*>; theorem :: MATRIX_3:21 for K being Field for a1,a2,b1,b2,c1,c2,d1,d2 being Element of K holds (a1,b1)][(c1,d1)* (a2,b2)][(c2,d2) = (a1*a2+b1*c2,a1*b2+b1*d2)][(c1*a2+d1*c2,c1*b2+ d1*d2); theorem :: MATRIX_3:22 for K being Field for A,B being Matrix of K st width A=len B & width B<>0 holds (A*B) @= (B @)*(A @); begin :: The product of Matrices definition let I,J be non empty set; let X be Element of Fin I; let Y be Element of Fin J; redefine func [:X,Y:]-> Element of Fin [:I,J:]; end; definition let I,J,D be non empty set; let G be BinOp of D; let f be Function of I,D; let g be Function of J,D; redefine func G*(f,g)-> Function of [:I,J:],D; end; theorem :: MATRIX_3:23 for I, J,D be non empty set for F,G be BinOp of D for f be Function of I,D for g being Function of J,D for X being Element of Fin I for Y being Element of Fin J st F is commutative & F is associative & ( [:Y,X:]<>{} or F is having_a_unity )& G is commutative holds F $$ ([:X,Y:],G*(f,g))=F$$([:Y ,X:],G*(g,f)); theorem :: MATRIX_3:24 for I, J be non empty set for F,G be BinOp of D for f be Function of I,D for g being Function of J,D st F is commutative & F is associative holds for x being Element of I for y being Element of J holds F $$( [:{.x.},{.y.}:],G*(f,g))=F$$({.x.},G[:](f,F$$({.y.},g))); theorem :: MATRIX_3:25 for I, J be non empty set for F,G be BinOp of D for f be Function of I,D for g being Function of J,D for X being Element of Fin I for Y being Element of Fin J st F is commutative & F is associative & F is having_a_unity & F is having_an_inverseOp & G is_distributive_wrt F holds for x being Element of I holds F $$([:{.x.},Y:],G*(f,g))=F$$({.x.},G[:](f,F$$(Y,g))); theorem :: MATRIX_3:26 for I, J being non empty set for F,G being BinOp of D for f being Function of I,D for g being Function of J,D for X being Element of Fin I for Y being Element of Fin J st F is having_a_unity & F is commutative & F is associative & F is having_an_inverseOp & G is_distributive_wrt F holds F$$([:X, Y:],G*(f,g))=F$$(X,G[:](f,F$$(Y,g))); theorem :: MATRIX_3:27 for I, J be non empty set for F,G be BinOp of D for f be Function of I ,D for g being Function of J,D st F is commutative associative & G is commutative holds for x being Element of I for y being Element of J holds F $$( [:{.x.},{.y.}:],G*(f,g))=F$$({.y.},G[;](F$$({.x.},f),g)); theorem :: MATRIX_3:28 for I, J being non empty set for F,G being BinOp of D for f being Function of I,D for g being Function of J,D for X being Element of Fin I for Y being Element of Fin J st F is having_a_unity & F is commutative associative & F is having_an_inverseOp & G is_distributive_wrt F & G is commutative holds F$$ ([:X,Y:],G*(f,g))=F$$(Y,G[;](F$$(X,f),g)); theorem :: MATRIX_3:29 for I, J being non empty set for F being BinOp of D for f being Function of [:I,J:],D for g being Function of I,D for Y being Element of Fin J st F is having_a_unity commutative associative holds for x being Element of I holds (for i being Element of I holds g.i=F$$(Y,(curry f).i)) implies F$$([:{.x .},Y:],f)=F$$({.x.},g); theorem :: MATRIX_3:30 for I, J being non empty set for F being BinOp of D for f being Function of [:I,J:],D for g being Function of I,D for X being Element of Fin I for Y being Element of Fin J st (for i being Element of I holds g.i=F$$(Y,( curry f).i))& F is having_a_unity & F is commutative & F is associative holds F $$([:X,Y:],f)=F$$(X,g); theorem :: MATRIX_3:31 for I, J being non empty set for F being BinOp of D for f being Function of [:I,J:],D for g being Function of J,D for X being Element of Fin I st F is having_a_unity & F is commutative & F is associative holds for y being Element of J holds (for j being Element of J holds g.j=F$$(X,(curry' f).j)) implies F$$([:X,{.y.}:],f)=F$$({.y.},g); theorem :: MATRIX_3:32 for I, J being non empty set for F being BinOp of D for f being Function of [:I,J:],D for g being Function of J,D for X being Element of Fin I for Y being Element of Fin J st (for j being Element of J holds g.j=F$$ (X, ( curry' f).j) )& F is having_a_unity & F is commutative & F is associative holds F$$([:X,Y:],f)=F$$(Y,g); theorem :: MATRIX_3:33 for K being commutative Ring for A,B,C being Matrix of K st width A=len B & width B=len C holds (A*B)*C=A*(B*C); begin :: Determinant definition let n,K; let M be Matrix of n,K; let p be Element of Permutations(n); func Path_matrix(p,M) -> FinSequence of K means :: MATRIX_3:def 7 len it=n & for i,j st i in dom it & j=p.i holds it.i=M*(i,j); end; definition let n; let K be Ring; let M be Matrix of n,K; func Path_product(M) -> Function of Permutations(n), the carrier of K means :: MATRIX_3:def 8 for p being Element of Permutations(n) holds it.p = -((the multF of K) $$ Path_matrix(p,M),p); end; definition let n; let K be Ring; let M be Matrix of n,K; func Det M -> Element of K equals :: MATRIX_3:def 9 (the addF of K) $$ (In(Permutations(n), Fin Permutations n),Path_product(M)); end; reserve a for Element of K; theorem :: MATRIX_3:34 for K be Ring, a being Element of K holds Det <*<*a*>*> =a; definition let n; let K; let M be Matrix of n,K; func diagonal_of_Matrix M -> FinSequence of K means :: MATRIX_3:def 10 len it = n & for i st i in Seg n holds it.i=M*(i,i); end;