:: Determinant and Inverse of Matrices of Real Elements
:: by Nobuyuki Tamura and Yatsuka Nakamura
::
:: Received July 17, 2007
:: Copyright (c) 2007-2021 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, XBOOLE_0, SUBSET_1, VECTSP_1, FINSEQ_1, ARYTM_1,
FUNCT_1, FINSEQ_2, ARYTM_3, EUCLID, MATRIX_1, XXREAL_0, INCSP_1, RELAT_1,
TREES_1, TARSKI, MATRIXR1, CARD_1, NAT_1, REAL_1, SUPINF_2, QC_LANG1,
ZFMISC_1, FVSUM_1, MATRIX_3, FUNCT_2, MESFUNC1, GROUP_1, ABIAN, BINOP_1,
ALGSTR_0, SETWISEO, CARD_3, RVSUM_1, FUNCT_4, AFINSQ_1, PRALG_1,
PARTFUN1, MATRIXR2, MATRIX_0, FUNCT_7, FUNCSDOM, FINSUB_1;
notations TARSKI, XBOOLE_0, SUBSET_1, XXREAL_0, ZFMISC_1, ORDINAL1, NUMBERS,
ENUMSET1, SETWOP_2, XCMPLX_0, XREAL_0, REAL_1, FUNCT_1, PARTFUN1,
BINOP_1, FUNCT_2, FINSEQ_1, FINSEQ_2, FINSEQ_4, FUNCT_7, STRUCT_0,
ALGSTR_0, MATRIX_0, MATRIX_1, FVSUM_1, FINSEQ_7, SETWISEO, GROUP_1,
FINSUB_1, MATRIX_3, MATRIX_6, MATRIXR1, EUCLID, MATRIX_7, MATRIX_4,
RVSUM_1, VECTSP_1, MATRPROB;
constructors FVSUM_1, BINOP_2, FINSEQ_7, SETWISEO, FINSOP_1, FINSEQ_4,
MATRIX_7, MATRIXR1, MATRIX_6, REAL_1, RVSUM_1, EUCLID, RELSET_1,
MATRIX_4, BINOP_1, VECTSP_2;
registrations FINSEQ_2, NAT_1, RELSET_1, MEMBERED, STRUCT_0, VECTSP_1,
NUMBERS, XXREAL_0, MATRIX_1, FINSEQ_1, FVSUM_1, XBOOLE_0, VALUED_0,
CARD_1, MATRIX_0, MATRIX_6, XREAL_0, VECTSP_2, ORDINAL1;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
begin :: Preliminaries
reserve x for set,
D for non empty set,
k,n,m,i,j,l for Nat,
K for Field;
theorem :: MATRIXR2:1
for x,y being FinSequence of REAL st len x=len y & x+y=0*(len x)
holds x=-y & y=-x;
theorem :: MATRIXR2:2
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;
theorem :: MATRIXR2:3
for a being Real, A being Matrix of REAL st [i,j] in
Indices A holds (a*A)*(i,j) = a*(A*(i,j));
theorem :: MATRIXR2:4
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;
theorem :: MATRIXR2:5
for a being Real,A being Matrix of REAL holds len (a*A)=
len A & width (a*A)=width A;
begin :: Calculation of Matrices
theorem :: 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 holds [i,j] in Indices
A implies (A-B)*(i,j) = A*(i,j) - B*(i,j);
definition
let n;
let A,B be Matrix of n,REAL;
redefine func A*B -> Matrix of n,REAL;
end;
theorem :: 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;
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;
theorem :: MATRIXR2:9
for A being Matrix of REAL holds (-1)*A = -A;
theorem :: MATRIXR2:10
for A being (Matrix of REAL), i,j being Nat st [i,j]
in Indices A holds (-A)*(i,j)=-(A*(i,j));
theorem :: MATRIXR2:11
for a,b being Real,A being Matrix of REAL holds (a*b)*A=a*(b*A);
theorem :: MATRIXR2:12
for a,b being Real,A being Matrix of REAL holds (a+b)*A=a*A + b* A;
theorem :: MATRIXR2:13
for a,b being Real,A being Matrix of REAL holds (a-b)*A=a*A - b*A;
theorem :: MATRIXR2:14
for A being Matrix of K st n>0 & len A >0 holds 0.(K,n,len A)*A=
0.(K,n,width A);
theorem :: MATRIXR2:15
for A,C being Matrix of K st len A=width C & len C>0 & len A>0
holds (-C)*A = -(C*A);
theorem :: MATRIXR2:16
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;
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;
theorem :: MATRIXR2:18
for m being Nat,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);
theorem :: MATRIXR2:19
for A,C being Matrix of K st width A=len C & len A>0 & len C>0
holds A*(-C) = -(A*C);
theorem :: MATRIXR2:20
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;
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;
theorem :: 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 Nat st [i,j] in
Indices A holds C*(i,j) = A*(i,j) - B*(i,j)) holds C=A-B;
theorem :: MATRIXR2:23
for x1,x2 being FinSequence of REAL st len x1=len x2 holds
LineVec2Mx (x1-x2)=LineVec2Mx (x1)-LineVec2Mx (x2);
theorem :: 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);
theorem :: 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);
theorem :: 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)
;
theorem :: MATRIXR2:27
for A being Matrix of n,k,REAL, B being Matrix of k,m,REAL,C being
Matrix of m,l,REAL st n>0 & k>0 & m>0 holds A*B*C=A*(B*C);
theorem :: MATRIXR2:28
for A,B,C being Matrix of n,REAL holds A*B*C=A*(B*C);
theorem :: MATRIXR2:29
for A being Matrix of n,D holds (A@)@=A;
theorem :: MATRIXR2:30
for A,B being Matrix of n,REAL holds (A*B)@ = (B@)*(A@);
theorem :: MATRIXR2:31
for A being Matrix of REAL st len A=n & width A=m holds -A+A= 0_Rmatrix(n,m);
begin :: Determinants
definition
let n;
let A be Matrix of n,REAL;
redefine func MXR2MXF A -> Matrix of n,F_Real;
end;
definition
let n;
let A be Matrix of n,REAL;
func Det A -> Real equals
:: MATRIXR2:def 1
Det MXR2MXF A;
end;
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));
theorem :: MATRIXR2:33
for s1,s2,s3 be FinSequence st len s1 = n & len s2 = n & len s3
= n holds <*s1,s2,s3*> is tabular;
theorem :: MATRIXR2:34
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;
theorem :: MATRIXR2:35
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;
theorem :: MATRIXR2:36
for A being Matrix of n,D for p being FinSequence of D, i being
Nat st p=A.i & i in Seg n holds len p=n;
theorem :: MATRIXR2:37
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) *> *>;
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));
theorem :: MATRIXR2:39
for f being Permutation of Seg 0 holds f=<*>NAT;
theorem :: MATRIXR2:40
Permutations 0 = {<*>NAT};
theorem :: MATRIXR2:41
for K being Ring
for A being Matrix of 0,K holds Det A = 1.K;
theorem :: MATRIXR2:42
for A being Matrix of 0,REAL holds Det A = 1;
:: Removing condition n>=1 from MATRIX7:37
theorem :: MATRIXR2:43
for n being Nat, A being Matrix of n,K holds Det A = Det (A@);
theorem :: MATRIXR2:44
for A being Matrix of n,REAL holds Det A = Det (A@);
:: Removing condition n>0 from MATRIX11:62
theorem :: MATRIXR2:45
for A,B being Matrix of n,K holds Det(A*B) = (Det A)*(Det B);
theorem :: MATRIXR2:46
for A,B being Matrix of n,REAL holds Det (A*B) = (Det A)*(Det B);
begin :: Matrix as Operator
theorem :: MATRIXR2:47
for x,y being FinSequence of REAL, 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;
theorem :: MATRIXR2:48
for x,y being FinSequence of REAL,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;
theorem :: MATRIXR2:49
for x being FinSequence of REAL, A being Matrix of REAL st len A=len x
& len x>0 & width A>0 holds (-x)*A=-(x*A);
theorem :: MATRIXR2:50
for x being FinSequence of REAL,A being Matrix of REAL st len x=width
A & len x > 0 holds A*(-x)=-(A*x);
theorem :: MATRIXR2:51
for x being FinSequence of REAL,A being Matrix of REAL st len x=len A
& len x>0 holds x*(-A)=-(x*A);
theorem :: MATRIXR2:52
for x being FinSequence of REAL,A being Matrix of REAL st len x=width
A & len A>0 & len x> 0 holds (-A)*x=-(A*x);
theorem :: MATRIXR2:53
for a being Real,x being FinSequence of REAL,A being Matrix of REAL st
width A=len x & len x>0 holds A*(a*x)=a*(A*x);
theorem :: MATRIXR2:54
for x being FinSequence of REAL, 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);
theorem :: MATRIXR2:55
for x being FinSequence of REAL, 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;
theorem :: MATRIXR2:56
for x being FinSequence of REAL,A being Matrix of REAL st len A=
len x holds (LineVec2Mx x)*A=LineVec2Mx (x*A);
theorem :: MATRIXR2:57
for x being FinSequence of REAL, A,B being Matrix of REAL st len
x=len A & width A=len B holds x*(A*B)=(x*A)*B;
theorem :: MATRIXR2:58
for x being FinSequence of REAL,A being Matrix of REAL st width
A=len x & len x>0 & len A>0 holds A*(ColVec2Mx x)=ColVec2Mx (A*x);
theorem :: MATRIXR2:59
for x being FinSequence of REAL, 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);
theorem :: MATRIXR2:60
for B being (Matrix of n,m,REAL),A being (Matrix of m,k,REAL) st n>0
holds (for i,j st [i,j] in Indices (B*A) holds (B*A)*(i,j)=((Line(B,i))*A).j)
;
theorem :: MATRIXR2:61
for A, B being Matrix of n,REAL holds for i,j st [i,j] in
Indices (B*A) holds (B*A)*(i,j)=((Line(B,i))*A).j;
theorem :: MATRIXR2:62
for A, B being Matrix of n,REAL st n>0 holds for i,j st [i,j] in
Indices (A*B) holds (A*B)*(i,j)=(A*(Col(B,j))).i;
begin :: Identity and Zero of Matrix of REAL
definition
let n be Nat;
func 1_Rmatrix(n) -> Matrix of n,REAL equals
:: MATRIXR2:def 2
MXF2MXR (1.(F_Real,n));
end;
theorem :: MATRIXR2:63
(for i st [i,i] in Indices 1_Rmatrix n holds (1_Rmatrix n)*(i,i)
= 1) & for i,j st [i,j] in Indices (1_Rmatrix n) & i <> j holds (1_Rmatrix n)*(
i,j) = 0;
theorem :: MATRIXR2:64
(1_Rmatrix(n))@=1_Rmatrix(n);
theorem :: MATRIXR2:65
for n,m being Nat st n>0 holds 0_Rmatrix(n,m)+
0_Rmatrix(n,m)=0_Rmatrix(n,m);
theorem :: MATRIXR2:66
for a being Real st n>0 holds a*(0_Rmatrix(n,m)) = 0_Rmatrix(n,m);
theorem :: MATRIXR2:67
for K being Field, A being Matrix of K holds A*(1.(K,width A))=A;
theorem :: MATRIXR2:68
for A being Matrix of K holds (1.(K,len A))*A=A;
theorem :: MATRIXR2:69
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);
theorem :: MATRIXR2:70
for A being Matrix of n,REAL holds (1_Rmatrix n)*A=A;
theorem :: MATRIXR2:71
for A be Matrix of n,REAL holds A*(1_Rmatrix(n))=A;
theorem :: MATRIXR2:72
Det 1_Rmatrix n=1;
definition
let n be Nat;
func 0_Rmatrix(n) -> Matrix of n,REAL equals
:: MATRIXR2:def 3
0_Rmatrix(n,n);
end;
theorem :: MATRIXR2:73
n>0 implies Det 0_Rmatrix n = 0;
definition
let n,i be Nat;
func Base_FinSeq(n,i) -> FinSequence of REAL equals
:: MATRIXR2:def 4
(n |-> 0)+*(i,1);
end;
reserve n,i,j for Nat;
theorem :: MATRIXR2:74
len Base_FinSeq(n,i) = n;
theorem :: MATRIXR2:75
1<=i & i<=n implies (Base_FinSeq(n,i)).i=1;
theorem :: MATRIXR2:76
1<=j & j<=n & i<>j implies (Base_FinSeq(n,i)).j=0;
reserve n for Nat;
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 *>;
theorem :: MATRIXR2:78
1<=i & i<=n implies (1_Rmatrix(n)).i=Base_FinSeq(n,i);
begin :: Inverse of Matrix
definition
let n be Nat,A be Matrix of n,REAL;
attr A is invertible means
:: MATRIXR2:def 5
ex B being Matrix of n,REAL st B*A= 1_Rmatrix(n) & A*B=1_Rmatrix(n);
end;
definition
let n be Nat,A be Matrix of n,REAL;
assume
A is invertible;
func Inv(A) -> Matrix of n,REAL means
:: MATRIXR2:def 6
it*A=1_Rmatrix(n) & A*it= 1_Rmatrix(n);
end;
registration
let n;
cluster 1_Rmatrix n -> invertible;
end;
theorem :: MATRIXR2:79
Inv(1_Rmatrix(n))=1_Rmatrix(n);
theorem :: MATRIXR2:80
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;
theorem :: MATRIXR2:81
for A being Matrix of n,REAL st A is invertible holds Det Inv A = (Det A)";
theorem :: MATRIXR2:82
for A being Matrix of n,REAL st A is invertible holds Det A <> 0;
theorem :: MATRIXR2:83
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);
theorem :: MATRIXR2:84
for A be Matrix of n,REAL st A is invertible holds Inv Inv A = A;
theorem :: MATRIXR2:85
1_Rmatrix(0)=0_Rmatrix(0) & 1_Rmatrix(0)={};
theorem :: MATRIXR2:86
for x being FinSequence of REAL st len x=n & n>0 holds ( 1_Rmatrix n)*x=x;
theorem :: MATRIXR2:87
for n being Nat,x,y being FinSequence of REAL, A be
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;
theorem :: MATRIXR2:88
for x being FinSequence of REAL st len x=n holds x*(1_Rmatrix n) =x;
theorem :: MATRIXR2:89
for x,y being FinSequence of REAL,A be Matrix of n,REAL st A is
invertible & len x=n & len y=n holds x*A=y iff x=y*Inv(A);
theorem :: MATRIXR2:90
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;
theorem :: MATRIXR2:91
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;
theorem :: MATRIXR2:92
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 Nat st 1<=j & j<=n holds y.j
=|(x,Col(A,j))|;
theorem :: MATRIXR2:93
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);
theorem :: MATRIXR2:94
for x being FinSequence of REAL, A being Matrix of n,REAL st n>0 & len
x=n holds (A@)*x = x*A;
theorem :: MATRIXR2:95
for x being FinSequence of REAL, A being Matrix of n,REAL st n>0
& len x=n holds x*(A@) = A*x;
theorem :: MATRIXR2:96
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);
theorem :: MATRIXR2:97
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;