:: Laplace Expansion :: by Karol P\c{a}k and Andrzej Trybulec :: :: Received August 13, 2007 :: Copyright (c) 2007-2012 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, SUBSET_1, NAT_1, XBOOLE_0, MATRIX11, FINSEQ_1, ARYTM_3, MATRIX_2, VECTSP_1, MATRIX_1, RELAT_1, FINSEQ_3, ARYTM_1, TREES_1, CARD_1, XXREAL_0, FUNCT_1, INCSP_1, TARSKI, ALGSTR_0, ZFMISC_1, STRUCT_0, REALSET1, SETWOP_2, FUNCT_2, FINSUB_1, GROUP_1, SETWISEO, INT_1, FINSET_1, ABIAN, FINSEQ_2, BINOP_1, QC_LANG1, AFINSQ_1, ABSVALUE, MATRIX_3, SUPINF_2, CARD_3, FINSOP_1, RVSUM_1, FVSUM_1, MESFUNC1, MATRIX_6, LAPLACE; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, NUMBERS, XCMPLX_0, XXREAL_0, FINSET_1, RELAT_1, RELSET_1, FUNCT_1, PARTFUN1, FUNCT_2, FINSEQ_1, BINOP_1, STRUCT_0, ALGSTR_0, GROUP_1, VECTSP_1, SETWISEO, SETWOP_2, FINSEQ_2, MATRIX_1, FINSUB_1, MATRIX_2, ORDINAL1, NAT_1, FVSUM_1, FINSOP_1, MATRIX_3, CARD_1, FINSEQ_7, NEWTON, MATRIX_7, FINSEQ_3, MATRIX11, MATRIX_6, NAT_D; constructors SETWISEO, FINSOP_1, SETWOP_2, ALGSTR_1, FVSUM_1, BINOP_1, FINSEQ_4, FINSEQ_7, WELLORD2, NEWTON, MATRIX_6, MATRIX_7, MATRIX11, NAT_D, BINOP_2, RELSET_1; registrations FUNCT_1, FINSUB_1, FINSET_1, STRUCT_0, FVSUM_1, MATRIX_2, VECTSP_1, FUNCT_2, PARTFUN1, XBOOLE_0, ORDINAL1, XXREAL_0, NAT_1, INT_1, RELAT_1, CARD_1, MATRIX11, XCMPLX_0, RELSET_1, FINSEQ_2, FINSEQ_1; requirements ARITHM, NUMERALS, REAL, BOOLE, SUBSET; definitions FINSEQ_2, FINSEQ_1, TARSKI, MATRIX_1, MATRIX_3, FVSUM_1, MATRIX_2, MATRIX_7, MATRIX11, RELAT_1, ALGSTR_0; theorems FINSEQ_1, FINSEQ_2, TARSKI, FUNCT_2, NAT_1, FUNCT_1, SETWISEO, VECTSP_1, ZFMISC_1, FVSUM_1, SETWOP_2, MATRIX_1, MATRIX_2, FINSUB_1, FINSEQ_3, RELAT_1, FINSOP_1, XBOOLE_0, XBOOLE_1, MATRIX_3, XREAL_1, MATRIX_7, ORDINAL1, CARD_1, CARD_2, MATRIX_9, STIRL2_1, SGRAPH1, CARD_FIN, HURWITZ, NEWTON, COMPUT_1, MATRIX11, GROUP_1, MATRIX_4, MATRIX_6, MATRIXR1, NAT_D, XXREAL_0, MATRIXR2, XREAL_0; schemes FUNCT_2, NAT_1, FINSEQ_1, FUNCT_1, SETWISEO, MATRIX_1; begin :: Preliminaries reserve x,y for set, N for Element of NAT, c,i,j,k,m,n for Nat, D for non empty set, s for Element of 2Set Seg (n+2), p for Element of Permutations(n) , p1, q1 for Element of Permutations(n+1), p2 for Element of Permutations(n +2), K for Field, a for Element of K, f for FinSequence of K, A for (Matrix of K), AD for Matrix of n,m,D, pD for FinSequence of D, M for Matrix of n,K; theorem Th1: for f be FinSequence, i be Nat st i in dom f holds len Del(f,i) = len f -' 1 proof let f be FinSequence, i be Nat; assume i in dom f; then ex m be Nat st len f = m + 1 & len Del(f,i) = m by FINSEQ_3:104; hence thesis by NAT_D:34; end; theorem Th2: for i,j,n being Nat, M being Matrix of n,K st i in dom M holds len Deleting(M,i,j) = n-'1 proof let i,j,n be Nat, M be Matrix of n,K; assume A1: i in dom M; A2: len M = n by MATRIX_1:def 2; thus len Deleting(M,i,j)= len DelLine(M,i) by MATRIX_2:def 5 .= n-'1 by A1,A2,Th1; end; theorem Th3: j in Seg width A implies width DelCol(A,j) = width A-'1 proof set DC=DelCol(A,j); A1: len DC = len A by MATRIX_2:def 5; assume A2: j in Seg width A; then Seg width A <> {}; then width A <>0; then len A > 0 by MATRIX_1:def 3; then consider t being FinSequence such that A3: t in rng DC and A4: len t = width DC by A1,MATRIX_1:def 3; consider k9 be set such that A5: k9 in dom DelCol(A,j) and A6: DC.k9 = t by A3,FUNCT_1:def 3; k9 in Seg len DC by A5,FINSEQ_1:def 3; then consider k being Element of NAT such that A7: k9=k and 1<=k and k<=len DC; k in dom A by A1,A5,A7,FINSEQ_3:29; then A8: t=Del(Line(A,k),j) by A6,A7,MATRIX_2:def 5; A9: len Line(A,k)=width A by MATRIX_1:def 7; then dom Line(A,k)=Seg (width A) by FINSEQ_1:def 3; hence thesis by A2,A4,A9,A8,Th1; end; theorem Th4: for i be Nat st len A > 1 holds width A = width DelLine(A,i) proof let i be Nat; assume A1: len A>1; per cases; suppose i in dom A; then consider m be Nat such that A2: len A = m + 1 and A3: len Del(A,i) = m by FINSEQ_3:104; A4: m>=1 by A1,A2,NAT_1:13; then A5: m in dom Del(A,i) by A3,FINSEQ_3:25; then A6: DelLine(A,i).m in rng Del(A,i) by FUNCT_1:def 3; A7: rng Del(A,i) c= rng A by FINSEQ_3:106; A8: DelLine(A,i).m=Line(DelLine(A,i),m) by A5,MATRIX_2:16; A is Matrix of len A,width A,K by A1,MATRIX_1:20; then len Line(DelLine(A,i),m)=width A by A6,A8,A7,MATRIX_1:def 2; hence thesis by A3,A4,A6,A8,MATRIX_1:def 3; end; suppose not i in dom A; hence thesis by FINSEQ_3:104; end; end; theorem Th5: for i being Nat st j in Seg width M holds width Deleting(M,i,j) = n-' 1 proof let i be Nat; assume A1: j in Seg width M; per cases; suppose A2: len M<=1 & i in dom M; Seg width M <> {} by A1; then width M <> {}; then len M > 0 by MATRIX_1:def 3; then A3: len M=1 by A2,NAT_1:25; A4: len Deleting(M,i,j)=n-'1 by A2,Th2; len M=n by MATRIX_1:24; then len Deleting(M,i,j)=0 by A3,A4,XREAL_1:232; hence thesis by A4,MATRIX_1:def 3; end; suppose A5: len M>1; A6: width M=n by MATRIX_1:24; width M=width DelLine(M,i) by A5,Th4; hence thesis by A1,A6,Th3; end; suppose A7: not i in dom M; A8: width M=n by MATRIX_1:24; DelLine(M,i)=M by A7,FINSEQ_3:104; hence thesis by A1,A8,Th3; end; end; definition let G be non empty multMagma; let B be Function of [:the carrier of G,NAT:], the carrier of G; let g be Element of G, i be Nat; redefine func B.(g,i) -> Element of G; coherence proof reconsider i as Element of NAT by ORDINAL1:def 12; B.(g,i) is Element of G; hence thesis; end; end; theorem Th6: card Permutations n = n! proof set P = Permutations(n); reconsider N=n as Element of NAT by ORDINAL1:def 12; set X=finSeg N; set PER={F where F is Function of X,X:F is Permutation of X}; A1: P c= PER proof let x; assume x in P; then x is Permutation of X by MATRIX_2:def 9; hence thesis; end; PER c= P proof let x; assume x in PER; then ex F be Function of X,X st x=F & F is Permutation of X; hence thesis by MATRIX_2:def 9; end; then P=PER by A1,XBOOLE_0:def 10; hence card P = card X! by CARD_FIN:8 .= n! by FINSEQ_1:57; end; theorem Th7: for i,j st i in Seg (n+1) & j in Seg (n+1) holds card {p1: p1.i = j} = n! proof let i,j such that A1: i in Seg (n+1) and A2: j in Seg (n+1); reconsider N = n as Element of NAT by ORDINAL1:def 12; set n1=N+1; set X=finSeg n1; set Y=X\{j}; A3: Y\/{j}=X by A2,ZFMISC_1:116; set X9=X\{i}; set P1=Permutations n1; set F={p where p is Element of P1:p.i=j}; set F9={f where f is Function of X9\/{i},Y\/{j}:f is one-to-one & f.i=j}; A4: X9\/{i}=X by A1,ZFMISC_1:116; A5: F9 c= F proof let x; assume x in F9; then consider f be Function of X,X such that A6: f=x and A7: f is one-to-one and A8: f.i=j by A4,A3; card X=card X; then f is onto by A7,STIRL2_1:60; then f in P1 by A7,MATRIX_2:def 9; hence thesis by A6,A8; end; F c= F9 proof let x; assume x in F; then consider p be Element of P1 such that A9: x=p and A10: p.i=j; reconsider p as Permutation of X by MATRIX_2:def 9; p.i=j by A10; hence thesis by A4,A3,A9; end; then A11: F=F9 by A5,XBOOLE_0:def 10; A12: card X=n1 by FINSEQ_1:57; A13: not j in Y by ZFMISC_1:56; then A14: card X=card Y+1 by A3,CARD_2:41; A15: not i in X9 by ZFMISC_1:56; then A16: card X=card X9+1 by A4,CARD_2:41; then Y is empty implies X9 is empty by A14; hence card {p1: p1.i = j} = card {f where f is Function of X9,Y:f is one-to-one} by A15,A13,A11,CARD_FIN:5 .= card Y!/((card Y-'card X9)!) by A16,A14,CARD_FIN:7 .= card Y!/1 by A16,A14,NEWTON:12,XREAL_1:232 .= n! by A14,A12; end; theorem Th8: for K be Fanoian Field for p2 for X,Y be Element of Fin 2Set Seg (n+2) st Y={s:s in X & Part_sgn(p2,K).s = -1_K} holds (the multF of K) $$ (X, Part_sgn(p2,K)) = power(K).(-1_K,card Y) proof let K be Fanoian Field; let p2; set n2=n+2; let X,Y be Element of Fin 2Set Seg n2 such that A1: Y={s:s in X & Part_sgn(p2,K).s = -1_K}; reconsider ID = id Seg n2 as Element of Permutations(n2) by MATRIX_2:def 9; set Y9= {s:s in X & Part_sgn(p2,K).s <> Part_sgn(ID,K).s}; A2: for x st x in X holds Part_sgn(ID,K).x = 1_K proof A3: X c= 2Set Seg n2 by FINSUB_1:def 5; let x; assume x in X; then consider i,j be Nat such that A4: i in Seg n2 and A5: j in Seg n2 and A6: i < j and A7: x = {i,j} by A3,MATRIX11:1; A8: ID.j=j by A5,FUNCT_1:17; ID.i=i by A4,FUNCT_1:17; hence thesis by A4,A5,A6,A7,A8,MATRIX11:def 1; end; A9: Y9 c= Y proof let y; assume y in Y9; then consider s such that A10: y=s and A11: s in X and A12: Part_sgn(p2,K).s <> Part_sgn(ID,K).s; Part_sgn(ID,K).s=1_K by A2,A11; then Part_sgn(p2,K).s =-1_K by A12,MATRIX11:5; hence thesis by A1,A10,A11; end; Y c= Y9 proof let y; A13: 1_K<>-1_K by MATRIX11:22; assume y in Y; then consider s such that A14: s=y and A15: s in X and A16: Part_sgn(p2,K).s = -1_K by A1; Part_sgn(ID,K).s=1_K by A2,A15; hence thesis by A14,A15,A16,A13; end; then A17: Y=Y9 by A9,XBOOLE_0:def 10; per cases by NAT_D:12; suppose A18: card Y mod 2 = 0; then consider t be Nat such that A19: card Y = 2 * t + 0 and 0 < 2 by NAT_D:def 2; t is Element of NAT by ORDINAL1:def 12; hence power(K).(-1_K,card Y)=1_K by A19,HURWITZ:4 .= (the multF of K) $$ (X,Part_sgn(ID,K)) by A2,MATRIX11:4 .= (the multF of K) $$ (X,Part_sgn(p2,K)) by A17,A18,MATRIX11:7; end; suppose A20: card Y mod 2 = 1; then consider t be Nat such that A21: card Y = 2 * t + 1 and 1 < 2 by NAT_D:def 2; t is Element of NAT by ORDINAL1:def 12; hence power(K).(-1_K,card Y)=-1_K by A21,HURWITZ:4 .= -(the multF of K) $$ (X,Part_sgn(ID,K)) by A2,MATRIX11:4 .= (the multF of K) $$ (X,Part_sgn(p2,K)) by A17,A20,MATRIX11:7; end; end; theorem Th9: for K be Fanoian Field for p2,i,j st i in Seg (n+2) & p2.i=j ex X be Element of Fin 2Set Seg (n+2) st X = {{N,i} : {N,i} in 2Set Seg (n+2)} & ( the multF of K) $$ (X,Part_sgn(p2,K)) = power(K).(-1_K,i+j) proof let K be Fanoian Field; let p2,i,j such that A1: i in Seg (n+2) and A2: p2.i=j; reconsider N=n as Element of NAT by ORDINAL1:def 12; set n2=N+2; reconsider p29=p2 as Permutation of finSeg n2 by MATRIX_2:def 9; A3: rng p29=Seg n2 by FUNCT_2:def 3; 1<=i by A1,FINSEQ_1:1; then reconsider i1=i-1 as Element of NAT by NAT_1:21; deffunc F(set)={$1,i}; set Ui=(finSeg n2)\(Seg i); set Li=finSeg i1; set SS=2Set Seg(n+2); set X={{k,i} where k is Element of NAT :{k,i} in 2Set Seg(n+2)}; A4: X c= SS proof let x; assume x in X; then ex k being Element of NAT st x={k,i} & {k,i} in 2Set Seg n2; hence thesis; end; then reconsider X as Element of Fin SS by FINSUB_1:def 5; set Y={s:s in X & Part_sgn(p2,K).s=-1_K}; A5: Y c= X proof let x; assume x in Y; then ex s st s=x & s in X & Part_sgn(p2,K).s=-1_K; hence thesis; end; then A6: Y c= SS by A4,XBOOLE_1:1; dom p29=Seg n2 by FUNCT_2:52; then A7: p2.i in rng p2 by A1,FUNCT_1:def 3; then 1<= j by A2,A3,FINSEQ_1:1; then reconsider j1=j-1 as Element of NAT by NAT_1:21; reconsider Y as Element of Fin SS by A6,FINSUB_1:def 5; consider f be Function such that A8: dom f = Li\/Ui & for x st x in Li\/Ui holds f.x = F(x) from FUNCT_1 :sch 3; A9: f"Y c= dom f by RELAT_1:132; then reconsider fY=f"Y as finite set by A8; A10: Li\/Ui c= Seg n2\{i} proof let x such that A11: x in Li\/Ui; per cases by A11,XBOOLE_0:def 3; suppose A12: x in Li; A13: i<=n2 by A1,FINSEQ_1:1; consider k being Element of NAT such that A14: x=k and A15: 1<=k and A16: k<=i1 by A12; A17: i1i by TARSKI:def 1; f.x1=F(x1) by A8,A21; then x1 in {i,x2} by A23,A24,TARSKI:def 2; hence thesis by A25,TARSKI:def 2; end; then f is one-to-one by FUNCT_1:def 4; then (f.:fY),(fY) are_equipotent by A9,CARD_1:33; then A26: card (f.:fY) = card fY by CARD_1:5; finSeg n2\{i} c= Li\/Ui proof let x such that A27: x in finSeg n2\{i}; x in finSeg n2 by A27; then consider k being Element of NAT such that A28: x=k and A29: 1<=k and A30: k<=n2; not k in {i} by A27,A28,XBOOLE_0:def 5; then A31: k<>i by TARSKI:def 1; per cases by A31,XXREAL_0:1; suppose ki1+1; then A32: not x in Seg i by A28,FINSEQ_1:1; x in Seg n2 by A28,A29,A30; then x in Ui by A32,XBOOLE_0:def 5; hence thesis by XBOOLE_0:def 3; end; end; then A33: finSeg n2\{i}=Li\/Ui by A10,XBOOLE_0:def 10; A34: rng f c= X proof let x; assume x in rng f; then consider y such that A35: y in dom f and A36: f.y=x by FUNCT_1:def 3; y in finSeg n2 by A33,A8,A35; then consider k being Element of NAT such that A37: k=y and A38: 1<= k and A39: k<=n2; A40: f.k={i,k} by A8,A35,A37; not y in {i} by A10,A8,A35,XBOOLE_0:def 5; then i<>k by A37,TARSKI:def 1; then A41: kp2.k by A1,A50,A55,FUNCT_1:def 4; A57: f.k=F(k) by A8,A52,A51; then F(k) in X by A34,A53; then ex m being Element of NAT st F(k)={m,i} & {m,i} in SS; then Part_sgn(p2,K).{k,i}<>-1_K by A34,A54,A53,A57; then p2.k <= p2.i by A1,A50,A55,MATRIX11:def 1; then p2.k < j1+1 by A2,A56,XXREAL_0:1; then A58: p2.k <= j1 by NAT_1:13; A59: rng p29=Seg n2 by FUNCT_2:def 3; p2.k in rng p29 by A43,A46,FUNCT_1:def 3; then 1<=p2.k by A59,FINSEQ_1:1; hence thesis by A45,A46,A58,FINSEQ_1:1; end; suppose A60: k in (Ui/\f"Y); then k in Ui by XBOOLE_0:def 4; then A61: not k in Seg i by XBOOLE_0:def 5; 1<= k by A60,FINSEQ_1:1; then A62: ip2.k by A1,A60,A62,FUNCT_1:def 4; 1_K<>-1_K by MATRIX11:22; then p2.i>=p2.k by A1,A60,A65,A66,A62,MATRIX11:def 1; then p2.k i by A83,SGRAPH1:10; A85: m in Seg n2 by A83,SGRAPH1:10; m in {x,i} by A82,TARSKI:def 2; then A86: m=x by A84,TARSKI:def 2; per cases by A83,SGRAPH1:10,XXREAL_0:1; suppose A87: mi; then not m in Seg i by FINSEQ_1:1; then A92: x in Ui by A86,A85,XBOOLE_0:def 5; Part_sgn(p2,K).{m,i}=-1_K by A1,A2,A72,A75,A76,A77,A86,A91,MATRIX11:def 1 ; then A93: f.x in Y by A34,A80,A81,A82,A83; x in dom f by A33,A8,A76,A78,XBOOLE_0:def 5; then x in f"Y by A93,FUNCT_1:def 7; then x in Ui/\f"Y by A92,XBOOLE_0:def 4; then x in (Li\f"Y)\/(Ui/\f"Y) by XBOOLE_0:def 3; hence thesis by A76,A77,FUNCT_1:def 6; end; end; then A94: Seg j1 = p29.:((Li\f"Y)\/(Ui/\f"Y)) by A42,XBOOLE_0:def 10; A95: Seg n2 = dom p29 by FUNCT_2:52; A96: Li\f"Y=Li\(f"Y/\Li) by XBOOLE_1:47; i1i by A99,SGRAPH1:10; then A100: not k in {i} by TARSKI:def 1; k in Seg n2 by A99,SGRAPH1:10; then A101: k in Li\/Ui by A33,A100,XBOOLE_0:def 5; then f.k=F(k) by A8; hence thesis by A8,A98,A101,FUNCT_1:def 3; end; then X = rng f by A34,XBOOLE_0:def 10; then A102: f.:fY = Y by A5,FUNCT_1:77; (Li/\f"Y)\/(Ui/\f"Y)=(dom f)/\f"Y by A8,XBOOLE_1:23; then A103: (Li/\f"Y)\/(Ui/\f"Y) = f"Y by RELAT_1:132,XBOOLE_1:28; A104: Ui/\f"Y c= Ui by XBOOLE_1:17; then (Li\f"Y)\/(Ui/\f"Y) c= finSeg n2\{i} by A33,XBOOLE_1:13; then finSeg j1,(Li\f"Y)\/(Ui/\f"Y) are_equipotent by A95,A94,CARD_1:33 ,XBOOLE_1:1; then A105: card (finSeg j1) = card ((Li\f"Y)\/(Ui/\f"Y)) by CARD_1:5 .= card (Li\(f"Y/\Li)) +card (Ui/\f"Y) by A97,A104,A96,CARD_2:40 ,XBOOLE_1:64 .= (card Li -card (f"Y/\Li))+card (Ui/\f"Y) by CARD_2:44,XBOOLE_1:17; per cases; suppose j>i; then reconsider ji=j-i as Element of NAT by NAT_1:21; card Y = card (Li/\fY)+card (finSeg j1)-card Li+card (fY/\Li) by A97,A70 ,A104,A103,A26,A102,A105,CARD_2:40,XBOOLE_1:64 .= 2*card (Li/\fY) +card (finSeg j1)-card Li .= 2*card (Li/\fY)+j1-card Li by FINSEQ_1:57 .= 2*card (Li/\fY)+j1-i1 by FINSEQ_1:57 .= 2*card (Li/\fY)+ji; hence (the multF of K) $$ (X,Part_sgn(p2,K)) = P.(-1_K,2*card (Li/\fY)+ji) by Th8 .= P.(-1_K,2*card (Li/\fY)) * P.(-1_K,ji) by HURWITZ:3 .= 1_K * P.(-1_K,ji) by HURWITZ:4 .= P.(-1_K,2*I)*P.(-1_K,ji) by HURWITZ:4 .= P.(-1_K,2*i+ji) by HURWITZ:3 .= P.(-1_K,i+j); end; suppose j<=i; then reconsider ij=i-j as Element of NAT by NAT_1:21; card Y = (card Li+card (Ui/\fY)-card (finSeg j1))+ card(Ui/\fY) by A97,A70 ,A104,A103,A26,A102,A105,CARD_2:40,XBOOLE_1:64 .= 2*card (Ui/\fY)-card (finSeg j1)+card Li .= 2*card (Ui/\fY)-j1+card Li by FINSEQ_1:57 .= 2*card (Ui/\fY)-j1+i1 by FINSEQ_1:57 .= 2*card (Ui/\fY)+ij; hence (the multF of K) $$ (X,Part_sgn(p2,K)) = P.(-1_K,2*card (Ui/\fY)+ij) by Th8 .= P.(-1_K,2*card (Ui/\fY)) * P.(-1_K,ij) by HURWITZ:3 .= 1_K * P.(-1_K,ij) by HURWITZ:4 .= P.(-1_K,2*J)*P.(-1_K,ij) by HURWITZ:4 .= P.(-1_K,2*j+ij) by HURWITZ:3 .= P.(-1_K,i+j); end; end; theorem Th10: for i,j st i in Seg (n+1) & n >= 2 ex Proj be Function of 2Set Seg n, 2Set Seg(n+1) st rng Proj = 2Set Seg(n+1)\{{N,i}:{N,i} in 2Set Seg(n+1)} & Proj is one-to-one & for k,m st k= i & k < i implies Proj.{k,m} = {k,m+1} ) & (m >= i & k >= i implies Proj.{k,m} = {k+1,m+1}) proof let i,j be Nat such that A1: i in Seg (n+1) and A2: n>=2; defpred P[set,set] means for k,m being Nat st {k,m}=$1 & k= i & k= i & k >= i implies $2={k+1,m+1}); set X={{N,i}:{N,i} in 2Set Seg(n+1)}; set SS=2Set Seg(n); set n1=n+1; set SS1=2Set Seg n1; A3: for k,m be Nat st {k,m} in X holds k=i or m=i proof let k,m be Nat; assume {k,m} in X; then consider m1 be Element of NAT such that A4: {k,m}={m1,i} and {m1,i} in SS1; i in {i,m1} by TARSKI:def 2; hence thesis by A4,TARSKI:def 2; end; A5: for x st x in SS ex y st y in SS1\X & P[x,y] proof n<=n+1 by NAT_1:11; then A6: Seg n c= Seg n1 by FINSEQ_1:5; reconsider N=n as Element of NAT by ORDINAL1:def 12; let x; assume x in SS; then consider k,m be Nat such that A7: k in Seg n and A8: m in Seg n and A9: k < m and A10: x={k,m} by MATRIX11:1; A11: m+1 in Seg (N+1) by A8,FINSEQ_1:60; reconsider e = k as Element of NAT by ORDINAL1:def 12; A12: e+1 in Seg(N+1) by A7,FINSEQ_1:60; per cases; suppose A13: m=i & ki by A16,NAT_1:13; then A19: not {k,m+1} in X by A3,A16; m+1>k by A9,NAT_1:13; then {k,m+1} in SS1 by A7,A6,A11,MATRIX11:1; then {k,m+1} in SS1\X by A19,XBOOLE_0:def 5; hence thesis by A10,A17; end; suppose m=i; hence thesis by A9,XXREAL_0:2; end; suppose A20: m>=i & k>=i; A21: P[{k,m},{k+1,m+1}] proof let k9,m9 be Nat such that A22: {k9,m9}={k,m} and A23: k9i by A20,NAT_1:13; m+1>k+1 by A9,XREAL_1:8; then A25: {k+1,m+1} in SS1 by A11,A12,MATRIX11:1; m+1>i by A20,NAT_1:13; then not {k+1,m+1} in X by A3,A24; then {k+1,m+1} in SS1\X by A25,XBOOLE_0:def 5; hence thesis by A10,A21; end; end; consider f be Function of SS,SS1\X such that A26: for x st x in SS holds P[x,f.x] from FUNCT_2:sch 1(A5); ex y st y in SS1\X & P[{1,2},y] by A2,A5,MATRIX11:3; then reconsider SSX=SS1\X as non empty set; reconsider f as Function of SS,SSX; A27: SSX c= rng f proof let x such that A28: x in SSX; consider k,m be Nat such that A29: k in Seg n1 and A30: m in Seg n1 and A31: k < m and A32: x={k,m} by A28,MATRIX11:1; A33: k<>i & m<>i proof assume k=i or m=i; then x in X by A28,A29,A30,A32; hence thesis by A28,XBOOLE_0:def 5; end; A34: 1<=m by A30,FINSEQ_1:1; 1<=k by A29,FINSEQ_1:1; then reconsider k1=k-1,m1=m-1 as Element of NAT by A34,NAT_1:21; reconsider m9=m,k9=k as Element of NAT by ORDINAL1:def 12; per cases by A33,XXREAL_0:1; suppose A35: ki & mi; 1<=i by A1,FINSEQ_1:1; then A43: 1< m1+1 by A42,XXREAL_0:2; then A44: i<=m1 by A42,NAT_1:13; then A45: ki & m>i; (k1+1) <= n+1 by A29,FINSEQ_1:1; then k1=i) & m2>=i; then A73: f.x2={k2,m2+1} or f.x2={k2+1,m2+1} by A26,A65,A67,A68; f.x1={k1,m1} by A26,A64,A69,A70,A72; then (k1=k2 or k1=m2+1) & (m1=k2 or m1=m2+1) or (k1=k2+1 or k1=m2+1)&( m1=k2+1 or m1=m2+1) by A66,A73,ZFMISC_1:6; hence thesis by A69,A72,NAT_1:13; end; suppose A74: k1=i & k2=i; then A75: f.x2={k2,m2+1} by A26,A65,A67,A68; A76: f.x1={k1,m1+1} by A26,A64,A69,A70,A74; then A77: m1+1=k2 or m1+1=m2+1 by A66,A75,ZFMISC_1:6; k1=k2 or k1=m2+1 by A66,A76,A75,ZFMISC_1:6; hence thesis by A70,A68,A74,A77,NAT_1:13; end; suppose A78: k1=i & ( k2>=i & m2>=i or k2=i & m1=i & m2=i & m1>=i & k2>=i & m2>=i; then A81: f.x2={k2+1,m2+1} by A26,A65,A67,A68; A82: f.x1={k1+1,m1+1} by A26,A64,A69,A70,A80; then A83: m1+1=k2+1 or m1+1=m2+1 by A66,A81,ZFMISC_1:6; k1+1=k2+1 or k1+1=m2+1 by A66,A82,A81,ZFMISC_1:6; hence thesis by A69,A70,A68,A83; end; suppose A84: k1>=i & m1>=i & ( k2=i ); then A85: f.x2={k2,m2} or f.x2={k2,m2+1} by A26,A65,A67,A68; f.x1={k1+1,m1+1} by A26,A64,A69,A70,A84; then (k1+1=k2 or k1+1=m2) & (m1+1=k2 or m1+1=m2) or (k1+1=k2 or k1+1=m2 +1)&(m1+1=k2 or m1+1=m2+1) by A66,A85,ZFMISC_1:6; hence thesis by A69,A84,NAT_1:13; end; end; hence thesis by A26,A27,A62,FUNCT_2:19,XBOOLE_0:def 10; end; theorem Th11: n < 2 implies for p be Element of Permutations n holds p is even & p=idseq n proof assume A1: n<2; let p be Element of Permutations n; reconsider P=p as Permutation of Seg n by MATRIX_2:def 9; now per cases by A1,NAT_1:23; suppose A2: n=0; then A3: Seg n={}; A4: len Permutations(n)=n by MATRIX_2:18; P={} by A2; hence thesis by A4,A3,MATRIX_2:25,RELAT_1:55; end; suppose A5: n=1; A6: len Permutations(n)=n by MATRIX_2:18; P=id Seg n by A5,MATRIX_2:19,TARSKI:def 1; hence thesis by A6,MATRIX_2:25; end; end; hence thesis; end; theorem Th12: for X,Y,D be non empty set for f be Function of X,Fin Y, g be Function of Fin Y,D, F be BinOp of D st (for A,B be Element of Fin Y st A misses B holds F.(g.A,g.B) = g.(A \/ B)) & F is commutative associative & F is having_a_unity & g.{} = the_unity_wrt F for I be Element of Fin X st for x,y st x in I & y in I & f.x meets f.y holds x = y holds F $$ (I,g*f) = F $$ (f.:I,g) & F $$ (f.:I,g) = g.union (f.:I) & union (f.:I) is Element of Fin Y proof let X,Y,D be non empty set; let f be Function of X,Fin Y, g be Function of Fin Y,D, F be BinOp of D such that A1: for A,B be Element of Fin Y st A misses B holds F.(g.A,g.B)=g.(A \/ B) and A2: F is commutative associative and A3: F is having_a_unity and A4: g.{}=the_unity_wrt F; defpred P[set] means for I be Element of Fin X st I=$1 & for x,y st x in I & y in I & f.x meets f.y holds x=y holds F $$ (I,g*f)=F $$ (f.:I,g) & F $$ (f.:I, g)= g.union (f.:I) & union (f.:I) is Element of Fin Y; A5: for I be (Element of Fin X), i be Element of X holds P[I] & not i in I implies P[I \/ {i}] proof let A be (Element of Fin X), a be Element of X such that A6: P[A] and A7: not a in A; let I be Element of Fin X such that A8: A\/{a}=I and A9: for x,y st x in I & y in I & f.x meets f.y holds x=y; A10: for x,y st x in A & y in A & f.x meets f.y holds x=y proof let x,y such that A11: x in A and A12: y in A and A13: f.x meets f.y; A c= I by A8,XBOOLE_1:7; hence thesis by A9,A11,A12,A13; end; then A14: F $$ (A,g*f)=F $$ (f.:A,g) by A6; A15: union (f.:A) is Element of Fin Y by A6,A10; dom f=X by FUNCT_2:def 1; then Im(f,a)={f.a} by FUNCT_1:59; then A16: f.:I=f.:A\/{f.a} by A8,RELAT_1:120; A17: F $$ (f.:A,g)=g.union(f.:A) by A6,A10; dom (g*f)=X by FUNCT_2:def 1; then A18: g.(f.a)=(g*f).a by FUNCT_1:12; per cases; suppose A19: f.a is non empty or not f.a in f.:A; not f.a in f.:A proof A20: A c= I by A8,XBOOLE_1:7; A21: {a} c= I by A8,XBOOLE_1:7; A22: a in {a} by TARSKI:def 1; assume A23: f.a in f.:A; then consider x such that x in dom f and A24: x in A and A25: f.x=f.a by FUNCT_1:def 6; f.x meets f.a by A19,A23,A25,XBOOLE_1:66; hence thesis by A7,A9,A24,A22,A21,A20; end; then A26: F $$ (f.:I,g)=F.(F$$(f.:A,g),(g*f).a) by A2,A3,A16,A18,SETWOP_2:2; A27: f.a c= Y by FINSUB_1:def 5; union (f.:A) c= Y by A15,FINSUB_1:def 5; then A28: (union (f.:A))\/f.a c= Y by A27,XBOOLE_1:8; now let x; assume x in f.:A; then A29: ex y st y in dom f & y in A & f.y=x by FUNCT_1:def 6; A30: a in {a} by TARSKI:def 1; A31: A c= I by A8,XBOOLE_1:7; A32: {a} c= I by A8,XBOOLE_1:7; assume x meets f.a; hence contradiction by A7,A9,A29,A30,A32,A31; end; then A33: union(f.:A) misses f.a by ZFMISC_1:80; union (f.:I) = union (f.:A)\/union {f.a} by A16,ZFMISC_1:78 .= union (f.:A)\/f.a by ZFMISC_1:25; hence thesis by A1,A2,A3,A7,A8,A14,A17,A15,A18,A26,A28,A33,FINSUB_1:def 5 ,SETWOP_2:2; end; suppose A34: f.a is empty & f.a in f.:A; then A35: f.:A\/{f.a}=f.:A by ZFMISC_1:40; F $$ (I,g*f) = F.(F $$ (f.:A,g),the_unity_wrt F) by A2,A3,A4,A7,A8,A14 ,A18,A34,SETWOP_2:2 .= F $$ (f.:I,g) by A3,A16,A35,SETWISEO:15; hence thesis by A6,A10,A16,A35; end; end; A36: P[{}.X] proof A37: {}c= Y by XBOOLE_1:2; let I be Element of Fin X such that A38: {}.X=I and for x,y st x in I & y in I & f.x meets f.y holds x=y; A39: f.:I={}.(Fin Y) by A38; F $$ (I,g*f)=g.{} by A2,A3,A4,A38,SETWISEO:31; hence thesis by A2,A3,A4,A39,A37,FINSUB_1:def 5,SETWISEO:31,ZFMISC_1:2; end; for I be Element of Fin X holds P[I] from SETWISEO:sch 2(A36,A5); hence thesis; end; begin :: Auxiliary notions definition let i,j,n be Nat; let K; let M be Matrix of n,K; assume that A1: i in Seg n and A2: j in Seg n; func Delete(M,i,j) -> Matrix of n-'1,K equals :Def1: Deleting(M,i,j); coherence proof set D=Deleting(M,i,j); A3: width M=n by MATRIX_1:24; len M=n by MATRIX_1:24; then dom M=Seg n by FINSEQ_1:def 3; then A4: len D=n-'1 by A1,Th2; per cases; suppose n-'1=0; then dom D = Seg 0 by A4,FINSEQ_1:def 3; then for f st f in rng D holds len f = n-'1 by RELAT_1:42; hence thesis by A4,MATRIX_1:def 2; end; suppose A5: n-'1>0; width Deleting(M,i,j)= n-' 1 by A2,A3,Th5; hence thesis by A4,A5,MATRIX_1:20; end; end; end; theorem Th13: for i,j st i in Seg n & j in Seg n for k,m st k in Seg (n-'1) & m in Seg (n-'1) holds (k < i & m < j implies Delete(M,i,j)*(k,m) = M*(k,m) )& ( k < i & m >= j implies Delete(M,i,j)*(k,m) = M*(k,m+1) )& (k >= i & m < j implies Delete(M,i,j)*(k,m) = M*(k+1,m) )& (k >= i & m >= j implies Delete(M,i, j)*(k,m) = M*(k+1,m+1)) proof let i,j such that A1: i in Seg n and A2: j in Seg n; set DM=Delete(M,i,j); A3: Deleting(M,i,j)=DM by A1,A2,Def1; n>0 by A1; then reconsider n9=n-1 as Element of NAT by NAT_1:20; set DL=DelLine(M,i); let k,m such that A4: k in Seg (n-'1) and A5: m in Seg (n-'1); A6: n-'1=n9 by XREAL_0:def 2; then A7: k+1 in Seg (n9+1) by A4,FINSEQ_1:60; reconsider I=i, J=j, K=k, U = m as Element of NAT by ORDINAL1:def 12; n9<=n9+1 by NAT_1:11; then A8: Seg n9 c= Seg n by FINSEQ_1:5; A9: len M=n by MATRIX_1:24; then A10: dom M=Seg n by FINSEQ_1:def 3; then len DL=n9 by A1,A6,A9,Th1; then A11: dom DL=Seg n9 by FINSEQ_1:def 3; then A12: Deleting(M,i,j).k=Del(Line(DL,k),j) by A4,A6,MATRIX_2:def 5; len DM=n9 by A6,MATRIX_1:24; then dom DM=Seg n9 by FINSEQ_1:def 3; then A13: DM.k=Line(DM,k) by A4,A6,MATRIX_2:16; width DM=n9 by A6,MATRIX_1:24; then A14: Line(DM,k).m=DM*(k,m) by A5,A6,MATRIX_1:def 7; A15: Line(DL,k)=DL.k by A4,A6,A11,MATRIX_2:16; A16: m+1 in Seg (n9+1) by A5,A6,FINSEQ_1:60; A17: K>=I implies (U=J implies DM*(K,U)=M* (K+1,U+1)) proof assume A18: K >=I; K<=n9 by A4,A6,FINSEQ_1:1; then A19: DL.K=M.(K+1) by A1,A9,A10,A7,A18,FINSEQ_3:111; A20: M.(K+1)=Line(M,K+1) by A10,A7,MATRIX_2:16; thus U=J; A23: U<=n9 by A5,A6,FINSEQ_1:1; A24: width M=n by MATRIX_1:24; A25: len Line(DL,K)=width M by A15,A19,A20,MATRIX_1:def 7; then J in dom Line(DL,K) by A2,A24,FINSEQ_1:def 3; then DM*(K,U)=Line(M,K+1).(U+1) by A12,A3,A13,A14,A15,A7,A19,A20,A22,A25,A23, FINSEQ_3:111,MATRIX_1:24; hence thesis by A16,A24,MATRIX_1:def 7; end; K=J implies DM*(K,U)=M*(K, U+1)) proof assume K < I; then A26: DL.K=M.K by FINSEQ_3:110; A27: M.K=Line(M,K) by A4,A6,A10,A8,MATRIX_2:16; thus U=J; A31: U<=n9 by A5,A6,FINSEQ_1:1; A32: width M=n by MATRIX_1:24; A33: len Line(DL,K)=width M by A15,A26,A27,MATRIX_1:def 7; then J in dom Line(DL,K) by A2,A32,FINSEQ_1:def 3; then DM*(K,U)=Line(M,K).(U+1) by A12,A3,A13,A14,A15,A7,A26,A27,A30,A33,A31, FINSEQ_3:111,MATRIX_1:24; hence thesis by A16,A32,MATRIX_1:def 7; end; hence thesis by A17; end; theorem Th14: for i,j st i in Seg n & j in Seg n holds Delete(M,i,j)@ = Delete (M@,j,i) proof let i,j such that A1: i in Seg n and A2: j in Seg n; n>0 by A1; then reconsider n1=n-1 as Element of NAT by NAT_1:20; set X1=Seg n; reconsider MT=M@ as Matrix of n,K; set D=Delete(M,i,j); set n9=n-'1; reconsider I=i as Element of NAT by ORDINAL1:def 12; reconsider DT=D@ as Matrix of n9,K; set D9=Delete(MT,j,i); set X=Seg n9; A3: n1+1-'1=n1 by NAT_D:34; now n9<=n by NAT_D:35; then A4: X c= X1 by FINSEQ_1:5; let k,m be Nat such that A5: [k,m] in Indices DT; [m,k] in Indices D by A5,MATRIX_1:def 6; then A6: DT*(k,m)=D*(m,k) by MATRIX_1:def 6; reconsider k9=k,m9=m as Element of NAT by ORDINAL1:def 12; A7: Indices DT=[:X,X:] by MATRIX_1:24; then A8: k in X by A5,ZFMISC_1:87; then A9: k+1 in X1 by A3,FINSEQ_1:60; A10: Indices M=[:X1,X1:] by MATRIX_1:24; A11: m in X by A5,A7,ZFMISC_1:87; then A12: m+1 in X1 by A3,FINSEQ_1:60; per cases; suppose A13: m9=j; then A17: D9*(k,m)=MT*(k+1,m) by A1,A2,A8,A11,Th13; A18: [m,k+1] in Indices M by A11,A4,A9,A10,ZFMISC_1:87; D*(m,k)=M*(m,k+1) by A1,A2,A8,A11,A16,Th13; hence DT*(k,m)=D9*(k,m) by A6,A18,A17,MATRIX_1:def 6; end; suppose A19: m9>=I & k9=I & k9>=j; then A23: D9*(k,m)=MT*(k+1,m+1) by A1,A2,A8,A11,Th13; A24: [m+1,k+1] in Indices M by A9,A12,A10,ZFMISC_1:87; D*(m,k)=M*(m+1,k+1) by A1,A2,A8,A11,A22,Th13; hence DT*(k,m)=D9*(k,m) by A6,A24,A23,MATRIX_1:def 6; end; end; hence thesis by MATRIX_1:27; end; theorem Th15: for f be FinSequence of K, i,j st i in Seg n & j in Seg n holds Delete(M,i,j) = Delete(RLine(M,i,f),i,j) proof let f be FinSequence of K, i,j such that A1: i in Seg n and A2: j in Seg n; A3: Delete(M,i,j) = Deleting(M,i,j) by A1,A2,Def1; A4: Delete(RLine(M,i,f),i,j) = Deleting(RLine(M,i,f),i,j) by A1,A2,Def1; reconsider f9=f as Element of (the carrier of K)* by FINSEQ_1:def 11; reconsider I=i as Element of NAT by ORDINAL1:def 12; per cases; suppose len f=width M; then RLine(M,I,f)=Replace(M,i,f9) by MATRIX11:29; hence thesis by A3,A4,COMPUT_1:3; end; suppose len f<>width M; hence thesis by MATRIX11:def 3; end; end; definition let c, n, m, D; let M be Matrix of n,m,D; let pD be FinSequence of D; func ReplaceCol(M,c,pD) -> Matrix of n,m,D means :Def2: len it = len M & width it = width M & for i,j st [i,j] in Indices M holds (j <> c implies it*(i, j) = M*(i,j)) & (j = c implies it*(i,c) = pD.i) if len pD = len M otherwise it = M; consistency; existence proof thus len pD=len M implies ex M1 be Matrix of n,m,D st len M1 = len M & width M1 = width M & for i,j st [i,j] in Indices M holds (j <> c implies M1*(i, j) = M*(i,j)) & (j = c implies M1*(i,c) = pD.i) proof reconsider M9=M as Matrix of len M,width M,D by MATRIX_2:7; reconsider V = n, U = m as Element of NAT by ORDINAL1:def 12; defpred P[set,set,set] means for i,j st i=$1 & j=$2 holds (j <>c implies $3 = M*(i,j)) & (j = c implies $3 = pD.i); assume A1: len pD=len M; A2: for i,j be Nat st [i,j] in [:Seg V, Seg U:] ex x being Element of D st P[i,j,x] proof let i,j be Nat such that A3: [i,j] in [:Seg V, Seg U:]; now per cases; case A4: j=c; A5: rng pD c= D by FINSEQ_1:def 4; len M=n by MATRIX_1:def 2; then i in Seg len pD by A1,A3,ZFMISC_1:87; then i in dom pD by FINSEQ_1:def 3; then A6: pD.i in rng pD by FUNCT_1:def 3; P[i,j,pD.i] by A4; hence thesis by A6,A5; end; case j<>c; then P[i,j,M*(i,j)]; hence thesis; end; end; hence thesis; end; consider M1 be Matrix of V,U,D such that A7: for i,j be Nat st [i,j] in Indices M1 holds P[i,j,M1*(i,j)] from MATRIX_1:sch 2(A2); reconsider M1 as Matrix of n,m,D; take M1; A8: now per cases; suppose A9: n=0; then len M1=0 by MATRIX_1:def 2; then A10: width M1=0 by MATRIX_1:def 3; len M=0 by A9,MATRIX_1:def 2; hence len M = len M1 & width M1=width M by A9,A10,MATRIX_1:def 2 ,def 3; end; suppose A11: n > 0; then A12: width M=m by MATRIX_1:23; len M=n by A11,MATRIX_1:23; hence len M = len M1 & width M = width M1 by A11,A12,MATRIX_1:23; end; end; Indices M9=Indices M1 by MATRIX_1:26; hence thesis by A7,A8; end; thus thesis; end; uniqueness proof let M1,M2 be Matrix of n,m,D; thus len pD=len M & (len M1 = len M & width M1 = width M & for i,j st [i,j ] in Indices M holds (j <> c implies M1*(i,j) = M*(i,j)) & (j = c implies M1*(i ,c) = pD.i))& (len M2 = len M & width M2 = width M & for i,j st [i,j] in Indices M holds (j <> c implies M2*(i,j) = M*(i,j)) & (j = c implies M2*(i,c) = pD.i)) implies M1=M2 proof assume len pD=len M; assume that A13: len M1=len M and A14: width M1=width M and A15: for i,j st [i,j] in Indices M holds (j <> c implies M1*(i,j) = M*(i, j))&(j = c implies M1*(i,c) = pD.i); assume that len M2=len M and width M2=width M and A16: for i,j st [i,j] in Indices M holds (j <> c implies M2*(i,j) = M*(i, j))&(j = c implies M2*(i,c) = pD.i); for i,j be Nat st [i,j] in Indices M1 holds M1*(i,j)=M2*(i,j) proof let i,j be Nat; assume [i,j] in Indices M1; then A17: [i,j] in Indices M by A13,A14,MATRIX_4:55; reconsider I=i,J=j as Element of NAT by ORDINAL1:def 12; A18: J=c implies M1*(I,c)=pD.I by A15,A17; A19: J<>c implies M2*(I,J)=M*(I,J) by A16,A17; J<>c implies M1*(I,J)=M*(I,J) by A15,A17; hence thesis by A16,A17,A18,A19; end; hence thesis by MATRIX_1:27; end; thus thesis; end; end; notation let c, n, m, D; let M be Matrix of n,m,D; let pD be FinSequence of D; synonym RCol(M,c,pD) for ReplaceCol(M,c,pD); end; theorem for i st i in Seg width AD holds (i = c & len pD = len AD implies Col( RCol(AD,c,pD),i) = pD) & (i <> c implies Col(RCol(AD,c,pD),i) = Col(AD,i)) proof let i such that A1: i in Seg width AD; set R=RCol(AD,c,pD); set CR=Col(R,i); thus i = c & len pD = len AD implies CR = pD proof assume that A2: i = c and A3: len pD = len AD; A4: len R = len pD by A3,Def2; A5: now let J be Nat such that A6: 1<=J and A7: J<=len pD; J in NAT by ORDINAL1:def 12; then J in Seg len pD by A6,A7; then A8: J in dom R by A4,FINSEQ_1:def 3; i in Seg width R by A1,A3,Def2; then A9: [J,c] in Indices R by A2,A8,ZFMISC_1:87; A10: Indices R=Indices AD by MATRIX_1:26; CR.J=R*(J,c) by A2,A8,MATRIX_1:def 8; hence CR.J=pD.J by A3,A9,A10,Def2; end; len CR=len pD by A4,MATRIX_1:def 8; hence thesis by A5,FINSEQ_1:14; end; set CA=Col(AD,i); A11: len AD=n by MATRIX_1:def 2; A12: len R=n by MATRIX_1:def 2; A13: len AD=len CA by MATRIX_1:def 8; assume A14: i <> c; A15: now let j be Nat such that A16: 1 <=j and A17: j <= len CA; j in NAT by ORDINAL1:def 12; then A18: j in Seg len AD by A13,A16,A17; then A19: j in dom AD by FINSEQ_1:def 3; then A20: CA.j=AD*(j,i) by MATRIX_1:def 8; j in dom R by A11,A12,A18,FINSEQ_1:def 3; then A21: CR.j=R*(j,i) by MATRIX_1:def 8; A22: [j,i] in Indices AD by A1,A19,ZFMISC_1:87; per cases; suppose len pD=len AD; hence CA.j=CR.j by A14,A20,A21,A22,Def2; end; suppose len pD<>len AD; hence CA.j=CR.j by Def2; end; end; len CR=len R by MATRIX_1:def 8; hence thesis by A11,A12,A13,A15,FINSEQ_1:14; end; theorem not c in Seg width AD implies RCol(AD,c,pD) = AD proof assume A1: not c in Seg width AD; set R=RCol(AD,c,pD); per cases; suppose A2: len pD=len AD; now let i,j be Nat such that A3: [i,j] in Indices AD; j in Seg width AD by A3,ZFMISC_1:87; hence R*(i,j) = AD*(i,j) by A1,A2,A3,Def2; end; hence thesis by MATRIX_1:27; end; suppose len pD<>len AD; hence thesis by Def2; end; end; theorem RCol(AD,c,Col(AD,c)) = AD proof set C=Col(AD,c); set R=RCol(AD,c,C); now reconsider c as Element of NAT by ORDINAL1:def 12; let i,j be Nat such that A1: [i,j] in Indices AD; A2: len C=len AD by MATRIX_1:def 8; reconsider I=i,J=j as Element of NAT by ORDINAL1:def 12; A3: i in dom AD by A1,ZFMISC_1:87; now per cases; suppose A4: c = j; hence R*(i,j) = C.I by A1,A2,Def2 .= AD*(i,j) by A3,A4,MATRIX_1:def 8; end; suppose c <> J; hence R*(i,j)=AD*(i,j) by A1,A2,Def2; end; end; hence R*(i,j)=AD*(i,j); end; hence thesis by MATRIX_1:27; end; theorem Th19: for A be Matrix of n,m,D, A9 be Matrix of m,n,D st A9 = A@ & (m= 0 implies n=0) holds ReplaceCol(A,c,pD) = ReplaceLine(A9,c,pD)@ proof let A be Matrix of n,m,D,A9 be Matrix of m,n,D such that A1: A9=A@ and A2: m=0 implies n=0; set RC=ReplaceCol(A,c,pD); set RL=ReplaceLine(A9,c,pD); now per cases; suppose A3: n=0; then 0=len A by MATRIX_1:def 2; then 0=width A by MATRIX_1:def 3 .=len A9 by A1,MATRIX_1:def 6; then m=0 by MATRIX_1:def 2; then len RL=0 by MATRIX_1:def 2; then width RL=0 by MATRIX_1:def 3; then len (RL@)=0 by MATRIX_1:def 6; then A4: RL@={}; len RC=0 by A3,MATRIX_1:def 2; hence thesis by A4; end; suppose A5: len pD <> len A & n>0; then A6: width A=m by MATRIX_1:23; then A7: width A9=len A by A1,A2,A5,MATRIX_2:10; A8: len A=n by A5,MATRIX_1:23; thus RC = A by A5,Def2 .= (A@)@ by A2,A5,A8,A6,MATRIX_2:13 .= RL@ by A1,A5,A7,MATRIX11:def 3; end; suppose A9: len pD = len A & n>0; then A10: width RL=n by A2,MATRIX_1:23; then A11: len (RL@)=n by A9,MATRIX_2:10; len RL=m by A2,A9,MATRIX_1:23; then width (RL@)=m by A9,A10,MATRIX_2:10; then reconsider RL9=RL@ as Matrix of n,m,D by A11,MATRIX_2:7; A12: len A=n by A9,MATRIX_1:23; A13: width A9=n by A2,A9,MATRIX_1:23; now A14: Indices RC=Indices A by MATRIX_1:26; A15: Indices RL=Indices A9 by MATRIX_1:26; let i,j be Nat such that A16: [i,j] in Indices RC; reconsider I=i,J=j as Element of NAT by ORDINAL1:def 12; Indices RC=Indices RL9 by MATRIX_1:26; then A17: [j,i] in Indices RL by A16,MATRIX_1:def 6; per cases; suppose A18: J=c; hence RC*(i,j) = pD.I by A9,A16,A14,Def2 .= RL*(J,I) by A9,A12,A13,A17,A15,A18,MATRIX11:def 3 .= RL9*(i,j) by A17,MATRIX_1:def 6; end; suppose A19: J<>c; hence RC*(i,j) = A*(I,J) by A9,A16,A14,Def2 .= A9*(j,i) by A1,A16,A14,MATRIX_1:def 6 .= RL*(J,I) by A9,A12,A13,A17,A15,A19,MATRIX11:def 3 .= RL9*(i,j) by A17,MATRIX_1:def 6; end; end; hence thesis by MATRIX_1:27; end; end; hence thesis; end; begin :: Permutations definition let i,n; let perm be Element of Permutations(n+1); assume A1: i in Seg (n+1); func Rem(perm,i) -> Element of Permutations n means :Def3: for k st k in Seg n holds (k= perm. i implies it.k = perm.k-1) )& (k>=i implies (perm.(k+1) < perm.i implies it.k = perm.(k+1) )& (perm.(k+1) >= perm.i implies it.k = perm.(k+1)-1)); existence proof set j=perm.i; set P = Permutations n; set p=perm; set n1 = n+1; reconsider N=n as Element of NAT by ORDINAL1:def 12; reconsider p9=p as Permutation of Seg n1 by MATRIX_2:def 9; A2: dom p9=Seg n1 by FUNCT_2:52; defpred Q[set,set] means for k st k in Seg n & $1=k holds (k=j implies $2=p.k-1))& (k>=i implies (p.(k+1)=j implies $2=p.(k+1)-1)); A3: rng p9=Seg n1 by FUNCT_2:def 3; then A4: j in Seg n1 by A1,A2,FUNCT_1:def 3; A5: for k9 be set st k9 in Seg n ex y st y in Seg n & Q[k9,y] proof let k9 be set; assume k9 in Seg n; then consider k being Element of NAT such that A6: k9=k and A7: 1<=k and A8: k <= n; A9: k=j; then p9.k<>p9.i by A1,A10,FUNCT_2:19; then A19: p.k > j by A18,XXREAL_0:1; then reconsider pk1=p.k-1 as Element of NAT by NAT_1:20; A20: Q[k9,pk1] by A6,A18; A21: pk1=1 by A4,FINSEQ_1:1; then pk1+1 > 1 by A19,XXREAL_0:2; then pk1 >= 1 by NAT_1:13; then pk1 in Seg n by A22; hence thesis by A20; end; suppose A23: k>=i & p.k1=i & p.k1>=j; then ip9.i by A1,A13,FUNCT_2:19; then A27: p.k1 > j by A26,XXREAL_0:1; then reconsider pk1=p.k1-1 as Element of NAT by NAT_1:20; A28: Q[k9,pk1] by A6,A26; A29: pk1=1 by A4,FINSEQ_1:1; then pk1+1 > 1 by A27,XXREAL_0:2; then pk1 >= 1 by NAT_1:13; then pk1 in Seg n by A30; hence thesis by A28; end; end; consider q be Function of Seg n,Seg n such that A31: for x st x in Seg n holds Q[x,q.x] from FUNCT_2:sch 1(A5); for x1,x2 be set st x1 in dom q & x2 in dom q & q.x1 = q.x2 holds x1 = x2 proof let x1,x2 be set such that A32: x1 in dom q and A33: x2 in dom q and A34: q.x1 = q.x2; A35: dom q=Seg n by FUNCT_2:52; then consider k1 be Element of NAT such that A36: x1=k1 and A37: 1<=k1 and A38: k1 <=n by A32; A39: 0+1<=k1+1 by NAT_1:13; A40: k1 < n+1 by A38,NAT_1:13; then A41: k1 in Seg n1 by A37; k1+1<=n+1 by A40,NAT_1:13; then A42: k1+1 in Seg n1 by A39; consider k2 be Element of NAT such that A43: x2=k2 and A44: 1<=k2 and A45: k2 <=n by A33,A35; A46: k2 < n+1 by A45,NAT_1:13; then A47: k2 in Seg n1 by A44; A48: 0+1<=k2+1 by NAT_1:13; k2+1<=n+1 by A46,NAT_1:13; then A49: k2+1 in Seg n1 by A48; per cases; suppose A50: k1=j; then q.k2=p.k2-1 by A31,A33,A43; then p.k1+1=p.k2 by A34,A36,A43,A51; then p.k2 <= j by A50,NAT_1:13; then p9.k2=p9.i by A52,XXREAL_0:1; hence thesis by A1,A2,A47,A52,FUNCT_1:def 4; end; suppose A53: k2>=i & p.(k2+1)=i & p.(k2+1)>=j; then p.k1=p.(k2+1)-1 by A31,A33,A34,A36,A43,A51; then p.k1+1=p.(k2+1); then p.(k2+1)<=j by A50,NAT_1:13; then p9.(k2+1) = p.i by A54,XXREAL_0:1; then k2+1 = i by A1,A2,A49,FUNCT_1:def 4; hence thesis by A54,NAT_1:13; end; end; suppose A55: k1= j; then A56: q.k1=p.k1-1 by A31,A32,A36; per cases; suppose A57: k2=j; then p.k1-1=p.k2-1 by A31,A33,A34,A36,A43,A56; hence thesis by A2,A36,A43,A41,A47,FUNCT_1:def 4; end; suppose A58: k2>=i & p.(k2+1)=i & p.(k2+1)>=j; then p.k1-1=p.(k2+1)-1 by A31,A33,A34,A36,A43,A56; then k1=k2+1 by A2,A41,A49,FUNCT_1:def 4; hence thesis by A55,A59,NAT_1:13; end; end; suppose A60: k1>=i & p.(k1+1)=j; then p.(k1+1)=p.k2-1 by A31,A33,A34,A36,A43,A61; then p.k2=p.(k1+1)+1; then p.k2<=j by A60,NAT_1:13; then p9.k2=p9.i by A63,XXREAL_0:1; hence thesis by A1,A2,A47,A63,FUNCT_1:def 4; end; suppose k2>=i & p.(k2+1)=i & p.(k2+1)>=j; then p.(k1+1)=p.(k2+1)-1 by A31,A33,A34,A36,A43,A61; then p.(k2+1)=p.(k1+1)+1; then p.(k2+1)<=j by A60,NAT_1:13; then p9.(k2+1)=p9.i by A64,XXREAL_0:1; then k2+1=i by A1,A2,A49,FUNCT_1:def 4; hence thesis by A64,NAT_1:13; end; end; suppose A65: k1>=i & p.(k1+1)>=j; then A66: q.k1=p.(k1+1)-1 by A31,A32,A36; per cases; suppose A67: k2=j; then p.(k1+1)-1=p.k2-1 by A31,A33,A34,A36,A43,A66; then k1+1=k2 by A2,A47,A42,FUNCT_1:def 4; hence thesis by A65,A68,NAT_1:13; end; suppose A69: k2>=i & p.(k2+1)=i & p.(k2+1)>=j; then p.(k1+1)-1=p.(k2+1)-1 by A31,A33,A34,A36,A43,A66; then k1+1=k2+1 by A2,A42,A49,FUNCT_1:def 4; hence thesis by A36,A43; end; end; end; then A70: q is one-to-one by FUNCT_1:def 4; card finSeg N=card finSeg N; then q is one-to-one onto by A70,STIRL2_1:60; then reconsider q as Element of P by MATRIX_2:def 9; take q; thus thesis by A31; end; uniqueness proof set p=perm; let q1,q2 be Element of Permutations n such that A71: for k st k in Seg n holds (k=p.i implies q1.k=p.k-1))& (k>=i implies (p.(k+1)=p.i implies q1.k=p.(k+1)-1)) and A72: for k st k in Seg n holds (k=p.i implies q2.k=p.k-1))& (k>=i implies (p.(k+1)=p.i implies q2.k=p.(k+1)-1)); A73: q1 is Permutation of Seg n by MATRIX_2:def 9; then A74: dom q1=Seg n by FUNCT_2:52; A75: now let x such that A76: x in dom q1; consider k being Element of NAT such that A77: x=k and 1<=k and k<=n by A74,A76; set k1=k+1; A78: p.k=p.i; A79: p.k1=p.i; k=i; then p.k < p.i & q1.k = p.k & q2.k=p.k or p.k >= p.i & q1.k = p.k-1 & q2.k=p.k-1 or p.k1 < p.i & q1.k = p.k1 & q2.k=p.k1 or p.k1 >= p.i & q1.k = p.k1 -1 & q2.k=p.k1-1 by A71,A72,A74,A76,A77,A78,A79; hence q1.x=q2.x by A77; end; q2 is Permutation of Seg n by MATRIX_2:def 9; then dom q2=Seg n by FUNCT_2:52; hence thesis by A73,A75,FUNCT_1:2,FUNCT_2:52; end; end; theorem Th20: for i,j st i in Seg (n+1) & j in Seg(n+1) for P be set st P = { p1: p1 .i = j} ex Proj be Function of P,Permutations n st Proj is bijective & for q1 st q1.i = j holds Proj.q1 = Rem(q1,i) proof let i,j such that A1: i in Seg (n+1) and A2: j in Seg(n+1); set n1 = n+1; reconsider N=n as Element of NAT by ORDINAL1:def 12; set P1 = Permutations(N+1); defpred F[set,set] means for p be Element of P1 st $1=p & p.i=j holds $2=Rem (p,i); let X be set such that A3: X={p1:p1.i=j}; A4: for x st x in X ex y st y in Permutations n & F[x,y] proof let x; assume x in X; then consider p be Element of P1 such that A5: p=x and p.i=j by A3; take Rem(p,i); thus thesis by A5; end; consider f be Function of X,Permutations n such that A6: for x st x in X holds F[x,f.x] from FUNCT_2:sch 1(A4); for x1,x2 be set st x1 in X & x2 in X & f.x1 = f.x2 holds x1 = x2 proof let x1,x2 be set such that A7: x1 in X and A8: x2 in X and A9: f.x1 = f.x2; consider p1 be Element of P1 such that A10: p1=x1 and A11: p1.i=j by A3,A7; set R1=Rem(p1,i); A12: f.x1 =R1 by A6,A7,A10,A11; consider p2 be Element of P1 such that A13: p2=x2 and A14: p2.i=j by A3,A8; set R2=Rem(p2,i); A15: f.x2 =R2 by A6,A8,A13,A14; reconsider p19=p1,p29=p2 as Permutation of Seg n1 by MATRIX_2:def 9; A16: dom p29=Seg n1 by FUNCT_2:52; A17: dom p19=Seg n1 by FUNCT_2:52; now let x such that A18: x in Seg n1; consider k being Element of NAT such that A19: x=k and A20: 1<=k and A21: k<=n1 by A18; per cases by XXREAL_0:1; suppose A22: k=j & p2.k>=j; then R1.k=p1.k & R2.k=p2.k or R1.k=p1.k-1 & R2.k=p2.k-1 by A1,A11,A14 ,A22,A23,Def3; hence p1.x=p2.x by A9,A12,A15,A19; end; suppose p1.k=j or p1.k>=j & p2.k=j or R1.k=p1.k-1 & R2. k=p2.k & p1.k>=j & p2.k=j or p1.k=p2.k+1 & p1.k>=j & p2.k< j by A9,A12,A15; then p2.k<=j & p2.k>=j or p1.k>=j & p1.k<=j by NAT_1:13; then p29.k=p29.i or p19.k=p19.i by A11,A14,XXREAL_0:1; hence p1.x=p2.x by A1,A17,A16,A18,A19,A22,FUNCT_1:def 4; end; end; suppose k=i; hence p1.x=p2.x by A11,A14,A19; end; suppose A24: k>i; then reconsider k1=k-1 as Element of NAT by NAT_1:20; k1+1>i by A24; then A25: k1>=i by NAT_1:13; k1+1 <= n1 by A21; then k1 < n1 by NAT_1:13; then A26: k1<=n by NAT_1:13; 1<=i by A1,FINSEQ_1:1; then 1=j&p2.(k1+1)>=j; then R1.k1=p1.k & R2.k1=p2.k or R1.k1=p1.k-1 & R2.k1=p2.k-1 by A1,A11 ,A14,A27,A25,Def3; hence p1.x=p2.x by A9,A12,A15,A19; end; suppose p1.(k1+1)=j or p1.(k1+1)>=j&p2.(k1+1)=j or R1.k1=p1.k-1 & R2.k1=p2.k & p1.k>=j & p2.k=j or p1.k=p2.k+1 & p1.k>=j & p2.k< j by A9,A12,A15; then p2.k<=j & p2.k>=j or p1.k>=j & p1.k<=j by NAT_1:13; then p29.k=p29.i or p19.k=p19.i by A11,A14,XXREAL_0:1; hence p1.x=p2.x by A1,A17,A16,A18,A19,A24,FUNCT_1:def 4; end; end; end; hence thesis by A10,A13,A17,A16,FUNCT_1:2; end; then A28: f is one-to-one by FUNCT_2:19; set P = Permutations(N); A29: card P=N! by Th6; card X= N! by A1,A2,A3,Th7; then reconsider P9=P,X9=X as finite set by A29; take f; A30: card P9=n! by Th6; card X9=n! by A1,A2,A3,Th7; then f is onto one-to-one by A28,A30,STIRL2_1:60; hence f is bijective; let p be Element of Permutations(n+1) such that A31: p.i=j; p in X by A3,A31; hence thesis by A6,A31; end; theorem Th21: for i,j st i in Seg (n+1) & p1.i = j holds -(a,p1) = power(K).(- 1_K,i+j) * -(a,Rem(p1,i)) proof set n1=n+1; let i,j such that A1: i in Seg n1 and A2: p1.i=j; A3: p1 is Permutation of Seg n1 by MATRIX_2:def 9; then A4: rng p1=Seg n1 by FUNCT_2:def 3; dom p1=Seg n1 by A3,FUNCT_2:52; then A5: j in Seg n1 by A1,A2,A4,FUNCT_1:def 3; set R=Rem(p1,i); per cases by NAT_1:23; suppose A6: n=0; then R is even by Th11; then A7: -(a,R)=a by MATRIX_2:def 13; A8: 1+1=2*1; p1 is even by A6,Th11; then A9: -(a,p1)=a by MATRIX_2:def 13; A10: j=1 by A5,A6,FINSEQ_1:2,TARSKI:def 1; i=1 by A1,A6,FINSEQ_1:2,TARSKI:def 1; then power(K).(-1_K,i+j)=1_K by A10,A8,HURWITZ:4; hence thesis by A9,A7,VECTSP_1:def 4; end; suppose A11: n=1; then A12: p1 is Permutation of Seg 2 by MATRIX_2:def 9; per cases by A12,MATRIX_7:1; suppose A13: p1=<*1,2*>; i=1 or i=2 by A1,A11,FINSEQ_1:2,TARSKI:def 2; then i=1 & p1.i=1 or i=2 & p1.i=2 by A13,FINSEQ_1:44; then i+j=2*1 or i+j=2*2 by A2; then A14: power(K).(-1_K,i+j)=1_K by HURWITZ:4; A15: len Permutations(2)=2 by MATRIX_2:18; R is even by A11,Th11; then A16: -(a,R)=a by MATRIX_2:def 13; id Seg 2 is even by MATRIX_2:25; then -(a,p1)=a by A11,A13,A15,FINSEQ_2:52,MATRIX_2:def 13; hence thesis by A14,A16,VECTSP_1:def 4; end; suppose A17: p1=<*2,1*>; len Permutations(2)=2 by MATRIX_2:18; then -(a,p1)=-a by A11,A17,MATRIX_2:def 13,MATRIX_9:12; then A18: -(a,p1)=-1_K*a by VECTSP_1:def 4; i=1 or i=2 by A1,A11,FINSEQ_1:2,TARSKI:def 2; then i+j=2*1+1 by A2,A17,FINSEQ_1:44; then A19: power(K).(-1_K,i+j)=-1_K by HURWITZ:4; R is even by A11,Th11; then -(a,R)=a by MATRIX_2:def 13; hence thesis by A19,A18,VECTSP_1:8; end; end; suppose A20: n >= 2; then reconsider n2=n-2 as Element of NAT by NAT_1:21; per cases; suppose A21: not K is Fanoian; A22: now per cases by NAT_D:12; suppose i+j mod 2=0; then consider t be Nat such that A23: i+j = 2 * t + 0 and 0 < 2 by NAT_D:def 2; t is Element of NAT by ORDINAL1:def 12; hence power(K).(-1_K,i+j)=1_K by A23,HURWITZ:4; end; suppose i+j mod 2=1; then consider t be Nat such that A24: i+j = 2 * t + 1 and 1 < 2 by NAT_D:def 2; A25: 1_K=-1_K by A21,MATRIX11:22; t is Element of NAT by ORDINAL1:def 12; hence power(K).(-1_K,i+j)=1_K by A24,A25,HURWITZ:4; end; end; A26: -(a,p1)=a or -(a,p1)=-a by MATRIX_2:def 13; -1_K=1_K by A21,MATRIX11:22; then A27: -a*1_K=a*(1_K) by VECTSP_1:9; A28: -a=-a*1_K by VECTSP_1:def 4; -(a,R)=a or -(a,R)=-a by MATRIX_2:def 13; then -(a,R)=a by A28,A27,VECTSP_1:def 4; hence thesis by A22,A26,A27,VECTSP_1:def 4; end; suppose A29: K is Fanoian; set mm=the multF of K; reconsider n1=n2+1 as Element of NAT; set P1=Permutations(n1+2); reconsider Q1=p1 as Element of P1; set SS1=2Set Seg (n1+2); consider X be Element of Fin SS1 such that A30: X = {{N,i}:{N,i} in SS1} and A31: mm $$ (X,Part_sgn(Q1,K)) = power(K).(-1_K,i+j) by A1,A2,A29,Th9; set PQ1=Part_sgn(Q1,K); set SS2=2Set Seg (n2+2); reconsider Q19=Q1 as Permutation of Seg (n1+2) by MATRIX_2:def 9; set P2=Permutations(n2+2); reconsider Q=R as Element of P2; reconsider Q9=Q as Permutation of Seg (n2+2) by MATRIX_2:def 9; set PQ=Part_sgn(Q,K); A32: FinOmega(SS1)=SS1 by MATRIX_2:def 14; reconsider SSX=SS1\X as Element of Fin SS1 by FINSUB_1:def 5; A33: X\/SSX=SS1\/X by XBOOLE_1:39; X c= SS1 by FINSUB_1:def 5; then A34: X\/SSX=SS1 by A33,XBOOLE_1:12; consider f be Function of SS2,SS1 such that A35: rng f=SS1\X and A36: f is one-to-one and A37: for k,m st k= i & k < i implies f.{k,m}={k,m+1}) & (m >= i & k >= i implies f.{k,m}={k+1,m+1}) by A1,A20,A30,Th10; set Pf=PQ1*f; A38: dom Pf=SS2 by FUNCT_2:def 1; A39: dom Q19=Seg (n1+2) by FUNCT_2:52; A40: now n<=n+1 by NAT_1:11; then A41: Seg (n2+2) c= Seg (n1+2) by FINSEQ_1:5; let x such that A42: x in SS2; consider k,m be Nat such that A43: k in Seg (n2+2) and A44: m in Seg (n2+2) and A45: k < m and A46: x={k,m} by A42,MATRIX11:1; reconsider k,m as Element of NAT by ORDINAL1:def 12; dom Q9=Seg (n2+2) by FUNCT_2:52; then Q9.k<>Q.m by A43,A44,A45,FUNCT_1:def 4; then A47: Q.k>Q.m or Q.k=j & Q1.m>=j; then Q.k=Q1.k&Q.m=Q1.m or Q.k=Q1.k-1&Q.m=Q1.m-1 by A1,A2,A43,A44 ,A51,Def3; then Q.kQ.m & Q1.k>Q1.m by A47,XREAL_1:9; then PQ1.x=1_K & PQ.x=1_K or PQ1.x=-1_K & PQ.x=-1_K by A43,A44,A45,A46 ,A41,MATRIX11:def 1; hence Pf.x=PQ.x by A38,A42,A53,FUNCT_1:12; end; suppose A54: Q1.k=j; then Q.m=Q1.m-1 by A1,A2,A44,A51,Def3; then A55: Q1.m=Q.m+1; Q19.m<>j by A1,A2,A39,A44,A41,A51,FUNCT_1:def 4; then Q1.m>j by A54,XXREAL_0:1; then A56: Q.m>=j by A55,NAT_1:13; Q1.k=j & Q1.mj by A1,A2,A39,A43,A41,A51,FUNCT_1:def 4; then Q1.k>j by A58,XXREAL_0:1; then A60: Q.k>=j by A59,NAT_1:13; Q1.k>Q1.m by A58,XXREAL_0:2; then A61: PQ1.x=-1_K by A43,A44,A45,A46,A41,MATRIX11:def 1; Q1.m=Q.m by A1,A2,A44,A51,A58,Def3; then Q.k>Q.m by A58,A60,XXREAL_0:2; hence Pf.x=PQ.x by A43,A44,A45,A46,A53,A52,A61,MATRIX11:def 1; end; end; suppose k>=i & m=i; A63: Pf.x=PQ1.(f.{k,m}) by A38,A42,A46,FUNCT_1:12; A64: f.{k,m}={k,m1} by A37,A42,A45,A46,A62; per cases; suppose Q1.k=j & Q1.m1>=j; then Q.k=Q1.k & Q.m=Q1.m1 or Q.k=Q1.k-1 & Q.m=Q1.m1-1 by A1,A2,A43 ,A44,A62,Def3; then A65: Q.kQ.m & Q1.k>Q1.m1 by A47,XREAL_1:9; k < m1 by A45,NAT_1:13; then PQ1.{k,m1}=1_K & PQ.x=1_K or PQ1.{k,m1}=-1_K & PQ.x=-1_K by A43,A44,A45,A46,A41,A50,A65,MATRIX11:def 1; hence Pf.x=PQ.x by A38,A42,A46,A64,FUNCT_1:12; end; suppose A66: Q1.k=j; m1>i by A62,NAT_1:13; then Q19.m1<>j by A1,A2,A39,A50,FUNCT_1:def 4; then A67: Q1.m1>j by A66,XXREAL_0:1; Q.m=Q1.m1-1 by A1,A2,A44,A62,A66,Def3; then Q1.m1=Q.m+1; then A68: Q.m>=j by A67,NAT_1:13; Q1.k=Q.k by A1,A2,A43,A62,A66,Def3; then A69: Q.k=j & Q1.m1j by A1,A2,A39,A43,A41,A62,FUNCT_1:def 4; then Q1.k>j by A71,XXREAL_0:1; then A73: Q.k>=j by A72,NAT_1:13; Q1.m1=Q.m by A1,A2,A44,A62,A71,Def3; then A74: Q.mQ1.m1 by A71,XXREAL_0:2; then PQ1.{k,m1}=-1_K by A43,A41,A50,A75,MATRIX11:def 1; hence Pf.x=PQ.x by A43,A44,A45,A46,A64,A63,A74,MATRIX11:def 1; end; end; suppose A76: k>=i & m>=i; A77: Pf.x=PQ1.(f.{k,m}) by A38,A42,A46,FUNCT_1:12; A78: k1=j & Q1.m1>=j; then Q.k=Q1.k1&Q.m=Q1.m1 or Q.k=Q1.k1-1&Q.m=Q1.m1-1 by A1,A2,A43 ,A44,A76,Def3; then Q.kQ.m & Q1.k1>Q1.m1 by A47, XREAL_1:9; then PQ1.{k1,m1}=1_K & PQ.x=1_K or PQ1.{m1,k1}=-1_K&PQ.x=-1_K by A43,A44,A45,A46,A49,A50,A78,MATRIX11:def 1; hence Pf.x=PQ.x by A38,A42,A46,A79,FUNCT_1:12; end; suppose A80: Q1.k1=j; m1>i by A76,NAT_1:13; then Q19.m1<>j by A1,A2,A39,A50,FUNCT_1:def 4; then A81: Q1.m1>j by A80,XXREAL_0:1; Q.m=Q1.m1-1 by A1,A2,A44,A76,A80,Def3; then Q1.m1=Q.m+1; then A82: Q.m>=j by A81,NAT_1:13; Q1.k1=j & Q1.m1i by A76,NAT_1:13; then Q19.k1<>j by A1,A2,A39,A49,FUNCT_1:def 4; then A85: Q1.k1>j by A84,XXREAL_0:1; Q.k=Q1.k1-1 by A1,A2,A43,A76,A84,Def3; then Q1.k1=Q.k+1; then A86: Q.k>=j by A85,NAT_1:13; Q1.k1>Q1.m1 by A84,XXREAL_0:2; then A87: PQ1.{k1,m1}=-1_K by A49,A50,A78,MATRIX11:def 1; Q1.m1=Q.m by A1,A2,A44,A76,A84,Def3; then Q.k>Q.m by A84,A86,XXREAL_0:2; hence Pf.x=PQ.x by A43,A44,A45,A46,A79,A77,A87,MATRIX11:def 1; end; end; end; reconsider domf=dom f as Element of Fin SS2 by FINSUB_1:def 5; A88: f.:domf=rng f by RELAT_1:113; dom f=SS2 by FUNCT_2:def 1; then A89: domf=FinOmega(SS2) by MATRIX_2:def 14; dom PQ=SS2 by FUNCT_2:def 1; then PQ=Pf by A38,A40,FUNCT_1:2; then A90: mm $$ (SSX,PQ1) = sgn(Q,K) by A35,A36,A89,A88,SETWOP_2:6; X misses SSX by XBOOLE_1:79; then sgn(Q1,K)=power(K).(-1_K,i+j)*sgn(Q,K) by A31,A90,A34,A32,SETWOP_2:4 ; hence -(a,p1) = power(K).(-1_K,i+j)*sgn(Q,K)*a by MATRIX11:26 .= power(K).(-1_K,i+j)*(sgn(Q,K)*a) by GROUP_1:def 3 .= power(K).(-1_K,i+j)*-(a,R) by MATRIX11:26; end; end; end; theorem Th22: for i,j st i in Seg (n+1) & p1.i = j for M be Matrix of n+1,K for DM be Matrix of n,K st DM = Delete(M,i,j) holds (Path_product M).p1 = power (K).(-1_K,i+j)*(M*(i,j))*(Path_product(DM)).Rem(p1,i) proof reconsider N=n as Element of NAT by ORDINAL1:def 12; set n1 = N+1; let i,j be Nat such that A1: i in Seg(n+1) and A2: p1.i=j; set mm=the multF of K; set R=Rem(p1,i); let M be (Matrix of n+1,K),DM be (Matrix of n,K) such that A3: DM=Delete(M,i,j); set PR=Path_matrix(R,DM); set Pp1=Path_matrix(p1,M); len Pp1=n1 by MATRIX_3:def 7; then dom Pp1=Seg n1 by FINSEQ_1:def 3; then A4: Pp1.i=M*(i,j) by A1,A2,MATRIX_3:def 7; A5: now per cases; suppose A6: N=0; then A7: len Pp1=1 by MATRIX_3:def 7; Pp1.1=M*(i,j) by A1,A4,A6,FINSEQ_1:2,TARSKI:def 1; then Pp1=<*M*(i,j)*> by A7,FINSEQ_1:40; then A8: mm $$ Pp1=M*(i,j) by FINSOP_1:11; len PR=0 by A6,MATRIX_3:def 7; then PR=<*>(the carrier of K); then A9: mm $$ PR = the_unity_wrt mm by FINSOP_1:10; the_unity_wrt mm=1_K by FVSUM_1:5; hence mm $$ Pp1=(M*(i,j))*(mm $$ PR) by A8,A9,VECTSP_1:def 4; end; suppose A10: N>0; len PR=n by MATRIX_3:def 7; then consider f be Function of NAT,the carrier of K such that A11: f.1 = PR.1 and A12: for k being Element of NAT st 0<>k & kk & k=i implies PR.k=Pp1.(k+1)) proof len Pp1=n1 by MATRIX_3:def 7; then A18: dom Pp1=Seg n1 by FINSEQ_1:def 3; len PR=n by MATRIX_3:def 7; then A19: dom PR=Seg n by FINSEQ_1:def 3; reconsider p19=p1 as Permutation of Seg n1 by MATRIX_2:def 9; reconsider R9=R as Permutation of Seg n by MATRIX_2:def 9; let k such that A20: k in Seg n; reconsider k1=k+1 as Element of NAT; A21: k1 in Seg n1 by A20,FINSEQ_1:60; A22: rng p19=Seg n1 by FUNCT_2:def 3; dom p19=Seg n1 by FUNCT_2:52; then A23: j in Seg n1 by A1,A2,A22,FUNCT_1:def 3; A24: rng R9=Seg n by FUNCT_2:def 3; dom R9=Seg n by FUNCT_2:52; then A25: R.k in Seg n by A20,A24,FUNCT_1:def 3; then consider Rk be Element of NAT such that A26: Rk=R.k and 1<=Rk and Rk<=n; A27: n1-'1=n1-1 by XREAL_0:def 2; n<=n1 by NAT_1:11; then A28: Seg n c= Seg n1 by FINSEQ_1:5; thus kp19.i by A1,A20,A28,A29,FUNCT_1:def 4; then p1.kj by A2,XXREAL_0:1; then Rk=p1.k & p1.kj&Rk=p1.k-1 by A1,A2,A20,A26,A29,Def3; then Rk=p1.k & p1.kj & p1.k=Rk+1; then Rk=p1.k & p1.kj & Rk>=j & p1.k=Rk+1 by NAT_1:13; then DM*(k,Rk)=M*(k,Rk) & PR.k=DM*(k,Rk) & Pp1.k=M*(k,Rk) or PR.k=DM *(k,Rk) & DM*(k,Rk)=M*(k,Rk+1) & Pp1.k=M*(k,Rk+1) by A1,A3,A20,A25,A23,A26,A28 ,A27,A19,A18,A29,Th13,MATRIX_3:def 7; hence thesis; end; A30: dom p19=Seg n1 by FUNCT_2:52; assume A31: k>=i; then k1 >i by NAT_1:13; then p19.k1<>p19.i by A1,A21,A30,FUNCT_1:def 4; then p1.k1j by A2,XXREAL_0:1; then Rk=p1.k1 & p1.k1j&Rk=p1.k1-1 by A1,A2,A20,A26,A31,Def3; then Rk=p1.k1 & p1.k1j & p1.k1=Rk+1; then Rk=p1.k1 & p1.k1j & Rk>=j & p1.k1=Rk+1 by NAT_1:13; then DM*(k,Rk)=M*(k+1,Rk) & PR.k=DM*(k,Rk) & Pp1.k1=M*(k+1,Rk) or PR.k =DM*(k,Rk) & DM*(k,Rk)=M*(k+1,Rk+1) & Pp1.k1=M*(k1,Rk+1) by A1,A3,A20,A25,A23 ,A26,A27,A21,A19,A18,A31,Th13,MATRIX_3:def 7; hence thesis; end; A32: for k st P[k] holds P[k+1] proof let k such that A33: P[k]; reconsider e=k as Element of NAT by ORDINAL1:def 12; assume that A34: 1<=k+1 and A35: k+1=1; i<=n1 by A1,FINSEQ_1:1; then A38: k11 implies for a st a=f.($1-1) holds F.$1=M*(i,j)*a); A41: P[0]; A42: for k holds P[k] from NAT_1:sch 2(A41,A32); A43: for k st Q[k] holds Q[k+1] proof let k such that A44: Q[k]; set k1=k+1; assume that A45: i<=k1 and A46: k1<=n1; per cases; suppose A47: k=0; 1<=i by A1,FINSEQ_1:1; hence thesis by A4,A14,A45,A47,XXREAL_0:1; end; suppose A48: k>0; hence k1=1 implies F.k1=M*(i,j); assume k1>1; let a such that A49: a=f.(k1-1); A50: k<=n by A46,XREAL_1:6; k>=1 by A48,NAT_1:14; then A51: k in Seg n by A50,FINSEQ_1:1; len PR=n by MATRIX_3:def 7; then A52: dom PR=Seg n by FINSEQ_1:def 3; then A53: PR.k=DM*(k,R.k) by A51,MATRIX_3:def 7; ki; A57: k=i by A56,NAT_1:13; i>=1 by A1,FINSEQ_1:1; then A59: k>=1 by A58,XXREAL_0:2; per cases by A59,XXREAL_0:1; suppose k=1; hence thesis by A11,A17,A44,A46,A49,A51,A54,A58,NAT_1:13; end; suppose A60: k>1; reconsider k9=k-1 as Element of NAT by A48,NAT_1:20; reconsider fk9=f.k9 as Element of K; k9+1<=n by A57,NAT_1:13; then A61: k90+1 by A60; then A62: a=mm.(fk9,PR.(k9+1)) by A12,A49,A61; F.k=M*(i,j)*fk9 by A44,A46,A56,A60,NAT_1:13; hence F.k1 = (M*(i,j)*fk9)*(DM*(k,R.k)) by A17,A51,A54,A53,A58 .= M*(i,j)*(fk9*(DM*(k,R.k)))by GROUP_1:def 3 .= M*(i,j)*a by A51,A52,A62,MATRIX_3:def 7; end; end; end; end; A63: Q[0]; A64: for k holds Q[k] from NAT_1:sch 2(A63,A43); A65: i<=n1 by A1,FINSEQ_1:1; A66: n1-1=n; n1>0+1 by A10,XREAL_1:6; hence mm $$ Pp1=M*(i,j)*mm $$ PR by A16,A13,A64,A65,A66; end; end; per cases; suppose A67: R is even; thus (Path_product(M)).p1 = -(mm $$ Pp1,p1) by MATRIX_3:def 8 .= power(K).(-1_K,i+j)*-(mm $$ Pp1,R) by A1,A2,Th21 .= power(K).(-1_K,i+j)*(M*(i,j)*mm $$ PR) by A5,A67,MATRIX_2:def 13 .= power(K).(-1_K,i+j) * (M*(i,j))*mm $$ PR by GROUP_1:def 3 .= power(K).(-1_K,i+j) * (M*(i,j))* -(mm $$ PR,R) by A67,MATRIX_2:def 13 .= power(K).(-1_K,i+j)*(M*(i,j))*(Path_product(DM)).R by MATRIX_3:def 8; end; suppose A68: R is odd; thus (Path_product(M)).p1=-(mm $$ Pp1,p1) by MATRIX_3:def 8 .= power(K).(-1_K,i+j)*-(mm $$ Pp1,R) by A1,A2,Th21 .= power(K).(-1_K,i+j)*(-(M*(i,j)*mm $$ PR)) by A5,A68,MATRIX_2:def 13 .= power(K).(-1_K,i+j)*((M*(i,j)*(-(mm $$ PR)))) by VECTSP_1:8 .= power(K).(-1_K,i+j)*(M*(i,j))*(-(mm $$ PR)) by GROUP_1:def 3 .= power(K).(-1_K,i+j)*(M*(i,j))*-(mm $$ PR,R) by A68,MATRIX_2:def 13 .= power(K).(-1_K,i+j)*(M*(i,j))*(Path_product(DM)).R by MATRIX_3:def 8; end; end; begin :: Minors & cofactors definition let i,j,n be Nat; let K; let M be Matrix of n,K; func Minor(M,i,j) -> Element of K equals Det Delete(M,i,j); coherence; end; definition let i,j,n be Nat; let K; let M be Matrix of n,K; func Cofactor(M,i,j) -> Element of K equals power(K).(-1_K,i+j)*Minor(M,i,j); coherence; end; theorem Th23: for i,j st i in Seg n & j in Seg n for P be Element of Fin Permutations n st P = {p:p.i = j} for M be Matrix of n,K holds (the addF of K) $$ (P,Path_product(M)) = M*(i,j)*Cofactor(M,i,j) proof let i,j be Nat such that A1: i in Seg n and A2: j in Seg n; n>0 by A1; then reconsider n9=n-1 as Element of NAT by NAT_1:20; set P=Permutations (n-'1); set n91=n9+1; set P1=Permutations n; A3: n91-'1=n9+1-1 by XREAL_0:def 2; set aa=the addF of K; A4: FinOmega(P)=P by MATRIX_2:26,def 14; let PP be Element of Fin P1 such that A5: PP={p:p.i=j}; consider Proj be Function of PP,P such that A6: Proj is bijective and A7: for q be Element of Permutations n91 st q.i=j holds Proj.q = Rem(q,i ) by A1,A2,A5,A3,Th20; let M be Matrix of n,K; set DM=Delete(M,i,j); set PathM=Path_product(M); set PathDM=Path_product(DM); set pm=power(K).(-1_K,i+j)*(M*(i,j)); defpred P[set] means for D be Element of Fin P1,ProjD be Element of Fin P st D=$1 & ProjD=Proj.:D & D c= PP holds aa $$ (D,PathM) = pm * aa $$ (ProjD,PathDM ); A8: for B9 be (Element of Fin P1), b be Element of P1 holds P[B9] & not b in B9 implies P[B9 \/ {b}] proof let B9 be (Element of Fin P1), b be Element of P1 such that A9: P[B9] and A10: not b in B9; A11: b in {b} by TARSKI:def 1; A12: rng Proj=P by A6,FUNCT_2:def 3; then Proj.:B9 c= P by RELAT_1:111; then reconsider ProjB9=Proj.:B9 as Element of Fin P by FINSUB_1:def 5; let D be Element of Fin P1,ProjD be Element of Fin P such that A13: D=B9\/{b} and A14: ProjD=Proj.:D and A15: D c= PP; A16: B9 c= D by A13,XBOOLE_1:7; B9 c= D by A13,XBOOLE_1:7; then A17: B9 c= PP by A15,XBOOLE_1:1; {b}c=D by A13,XBOOLE_1:7; then A18: b in PP by A15,A11,TARSKI:def 3; then consider Q1 be Element of P1 such that A19: Q1=b and A20: Q1.i=j by A5; A21: dom Proj = PP by FUNCT_2:def 1; then A22: Im(Proj,b)={Proj.b} by A18,FUNCT_1:59; reconsider Q=Proj.b as Element of P by A18,A21,A12,FUNCT_1:def 3; A23: Proj.b in rng Proj by A18,A21,FUNCT_1:def 3; reconsider Q19=Q1 as Element of Permutations (n9+1); A24: Rem(Q19,i)=Q by A7,A19,A20; then A25: PathM.Q1=pm*PathDM.Q by A1,A3,A20,Th22; A26: not Q in ProjB9 proof assume Q in ProjB9; then ex x st x in dom Proj & x in B9 & Proj.x=Q by FUNCT_1:def 6; hence thesis by A6,A10,A18,A21,FUNCT_1:def 4; end; per cases; suppose A27: B9={}; then A28: aa $$ (D,PathM)=PathM.b by A13,SETWISEO:17; aa $$ (ProjD,PathDM)=PathDM.(Proj.b) by A13,A14,A22,A23,A12,A27, SETWISEO:17; hence thesis by A1,A3,A19,A20,A24,A28,Th22; end; suppose A29: B9<>{}; ProjD=ProjB9\/{Q} by A13,A14,A22,RELAT_1:120; hence pm *aa $$ (ProjD,PathDM) = pm*(aa $$(ProjB9,PathDM)+PathDM.Q) by A18,A17,A21,A26,A29,SETWOP_2:2 .= (pm * aa $$ (ProjB9,PathDM))+(pm * PathDM.Q) by VECTSP_1:def 2 .= aa.(aa $$ (B9,PathM),PathM.b) by A9,A15,A19,A16,A25,XBOOLE_1:1 .= aa $$ (D,PathM) by A10,A13,A29,SETWOP_2:2; end; end; A30: P[{}.P1] proof let B be Element of Fin P1,ProjB be Element of Fin P such that A31: B = {}.P1 and A32: ProjB = Proj.:B and B c= PP; ProjB={}.P by A31,A32; then A33: aa $$ (ProjB,PathDM)=the_unity_wrt aa by FVSUM_1:8,SETWISEO:31; A34: the_unity_wrt aa=0.K by FVSUM_1:7; aa $$ (B,PathM)=the_unity_wrt aa by A31,FVSUM_1:8,SETWISEO:31; hence thesis by A33,A34,VECTSP_1:6; end; A35: for B being Element of Fin P1 holds P[B] from SETWISEO:sch 2(A30,A8 ); A36: dom Proj=PP by FUNCT_2:def 1; rng Proj=P by A6,FUNCT_2:def 3; then Proj.:PP=FinOmega(P) by A4,A36,RELAT_1:113; hence aa $$ (PP,PathM) = M*(i,j) * power(K).(-1_K,i+j)* Det (Delete(M,i,j)) by A35 .= M*(i,j) * Cofactor(M,i,j) by GROUP_1:def 3; end; theorem Th24: for i,j st i in Seg n & j in Seg n holds Minor(M,i,j) = Minor(M@ ,j,i) proof let i,j such that A1: i in Seg n and A2: j in Seg n; thus Minor(M,i,j) = Det Delete(M,i,j)@ by MATRIXR2:43 .= Minor(M@,j,i) by A1,A2,Th14; end; definition let n,K; let M be Matrix of n,K; func Matrix_of_Cofactor(M) -> Matrix of n,K means :Def6: for i,j being Nat st [i,j] in Indices it holds it*(i,j) = Cofactor(M,i,j); existence proof reconsider N=n as Element of NAT by ORDINAL1:def 12; deffunc C(Nat,Nat)=Cofactor(M,$1,$2); ex M being Matrix of N,N,K st for i,j being Nat st [i,j] in Indices M holds M*(i,j) = C(i,j) from MATRIX_1:sch 1; hence thesis; end; uniqueness proof let C1,C2 be Matrix of n,K such that A1: for i,j being Nat st [i,j] in Indices C1 holds C1*(i,j) = Cofactor (M,i,j) and A2: for i,j being Nat st [i,j] in Indices C2 holds C2*(i,j) = Cofactor (M,i,j); now A3: Indices C1=Indices C2 by MATRIX_1:26; let i,j be Nat such that A4: [i,j] in Indices C1; reconsider i9=i,j9=j as Element of NAT by ORDINAL1:def 12; C1*(i,j) = Cofactor(M,i9,j9) by A1,A4; hence C1*(i,j)=C2*(i,j) by A2,A4,A3; end; hence thesis by MATRIX_1:27; end; end; begin :: Laplace expansion definition let n,i,K; let M be Matrix of n,K; ::$N Laplace expansion func LaplaceExpL(M,i) -> FinSequence of K means :Def7: len it = n & for j st j in dom it holds it.j = M*(i,j)*Cofactor(M,i,j); existence proof reconsider N=n as Element of NAT by ORDINAL1:def 12; deffunc L(Nat)=M*(i,$1)*Cofactor(M,i,$1); consider LL be FinSequence such that A1: len LL = N & for k being Nat st k in dom LL holds LL.k=L(k) from FINSEQ_1:sch 2; rng LL c= the carrier of K proof let x; assume x in rng LL; then consider y such that A2: y in dom LL and A3: LL.y=x by FUNCT_1:def 3; dom LL=Seg n by A1,FINSEQ_1:def 3; then consider k being Element of NAT such that A4: k=y and 1<=k and k<=n by A2; L(k) is Element of K; then LL.k is Element of K by A1,A2,A4; hence thesis by A3,A4; end; then reconsider LL as FinSequence of K by FINSEQ_1:def 4; take LL; thus len LL = n by A1; thus thesis by A1; end; uniqueness proof let L1,L2 be FinSequence of K such that A5: len L1=n and A6: for j st j in dom L1 holds L1.j=M*(i,j)*Cofactor(M,i,j) and A7: len L2=n and A8: for j st j in dom L2 holds L2.j = M*(i,j)*Cofactor(M,i,j); A9: dom L2=Seg n by A7,FINSEQ_1:def 3; A10: dom L1=Seg n by A5,FINSEQ_1:def 3; now let k be Nat such that A11: k in dom L1; L1.k=M*(i,k)*Cofactor(M,i,k) by A6,A11; hence L1.k=L2.k by A8,A10,A9,A11; end; hence thesis by A10,A9,FINSEQ_1:13; end; end; definition let n; let j be Nat,K; let M be Matrix of n,K; func LaplaceExpC(M,j) -> FinSequence of K means :Def8: len it = n & for i st i in dom it holds it.i = M*(i,j)*Cofactor(M,i,j); existence proof reconsider N=n as Element of NAT by ORDINAL1:def 12; deffunc L(Nat)=M*($1,j)*Cofactor(M,$1,j); consider LL be FinSequence such that A1: len LL = N & for k being Nat st k in dom LL holds LL.k=L(k) from FINSEQ_1:sch 2; rng LL c= the carrier of K proof let x; assume x in rng LL; then consider y such that A2: y in dom LL and A3: LL.y=x by FUNCT_1:def 3; dom LL=Seg n by A1,FINSEQ_1:def 3; then consider k being Element of NAT such that A4: k=y and 1<=k and k<=n by A2; L(k) is Element of K; then LL.k is Element of K by A1,A2,A4; hence thesis by A3,A4; end; then reconsider LL as FinSequence of K by FINSEQ_1:def 4; take LL; thus len LL = n by A1; let i; assume i in dom LL; hence thesis by A1; end; uniqueness proof let L1,L2 be FinSequence of K such that A5: len L1=n and A6: for i st i in dom L1 holds L1.i=M*(i,j)*Cofactor(M,i,j) and A7: len L2=n and A8: for i st i in dom L2 holds L2.i = M*(i,j)*Cofactor(M,i,j); A9: dom L2=Seg n by A7,FINSEQ_1:def 3; A10: dom L1=Seg n by A5,FINSEQ_1:def 3; now let k be Nat such that A11: k in dom L1; L1.k=M*(k,j)*Cofactor(M,k,j) by A6,A11; hence L1.k=L2.k by A8,A10,A9,A11; end; hence thesis by A10,A9,FINSEQ_1:13; end; end; theorem Th25: for i be Nat, M be Matrix of n,K st i in Seg n holds Det M = Sum LaplaceExpL(M,i) proof reconsider N=n as Element of NAT by ORDINAL1:def 12; set P=Permutations n; set KK=the carrier of K; set aa=the addF of K; A1: aa is having_a_unity by FVSUM_1:8; let i be Nat, M be Matrix of n,K such that A2: i in Seg n; reconsider X=finSeg N as non empty set by A2; set Path=Path_product(M); deffunc G(Element of Fin P)=aa $$ ($1,Path); consider g be Function of Fin P,KK such that A3: for x being Element of Fin P holds g.x = G(x) from FUNCT_2:sch 4; A4: for A,B be Element of Fin P st A misses B holds aa.(g.A,g.B)=g.(A \/ B) proof let A,B be Element of Fin P such that A5: A misses B; A6: g.(A)=G(A) by A3; A7: g.B=G(B) by A3; g.(A \/ B)=G(A\/B) by A3; hence thesis by A5,A6,A7,FVSUM_1:8,SETWOP_2:4; end; deffunc F(set) = {p:p.i=$1}; consider f be Function such that A8: dom f = X & for x st x in X holds f.x = F(x) from FUNCT_1:sch 3; rng f c= Fin P proof let x; assume x in rng f; then consider y such that A9: y in dom f and A10: f.y=x by FUNCT_1:def 3; A11: F(y) c= P proof let z be set; assume z in F(y); then ex p st p=z& p.i=y; hence thesis; end; P is finite by MATRIX_2:26; then F(y) in Fin P by A11,FINSUB_1:def 5; hence thesis by A8,A9,A10; end; then reconsider f as Function of X,Fin P by A8,FUNCT_2:2; A12: g.FinOmega(P)=Det M by A3; set gf=g*f; A13: dom gf=X by FUNCT_2:def 1; then A14: gf*(id X)=gf by RELAT_1:52; A15: P c= union (f.:X) proof let x; assume A16: x in P; then reconsider p=x as Permutation of X by MATRIX_2:def 9; A17: x in F(p.i) by A16; A18: rng p=X by FUNCT_2:def 3; dom p=X by FUNCT_2:52; then A19: p.i in X by A2,A18,FUNCT_1:def 3; then A20: f.(p.i) in f.:X by A8,FUNCT_1:def 6; f.(p.i)=F(p.i) by A8,A19; hence thesis by A17,A20,TARSKI:def 4; end; set L=LaplaceExpL(M,i); len L=n by Def7; then A21: dom L=Seg n by FINSEQ_1:def 3; then A22: dom id X=dom L; reconsider X9=X as Element of Fin X by FINSUB_1:def 5; A23: FinOmega(P)=P by MATRIX_2:26,def 14; g.{}.Fin P=aa $$ ({}.P,Path) by A3; then A24: g.{}=the_unity_wrt aa by FVSUM_1:8,SETWISEO:31; A25: now let x,y such that A26: x in X9 and A27: y in X9 and A28: f.x meets f.y; consider z be set such that A29: z in f.x and A30: z in f.y by A28,XBOOLE_0:3; f.y=F(y) by A8,A27; then A31: ex p st p=z& p.i=y by A30; f.x=F(x) by A8,A26; then ex p st p=z& p.i=x by A29; hence x=y by A31; end; now A32: rng f c= Fin P by RELAT_1:def 19; let x such that A33: x in dom gf; consider k being Element of NAT such that A34: k=x and 1<=k and k<=n by A13,A33; f.k in rng f by A8,A33,A34,FUNCT_1:def 3; then reconsider Fk=F(k) as Element of Fin P by A8,A33,A34,A32; A35: f.k=Fk by A8,A33,A34; gf.k=g.(f.k) by A8,A33,A34,FUNCT_1:13; then A36: gf.k=G(Fk) by A3,A35; G(Fk)=M*(i,k)*Cofactor(M,i,k) by A2,A33,A34,Th23; hence L.x=gf.x by A21,A33,A34,A36,Def7; end; then A37: L=gf by A21,A13,FUNCT_1:2; set Laa=[#](L,the_unity_wrt aa); A38: rng id X=X9; A39: Laa| (dom L)=L by SETWOP_2:21; union (f.:X) c= P proof let x; assume x in union (f.:X); then consider y such that A40: x in y and A41: y in f.:X by TARSKI:def 4; consider z be set such that A42: z in dom f and z in X and A43: f.z=y by A41,FUNCT_1:def 6; y=F(z) by A8,A42,A43; then ex p st x=p & p.i=z by A40; hence thesis; end; then P=union (f.:X) by A15,XBOOLE_0:def 10; then A44: aa $$ (f.:X9,g)= g.FinOmega(P) by A25,A4,A1,A24,A23,Th12; aa $$ (X9,g*f)=aa $$ (f.:X9,g) by A25,A4,A1,A24,Th12; hence Det M = aa $$(findom L,Laa) by A22,A38,A39,A14,A37,A44,A12,SETWOP_2:5 .= Sum L by FVSUM_1:8,SETWOP_2:def 2; end; theorem Th26: for i st i in Seg n holds LaplaceExpC(M,i) = LaplaceExpL(M@,i) proof let i such that A1: i in Seg n; set LL=LaplaceExpL(M@,i); set LC=LaplaceExpC(M,i); reconsider I=i as Element of NAT by ORDINAL1:def 12; A2: len LL=n by Def7; A3: len LC=n by Def8; now let k be Nat such that A4: 1 <=k and A5: k <= n; k in NAT by ORDINAL1:def 12; then A6: k in Seg n by A4,A5; dom LC=Seg n by A3,FINSEQ_1:def 3; then A7: LC.k=M*(k,I)*Cofactor(M,k,I) by A6,Def8; Indices M=[:Seg n,Seg n:] by MATRIX_1:24; then A8: [k,i] in Indices M by A1,A6,ZFMISC_1:87; dom LL=Seg n by A2,FINSEQ_1:def 3; then A9: LL.k=M@*(I,k)*Cofactor(M@,I,k) by A6,Def7; Cofactor(M,k,I)=Cofactor(M@,I,k) by A1,A6,Th24; hence LC.k=LL.k by A8,A7,A9,MATRIX_1:def 6; end; hence thesis by A3,A2,FINSEQ_1:14; end; theorem for j be Nat, M be Matrix of n,K st j in Seg n holds Det M = Sum LaplaceExpC(M,j) proof let j be Nat, M be Matrix of n,K such that A1: j in Seg n; thus Det M = Det M@ by MATRIXR2:43 .= Sum LaplaceExpL(M@,j) by A1,Th25 .= Sum LaplaceExpC(M,j) by A1,Th26; end; theorem Th28: for p,i st len f=n & i in Seg n holds mlt(Line( Matrix_of_Cofactor M,i),f) = LaplaceExpL(RLine(M,i,f),i) proof let p,i such that A1: len f=n and A2: i in Seg n; reconsider N=n as Element of NAT by ORDINAL1:def 12; set KK=the carrier of K; set C=Matrix_of_Cofactor M; reconsider Tp=f,TL=Line(C,i) as Element of N-tuples_on KK by A1,FINSEQ_2:92 ,MATRIX_1:24; set R=RLine(M,i,f); set LL=LaplaceExpL(R,i); set MLT=mlt(TL,Tp); A3: len LL=n by Def7; A4: now A5: dom LL=Seg n by A3,FINSEQ_1:def 3; A6: n=width M by MATRIX_1:24; let j be Nat such that A7: 1<=j and A8: j<=n; j in NAT by ORDINAL1:def 12; then A9: j in Seg n by A7,A8; n=width C by MATRIX_1:24; then A10: Line(C,i).j=C*(i,j) by A9,MATRIX_1:def 7; Indices M=[:Seg n,Seg n:] by MATRIX_1:24; then [i,j] in Indices M by A2,A9,ZFMISC_1:87; then A11: R*(i,j)=f.j by A1,A6,MATRIX11:def 3; Indices C=[:Seg n,Seg n:] by MATRIX_1:24; then [i,j] in Indices C by A2,A9,ZFMISC_1:87; then Line(C,i).j=Cofactor(M,i,j) by A10,Def6; then A12: MLT.j=Cofactor(M,i,j)*(R*(i,j)) by A9,A11,FVSUM_1:61; Cofactor(M,i,j)=Cofactor(R,i,j) by A2,A9,Th15; hence MLT.j=LL.j by A9,A5,A12,Def7; end; len MLT=n by CARD_1:def 7; hence thesis by A3,A4,FINSEQ_1:14; end; theorem Th29: i in Seg n implies Line(M,j) "*" Col((Matrix_of_Cofactor M)@,i) = Det RLine(M,i,Line(M,j)) proof assume A1: i in Seg n; set C=Matrix_of_Cofactor M; len C=n by MATRIX_1:24; then dom C=Seg n by FINSEQ_1:def 3; then A2: Line(C,i)=Col(C@,i) by A1,MATRIX_2:14; width M=n by MATRIX_1:24; then A3: len Line(M,j)=n by MATRIX_1:def 7; thus Det RLine(M,i,Line(M,j)) = Sum LaplaceExpL(RLine(M,i,Line(M,j)),i) by A1 ,Th25 .= Sum mlt(Col(C@,i),Line(M,j)) by A1,A2,A3,Th28 .= Line(M,j) "*" Col(C@,i) by FVSUM_1:64; end; theorem Th30: Det M <> 0.K implies M * ((Det M)" * (Matrix_of_Cofactor M)@) = 1.(K,n) proof set D=Det M; set D9=D"; set C=Matrix_of_Cofactor M; set DC=D9*(C@); set MC=M*DC; set ID=1.(K,n); assume A1: D<>0.K; now A2: Indices MC=Indices ID by MATRIX_1:26; reconsider N=n as Element of NAT by ORDINAL1:def 12; let i,j be Nat such that A3: [i,j] in Indices MC; reconsider COL=Col(C@,j),L=Line(M,i) as Element of N-tuples_on the carrier of K by MATRIX_1:24; reconsider i9=i,j9=j as Element of NAT by ORDINAL1:def 12; A4: len DC=n by MATRIX_1:24; A5: Indices MC=[:Seg n,Seg n:] by MATRIX_1:24; then A6: i in Seg n by A3,ZFMISC_1:87; A7: j in Seg n by A3,A5,ZFMISC_1:87; then A8: 1<=j by FINSEQ_1:1; width (C@)=n by MATRIX_1:24; then j<=width (C@) by A7,FINSEQ_1:1; then Col(DC,j)=D9*COL by A8,MATRIXR1:19; then mlt(Line(M,i),Col(DC,j)) = D9* mlt(L,COL) by FVSUM_1:69; then A9: Line(M,i) "*" Col(DC,j) = D9*(Line(M,i)"*"Col(C@,j)) by FVSUM_1:73 .= D9* Det RLine(M,j9,Line(M,i9))by A7,Th29; A10: width M=n by MATRIX_1:24; then A11: MC*(i,j)=D9* Det RLine(M,j,Line(M,i)) by A3,A4,A9,MATRIX_3:def 4; per cases; suppose A12: i=j; then A13: RLine(M,j,Line(M,i))=M by MATRIX11:30; A14: D*D9=1_K by A1,VECTSP_1:def 10; ID*(i,j) = 1_K by A3,A2,A12,MATRIX_1:def 11; hence ID*(i,j) = MC*(i,j) by A3,A10,A4,A9,A13,A14,MATRIX_3:def 4; end; suppose A15: i<>j; then A16: ID*(i,j) = 0.K by A3,A2,MATRIX_1:def 11; Det RLine(M,j9,Line(M,i9))=0.K by A6,A7,A15,MATRIX11:51; hence ID*(i,j) = MC*(i,j) by A11,A16,VECTSP_1:6; end; end; hence thesis by MATRIX_1:27; end; theorem Th31: for f,i st len f=n & i in Seg n holds mlt(Col(Matrix_of_Cofactor M,i),f) = LaplaceExpL(RLine(M@,i,f),i) proof let f,i such that A1: len f=n and A2: i in Seg n; reconsider N=n as Element of NAT by ORDINAL1:def 12; set KK=the carrier of K; set C=Matrix_of_Cofactor M; reconsider Tp=f,TC=Col(C,i) as Element of N-tuples_on KK by A1,FINSEQ_2:92 ,MATRIX_1:24; set R=RLine(M@,i,f); set LL=LaplaceExpL(R,i); set MCT=mlt(TC,Tp); A3: len LL=n by Def7; A4: now A5: Indices M@=[:Seg n,Seg n:] by MATRIX_1:24; A6: dom LL=Seg n by A3,FINSEQ_1:def 3; A7: width (M@)=n by MATRIX_1:24; let j be Nat such that A8: 1<=j and A9: j<=n; j in NAT by ORDINAL1:def 12; then A10: j in Seg n by A8,A9; then Delete(M@,i,j)=Delete(M,j,i)@ by A2,Th14; then A11: Cofactor(M@,i,j)=Cofactor(M,j,i) by MATRIXR2:43; Indices C=[:Seg n,Seg n:] by MATRIX_1:24; then [j,i] in Indices C by A2,A10,ZFMISC_1:87; then A12: C*(j,i)=Cofactor(M,j,i) by Def6; n=len C by MATRIX_1:24; then dom C=Seg n by FINSEQ_1:def 3; then A13: Col(C,i).j=C*(j,i) by A10,MATRIX_1:def 8; A14: Indices M=[:Seg n,Seg n:] by MATRIX_1:24; then [i,j] in Indices M by A2,A10,ZFMISC_1:87; then R*(i,j)=f.j by A1,A7,A14,A5,MATRIX11:def 3; then A15: MCT.j=Cofactor(M,j,i)*(R*(i,j)) by A10,A13,A12,FVSUM_1:61; Cofactor(R,i,j)=Cofactor(M@,i,j) by A2,A10,Th15; hence MCT.j=LL.j by A10,A11,A6,A15,Def7; end; len MCT=n by CARD_1:def 7; hence thesis by A3,A4,FINSEQ_1:14; end; theorem Th32: i in Seg n & j in Seg n implies Line((Matrix_of_Cofactor M)@,i) "*" Col(M,j) = Det RLine(M@,i,Line(M@,j)) proof assume that A1: i in Seg n and A2: j in Seg n; set C=Matrix_of_Cofactor M; set L=Line(M@,j); A3: width C = n by MATRIX_1:24; width (M@)=n by MATRIX_1:24; then A4: len L=n by MATRIX_1:def 7; A5: width M=n by MATRIX_1:24; thus Det RLine(M@,i,L) = Sum LaplaceExpL(RLine(M@,i,L),i) by A1,Th25 .= Sum mlt(Col(C,i),L) by A1,A4,Th31 .= Line(C@,i) "*" L by A1,A3,MATRIX_2:15 .= Line(C@,i) "*" Col(M,j) by A2,A5,MATRIX_2:15; end; theorem Th33: Det M <> 0.K implies ((Det M)" * (Matrix_of_Cofactor M)@) * M = 1.(K,n) proof set D=Det M; set D9=D"; set C=Matrix_of_Cofactor M; set DC=D9*(C@); set CM=DC*M; set ID=1.(K,n); assume A1: D<>0.K; now A2: Indices CM=Indices ID by MATRIX_1:26; reconsider N=n as Element of NAT by ORDINAL1:def 12; let i,j be Nat such that A3: [i,j] in Indices CM; reconsider COL=Col(M,j),L=Line(C@,i) as Element of N-tuples_on the carrier of K by MATRIX_1:24; reconsider i9=i,j9=j as Element of NAT by ORDINAL1:def 12; A4: len M=n by MATRIX_1:24; A5: Indices CM=[:Seg n,Seg n:] by MATRIX_1:24; then A6: i in Seg n by A3,ZFMISC_1:87; then A7: 1<=i by FINSEQ_1:1; A8: j in Seg n by A3,A5,ZFMISC_1:87; len (C@)=n by MATRIX_1:24; then i<=len (C@) by A6,FINSEQ_1:1; then Line(DC,i)=D9*L by A7,MATRIXR1:20; then mlt(Line(DC,i),Col(M,j)) = D9* mlt(L,COL) by FVSUM_1:69; then A9: Line(DC,i)"*"Col(M,j) = D9*(Line(C@,i)"*"Col(M,j)) by FVSUM_1:73 .= D9*Det RLine(M@,i9,Line(M@,j9))by A6,A8,Th32; A10: width DC=n by MATRIX_1:24; then A11: CM*(i,j)=D9* Det RLine(M@,i,Line(M@,j)) by A3,A4,A9,MATRIX_3:def 4; per cases; suppose A12: i=j; then A13: RLine(M@,i,Line(M@,j))=M@ by MATRIX11:30; A14: D=Det M@ by MATRIXR2:43; A15: D9*D=1_K by A1,VECTSP_1:def 10; ID*(i,j) = 1_K by A3,A2,A12,MATRIX_1:def 11; hence ID*(i,j) = CM*(i,j) by A3,A10,A4,A9,A13,A15,A14,MATRIX_3:def 4; end; suppose A16: i<>j; then A17: ID*(i,j) = 0.K by A3,A2,MATRIX_1:def 11; Det RLine(M@,i9,Line(M@,j9))=0.K by A6,A8,A16,MATRIX11:51; hence ID*(i,j) = CM*(i,j) by A11,A17,VECTSP_1:6; end; end; hence thesis by MATRIX_1:27; end; theorem Th34: M is invertible iff Det M <> 0.K proof thus M is invertible implies Det M <> 0.K proof reconsider N=n as Element of NAT by ORDINAL1:def 12; assume M is invertible; then consider M1 be Matrix of n,K such that A1: M is_reverse_of M1 by MATRIX_6:def 3; per cases by NAT_1:14; suppose N=0; then Det M=1_K by MATRIXR2:41; hence thesis; end; suppose A2: N>=1; A3: M*M1=(1.(K,n)) by A1,MATRIX_6:def 2; Det (1.(K,n))=1_K by A2,MATRIX_7:16; then Det M*Det M1=1_K by A2,A3,MATRIX11:62; hence thesis by VECTSP_1:12; end; end; set C=(Det M)" * (Matrix_of_Cofactor M)@; assume A4: Det M <> 0.K; then A5: M*C=1.(K,n) by Th30; C*M=1.(K,n) by A4,Th33; then M is_reverse_of C by A5,MATRIX_6:def 2; hence thesis by MATRIX_6:def 3; end; theorem Th35: Det M <> 0.K implies M~ = (Det M)" * (Matrix_of_Cofactor M)@ proof set C=(Det M)" * (Matrix_of_Cofactor M)@; assume A1: Det M <> 0.K; then A2: M*C=1.(K,n) by Th30; C*M=1.(K,n) by A1,Th33; then A3: M is_reverse_of C by A2,MATRIX_6:def 2; M is invertible by A1,Th34; hence thesis by A3,MATRIX_6:def 4; end; theorem for M be Matrix of n,K st M is invertible for i,j st [i,j] in Indices (M~) holds M~*(i,j) = (Det M)" * power(K).(-1_K,i+j) * Minor(M,j,i) proof let M be Matrix of n,K; assume M is invertible; then A1: Det M<>0.K by Th34; set D=Det M; set COF=Matrix_of_Cofactor M; let i,j; assume [i,j] in Indices (M~); then A2: [i,j] in Indices (COF@) by MATRIX_1:26; then A3: [j,i] in Indices COF by MATRIX_1:def 6; thus M~*(i,j)=(D" * COF@)*(i,j) by A1,Th35 .=D"*((COF@)*(i,j)) by A2,MATRIX_3:def 5 .=D"*(COF*(j,i)) by A3,MATRIX_1:def 6 .=D"*Cofactor(M,j,i) by A3,Def6 .=D"*power(K).(-1_K,i+j) * Minor(M,j,i) by GROUP_1:def 3; end; theorem Th37: for A be Matrix of n,K st Det A <> 0.K for x,b be Matrix of K st len x = n & A * x = b holds x = A~ * b & for i,j st [i,j] in Indices x holds x* (i,j) = (Det A)" * Det ReplaceCol(A,i,Col(b,j)) proof let A be Matrix of n,K such that A1: Det A <> 0.K; A is invertible by A1,Th34; then A~ is_reverse_of A by MATRIX_6:def 4; then A2: A~*A=1.(K,n) by MATRIX_6:def 2; set MC=Matrix_of_Cofactor A; set D=Det A; A3: width MC=n by MATRIX_1:24; A4: len (MC@)=n by MATRIX_1:24; A5: width (MC@)=n by MATRIX_1:24; A6: width (A~)=n by MATRIX_1:24; A7: width A=n by MATRIX_1:24; let x,b be Matrix of K such that A8: len x = n and A9: A * x = b; A10: len A=n by MATRIX_1:24; then A11: len b=n by A8,A9,A7,MATRIX_3:def 4; x = 1.(K,n) * x by A8,MATRIXR2:68; hence A12: x=A~ * b by A8,A9,A6,A10,A7,A2,MATRIX_3:33; let i,j such that A13: [i,j] in Indices x; A14: len Col(b,j)=n by A11,MATRIX_1:def 8; Indices x=[:Seg n,Seg width x:] by A8,FINSEQ_1:def 3; then A15: i in Seg n by A13,ZFMISC_1:87; then A16: 1<=i by FINSEQ_1:1; A17: i<= n by A15,FINSEQ_1:1; thus x*(i,j) = Line(A~,i)"*"Col(b,j) by A6,A12,A13,A11,MATRIX_3:def 4 .= Line(D" * MC@,i)"*"Col(b,j) by A1,Th35 .= (D"*Line(MC@,i))"*"Col(b,j) by A4,A16,A17,MATRIXR1:20 .= Sum(D"*mlt(Line(MC@,i),Col(b,j))) by A5,A11,FVSUM_1:68 .= D"*(Line(MC@,i)"*"Col(b,j)) by FVSUM_1:73 .= D"*(Col(MC,i)"*"Col(b,j)) by A3,A15,MATRIX_2:15 .= D"*Sum(LaplaceExpL(RLine(A@,i,Col(b,j)),i)) by A15,A14,Th31 .= D"*Det RLine(A@,i,Col(b,j)) by A15,Th25 .= D"*Det (RLine(A@,i,Col(b,j))@) by MATRIXR2:43 .= D"*Det RCol(A,i,Col(b,j)) by Th19; end; theorem Th38: for A be Matrix of n,K st Det A <> 0.K for x,b be Matrix of K st width x = n & x * A = b holds x = b * A~ & for i,j st [i,j] in Indices x holds x*(i,j) = (Det A)" * Det ReplaceLine(A,j,Line(b,i)) proof let A be Matrix of n,K such that A1: Det A <> 0.K; A is invertible by A1,Th34; then A~ is_reverse_of A by MATRIX_6:def 4; then A2: A*A~=1.(K,n) by MATRIX_6:def 2; A3: width A=n by MATRIX_1:24; let x,b be Matrix of K such that A4: width x = n and A5: x * A = b; A6: len A=n by MATRIX_1:24; then A7: width b=n by A4,A5,A3,MATRIX_3:def 4; set MC=Matrix_of_Cofactor A; set D=Det A; A8: len (MC@)=n by MATRIX_1:24; A9: width (MC@)=n by MATRIX_1:24; len MC=n by MATRIX_1:24; then A10: Seg n=dom MC by FINSEQ_1:def 3; A11: len (A~)=n by MATRIX_1:24; x = x* 1.(K,n) by A4,MATRIXR2:67; hence A12: x= b * A~ by A4,A5,A11,A6,A3,A2,MATRIX_3:33; let i,j such that A13: [i,j] in Indices x; A14: j in Seg n by A4,A13,ZFMISC_1:87; then A15: 1<=j by FINSEQ_1:1; A16: len Line(b,i)=n by A7,MATRIX_1:def 7; A17: j<= n by A14,FINSEQ_1:1; thus x*(i,j) = Line(b,i)"*"Col(A~,j) by A11,A12,A13,A7,MATRIX_3:def 4 .= Line(b,i)"*"Col(D" * MC@,j) by A1,Th35 .= Line(b,i)"*"(D"*Col(MC@,j)) by A9,A15,A17,MATRIXR1:19 .= (D"*Col(MC@,j))"*"Line(b,i) by FVSUM_1:90 .= Sum(D"*mlt(Col(MC@,j),Line(b,i))) by A8,A7,FVSUM_1:69 .= D"*(Col(MC@,j)"*"Line(b,i)) by FVSUM_1:73 .= D"*(Line(MC,j)"*"Line(b,i)) by A14,A10,MATRIX_2:14 .= D"*Sum(LaplaceExpL(RLine(A,j,Line(b,i)),j)) by A14,A16,Th28 .= D"*Det RLine(A,j,Line(b,i)) by A14,Th25; end; begin :: Product by a vector definition let D be non empty set; let f be FinSequence of D; redefine func <*f*> -> Matrix of 1,len f,D; coherence by MATRIX_1:11; end; definition let K; let M be Matrix of K; let f be FinSequence of K; func M * f -> Matrix of K equals M * (<*f*>@); coherence; func f * M -> Matrix of K equals <*f*> * M; coherence; end; theorem for A be Matrix of n,K st Det A <> 0.K for x,b be FinSequence of K st len x = n & A * x = <*b*>@ holds <*x*>@ = A~ * b & for i st i in Seg n holds x. i = (Det A)" * Det ReplaceCol(A,i,b) proof let A be Matrix of n,K such that A1: Det A <> 0.K; let x,b be FinSequence of K such that A2: len x = n and A3: A * x = <*b*>@; set X=<*x*>; len X=1 by MATRIX_1:def 2; then A4: len x=width X by MATRIX_1:20; then A5: len (X@)=len x by MATRIX_1:def 6; hence X@ = A~ * b by A1,A2,A3,Th37; set B=<*b*>; A6: 1 in Seg 1; then A7: Line(X,1)=X.1 by MATRIX_2:8; len B=1 by MATRIX_1:def 2; then A8: 1 in dom B by A6,FINSEQ_1:def 3; A9: Line(B,1)=B.1 by A6,MATRIX_2:8; let i such that A10: i in Seg n; n>0 by A10; then width (X@) = len X by A2,A4,MATRIX_2:10 .= 1 by MATRIX_1:def 2; then Indices (X@)=[:Seg n,Seg 1:] by A2,A5,FINSEQ_1:def 3; then A11: [i,1] in Indices (X@) by A10,A6,ZFMISC_1:87; then [1,i] in Indices X by MATRIX_1:def 6; then (X@)*(i,1) = X*(1,i) by MATRIX_1:def 6 .= Line(X,1).i by A2,A4,A10,MATRIX_1:def 7 .= x.i by A7,FINSEQ_1:40; hence x.i = (Det A)" * Det ReplaceCol(A,i,Col(B@,1)) by A1,A2,A3,A5,A11,Th37 .= (Det A)" * Det ReplaceCol(A,i,Line(B,1)) by A8,MATRIX_2:14 .= (Det A)" * Det ReplaceCol(A,i,b) by A9,FINSEQ_1:40; end; ::$N Cramer's Rule theorem for A be Matrix of n,K st Det A <> 0.K for x,b be FinSequence of K st len x = n & x * A = <*b*> holds <*x*> = b * A~ & for i st i in Seg n holds x.i = (Det A)" * Det ReplaceLine(A,i,b) proof let A be Matrix of n,K such that A1: Det A <> 0.K; let x,b be FinSequence of K such that A2: len x = n and A3: x * A = <*b*>; set X=<*x*>; A4: width X=len x by MATRIX_1:23; hence X = b * A~ by A1,A2,A3,Th38; A5: [:Seg 1,Seg n:]= Indices X by A2,MATRIX_1:23; set B=<*b*>; A6: 1 in Seg 1; then A7: Line(X,1)=X. 1 by MATRIX_2:8; let i such that A8: i in Seg n; A9: [1,i] in [:Seg 1,Seg n:] by A8,A6,ZFMISC_1:87; A10: Line(B,1)=B.1 by A6,MATRIX_2:8; X*(1,i) = Line(X,1).i by A2,A4,A8,MATRIX_1:def 7 .= x.i by A7,FINSEQ_1:40; hence x.i = (Det A)" * Det ReplaceLine(A,i,Line(B,1)) by A1,A2,A3,A4,A9,A5 ,Th38 .= (Det A)" * Det ReplaceLine(A,i,b) by A10,FINSEQ_1:40; end;