---

Step * 2 2 of Lemma adjugate-property


1. r : CRng
2. n : ℕ
3. M : Matrix(n;n;r)
4. ¬(n = 0 ∈ ℤ)
5. x : ℕn@i
6. y : ℕn@i
7. |matrix(if a=y then M[x,b] else M[a,b])| = (|M| * if x=y then 1 else 0) ∈ |r|
8. ∀M:Matrix(n;n;r). ∀x:ℕn.
     (|M| = (Σ(r) 0 ≤ i < n. if isEven(i + x) then M[x,i] else -r M[x,i] fi  * |matrix-minor(x;i;M)|) ∈ |r|)
⊢ |matrix(if a=y then M[x,b] else M[a,b])|
= (Σ(r) 0 
        ≤ i 
        < n
    M[x,i] * if isEven(i + y) then |matrix-minor(y;i;M)| else -r |matrix-minor(y;i;M)| fi )
∈ |r|
BY
{ ((InstHyp [⌜matrix(if a=y then M[x,b] else M[a,b])⌝;⌜y⌝] (-1)⋅ THENA Auto)
   THEN NthHypEqTrans (-1)
   THEN EqCDA
   THEN (Reduce 0 THENA Auto)
   THEN Subst' matrix-minor(y;i;matrix(if a=y then M[x,b] else M[a,b])) = matrix-minor(y;i;M) ∈ Matrix(n - 1;n - 1;r) 0
   THEN Auto) }

1
.....equality..... 
1. r : CRng
2. n : ℕ
3. M : Matrix(n;n;r)
4. ¬(n = 0 ∈ ℤ)
5. x : ℕn@i
6. y : ℕn@i
7. |matrix(if a=y then M[x,b] else M[a,b])| = (|M| * if x=y then 1 else 0) ∈ |r|
8. ∀M:Matrix(n;n;r). ∀x:ℕn.
     (|M| = (Σ(r) 0 ≤ i < n. if isEven(i + x) then M[x,i] else -r M[x,i] fi  * |matrix-minor(x;i;M)|) ∈ |r|)
9. |matrix(if a=y then M[x,b] else M[a,b])|
= (Σ(r) 0 
        ≤ i 
        < n
    if isEven(i + y)
    then matrix(if a=y then M[x,b] else M[a,b])[y,i]
    else -r matrix(if a=y then M[x,b] else M[a,b])[y,i]
    fi  
    * 
    |matrix-minor(y;i;matrix(if a=y then M[x,b] else M[a,b]))|)
∈ |r|
10. i : ℕn@i
⊢ matrix-minor(y;i;matrix(if a=y then M[x,b] else M[a,b])) = matrix-minor(y;i;M) ∈ Matrix(n - 1;n - 1;r)

---

Latex:

---

Latex:

1.  r  :  CRng
2.  n  :  \mBbbN{}
3.  M  :  Matrix(n;n;r)
4.  \mneg{}(n  =  0)
5.  x  :  \mBbbN{}n@i
6.  y  :  \mBbbN{}n@i
7.  |matrix(if  a=y  then  M[x,b]  else  M[a,b])|  =  (|M|  *  if  x=y  then  1  else  0)
8.  \mforall{}M:Matrix(n;n;r).  \mforall{}x:\mBbbN{}n.
          (|M|
          =  (\mSigma{}(r)  0 
                          \mleq{}  i 
                          <  n
                  if  isEven(i  +  x)  then  M[x,i]  else  -r  M[x,i]  fi    *  |matrix-minor(x;i;M)|))
\mvdash{}  |matrix(if  a=y  then  M[x,b]  else  M[a,b])|
=  (\mSigma{}(r)  0 
                \mleq{}  i 
                <  n
        M[x,i]  *  if  isEven(i  +  y)  then  |matrix-minor(y;i;M)|  else  -r  |matrix-minor(y;i;M)|  fi  )


By

---

Latex:
((InstHyp  [\mkleeneopen{}matrix(if  a=y  then  M[x,b]  else  M[a,b])\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{}]  (-1)\mcdot{}  THENA  Auto)
  THEN  NthHypEqTrans  (-1)
  THEN  EqCDA
  THEN  (Reduce  0  THENA  Auto)
  THEN  Subst'  matrix-minor(y;i;matrix(if  a=y  then  M[x,b]  else  M[a,b]))  =  matrix-minor(y;i;M)  0
  THEN  Auto)

---

Home Index