:: Laplace Expansion
::  by Karol P\c{a}k and Andrzej Trybulec
::
:: Received August 13, 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, SUBSET_1, NAT_1, XBOOLE_0, MATRIX11, FINSEQ_1, ARYTM_3,
      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, FUNCT_7;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, 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_0, FINSUB_1, MATRIX_1, 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, XXREAL_0, NAT_1, VECTSP_2;
 registrations FUNCT_1, FINSUB_1, FINSET_1, STRUCT_0, FVSUM_1, MATRIX_1,
      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,
      MATRIX_0, MATRIX_6, VECTSP_2;
 requirements ARITHM, NUMERALS, REAL, BOOLE, SUBSET;


begin :: Preliminaries

reserve x,y for object,
  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 :: LAPLACE:1
  for f be FinSequence, i be Nat st i in dom f holds len Del(f,i) = len f -' 1;

theorem :: LAPLACE:2
  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;

theorem :: LAPLACE:3
  j in Seg width A implies width DelCol(A,j) = width A-'1;

theorem :: LAPLACE:4
  for i be Nat st len A > 1 holds width A = width DelLine(A,i);

theorem :: LAPLACE:5
  for i being Nat st j in Seg width M holds width Deleting(M,i,j) = n-' 1;

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

theorem :: LAPLACE:6
  card Permutations n = n!;

theorem :: LAPLACE:7
  for i,j st i in Seg (n+1) & j in Seg (n+1) holds card {p1: p1.i = j} = n!;

theorem :: LAPLACE:8
  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);

theorem :: LAPLACE:9
  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} where N is Nat : {N,i} in 2Set Seg (n+2)} & (
  the multF of K) $$ (X,Part_sgn(p2,K)) = power(K).(-1_K,i+j);

theorem :: LAPLACE:10
  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} where N is Nat:{N,i} in 2Set Seg(n+1)}
& Proj is one-to-one & for k,m 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});

theorem :: LAPLACE:11
  n < 2 implies for p be Element of Permutations n holds p is even & p=idseq n;

theorem :: LAPLACE:12
  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;

begin :: Auxiliary notions

definition
  let i,j,n be Nat;
  let K;
  let M be Matrix of n,K;
  assume that
 i in Seg n and
 j in Seg n;
  func Delete(M,i,j) -> Matrix of n-'1,K equals
:: LAPLACE:def 1

  Deleting(M,i,j);
end;

theorem :: LAPLACE:13
  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));

theorem :: LAPLACE:14
  for i,j st i in Seg n & j in Seg n holds Delete(M,i,j)@ = Delete (M@,j,i);

theorem :: LAPLACE:15
  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);

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
:: LAPLACE:def 2

  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;
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 :: LAPLACE:16
  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));

theorem :: LAPLACE:17
  not c in Seg width AD implies RCol(AD,c,pD) = AD;

theorem :: LAPLACE:18
  RCol(AD,c,Col(AD,c)) = AD;

theorem :: LAPLACE:19
  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)@;

begin :: Permutations

definition
  let i,n;
  let perm be Element of Permutations(n+1);
  assume
 i in Seg (n+1);
  func Rem(perm,i) -> Element of Permutations n means
:: LAPLACE:def 3

  for k 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));
end;

theorem :: LAPLACE:20
  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);

theorem :: LAPLACE:21
  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));

theorem :: LAPLACE:22
  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);

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
:: LAPLACE:def 4
  Det Delete(M,i,j);
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
:: LAPLACE:def 5
  power(K).(-1_K,i+j)*Minor(M,i,j);
end;

theorem :: LAPLACE:23
  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);

theorem :: LAPLACE:24
  for i,j st i in Seg n & j in Seg n holds Minor(M,i,j) = Minor(M@ ,j,i);

definition
  let n,K;
  let M be Matrix of n,K;
  func Matrix_of_Cofactor(M) -> Matrix of n,K means
:: LAPLACE:def 6

  for i,j being Nat st [i,j] in Indices it holds it*(i,j) = Cofactor(M,i,j);
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
:: LAPLACE:def 7

  len it = n & for j st j in dom it holds it.j = M*(i,j)*Cofactor(M,i,j);
end;

definition
  let n;
  let j be Nat,K;
  let M be Matrix of n,K;
  func LaplaceExpC(M,j) -> FinSequence of K means
:: LAPLACE:def 8

  len it = n & for i st i in dom it holds it.i = M*(i,j)*Cofactor(M,i,j);
end;

theorem :: LAPLACE:25
  for i be Nat, M be Matrix of n,K st i in Seg n holds Det M = Sum
  LaplaceExpL(M,i);

theorem :: LAPLACE:26
  for i st i in Seg n holds LaplaceExpC(M,i) = LaplaceExpL(M@,i);

theorem :: LAPLACE:27
  for j be Nat, M be Matrix of n,K st j in Seg n holds Det M = Sum
  LaplaceExpC(M,j);

theorem :: LAPLACE:28
  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);

theorem :: LAPLACE:29
  i in Seg n implies Line(M,j) "*" Col((Matrix_of_Cofactor M)@,i)
  = Det RLine(M,i,Line(M,j));

theorem :: LAPLACE:30
  Det M <> 0.K implies M * ((Det M)" * (Matrix_of_Cofactor M)@) = 1.(K,n);

theorem :: LAPLACE:31
  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);

theorem :: LAPLACE:32
  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));

theorem :: LAPLACE:33
  Det M <> 0.K implies ((Det M)" * (Matrix_of_Cofactor M)@) * M = 1.(K,n);

theorem :: LAPLACE:34
  M is invertible iff Det M <> 0.K;

theorem :: LAPLACE:35
  Det M <> 0.K implies M~ = (Det M)" * (Matrix_of_Cofactor M)@;

theorem :: LAPLACE:36
  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);

theorem :: LAPLACE:37
  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));

theorem :: LAPLACE:38
  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));

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

definition
  let K;
  let M be Matrix of K;
  let f be FinSequence of K;
  func M * f -> Matrix of K equals
:: LAPLACE:def 9
  M * (<*f*>@);
  func f * M -> Matrix of K equals
:: LAPLACE:def 10
  <*f*> * M;
end;

theorem :: LAPLACE:39
  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);

::$N Cramer's Rule
theorem :: LAPLACE:40
  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);