:: Laplace Expansion :: by Karol P\c{a}k and Andrzej Trybulec :: :: Received August 13, 2007 :: Copyright (c) 2007-2012 Association of Mizar Users begin theorem Th1: :: LAPLACE:1 for f being FinSequence for i being Nat st i in dom f holds len (Del (f,i)) = (len f) -' 1 proofend; theorem Th2: :: LAPLACE:2 for K being Field for i, j, n being Nat for M being Matrix of n,K st i in dom M holds len (Deleting (M,i,j)) = n -' 1 proofend; theorem Th3: :: LAPLACE:3 for j being Nat for K being Field for A being Matrix of K st j in Seg (width A) holds width (DelCol (A,j)) = (width A) -' 1 proofend; theorem Th4: :: LAPLACE:4 for K being Field for A being Matrix of K for i being Nat st len A > 1 holds width A = width (DelLine (A,i)) proofend; theorem Th5: :: LAPLACE:5 for j, n being Nat for K being Field for M being Matrix of n,K for i being Nat st j in Seg (width M) holds width (Deleting (M,i,j)) = n -' 1 proofend; 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; let i be Nat; :: original:. redefine funcB . (g,i) -> Element of G; coherence B . (g,i) is Element of G proofend; end; theorem Th6: :: LAPLACE:6 for n being Nat holds card (Permutations n) = n ! proofend; theorem Th7: :: LAPLACE:7 for n, i, j being Nat st i in Seg (n + 1) & j in Seg (n + 1) holds card { p1 where p1 is Element of Permutations (n + 1) : p1 . i = j } = n ! proofend; theorem Th8: :: LAPLACE:8 for n being Nat for K being Fanoian Field for p2 being Element of Permutations (n + 2) for X, Y being Element of Fin (2Set (Seg (n + 2))) st Y = { s where s is Element of 2Set (Seg (n + 2)) : ( 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)) proofend; theorem Th9: :: LAPLACE:9 for n being Nat for K being Fanoian Field for p2 being Element of Permutations (n + 2) for i, j being Nat st i in Seg (n + 2) & p2 . i = j holds ex X being Element of Fin (2Set (Seg (n + 2))) st ( X = { {N,i} where N is Element of NAT : {N,i} in 2Set (Seg (n + 2)) } & the multF of K $$ (X,(Part_sgn (p2,K))) = (power K) . ((- (1_ K)),(i + j)) ) proofend; theorem Th10: :: LAPLACE:10 for n, i, j being Nat st i in Seg (n + 1) & n >= 2 holds ex Proj being Function of (2Set (Seg n)),(2Set (Seg (n + 1))) st ( rng Proj = (2Set (Seg (n + 1))) \ { {N,i} where N is Element of NAT : {N,i} in 2Set (Seg (n + 1)) } & Proj is one-to-one & ( for k, m being Nat st k < m & {k,m} in 2Set (Seg n) holds ( ( m < i & k < i implies Proj . {k,m} = {k,m} ) & ( m >= i & k < i implies Proj . {k,m} = {k,(m + 1)} ) & ( m >= i & k >= i implies Proj . {k,m} = {(k + 1),(m + 1)} ) ) ) ) proofend; theorem Th11: :: LAPLACE:11 for n being Nat st n < 2 holds for p being Element of Permutations n holds ( p is even & p = idseq n ) proofend; theorem Th12: :: LAPLACE:12 for X, Y, D being non empty set for f being Function of X,(Fin Y) for g being Function of (Fin Y),D for F being BinOp of D st ( for A, B being Element of Fin Y st A misses B holds F . ((g . A),(g . B)) = g . (A \/ B) ) & F is commutative & F is associative & F is having_a_unity & g . {} = the_unity_wrt F holds for I being Element of Fin X st ( for x, y being set 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 ) proofend; begin definition let i, j, n be Nat; let K be Field; 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: :: LAPLACE:def 1 Deleting (M,i,j); coherence Deleting (M,i,j) is Matrix of n -' 1,K proofend; end; :: deftheorem Def1 defines Delete LAPLACE:def_1_:_ for i, j, n being Nat for K being Field for M being Matrix of n,K st i in Seg n & j in Seg n holds Delete (M,i,j) = Deleting (M,i,j); theorem Th13: :: LAPLACE:13 for n being Nat for K being Field for M being Matrix of n,K for i, j being Nat st i in Seg n & j in Seg n holds for k, m being Nat 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)) ) ) proofend; theorem Th14: :: LAPLACE:14 for n being Nat for K being Field for M being Matrix of n,K for i, j being Nat st i in Seg n & j in Seg n holds (Delete (M,i,j)) @ = Delete ((M @),j,i) proofend; theorem Th15: :: LAPLACE:15 for n being Nat for K being Field for M being Matrix of n,K for f being FinSequence of K for i, j being Nat st i in Seg n & j in Seg n holds Delete (M,i,j) = Delete ((RLine (M,i,f)),i,j) proofend; definition let c, n, m be Nat; let D be non empty set ; 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: :: LAPLACE:def 2 ( len it = len M & width it = width M & ( for i, j being Nat 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 for b1 being Matrix of n,m,D holds verum ; existence ( ( len pD = len M implies ex b1 being Matrix of n,m,D st ( len b1 = len M & width b1 = width M & ( for i, j being Nat st [i,j] in Indices M holds ( ( j <> c implies b1 * (i,j) = M * (i,j) ) & ( j = c implies b1 * (i,c) = pD . i ) ) ) ) ) & ( not len pD = len M implies ex b1 being Matrix of n,m,D st b1 = M ) ) proofend; uniqueness for b1, b2 being Matrix of n,m,D holds ( ( len pD = len M & len b1 = len M & width b1 = width M & ( for i, j being Nat st [i,j] in Indices M holds ( ( j <> c implies b1 * (i,j) = M * (i,j) ) & ( j = c implies b1 * (i,c) = pD . i ) ) ) & len b2 = len M & width b2 = width M & ( for i, j being Nat st [i,j] in Indices M holds ( ( j <> c implies b2 * (i,j) = M * (i,j) ) & ( j = c implies b2 * (i,c) = pD . i ) ) ) implies b1 = b2 ) & ( not len pD = len M & b1 = M & b2 = M implies b1 = b2 ) ) proofend; end; :: deftheorem Def2 defines ReplaceCol LAPLACE:def_2_:_ for c, n, m being Nat for D being non empty set for M being Matrix of n,m,D for pD being FinSequence of D for b7 being Matrix of n,m,D holds ( ( len pD = len M implies ( b7 = ReplaceCol (M,c,pD) iff ( len b7 = len M & width b7 = width M & ( for i, j being Nat st [i,j] in Indices M holds ( ( j <> c implies b7 * (i,j) = M * (i,j) ) & ( j = c implies b7 * (i,c) = pD . i ) ) ) ) ) ) & ( not len pD = len M implies ( b7 = ReplaceCol (M,c,pD) iff b7 = M ) ) ); notation let c, n, m be Nat; let D be non empty set ; 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 :: LAPLACE:16 for n, m, c being Nat for D being non empty set for AD being Matrix of n,m,D for pD being FinSequence of D for i being Nat 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) ) ) proofend; theorem :: LAPLACE:17 for n, m, c being Nat for D being non empty set for AD being Matrix of n,m,D for pD being FinSequence of D st not c in Seg (width AD) holds RCol (AD,c,pD) = AD proofend; theorem :: LAPLACE:18 for n, m, c being Nat for D being non empty set for AD being Matrix of n,m,D holds RCol (AD,c,(Col (AD,c))) = AD proofend; theorem Th19: :: LAPLACE:19 for n, m, c being Nat for D being non empty set for pD being FinSequence of D for A being Matrix of n,m,D for A9 being Matrix of m,n,D st A9 = A @ & ( m = 0 implies n = 0 ) holds ReplaceCol (A,c,pD) = (ReplaceLine (A9,c,pD)) @ proofend; begin definition let i, n be Nat; 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: :: LAPLACE:def 3 for k being Nat st k in Seg n holds ( ( k < i implies ( ( perm . k < perm . i implies it . k = perm . k ) & ( perm . 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 ex b1 being Element of Permutations n st for k being Nat st k in Seg n holds ( ( k < i implies ( ( perm . k < perm . i implies b1 . k = perm . k ) & ( perm . k >= perm . i implies b1 . k = (perm . k) - 1 ) ) ) & ( k >= i implies ( ( perm . (k + 1) < perm . i implies b1 . k = perm . (k + 1) ) & ( perm . (k + 1) >= perm . i implies b1 . k = (perm . (k + 1)) - 1 ) ) ) ) proofend; uniqueness for b1, b2 being Element of Permutations n st ( for k being Nat st k in Seg n holds ( ( k < i implies ( ( perm . k < perm . i implies b1 . k = perm . k ) & ( perm . k >= perm . i implies b1 . k = (perm . k) - 1 ) ) ) & ( k >= i implies ( ( perm . (k + 1) < perm . i implies b1 . k = perm . (k + 1) ) & ( perm . (k + 1) >= perm . i implies b1 . k = (perm . (k + 1)) - 1 ) ) ) ) ) & ( for k being Nat st k in Seg n holds ( ( k < i implies ( ( perm . k < perm . i implies b2 . k = perm . k ) & ( perm . k >= perm . i implies b2 . k = (perm . k) - 1 ) ) ) & ( k >= i implies ( ( perm . (k + 1) < perm . i implies b2 . k = perm . (k + 1) ) & ( perm . (k + 1) >= perm . i implies b2 . k = (perm . (k + 1)) - 1 ) ) ) ) ) holds b1 = b2 proofend; end; :: deftheorem Def3 defines Rem LAPLACE:def_3_:_ for i, n being Nat for perm being Element of Permutations (n + 1) st i in Seg (n + 1) holds for b4 being Element of Permutations n holds ( b4 = Rem (perm,i) iff for k being Nat st k in Seg n holds ( ( k < i implies ( ( perm . k < perm . i implies b4 . k = perm . k ) & ( perm . k >= perm . i implies b4 . k = (perm . k) - 1 ) ) ) & ( k >= i implies ( ( perm . (k + 1) < perm . i implies b4 . k = perm . (k + 1) ) & ( perm . (k + 1) >= perm . i implies b4 . k = (perm . (k + 1)) - 1 ) ) ) ) ); theorem Th20: :: LAPLACE:20 for n, i, j being Nat st i in Seg (n + 1) & j in Seg (n + 1) holds for P being set st P = { p1 where p1 is Element of Permutations (n + 1) : p1 . i = j } holds ex Proj being Function of P,(Permutations n) st ( Proj is bijective & ( for q1 being Element of Permutations (n + 1) st q1 . i = j holds Proj . q1 = Rem (q1,i) ) ) proofend; theorem Th21: :: LAPLACE:21 for n being Nat for p1 being Element of Permutations (n + 1) for K being Field for a being Element of K for i, j being Nat st i in Seg (n + 1) & p1 . i = j holds - (a,p1) = ((power K) . ((- (1_ K)),(i + j))) * (- (a,(Rem (p1,i)))) proofend; theorem Th22: :: LAPLACE:22 for n being Nat for p1 being Element of Permutations (n + 1) for K being Field for i, j being Nat st i in Seg (n + 1) & p1 . i = j holds for M being Matrix of n + 1,K for DM being 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))) proofend; begin definition let i, j, n be Nat; let K be Field; let M be Matrix of n,K; func Minor (M,i,j) -> Element of K equals :: LAPLACE:def 4 Det (Delete (M,i,j)); coherence Det (Delete (M,i,j)) is Element of K ; end; :: deftheorem defines Minor LAPLACE:def_4_:_ for i, j, n being Nat for K being Field for M being Matrix of n,K holds Minor (M,i,j) = Det (Delete (M,i,j)); definition let i, j, n be Nat; let K be Field; let M be Matrix of n,K; func Cofactor (M,i,j) -> Element of K equals :: LAPLACE:def 5 ((power K) . ((- (1_ K)),(i + j))) * (Minor (M,i,j)); coherence ((power K) . ((- (1_ K)),(i + j))) * (Minor (M,i,j)) is Element of K ; end; :: deftheorem defines Cofactor LAPLACE:def_5_:_ for i, j, n being Nat for K being Field for M being Matrix of n,K holds Cofactor (M,i,j) = ((power K) . ((- (1_ K)),(i + j))) * (Minor (M,i,j)); theorem Th23: :: LAPLACE:23 for n being Nat for K being Field for i, j being Nat st i in Seg n & j in Seg n holds for P being Element of Fin (Permutations n) st P = { p where p is Element of Permutations n : p . i = j } holds for M being Matrix of n,K holds the addF of K $$ (P,(Path_product M)) = (M * (i,j)) * (Cofactor (M,i,j)) proofend; theorem Th24: :: LAPLACE:24 for n being Nat for K being Field for M being Matrix of n,K for i, j being Nat st i in Seg n & j in Seg n holds Minor (M,i,j) = Minor ((M @),j,i) proofend; definition let n be Nat; let K be Field; let M be Matrix of n,K; func Matrix_of_Cofactor M -> Matrix of n,K means :Def6: :: LAPLACE:def 6 for i, j being Nat st [i,j] in Indices it holds it * (i,j) = Cofactor (M,i,j); existence ex b1 being Matrix of n,K st for i, j being Nat st [i,j] in Indices b1 holds b1 * (i,j) = Cofactor (M,i,j) proofend; uniqueness for b1, b2 being Matrix of n,K st ( for i, j being Nat st [i,j] in Indices b1 holds b1 * (i,j) = Cofactor (M,i,j) ) & ( for i, j being Nat st [i,j] in Indices b2 holds b2 * (i,j) = Cofactor (M,i,j) ) holds b1 = b2 proofend; end; :: deftheorem Def6 defines Matrix_of_Cofactor LAPLACE:def_6_:_ for n being Nat for K being Field for M, b4 being Matrix of n,K holds ( b4 = Matrix_of_Cofactor M iff for i, j being Nat st [i,j] in Indices b4 holds b4 * (i,j) = Cofactor (M,i,j) ); begin definition let n, i be Nat; let K be Field; let M be Matrix of n,K; func LaplaceExpL (M,i) -> FinSequence of K means :Def7: :: LAPLACE:def 7 ( len it = n & ( for j being Nat st j in dom it holds it . j = (M * (i,j)) * (Cofactor (M,i,j)) ) ); existence ex b1 being FinSequence of K st ( len b1 = n & ( for j being Nat st j in dom b1 holds b1 . j = (M * (i,j)) * (Cofactor (M,i,j)) ) ) proofend; uniqueness for b1, b2 being FinSequence of K st len b1 = n & ( for j being Nat st j in dom b1 holds b1 . j = (M * (i,j)) * (Cofactor (M,i,j)) ) & len b2 = n & ( for j being Nat st j in dom b2 holds b2 . j = (M * (i,j)) * (Cofactor (M,i,j)) ) holds b1 = b2 proofend; end; :: deftheorem Def7 defines LaplaceExpL LAPLACE:def_7_:_ for n, i being Nat for K being Field for M being Matrix of n,K for b5 being FinSequence of K holds ( b5 = LaplaceExpL (M,i) iff ( len b5 = n & ( for j being Nat st j in dom b5 holds b5 . j = (M * (i,j)) * (Cofactor (M,i,j)) ) ) ); definition let n, j be Nat; let K be Field; let M be Matrix of n,K; func LaplaceExpC (M,j) -> FinSequence of K means :Def8: :: LAPLACE:def 8 ( len it = n & ( for i being Nat st i in dom it holds it . i = (M * (i,j)) * (Cofactor (M,i,j)) ) ); existence ex b1 being FinSequence of K st ( len b1 = n & ( for i being Nat st i in dom b1 holds b1 . i = (M * (i,j)) * (Cofactor (M,i,j)) ) ) proofend; uniqueness for b1, b2 being FinSequence of K st len b1 = n & ( for i being Nat st i in dom b1 holds b1 . i = (M * (i,j)) * (Cofactor (M,i,j)) ) & len b2 = n & ( for i being Nat st i in dom b2 holds b2 . i = (M * (i,j)) * (Cofactor (M,i,j)) ) holds b1 = b2 proofend; end; :: deftheorem Def8 defines LaplaceExpC LAPLACE:def_8_:_ for n, j being Nat for K being Field for M being Matrix of n,K for b5 being FinSequence of K holds ( b5 = LaplaceExpC (M,j) iff ( len b5 = n & ( for i being Nat st i in dom b5 holds b5 . i = (M * (i,j)) * (Cofactor (M,i,j)) ) ) ); theorem Th25: :: LAPLACE:25 for n being Nat for K being Field for i being Nat for M being Matrix of n,K st i in Seg n holds Det M = Sum (LaplaceExpL (M,i)) proofend; theorem Th26: :: LAPLACE:26 for n being Nat for K being Field for M being Matrix of n,K for i being Nat st i in Seg n holds LaplaceExpC (M,i) = LaplaceExpL ((M @),i) proofend; theorem :: LAPLACE:27 for n being Nat for K being Field for j being Nat for M being Matrix of n,K st j in Seg n holds Det M = Sum (LaplaceExpC (M,j)) proofend; theorem Th28: :: LAPLACE:28 for n being Nat for K being Field for f being FinSequence of K for M being Matrix of n,K for p being Element of Permutations n for i being Nat st len f = n & i in Seg n holds mlt ((Line ((Matrix_of_Cofactor M),i)),f) = LaplaceExpL ((RLine (M,i,f)),i) proofend; theorem Th29: :: LAPLACE:29 for i, n, j being Nat for K being Field for M being Matrix of n,K st i in Seg n holds (Line (M,j)) "*" (Col (((Matrix_of_Cofactor M) @),i)) = Det (RLine (M,i,(Line (M,j)))) proofend; theorem Th30: :: LAPLACE:30 for n being Nat for K being Field for M being Matrix of n,K st Det M <> 0. K holds M * (((Det M) ") * ((Matrix_of_Cofactor M) @)) = 1. (K,n) proofend; theorem Th31: :: LAPLACE:31 for n being Nat for K being Field for M being Matrix of n,K for f being FinSequence of K for i being Nat st len f = n & i in Seg n holds mlt ((Col ((Matrix_of_Cofactor M),i)),f) = LaplaceExpL ((RLine ((M @),i,f)),i) proofend; theorem Th32: :: LAPLACE:32 for i, n, j being Nat for K being Field for M being Matrix of n,K st i in Seg n & j in Seg n holds (Line (((Matrix_of_Cofactor M) @),i)) "*" (Col (M,j)) = Det (RLine ((M @),i,(Line ((M @),j)))) proofend; theorem Th33: :: LAPLACE:33 for n being Nat for K being Field for M being Matrix of n,K st Det M <> 0. K holds (((Det M) ") * ((Matrix_of_Cofactor M) @)) * M = 1. (K,n) proofend; theorem Th34: :: LAPLACE:34 for n being Nat for K being Field for M being Matrix of n,K holds ( M is invertible iff Det M <> 0. K ) proofend; theorem Th35: :: LAPLACE:35 for n being Nat for K being Field for M being Matrix of n,K st Det M <> 0. K holds M ~ = ((Det M) ") * ((Matrix_of_Cofactor M) @) proofend; theorem :: LAPLACE:36 for n being Nat for K being Field for M being Matrix of n,K st M is invertible holds for i, j being Nat st [i,j] in Indices (M ~) holds (M ~) * (i,j) = (((Det M) ") * ((power K) . ((- (1_ K)),(i + j)))) * (Minor (M,j,i)) proofend; theorem Th37: :: LAPLACE:37 for n being Nat for K being Field for A being Matrix of n,K st Det A <> 0. K holds for x, b being Matrix of K st len x = n & A * x = b holds ( x = (A ~) * b & ( for i, j being Nat st [i,j] in Indices x holds x * (i,j) = ((Det A) ") * (Det (ReplaceCol (A,i,(Col (b,j))))) ) ) proofend; theorem Th38: :: LAPLACE:38 for n being Nat for K being Field for A being Matrix of n,K st Det A <> 0. K holds for x, b being Matrix of K st width x = n & x * A = b holds ( x = b * (A ~) & ( for i, j being Nat st [i,j] in Indices x holds x * (i,j) = ((Det A) ") * (Det (ReplaceLine (A,j,(Line (b,i))))) ) ) proofend; begin definition let D be non empty set ; let f be FinSequence of D; :: original:<* redefine func<*f*> -> Matrix of 1, len f,D; coherence <*f*> is Matrix of 1, len f,D by MATRIX_1:11; end; definition let K be Field; let M be Matrix of K; let f be FinSequence of K; funcM * f -> Matrix of K equals :: LAPLACE:def 9 M * (<*f*> @); coherence M * (<*f*> @) is Matrix of K ; funcf * M -> Matrix of K equals :: LAPLACE:def 10 <*f*> * M; coherence <*f*> * M is Matrix of K ; end; :: deftheorem defines * LAPLACE:def_9_:_ for K being Field for M being Matrix of K for f being FinSequence of K holds M * f = M * (<*f*> @); :: deftheorem defines * LAPLACE:def_10_:_ for K being Field for M being Matrix of K for f being FinSequence of K holds f * M = <*f*> * M; theorem :: LAPLACE:39 for n being Nat for K being Field for A being Matrix of n,K st Det A <> 0. K holds for x, b being FinSequence of K st len x = n & A * x = <*b*> @ holds ( <*x*> @ = (A ~) * b & ( for i being Nat st i in Seg n holds x . i = ((Det A) ") * (Det (ReplaceCol (A,i,b))) ) ) proofend; :: [WP: ] Cramer's_Rule theorem :: LAPLACE:40 for n being Nat for K being Field for A being Matrix of n,K st Det A <> 0. K holds for x, b being FinSequence of K st len x = n & x * A = <*b*> holds ( <*x*> = b * (A ~) & ( for i being Nat st i in Seg n holds x . i = ((Det A) ") * (Det (ReplaceLine (A,i,b))) ) ) proofend;