:: On the Permanent of a Matrix :: by Ewa Romanowicz and Adam Grabowski :: :: Received January 4, 2006 :: Copyright (c) 2006-2018 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, FINSUB_1, TARSKI, XBOOLE_0, SUBSET_1, FINSEQ_2, FINSET_1, FINSEQ_1, FUNCT_1, RELAT_1, FINSEQ_5, FUNCT_2, CARD_1, MATRIX_1, STRUCT_0, ALGSTR_0, SETWISEO, MATRIX_3, CALCUL_2, XXREAL_0, SUPINF_2, FUNCOP_1, BINOP_1, ARYTM_3, ORDINAL4, TREES_1, ZFMISC_1, ARYTM_1, CARD_3, ABIAN, INT_1, PARTFUN1, GROUP_1, FUNCT_7, MATRIX_9; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, NAT_1, NAT_D, ENUMSET1, FINSET_1, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, FINSEQ_1, FUNCOP_1, FINSEQ_2, BINOP_1, STRUCT_0, ALGSTR_0, GROUP_1, VECTSP_1, SETWISEO, GROUP_4, SETWOP_2, FINSUB_1, MATRIX_0, FINSEQ_4, FINSEQ_5, MATRIX_1, MATRIX_3, XXREAL_0; constructors BINOP_1, SETWISEO, NAT_1, NAT_D, FINSEQ_4, FINSOP_1, FINSEQ_5, ALGSTR_1, GROUP_4, MATRIX_7, RELSET_1; registrations XBOOLE_0, SUBSET_1, FUNCT_1, ORDINAL1, PARTFUN1, FUNCT_2, FINSET_1, FINSUB_1, XXREAL_0, XREAL_0, FINSEQ_1, FINSEQ_5, FINSEQ_6, STRUCT_0, GROUP_1, VECTSP_1, MATRIX_1, FVSUM_1, RELSET_1, FINSEQ_2, CARD_1; requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM; begin :: Preliminaries reserve x for set, i,j,k,n for Nat, K for Field; theorem :: MATRIX_9:1 for a, A being set st a in A holds {a} in Fin A; registration let n be Nat; cluster non empty for Element of Fin Permutations n; end; scheme :: MATRIX_9:sch 1 NonEmptyFiniteX { n() -> Element of NAT, A() -> non empty Element of Fin Permutations n(), P[set] } : P[A()] provided for x being Element of Permutations n() st x in A() holds P[{x}] and for x being Element of Permutations n(), B being non empty Element of Fin Permutations n() st x in A() & B c= A() & not x in B & P[B] holds P[B \/ {x}]; registration let n; cluster one-to-one FinSequence-like for Function of Seg n, Seg n; end; registration let n; cluster id Seg n -> FinSequence-like; end; theorem :: MATRIX_9:2 (Rev idseq 2).1 = 2 & (Rev idseq 2).2 = 1; theorem :: MATRIX_9:3 for f being one-to-one Function st dom f = Seg 2 & rng f = Seg 2 holds f = id Seg 2 or f = Rev id Seg 2; begin :: Permutations theorem :: MATRIX_9:4 Rev idseq n in Permutations n; theorem :: MATRIX_9:5 for f being FinSequence st n <> 0 & f in Permutations n holds Rev f in Permutations n; theorem :: MATRIX_9:6 Permutations 2 = { idseq 2, Rev idseq 2 }; begin :: The Permanent of a Matrix definition let n,K; let M be Matrix of n,K; func PPath_product M -> Function of Permutations n, the carrier of K means :: MATRIX_9:def 1 for p being Element of Permutations(n) holds it.p = (the multF of K) \$\$ Path_matrix(p,M); end; definition let n, K; let M be Matrix of n,K; func Per M -> Element of K equals :: MATRIX_9:def 2 (the addF of K) \$\$ (In (Permutations n, Fin Permutations n), PPath_product M); end; reserve a,b,c,d for Element of K; theorem :: MATRIX_9:7 Per <*<*a*>*> = a; theorem :: MATRIX_9:8 for K being Field, n being Element of NAT st n >= 1 holds Per (0.(K,n, n)) = 0.K; theorem :: MATRIX_9:9 for p being Element of Permutations 2 st p = idseq 2 holds Path_matrix (p, (a,b)][(c,d)) = <* a,d *>; theorem :: MATRIX_9:10 for p being Element of Permutations 2 st p = Rev idseq 2 holds Path_matrix (p, (a,b)][(c,d)) = <* b,c *>; theorem :: MATRIX_9:11 (the multF of K) \$\$ <* a,b *> = a * b; begin registration cluster odd for Permutation of Seg 2; end; registration let n be Nat; cluster even for Permutation of Seg n; end; theorem :: MATRIX_9:12 <*2,1*> is odd Permutation of Seg 2; theorem :: MATRIX_9:13 Det (a,b)][(c,d) = a * d - b * c; theorem :: MATRIX_9:14 Per (a,b)][(c,d) = a * d + b * c; theorem :: MATRIX_9:15 Rev idseq 3 = <*3,2,1*>; reserve D for non empty set; theorem :: MATRIX_9:16 for x,y,z being Element of D for f being FinSequence of D st f = <*x,y ,z*> holds Rev f = <*z,y,x*>; theorem :: MATRIX_9:17 for f, g being FinSequence st f ^ g in Permutations n holds f ^ Rev g in Permutations n; theorem :: MATRIX_9:18 for f, g being FinSequence st f ^ g in Permutations n holds g ^ f in Permutations n; theorem :: MATRIX_9:19 Permutations 3 = {<*1,2,3*>,<*3,2,1*>,<*1,3,2*>,<*2,3,1*>,<*2,1, 3*>,<*3,1,2*>}; theorem :: MATRIX_9:20 for a,b,c,d,e,f,g,h,i being Element of K for M being Matrix of 3 ,K st M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*> for p being Element of Permutations 3 st p = <*1,2,3*> holds Path_matrix (p,M) = <* a,e,i *>; theorem :: MATRIX_9:21 for a,b,c,d,e,f,g,h,i being Element of K for M being Matrix of 3 ,K st M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*> for p being Element of Permutations 3 st p = <*3,2,1*> holds Path_matrix (p,M) = <* c,e,g *>; theorem :: MATRIX_9:22 for a,b,c,d,e,f,g,h,i being Element of K for M being Matrix of 3 ,K st M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*> for p being Element of Permutations 3 st p = <*1,3,2*> holds Path_matrix (p,M) = <* a,f,h *>; theorem :: MATRIX_9:23 for a,b,c,d,e,f,g,h,i being Element of K for M being Matrix of 3 ,K st M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*> for p being Element of Permutations 3 st p = <*2,3,1*> holds Path_matrix (p,M) = <* b,f,g *>; theorem :: MATRIX_9:24 for a,b,c,d,e,f,g,h,i being Element of K for M being Matrix of 3 ,K st M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*> for p being Element of Permutations 3 st p = <*2,1,3*> holds Path_matrix (p,M) = <* b,d,i *>; theorem :: MATRIX_9:25 for a,b,c,d,e,f,g,h,i being Element of K for M being Matrix of 3 ,K st M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*> for p being Element of Permutations 3 st p = <*3,1,2*> holds Path_matrix (p,M) = <* c,d,h *>; theorem :: MATRIX_9:26 (the multF of K) \$\$ <* a,b,c *> = a * b * c; theorem :: MATRIX_9:27 <*1,3,2*> in Permutations 3 & <*2,3,1*> in Permutations 3 & <*2, 1,3*> in Permutations 3 & <*3,1,2*> in Permutations 3 & <*1,2,3*> in Permutations 3 & <*3,2,1*> in Permutations 3; theorem :: MATRIX_9:28 <*2,3,1*>" = <*3,1,2*>; theorem :: MATRIX_9:29 for a being Element of Group_of_Perm 3 st a = <*2,3,1*> holds a" = <*3 ,1,2*> ; begin :: Transpositions theorem :: MATRIX_9:30 for p being Permutation of Seg 3 st p = <* 1,3,2 *> holds p is being_transposition; theorem :: MATRIX_9:31 for p being Permutation of Seg 3 st p = <* 2,1,3 *> holds p is being_transposition; theorem :: MATRIX_9:32 for p being Permutation of Seg 3 st p = <* 3,2,1 *> holds p is being_transposition; theorem :: MATRIX_9:33 for p being Permutation of Seg n st p = id Seg n holds not p is being_transposition; theorem :: MATRIX_9:34 for p being Permutation of Seg 3 st p = <* 3,1,2 *> holds not p is being_transposition; theorem :: MATRIX_9:35 for p being Permutation of Seg 3 st p = <* 2,3,1 *> holds not p is being_transposition; begin :: Corrollaries theorem :: MATRIX_9:36 for f being Permutation of Seg n holds f is FinSequence of Seg n; theorem :: MATRIX_9:37 <*2,1,3*> * <*1,3,2*> = <*2,3,1*> & <*1,3,2*> * <*2,1,3*> = <*3, 1,2*> & <*2,1,3*> * <*3,2,1*> = <*3,1,2*> & <*3,2,1*> * <*2,1,3*> = <*2,3,1*> & <*3,2,1*> * <*3,2,1*> = <*1,2,3*> & <*2,1,3*> * <*2,1,3*> = <*1,2,3*> & <*1,3,2 *> * <*1,3,2*> = <*1,2,3*> & <*1,3,2*> * <*2,3,1*> = <*3,2,1*> & <*2,3,1*> * <* 2,3,1*> = <*3,1,2*> & <*2,3,1*> * <*3,1,2*> = <*1,2,3*> & <*3,1,2*> * <*2,3,1*> = <*1,2,3*> & <*3,1,2*> * <*3,1,2*> = <*2,3,1*> & <*1,3,2*> * <*3,2,1*> = <*2,3 ,1*> & <*3,2,1*> * <*1,3,2*> = <*3,1,2*>; theorem :: MATRIX_9:38 for p being Permutation of Seg 3 st p is being_transposition holds p = <*2,1,3*> or p = <*1,3,2*> or p = <*3,2,1*>; theorem :: MATRIX_9:39 for f, g being Element of Permutations n holds f * g in Permutations n; theorem :: MATRIX_9:40 for l being FinSequence of Group_of_Perm n st (len l) mod 2 = 0 & (for i being Element of NAT st i in dom l ex q being Element of Permutations n st l. i = q & q is being_transposition) holds Product l is even Permutation of Seg n; theorem :: MATRIX_9:41 for l being FinSequence of Group_of_Perm 3 st (len l) mod 2 = 0 & (for i being Element of NAT st i in dom l ex q being Element of Permutations 3 st l.i = q & q is being_transposition) holds Product l = <*1,2,3*> or Product l = <*2,3,1*> or Product l = <*3,1,2*>; registration cluster odd for Permutation of Seg 3; end; theorem :: MATRIX_9:42 <*3,2,1*> is odd Permutation of Seg 3; theorem :: MATRIX_9:43 <*2,1,3*> is odd Permutation of Seg 3; theorem :: MATRIX_9:44 <*1,3,2*> is odd Permutation of Seg 3; theorem :: MATRIX_9:45 for p being odd Permutation of Seg 3 holds p = <*3,2,1*> or p = <*1,3, 2*> or p = <*2,1,3*>; begin :: Determinant and Permanent theorem :: MATRIX_9:46 for a,b,c,d,e,f,g,h,i being Element of K for M being Matrix of 3,K st M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*> holds Det M = a*e*i - c*e*g - a*f*h + b*f *g - b*d*i + c*d*h; theorem :: MATRIX_9:47 for a,b,c,d,e,f,g,h,i being Element of K for M being Matrix of 3,K st M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*> holds Per M = a*e*i + c*e*g + a*f*h + b*f *g + b*d*i + c*d*h; theorem :: MATRIX_9:48 for i,n being Element of NAT for p being Element of Permutations n st i in Seg n holds ex k being Element of NAT st k in Seg n & i = p.k; theorem :: MATRIX_9:49 for M being Matrix of n, K st (ex i being Element of NAT st i in Seg n & for k being Element of NAT st k in Seg n holds Col(M,i).k = 0.K) holds for p being Element of Permutations n holds ex l being Element of NAT st l in Seg n & Path_matrix (p,M).l = 0.K; theorem :: MATRIX_9:50 for p being Element of Permutations n for M being Matrix of n, K st (ex i being Element of NAT st i in Seg n & for k being Element of NAT st k in Seg n holds Col(M,i).k = 0.K) holds (Path_product M).p = 0.K; theorem :: MATRIX_9:51 for M being Matrix of n, K st (ex i being Element of NAT st i in Seg n & for k being Element of NAT st k in Seg n holds Col(M,i).k = 0.K) holds (the addF of K) \$\$ (In(Permutations n,Fin Permutations n), Path_product M) = 0.K; theorem :: MATRIX_9:52 for p being Element of Permutations n for M being Matrix of n, K st (ex i being Element of NAT st i in Seg n & (for k being Element of NAT st k in Seg n holds Col(M,i).k = 0.K)) holds (PPath_product M).p = 0.K; theorem :: MATRIX_9:53 for M being Matrix of n, K st (ex i being Element of NAT st i in Seg n & for k being Element of NAT st k in Seg n holds Col(M,i).k = 0.K) holds Det M = 0.K; theorem :: MATRIX_9:54 for M being Matrix of n, K st (ex i being Element of NAT st i in Seg n & for k being Element of NAT st k in Seg n holds Col(M,i).k = 0.K) holds Per M = 0.K; begin :: Auxiliary Lemmas for Further Work theorem :: MATRIX_9:55 for M,N being Matrix of n, K st i in Seg n for p being Element of Permutations n holds ex k being Element of NAT st k in Seg n & i = p.k & Col(N, i)/.k = Path_matrix (p, N)/.k; theorem :: MATRIX_9:56 for a being Element of K for M,N being Matrix of n, K st (ex i being Element of NAT st i in Seg n & (for k being Element of NAT st k in Seg n holds Col(M,i).k = a * Col(N,i)/.k) & (for l being Element of NAT st l <> i & l in Seg n holds Col(M,l) = Col(N,l))) for p being Element of Permutations n holds ex l being Element of NAT st l in Seg n & Path_matrix (p,M)/.l = a * ( Path_matrix (p,N)/.l);