Volume 5, 1993

University of Bialystok

Copyright (c) 1993 Association of Mizar Users

### The abstract of the Mizar article:

### The Product and the Determinant of Matrices with Entries in a Field

**by****Katarzyna Zawadzka**- Received May 17, 1993
- MML identifier: MATRIX_3

- [ Mizar article, MML identifier index ]

environ vocabulary VECTSP_1, RLVECT_1, MATRIX_1, FINSEQ_2, ARYTM_1, FINSEQ_1, TREES_1, FUNCT_1, RELAT_1, BOOLE, INCSP_1, CAT_3, RVSUM_1, GROUP_1, BINOP_1, SETWISEO, SQUARE_1, MATRIX_2, QC_LANG1, FINSUB_1, FINSET_1, FUNCOP_1, PARTFUN1, FINSEQOP, FUNCT_5, SUBSET_1, FVSUM_1, MATRIX_3; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, NUMBERS, XREAL_0, STRUCT_0, FINSET_1, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, FINSEQ_1, BINOP_1, FUNCT_3, FUNCOP_1, RLVECT_1, VECTSP_1, SETWISEO, SETWOP_2, FINSEQ_2, FINSEQOP, MATRIX_1, FINSUB_1, MATRIX_2, NAT_1, SQUARE_1, FVSUM_1, TREES_1, FUNCT_5, CAT_2; constructors ALGSTR_1, BINOP_1, SETWISEO, SETWOP_2, FINSEQOP, MATRIX_2, NAT_1, SQUARE_1, FVSUM_1, CAT_2, FINSOP_1, MEMBERED, PARTFUN1, RELAT_2, XBOOLE_0; clusters SUBSET_1, FUNCT_1, FINSUB_1, FINSET_1, RELSET_1, STRUCT_0, FVSUM_1, MATRIX_2, FUNCOP_1, XREAL_0, ARYTM_3, VECTSP_1, MEMBERED, ZFMISC_1, FUNCT_2, PARTFUN1, XBOOLE_0, NUMBERS, ORDINAL2; requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM; begin reserve x,y,z,x1,x2,y1,y2,z1,z2 for set, i,j,k,l,n,m for Nat, D for non empty set, K for Field; :: Auxiliary theorems theorem :: MATRIX_3:1 n = n + k implies k=0; definition let K,n,m; func 0.(K,n,m) -> Matrix of n,m,K equals :: MATRIX_3:def 1 n |-> (m |-> 0.K); end; definition let K;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;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; canceled; theorem :: MATRIX_3:3 for i,j st [i,j] in Indices (0.(K,n,m)) holds (0.(K,n,m))*(i,j)= 0.K; theorem :: MATRIX_3:4 for A,B being Matrix of K st len A= len B & width A=width B holds A + B = B + A; theorem :: MATRIX_3:5 for A,B,C being Matrix of K st len A=len B & len A=len C & width A=width B & width A=width C holds (A + B) + C= A + (B + C); theorem :: MATRIX_3:6 for A being Matrix of n,m,K holds A + 0.(K,n,m)= A; theorem :: MATRIX_3:7 for A being Matrix of n,m,K holds A + (-A) = 0.(K,n,m); definition let K;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;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;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;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:8 for p,q being FinSequence of the carrier of K st len p=len q holds len (mlt(p,q))=len p & len (mlt(p,q))=len q; theorem :: MATRIX_3:9 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:10 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:11 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:12 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:13 for K being add-associative right_zeroed right_complementable (non empty LoopStr) holds Sum (n |-> 0.K) = 0.K; theorem :: MATRIX_3:14 for K being add-associative right_zeroed right_complementable (non empty LoopStr) for p being FinSequence of the carrier 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:15 for p,q being FinSequence of the carrier of K holds len (mlt(p,q))=min(len p,len q); theorem :: MATRIX_3:16 for p,q being FinSequence of the carrier of K for i st i in dom p & 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:17 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:18 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:19 for p,q being FinSequence of the carrier 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:20 for A being Matrix of n,K holds 1.(K,n)*A=A; theorem :: MATRIX_3:21 for A being Matrix of n,K holds A*(1.(K,n))=A; theorem :: MATRIX_3:22 for a,b being Element of K holds <*<*a*>*> * <*<*b*>*> =<*<*a*b*>*>; theorem :: MATRIX_3:23 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:24 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:25 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 has_a_unity )& G is commutative holds F $$ ([:X,Y:],G*(f,g))=F$$([:Y,X:],G*(g,f)); theorem :: MATRIX_3:26 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 & F has_a_unity 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: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 for X being Element of Fin I for Y being Element of Fin J st F is commutative & F is associative & F has_a_unity & F has_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: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 has_a_unity & F is commutative & F is associative & F has_an_inverseOp & G is_distributive_wrt F holds F$$([:X,Y:],G*(f,g))=F$$(X,G[:](f,F$$(Y,g))); theorem :: MATRIX_3:29 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 & F has_a_unity & 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:30 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 has_a_unity & F is commutative associative & F has_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: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 I,D for Y being Element of Fin J st F has_a_unity & F is commutative associative & F has_an_inverseOp 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: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 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 has_a_unity & F is commutative & F is associative & F has_an_inverseOp holds F$$([:X,Y:],f)=F$$(X,g); theorem :: MATRIX_3:33 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 has_a_unity & F is commutative & F is associative & F has_an_inverseOp 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:34 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 has_a_unity & F is commutative & F is associative & F has_an_inverseOp holds F$$([:X,Y:],f)=F$$(Y,g); theorem :: MATRIX_3:35 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 the carrier 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,K;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 mult of K) $$ Path_matrix(p,M),p); end; definition let n;let K;let M be Matrix of n,K; func Det M -> Element of (the carrier of K) equals :: MATRIX_3:def 9 (the add of K) $$ (FinOmega(Permutations(n)),Path_product(M)); end; reserve a for Element of K; theorem :: MATRIX_3:36 Det <*<*a*>*> =a; definition let n;let K; let M be Matrix of n,K; func diagonal_of_Matrix(M) -> FinSequence of the carrier of K means :: MATRIX_3:def 10 len it = n & for i st i in Seg n holds it.i=M*(i,i); end;

Back to top