---

Step * 2 1 1 2 of Lemma det-fun-is-determinant


1. r : CRng
2. n : ℤ
3. ¬n < 1
4. 0 < n
5. d : det-fun(r;n)
6. ∀i:ℕn. ∀M:Matrix(n;n;r).
     ((d matrix+(r;i;matrix-minor(0;i;M)))
     = (if isEven(i) then d I else -r (d I) fi  * (determinant(n - 1;r) matrix-minor(0;i;M)))
     ∈ |r|)
7. M : Matrix(n;n;r)
8. (d M)
= (Σ(r) 0 
        ≤ i 
        < (n - 1) + 1
    M[0,i] * (if isEven(i) then d I else -r (d I) fi  * (determinant(n - 1;r) matrix-minor(0;i;M))))
∈ |r|
⊢ (d M)
= ((d I) 
   * 
   (Σ(r) 0 
         ≤ i 
         < (n - 1) + 1
     if isEven(i) then M[0,i] else -r M[0,i] fi  * (determinant(n - 1;r) matrix-minor(0;i;M))))
∈ |r|
BY
{ (NthHypEqTrans (-1) THEN ((RWO "rng_times_sum_l" 0 THENM EqCDA) THENA Auto) THEN AutoSplit) }

---

Latex:

---

Latex:

1.  r  :  CRng
2.  n  :  \mBbbZ{}
3.  \mneg{}n  <  1
4.  0  <  n
5.  d  :  det-fun(r;n)
6.  \mforall{}i:\mBbbN{}n.  \mforall{}M:Matrix(n;n;r).
          ((d  matrix+(r;i;matrix-minor(0;i;M)))
          =  (if  isEven(i)  then  d  I  else  -r  (d  I)  fi    *  (determinant(n  -  1;r)  matrix-minor(0;i;M))))
7.  M  :  Matrix(n;n;r)
8.  (d  M)
=  (\mSigma{}(r)  0 
                \mleq{}  i 
                <  (n  -  1)  +  1
        M[0,i]  *  (if  isEven(i)  then  d  I  else  -r  (d  I)  fi    *  (determinant(n  -  1;r)  matrix-minor(0;i;M))))
\mvdash{}  (d  M)
=  ((d  I) 
      * 
      (\mSigma{}(r)  0 
                  \mleq{}  i 
                  <  (n  -  1)  +  1
          if  isEven(i)  then  M[0,i]  else  -r  M[0,i]  fi    *  (determinant(n  -  1;r)  matrix-minor(0;i;M))))


By

---

Latex:
(NthHypEqTrans  (-1)  THEN  ((RWO  "rng\_times\_sum\_l"  0  THENM  EqCDA)  THENA  Auto)  THEN  AutoSplit)

---

Home Index