:: Determinant of Some Matrices of Field Elements :: by Yatsuka Nakamura :: :: Received January 4, 2006 :: Copyright (c) 2006-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, FUNCT_2, FINSEQ_1, RELAT_1, FUNCT_1, TARSKI, FINSEQ_2, XBOOLE_0, SUBSET_1, XXREAL_0, ARYTM_3, JORDAN3, ORDINAL4, ARYTM_1, CARD_1, STRUCT_0, INT_1, CARD_3, GROUP_1, VECTSP_1, MATRIX_1, MATRIX_3, ALGSTR_0, SETWISEO, FINSUB_1, BINOP_1, FINSOP_1, ABIAN, TREES_1, SUPINF_2, FUNCOP_1, MESFUNC1, ZFMISC_1, QC_LANG1, PARTFUN1, FINSEQ_5, CLASSES1, RFINSEQ, FUNCSDOM, MATRIX_7, FUNCT_7; notations TARSKI, XBOOLE_0, SUBSET_1, XCMPLX_0, XXREAL_0, ORDINAL1, NAT_1, NAT_D, RELAT_1, FUNCT_1, BINOP_1, ZFMISC_1, CARD_1, NUMBERS, VECTSP_1, FUNCT_2, FUNCOP_1, SETWISEO, PARTFUN1, GROUP_4, FINSUB_1, NEWTON, FINSOP_1, SETWOP_2, FINSEQ_1, FINSEQ_2, STRUCT_0, ALGSTR_0, MATRIX_1, MATRIX_3, FINSEQ_6, MATRIX_0, CLASSES1, RFINSEQ, FINSEQ_5, GROUP_1; constructors SETWISEO, REAL_1, NAT_1, NAT_D, FINSOP_1, NEWTON, RFINSEQ, FINSEQ_5, ALGSTR_1, GROUP_4, MATRIX_3, FINSEQ_6, CLASSES1, RELSET_1, BINOP_1, MATRIX_1; registrations SUBSET_1, FUNCT_1, ORDINAL1, PARTFUN1, FUNCT_2, FINSUB_1, XXREAL_0, XREAL_0, NAT_1, FINSEQ_1, STRUCT_0, GROUP_1, VECTSP_1, MATRIX_1, FVSUM_1, FINSET_1, CARD_1, RELSET_1, FINSEQ_2, MATRIX_0; requirements NUMERALS, BOOLE, SUBSET, ARITHM, REAL; begin reserve k,n,i,j for Nat; theorem :: MATRIX_7:1 for f being Permutation of Seg 2 holds f=<*1,2*> or f=<*2,1*>; theorem :: MATRIX_7:2 for f being FinSequence st f=<*1,2*> or f=<*2,1*> holds f is Permutation of Seg 2; theorem :: MATRIX_7:3 Permutations(2)={<*1,2*>,<*2,1*>}; theorem :: MATRIX_7:4 for p being Permutation of Seg 2 st p is being_transposition holds p = <*2,1*>; theorem :: MATRIX_7:5 for D being non empty set, f being FinSequence of D, k2 being Nat st 1<=k2 & k2< len f holds f = mid(f,1,k2)^mid(f,k2+1,len f); theorem :: MATRIX_7:6 for D being non empty set, f being FinSequence of D st 2<= len f holds f = (f|(len f-'2))^mid(f,len f-'1,len f); theorem :: MATRIX_7:7 for D being non empty set, f being FinSequence of D st 1<= len f holds f = (f|(len f-'1))^mid(f,len f,len f); theorem :: MATRIX_7:8 for a being Element of Group_of_Perm 2 st (ex q being Element of Permutations 2 st q=a & q is being_transposition) holds a = <*2,1*>; theorem :: MATRIX_7:9 for n being Nat,a,b being Element of Group_of_Perm n, pa,pb being Element of Permutations n st a=pa & b=pb holds a*b=pb*pa; theorem :: MATRIX_7:10 for a,b being Element of Group_of_Perm 2 st (ex p being Element of Permutations 2 st p=a & p is being_transposition)& (ex q being Element of Permutations 2 st q=b & q is being_transposition) holds a*b = <*1,2*>; theorem :: MATRIX_7:11 for l being FinSequence of Group_of_Perm 2 st (len l) mod 2=0 & (for i st i in dom l holds (ex q being Element of Permutations 2 st l.i=q & q is being_transposition)) holds Product l = <*1,2*>; theorem :: MATRIX_7:12 for K being Field, M being Matrix of 2,K holds Det M = (M*(1,1))*(M*(2 ,2))-(M*(1,2))*(M*(2,1)); definition let n be Nat,K be commutative Ring; let M be (Matrix of n,K), a be Element of K; redefine func a*M -> Matrix of n,K; end; theorem :: MATRIX_7:13 for K being Ring, n,m being Nat holds len (0.(K,n,m))=n & dom (0.(K,n,m))=Seg n; theorem :: MATRIX_7:14 for K being Ring, n being Nat, p being Element of Permutations n, i being Nat st i in Seg n holds p.i in Seg n; theorem :: MATRIX_7:15 for K being Ring, n being Nat st n>=1 holds Det (0.(K,n,n) ) = 0.K; definition let x be object; let y be set; let a,b be object; func IFIN(x,y,a,b) -> object equals :: MATRIX_7:def 1 a if x in y otherwise b; end; theorem :: MATRIX_7:16 for K being Ring, n being Nat st n>=1 holds Det (1.(K,n)) = 1_K; definition let n be Nat, K be Field, M be Matrix of n,K; redefine attr M is diagonal means :: MATRIX_7:def 2 for i,j being Nat st i in Seg n & j in Seg n & i <> j holds M*(i,j) = 0.K; end; theorem :: MATRIX_7:17 for K being Field, n being Nat, A being Matrix of n,K st n >=1 & A is diagonal holds Det A = (the multF of K) $$ (diagonal_of_Matrix A); theorem :: MATRIX_7:18 for p being Element of Permutations(n) holds p" is Element of Permutations(n) ; definition let n; let p be Element of Permutations(n); redefine func p" -> Element of Permutations(n); end; ::$CT theorem :: MATRIX_7:20 for G being Group, f1,f2 being FinSequence of G holds (Product (f1^f2))" = (Product f2)" * (Product f1)"; definition let G be Group, f be FinSequence of G; ::$CD func f" -> FinSequence of G means :: MATRIX_7:def 4 len it = len f & for i being Nat st i in dom f holds it/.i = (f/.i)"; end; theorem :: MATRIX_7:21 for G being Group holds (<*>(the carrier of G))"=<*>(the carrier of G); theorem :: MATRIX_7:22 for G being Group, f,g being FinSequence of G holds (f^g)"=(f")^ (g"); theorem :: MATRIX_7:23 for G being Group,a being Element of G holds (<*a*>)" =<* a" *>; theorem :: MATRIX_7:24 for G being Group, f being FinSequence of G holds Product (f^( Rev f)")=1_G; theorem :: MATRIX_7:25 for G being Group,f being FinSequence of G holds Product ((Rev f )" ^f)=1_G; theorem :: MATRIX_7:26 for G being Group,f being FinSequence of G holds (Product f)" = Product ((Rev f)"); theorem :: MATRIX_7:27 for ITP being Element of Permutations(n), ITG being Element of Group_of_Perm(n) st ITG=ITP & n>=1 holds ITP"=ITG"; theorem :: MATRIX_7:28 for n being Nat, IT being Element of Permutations(n) st n>=1 holds IT is even iff IT" is even; theorem :: MATRIX_7:29 for n being Nat,K being commutative Ring, p being Element of Permutations(n), x being Element of K st n>=1 holds -(x,p) = -(x,p"); theorem :: MATRIX_7:30 for K being commutative Ring, f1,f2 being FinSequence of K holds (the multF of K) $$ (f1^f2) = ((the multF of K)$$f1)*((the multF of K)$$f2); theorem :: MATRIX_7:31 for K being commutative Ring,R1,R2 be FinSequence of K st R1,R2 are_fiberwise_equipotent holds (the multF of K)$$ R1 = (the multF of K)$$ R2; theorem :: MATRIX_7:32 for n being Nat, K being commutative Ring, p being Element of Permutations(n), f,g being FinSequence of K st len f=n & g=f*p holds f,g are_fiberwise_equipotent; theorem :: MATRIX_7:33 for n being Nat, K being commutative Ring, p being Element of Permutations(n), f,g being FinSequence of K st n>=1 & len f=n & g=f*p holds ( the multF of K) $$ f = (the multF of K) $$ g; theorem :: MATRIX_7:34 for n being Nat, K being Ring, p being Element of Permutations(n), f being FinSequence of K st n>=1 & len f=n holds f*p is FinSequence of K; theorem :: MATRIX_7:35 for n being Nat, K being commutative Ring, p being Element of Permutations(n), A being Matrix of n,K st n>=1 holds Path_matrix(p",A@) = ( Path_matrix(p,A))*p"; theorem :: MATRIX_7:36 for n being Nat, K being commutative Ring, p being Element of Permutations(n), A being Matrix of n,K st n>=1 holds (Path_product(A@)).(p") = (Path_product(A)).p; theorem :: MATRIX_7:37 for n being Nat, K being commutative Ring, A being Matrix of n,K st n >=1 holds Det (A) = Det (A@);