---

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

.....upcase..... 
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|))
⊢ ∀[d:det-fun(r;n)]. (d = (λM.((d I) * (determinant(n;r) M))) ∈ (Matrix(n;n;r) ⟶ |r|))
BY
{ (Intro
   THEN (Assert ∀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|)) BY
               (Intro
                THEN (D -3 With ⌜λM.(d matrix+(r;J;M))⌝  THENW (BLemma `det-fun+` THEN Auto))
                THEN (NthHypEqTrans (-1) THEN (FunExt THENA Auto) THEN Reduce 0)
                THEN EqCDA
                THEN Using [`n',⌜n - 1⌝] (BLemma `det-fun+-at-identity`)⋅
                THEN Auto))
   ) }

1
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|)

---

Latex:

---

Latex:
.....upcase..... 
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))))
\mvdash{}  \mforall{}[d:det-fun(r;n)].  (d  =  (\mlambda{}M.((d  I)  *  (determinant(n;r)  M))))


By

---

Latex:
(Intro
  THEN  (Assert  \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))))  BY
                          (Intro
                            THEN  (D  -3  With  \mkleeneopen{}\mlambda{}M.(d  matrix+(r;J;M))\mkleeneclose{}    THENW  (BLemma  `det-fun+`  THEN  Auto))
                            THEN  (NthHypEqTrans  (-1)  THEN  (FunExt  THENA  Auto)  THEN  Reduce  0)
                            THEN  EqCDA
                            THEN  Using  [`n',\mkleeneopen{}n  -  1\mkleeneclose{}]  (BLemma  `det-fun+-at-identity`)\mcdot{}
                            THEN  Auto))
  )

---

Home Index