---

Step * 1 of Lemma matrix-det-is-determinant


1. [r] : CRng
2. [n] : ℕ
3. (λm.|m|) = (λM.(((λm.|m|) I) * (determinant(n;r) M))) ∈ (Matrix(n;n;r) ⟶ |r|)
⊢ ∀[M:Matrix(n;n;r)]. (|M| = (determinant(n;r) M) ∈ |r|)
BY
{ (Intro THEN (ApFunToHypEquands `Z' ⌜Z M⌝ ⌜|r|⌝ (-2)⋅ THENA Auto) THEN Reduce -1 THEN NthHypEqTrans (-1)) }

1
.....assertion..... 
1. r : CRng
2. n : ℕ
3. (λm.|m|) = (λM.(((λm.|m|) I) * (determinant(n;r) M))) ∈ (Matrix(n;n;r) ⟶ |r|)
4. M : Matrix(n;n;r)
5. |M| = (|I| * (determinant(n;r) M)) ∈ |r|
⊢ (|I| * (determinant(n;r) M)) = (determinant(n;r) M) ∈ |r|

---

Latex:

---

Latex:

1.  [r]  :  CRng
2.  [n]  :  \mBbbN{}
3.  (\mlambda{}m.|m|)  =  (\mlambda{}M.(((\mlambda{}m.|m|)  I)  *  (determinant(n;r)  M)))
\mvdash{}  \mforall{}[M:Matrix(n;n;r)].  (|M|  =  (determinant(n;r)  M))


By

---

Latex:
(Intro
  THEN  (ApFunToHypEquands  `Z'  \mkleeneopen{}Z  M\mkleeneclose{}  \mkleeneopen{}|r|\mkleeneclose{}  (-2)\mcdot{}  THENA  Auto)
  THEN  Reduce  -1
  THEN  NthHypEqTrans  (-1))

---

Home Index