:: 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;