---

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


1. r : CRng
2. n : ℤ
3. 0 < n
4. ∀[d:det-fun(r;n - 1)]. (d = (λM.((d I) * (determinant(n - 1;r) M))) ∈ (Matrix(n - 1;n - 1;r) ⟶ |r|))
5. d : det-fun(r;n)
6. ∀J:ℕn
     ((λM.(d matrix+(r;J;M)))
     = (λM.(if isEven(J) then d I else -r (d I) fi  * (determinant(n - 1;r) M)))
     ∈ (Matrix(n - 1;n - 1;r) ⟶ |r|))
⊢ d = (λM.((d I) * (determinant(n;r) M))) ∈ (Matrix(n;n;r) ⟶ |r|)
BY
{ ((Assert ∀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|) BY
          ((ParallelLast THEN Auto)
           THEN (ApFunToHypEquands `Z' ⌜Z matrix-minor(0;i;M)⌝ ⌜|r|⌝ (-2)⋅ THENA Auto)
           THEN Reduce -1
           THEN Auto))
   THEN Thin (-4)
   THEN Thin (-2)) }

1
1. r : CRng
2. n : ℤ
3. 0 < n
4. d : det-fun(r;n)
5. ∀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|)
⊢ d = (λM.((d I) * (determinant(n;r) M))) ∈ (Matrix(n;n;r) ⟶ |r|)

---

Latex:

---

Latex:

1.  r  :  CRng
2.  n  :  \mBbbZ{}
3.  0  <  n
4.  \mforall{}[d:det-fun(r;n  -  1)].  (d  =  (\mlambda{}M.((d  I)  *  (determinant(n  -  1;r)  M))))
5.  d  :  det-fun(r;n)
6.  \mforall{}J:\mBbbN{}n
          ((\mlambda{}M.(d  matrix+(r;J;M)))
          =  (\mlambda{}M.(if  isEven(J)  then  d  I  else  -r  (d  I)  fi    *  (determinant(n  -  1;r)  M))))
\mvdash{}  d  =  (\mlambda{}M.((d  I)  *  (determinant(n;r)  M)))


By

---

Latex:
((Assert  \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))))  BY
                ((ParallelLast  THEN  Auto)
                  THEN  (ApFunToHypEquands  `Z'  \mkleeneopen{}Z  matrix-minor(0;i;M)\mkleeneclose{}  \mkleeneopen{}|r|\mkleeneclose{}  (-2)\mcdot{}  THENA  Auto)
                  THEN  Reduce  -1
                  THEN  Auto))
  THEN  Thin  (-4)
  THEN  Thin  (-2))

---

Home Index