:: Determinant and Inverse of Matrices of Real Elements :: by Nobuyuki Tamura and Yatsuka Nakamura :: :: Received July 17, 2007 :: Copyright (c) 2007-2012 Association of Mizar Users begin Lm1: for F1, F2 being FinSequence of REAL for j being Element of NAT st len F1 = len F2 holds (F1 - F2) . j = (F1 . j) - (F2 . j) proofend; theorem Th1: :: MATRIXR2:1 for x, y being FinSequence of REAL st len x = len y & x + y = 0* (len x) holds ( x = - y & y = - x ) proofend; Lm2: for D being non empty set for i being Element of NAT for A being Matrix of D st 1 <= i & i <= len A holds Line (A,i) = A . i proofend; theorem Th2: :: MATRIXR2:2 for D being non empty set for i, j being Element of NAT for A being Matrix of D for p being FinSequence of D st p = A . i & 1 <= i & i <= len A & 1 <= j & j <= width A & len p = width A holds A * (i,j) = p . j proofend; theorem Th3: :: MATRIXR2:3 for i, j being Element of NAT for a being real number for A being Matrix of REAL st [i,j] in Indices A holds (a * A) * (i,j) = a * (A * (i,j)) proofend; theorem Th4: :: MATRIXR2:4 for n being Element of NAT for A, B being Matrix of n, REAL holds ( len (A * B) = len A & width (A * B) = width B & len (A * B) = n & width (A * B) = n ) proofend; theorem Th5: :: MATRIXR2:5 for a being real number for A being Matrix of REAL holds ( len (a * A) = len A & width (a * A) = width A ) proofend; begin theorem Th6: :: MATRIXR2:6 for A, B being Matrix of REAL st len A = len B & width A = width B holds ( len (A - B) = len A & width (A - B) = width A & ( for i, j being Element of NAT st [i,j] in Indices A holds (A - B) * (i,j) = (A * (i,j)) - (B * (i,j)) ) ) proofend; definition let n be Element of NAT ; let A, B be Matrix of n, REAL ; :: original:* redefine funcA * B -> Matrix of n, REAL ; coherence A * B is Matrix of n, REAL proofend; end; theorem Th7: :: MATRIXR2:7 for A, B being Matrix of REAL st len A = len B & width A = width B & len A > 0 holds A + (B - B) = A proofend; theorem :: MATRIXR2:8 for A, B being Matrix of REAL st len A = len B & width A = width B & len A > 0 holds (A + B) - B = A proofend; Lm3: for i, j being Element of NAT for A being Matrix of REAL st [i,j] in Indices A holds (- A) * (i,j) = - (A * (i,j)) proofend; theorem Th9: :: MATRIXR2:9 for A being Matrix of REAL holds (- 1) * A = - A proofend; theorem Th10: :: MATRIXR2:10 for A being Matrix of REAL for i, j being Element of NAT st [i,j] in Indices A holds (- A) * (i,j) = - (A * (i,j)) proofend; theorem :: MATRIXR2:11 for a, b being Real for A being Matrix of REAL holds (a * b) * A = a * (b * A) proofend; theorem Th12: :: MATRIXR2:12 for a, b being Real for A being Matrix of REAL holds (a + b) * A = (a * A) + (b * A) proofend; theorem :: MATRIXR2:13 for a, b being Real for A being Matrix of REAL holds (a - b) * A = (a * A) - (b * A) proofend; theorem Th14: :: MATRIXR2:14 for n being Element of NAT for K being Field for A being Matrix of K st n > 0 & len A > 0 holds (0. (K,n,(len A))) * A = 0. (K,n,(width A)) proofend; theorem Th15: :: MATRIXR2:15 for K being Field for A, C being Matrix of K st len A = width C & len C > 0 & len A > 0 holds (- C) * A = - (C * A) proofend; theorem Th16: :: MATRIXR2:16 for K being Field for A, B, C being Matrix of K st len B = len C & width B = width C & len A = width B & len B > 0 & len A > 0 holds (B - C) * A = (B * A) - (C * A) proofend; theorem :: MATRIXR2:17 for A, B, C being Matrix of REAL st len A = len B & width A = width B & len C = width A & len A > 0 & len C > 0 holds (A - B) * C = (A * C) - (B * C) by Th16; theorem Th18: :: MATRIXR2:18 for K being Field for m being Element of NAT for A, C being Matrix of K st width A > 0 & len A > 0 holds A * (0. (K,(width A),m)) = 0. (K,(len A),m) proofend; theorem Th19: :: MATRIXR2:19 for K being Field for A, C being Matrix of K st width A = len C & len A > 0 & len C > 0 holds A * (- C) = - (A * C) proofend; theorem Th20: :: MATRIXR2:20 for K being Field for A, B, C being Matrix of K st len B = len C & width B = width C & len B = width A & len B > 0 & len A > 0 holds A * (B - C) = (A * B) - (A * C) proofend; theorem :: MATRIXR2:21 for A, B, C being Matrix of REAL st len A = len B & width A = width B & width C = len A & len C > 0 & len A > 0 holds C * (A - B) = (C * A) - (C * B) by Th20; theorem Th22: :: MATRIXR2:22 for A, B, C being Matrix of REAL st len A = len B & width A = width B & len C = len A & width C = width A & ( for i, j being Element of NAT st [i,j] in Indices A holds C * (i,j) = (A * (i,j)) - (B * (i,j)) ) holds C = A - B proofend; theorem Th23: :: MATRIXR2:23 for x1, x2 being FinSequence of REAL st len x1 = len x2 holds LineVec2Mx (x1 - x2) = (LineVec2Mx x1) - (LineVec2Mx x2) proofend; theorem Th24: :: MATRIXR2:24 for x1, x2 being FinSequence of REAL st len x1 = len x2 & len x1 > 0 holds ColVec2Mx (x1 - x2) = (ColVec2Mx x1) - (ColVec2Mx x2) proofend; theorem Th25: :: MATRIXR2:25 for A, B being Matrix of REAL st len A = len B & width A = width B holds for i being Nat st 1 <= i & i <= len A holds Line ((A - B),i) = (Line (A,i)) - (Line (B,i)) proofend; theorem Th26: :: MATRIXR2:26 for A, B being Matrix of REAL st len A = len B & width A = width B holds for i being Nat st 1 <= i & i <= width A holds Col ((A - B),i) = (Col (A,i)) - (Col (B,i)) proofend; theorem :: MATRIXR2:27 for n, k, m, l being Element of NAT for A being Matrix of n,k, REAL for B being Matrix of k,m, REAL for C being Matrix of m,l, REAL st n > 0 & k > 0 & m > 0 holds (A * B) * C = A * (B * C) proofend; theorem Th28: :: MATRIXR2:28 for n being Element of NAT for A, B, C being Matrix of n, REAL holds (A * B) * C = A * (B * C) proofend; theorem Th29: :: MATRIXR2:29 for D being non empty set for n being Element of NAT for A being Matrix of n,D holds (A @) @ = A proofend; theorem Th30: :: MATRIXR2:30 for n being Element of NAT for A, B being Matrix of n, REAL holds (A * B) @ = (B @) * (A @) proofend; theorem Th31: :: MATRIXR2:31 for n, m being Element of NAT for A being Matrix of REAL st len A = n & width A = m holds (- A) + A = 0_Rmatrix (n,m) proofend; begin definition let n be Element of NAT ; let A be Matrix of n, REAL ; :: original:MXR2MXF redefine func MXR2MXF A -> Matrix of n,F_Real; coherence MXR2MXF A is Matrix of n,F_Real ; end; definition let n be Element of NAT ; let A be Matrix of n, REAL ; func Det A -> Real equals :: MATRIXR2:def 1 Det (MXR2MXF A); coherence Det (MXR2MXF A) is Real ; end; :: deftheorem defines Det MATRIXR2:def_1_:_ for n being Element of NAT for A being Matrix of n, REAL holds Det A = Det (MXR2MXF A); theorem :: MATRIXR2:32 for A being Matrix of 2, REAL holds Det A = ((A * (1,1)) * (A * (2,2))) - ((A * (1,2)) * (A * (2,1))) proofend; theorem Th33: :: MATRIXR2:33 for n being Element of NAT for s1, s2, s3 being FinSequence st len s1 = n & len s2 = n & len s3 = n holds <*s1,s2,s3*> is tabular proofend; theorem Th34: :: MATRIXR2:34 for D being non empty set for n being Element of NAT for p1, p2, p3 being FinSequence of D st len p1 = n & len p2 = n & len p3 = n holds <*p1,p2,p3*> is Matrix of 3,n,D proofend; theorem Th35: :: MATRIXR2:35 for D being non empty set for a1, a2, a3, b1, b2, b3, c1, c2, c3 being Element of D holds <*<*a1,a2,a3*>,<*b1,b2,b3*>,<*c1,c2,c3*>*> is Matrix of 3,D proofend; theorem Th36: :: MATRIXR2:36 for D being non empty set for n being Element of NAT for A being Matrix of n,D for p being FinSequence of D for i being Nat st p = A . i & i in Seg n holds len p = n proofend; theorem Th37: :: MATRIXR2:37 for D being non empty set for A being Matrix of 3,D holds A = <*<*(A * (1,1)),(A * (1,2)),(A * (1,3))*>,<*(A * (2,1)),(A * (2,2)),(A * (2,3))*>,<*(A * (3,1)),(A * (3,2)),(A * (3,3))*>*> proofend; theorem :: MATRIXR2:38 for A being Matrix of 3, REAL holds Det A = (((((((A * (1,1)) * (A * (2,2))) * (A * (3,3))) - (((A * (1,3)) * (A * (2,2))) * (A * (3,1)))) - (((A * (1,1)) * (A * (2,3))) * (A * (3,2)))) + (((A * (1,2)) * (A * (2,3))) * (A * (3,1)))) - (((A * (1,2)) * (A * (2,1))) * (A * (3,3)))) + (((A * (1,3)) * (A * (2,1))) * (A * (3,2))) proofend; theorem :: MATRIXR2:39 for f being Permutation of (Seg 0) holds f = <*> NAT ; Lm4: idseq 0 is Permutation of (Seg 0) by FINSEQ_2:55; theorem Th40: :: MATRIXR2:40 Permutations 0 = {(<*> NAT)} proofend; theorem Th41: :: MATRIXR2:41 for K being Field for A being Matrix of 0 ,K holds Det A = 1. K proofend; theorem :: MATRIXR2:42 for A being Matrix of 0 , REAL holds Det A = 1 proofend; :: Removing condition n>=1 from MATRIX7:37 theorem Th43: :: MATRIXR2:43 for K being Field for n being Nat for A being Matrix of n,K holds Det A = Det (A @) proofend; theorem :: MATRIXR2:44 for n being Element of NAT for A being Matrix of n, REAL holds Det A = Det (A @) proofend; :: Removing condition n>0 from MATRIX11:62 theorem Th45: :: MATRIXR2:45 for n being Element of NAT for K being Field for A, B being Matrix of n,K holds Det (A * B) = (Det A) * (Det B) proofend; theorem Th46: :: MATRIXR2:46 for n being Element of NAT for A, B being Matrix of n, REAL holds Det (A * B) = (Det A) * (Det B) proofend; begin theorem :: MATRIXR2:47 for x, y being FinSequence of REAL for A being Matrix of REAL st len x = len A & len y = len x & len x > 0 holds (x - y) * A = (x * A) - (y * A) proofend; theorem :: MATRIXR2:48 for x, y being FinSequence of REAL for A being Matrix of REAL st len x = width A & len y = len x & len x > 0 & len A > 0 holds A * (x - y) = (A * x) - (A * y) proofend; theorem :: MATRIXR2:49 for x being FinSequence of REAL for A being Matrix of REAL st len A = len x & len x > 0 & width A > 0 holds (- x) * A = - (x * A) proofend; theorem :: MATRIXR2:50 for x being FinSequence of REAL for A being Matrix of REAL st len x = width A & len x > 0 holds A * (- x) = - (A * x) proofend; theorem :: MATRIXR2:51 for x being FinSequence of REAL for A being Matrix of REAL st len x = len A & len x > 0 holds x * (- A) = - (x * A) proofend; theorem :: MATRIXR2:52 for x being FinSequence of REAL for A being Matrix of REAL st len x = width A & len A > 0 & len x > 0 holds (- A) * x = - (A * x) proofend; theorem :: MATRIXR2:53 for a being Real for x being FinSequence of REAL for A being Matrix of REAL st width A = len x & len x > 0 holds A * (a * x) = a * (A * x) proofend; theorem :: MATRIXR2:54 for x being FinSequence of REAL for A, B being Matrix of REAL st len x = len A & len A = len B & width A = width B & len A > 0 holds x * (A - B) = (x * A) - (x * B) proofend; theorem :: MATRIXR2:55 for x being FinSequence of REAL for A, B being Matrix of REAL st len x = width A & len A = len B & width A = width B & len x > 0 & len A > 0 holds (A - B) * x = (A * x) - (B * x) proofend; theorem Th56: :: MATRIXR2:56 for x being FinSequence of REAL for A being Matrix of REAL st len A = len x holds (LineVec2Mx x) * A = LineVec2Mx (x * A) proofend; theorem Th57: :: MATRIXR2:57 for x being FinSequence of REAL for A, B being Matrix of REAL st len x = len A & width A = len B holds x * (A * B) = (x * A) * B proofend; theorem Th58: :: MATRIXR2:58 for x being FinSequence of REAL for A being Matrix of REAL st width A = len x & len x > 0 & len A > 0 holds A * (ColVec2Mx x) = ColVec2Mx (A * x) proofend; theorem Th59: :: MATRIXR2:59 for x being FinSequence of REAL for A, B being Matrix of REAL st len x = width B & width A = len B & len x > 0 & len B > 0 holds (A * B) * x = A * (B * x) proofend; theorem :: MATRIXR2:60 for n, m, k being Element of NAT for B being Matrix of n,m, REAL for A being Matrix of m,k, REAL st n > 0 holds for i, j being Element of NAT st [i,j] in Indices (B * A) holds (B * A) * (i,j) = ((Line (B,i)) * A) . j proofend; theorem Th61: :: MATRIXR2:61 for n being Element of NAT for A, B being Matrix of n, REAL for i, j being Element of NAT st [i,j] in Indices (B * A) holds (B * A) * (i,j) = ((Line (B,i)) * A) . j proofend; theorem :: MATRIXR2:62 for n being Element of NAT for A, B being Matrix of n, REAL st n > 0 holds for i, j being Element of NAT st [i,j] in Indices (A * B) holds (A * B) * (i,j) = (A * (Col (B,j))) . i proofend; begin definition let n be Element of NAT ; func 1_Rmatrix n -> Matrix of n, REAL equals :: MATRIXR2:def 2 MXF2MXR (1. (F_Real,n)); correctness coherence MXF2MXR (1. (F_Real,n)) is Matrix of n, REAL ; ; end; :: deftheorem defines 1_Rmatrix MATRIXR2:def_2_:_ for n being Element of NAT holds 1_Rmatrix n = MXF2MXR (1. (F_Real,n)); theorem Th63: :: MATRIXR2:63 for n being Element of NAT holds ( ( for i being Element of NAT st [i,i] in Indices (1_Rmatrix n) holds (1_Rmatrix n) * (i,i) = 1 ) & ( for i, j being Element of NAT st [i,j] in Indices (1_Rmatrix n) & i <> j holds (1_Rmatrix n) * (i,j) = 0 ) ) proofend; theorem Th64: :: MATRIXR2:64 for n being Element of NAT holds (1_Rmatrix n) @ = 1_Rmatrix n proofend; theorem Th65: :: MATRIXR2:65 for n, m being Element of NAT st n > 0 holds (0_Rmatrix (n,m)) + (0_Rmatrix (n,m)) = 0_Rmatrix (n,m) proofend; theorem :: MATRIXR2:66 for n, m being Element of NAT for a being Real st n > 0 holds a * (0_Rmatrix (n,m)) = 0_Rmatrix (n,m) proofend; theorem Th67: :: MATRIXR2:67 for K being Field for A being Matrix of K holds A * (1. (K,(width A))) = A proofend; theorem Th68: :: MATRIXR2:68 for K being Field for A being Matrix of K holds (1. (K,(len A))) * A = A proofend; theorem :: MATRIXR2:69 for n, m being Element of NAT for A being Matrix of REAL holds ( ( n = width A implies A * (1_Rmatrix n) = A ) & ( m = len A implies (1_Rmatrix m) * A = A ) ) by Th67, Th68; theorem Th70: :: MATRIXR2:70 for n being Element of NAT for A being Matrix of n, REAL holds (1_Rmatrix n) * A = A proofend; theorem Th71: :: MATRIXR2:71 for n being Element of NAT for A being Matrix of n, REAL holds A * (1_Rmatrix n) = A proofend; theorem Th72: :: MATRIXR2:72 for n being Element of NAT holds Det (1_Rmatrix n) = 1 proofend; definition let n be Element of NAT ; func 0_Rmatrix n -> Matrix of n, REAL equals :: MATRIXR2:def 3 0_Rmatrix (n,n); correctness coherence 0_Rmatrix (n,n) is Matrix of n, REAL ; ; end; :: deftheorem defines 0_Rmatrix MATRIXR2:def_3_:_ for n being Element of NAT holds 0_Rmatrix n = 0_Rmatrix (n,n); theorem :: MATRIXR2:73 for n being Element of NAT st n > 0 holds Det (0_Rmatrix n) = 0 proofend; definition let n, i be Nat; func Base_FinSeq (n,i) -> FinSequence of REAL equals :: MATRIXR2:def 4 (n |-> 0) +* (i,1); coherence (n |-> 0) +* (i,1) is FinSequence of REAL proofend; end; :: deftheorem defines Base_FinSeq MATRIXR2:def_4_:_ for n, i being Nat holds Base_FinSeq (n,i) = (n |-> 0) +* (i,1); theorem Th74: :: MATRIXR2:74 for n, i being Nat holds len (Base_FinSeq (n,i)) = n proofend; theorem Th75: :: MATRIXR2:75 for i, n being Nat st 1 <= i & i <= n holds (Base_FinSeq (n,i)) . i = 1 proofend; theorem Th76: :: MATRIXR2:76 for j, n, i being Nat st 1 <= j & j <= n & i <> j holds (Base_FinSeq (n,i)) . j = 0 proofend; theorem :: MATRIXR2:77 ( Base_FinSeq (1,1) = <*1*> & Base_FinSeq (2,1) = <*1,0*> & Base_FinSeq (2,2) = <*0,1*> & Base_FinSeq (3,1) = <*1,0,0*> & Base_FinSeq (3,2) = <*0,1,0*> & Base_FinSeq (3,3) = <*0,0,1*> ) proofend; theorem Th78: :: MATRIXR2:78 for i being Nat for n being Element of NAT st 1 <= i & i <= n holds (1_Rmatrix n) . i = Base_FinSeq (n,i) proofend; begin definition let n be Element of NAT ; let A be Matrix of n, REAL ; attrA is invertible means :Def5: :: MATRIXR2:def 5 ex B being Matrix of n, REAL st ( B * A = 1_Rmatrix n & A * B = 1_Rmatrix n ); end; :: deftheorem Def5 defines invertible MATRIXR2:def_5_:_ for n being Element of NAT for A being Matrix of n, REAL holds ( A is invertible iff ex B being Matrix of n, REAL st ( B * A = 1_Rmatrix n & A * B = 1_Rmatrix n ) ); definition let n be Element of NAT ; let A be Matrix of n, REAL ; assume A1: A is invertible ; func Inv A -> Matrix of n, REAL means :Def6: :: MATRIXR2:def 6 ( it * A = 1_Rmatrix n & A * it = 1_Rmatrix n ); existence ex b1 being Matrix of n, REAL st ( b1 * A = 1_Rmatrix n & A * b1 = 1_Rmatrix n ) by A1, Def5; uniqueness for b1, b2 being Matrix of n, REAL st b1 * A = 1_Rmatrix n & A * b1 = 1_Rmatrix n & b2 * A = 1_Rmatrix n & A * b2 = 1_Rmatrix n holds b1 = b2 proofend; end; :: deftheorem Def6 defines Inv MATRIXR2:def_6_:_ for n being Element of NAT for A being Matrix of n, REAL st A is invertible holds for b3 being Matrix of n, REAL holds ( b3 = Inv A iff ( b3 * A = 1_Rmatrix n & A * b3 = 1_Rmatrix n ) ); registration let n be Element of NAT ; cluster 1_Rmatrix n -> invertible ; coherence 1_Rmatrix n is invertible proofend; end; theorem :: MATRIXR2:79 for n being Element of NAT holds Inv (1_Rmatrix n) = 1_Rmatrix n proofend; theorem Th80: :: MATRIXR2:80 for n being Element of NAT for A, B1, B2 being Matrix of n, REAL st B1 * A = 1_Rmatrix n & A * B2 = 1_Rmatrix n holds ( B1 = B2 & A is invertible ) proofend; theorem :: MATRIXR2:81 for n being Element of NAT for A being Matrix of n, REAL st A is invertible holds Det (Inv A) = (Det A) " proofend; theorem :: MATRIXR2:82 for n being Element of NAT for A being Matrix of n, REAL st A is invertible holds Det A <> 0 proofend; theorem :: MATRIXR2:83 for n being Element of NAT for A, B being Matrix of n, REAL st A is invertible & B is invertible holds ( A * B is invertible & Inv (A * B) = (Inv B) * (Inv A) ) proofend; theorem :: MATRIXR2:84 for n being Element of NAT for A being Matrix of n, REAL st A is invertible holds Inv (Inv A) = A proofend; theorem :: MATRIXR2:85 ( 1_Rmatrix 0 = 0_Rmatrix 0 & 1_Rmatrix 0 = {} ) proofend; theorem Th86: :: MATRIXR2:86 for n being Element of NAT for x being FinSequence of REAL st len x = n & n > 0 holds (1_Rmatrix n) * x = x proofend; theorem Th87: :: MATRIXR2:87 for n being Element of NAT for x, y being FinSequence of REAL for A being Matrix of n, REAL st A is invertible & len x = n & len y = n & n > 0 holds ( A * x = y iff x = (Inv A) * y ) proofend; theorem Th88: :: MATRIXR2:88 for n being Element of NAT for x being FinSequence of REAL st len x = n holds x * (1_Rmatrix n) = x proofend; theorem Th89: :: MATRIXR2:89 for n being Element of NAT for x, y being FinSequence of REAL for A being Matrix of n, REAL st A is invertible & len x = n & len y = n holds ( x * A = y iff x = y * (Inv A) ) proofend; theorem :: MATRIXR2:90 for n being Element of NAT for A being Matrix of n, REAL st n > 0 & A is invertible holds for y being FinSequence of REAL st len y = n holds ex x being FinSequence of REAL st ( len x = n & A * x = y ) proofend; theorem :: MATRIXR2:91 for n being Element of NAT for A being Matrix of n, REAL st A is invertible holds for y being FinSequence of REAL st len y = n holds ex x being FinSequence of REAL st ( len x = n & x * A = y ) proofend; theorem :: MATRIXR2:92 for n being Element of NAT for A being Matrix of n, REAL for x, y being FinSequence of REAL st len x = n & len y = n & x * A = y holds for j being Element of NAT st 1 <= j & j <= n holds y . j = |(x,(Col (A,j)))| proofend; theorem Th93: :: MATRIXR2:93 for n being Element of NAT for A being Matrix of n, REAL st ( for y being FinSequence of REAL st len y = n holds ex x being FinSequence of REAL st ( len x = n & x * A = y ) ) holds ex B being Matrix of n, REAL st B * A = 1_Rmatrix n proofend; theorem :: MATRIXR2:94 for n being Element of NAT for x being FinSequence of REAL for A being Matrix of n, REAL st n > 0 & len x = n holds (A @) * x = x * A proofend; theorem Th95: :: MATRIXR2:95 for n being Element of NAT for x being FinSequence of REAL for A being Matrix of n, REAL st n > 0 & len x = n holds x * (A @) = A * x proofend; theorem Th96: :: MATRIXR2:96 for n being Element of NAT for A being Matrix of n, REAL st n > 0 & ( for y being FinSequence of REAL st len y = n holds ex x being FinSequence of REAL st ( len x = n & A * x = y ) ) holds ex B being Matrix of n, REAL st A * B = 1_Rmatrix n proofend; theorem :: MATRIXR2:97 for n being Element of NAT for A being Matrix of n, REAL st n > 0 & ( for y being FinSequence of REAL st len y = n holds ex x1, x2 being FinSequence of REAL st ( len x1 = n & len x2 = n & A * x1 = y & x2 * A = y ) ) holds A is invertible proofend;