---

Step * of Lemma det-fun-zero-row

∀[r:Rng]. ∀[n:ℕ]. ∀[d:det-fun(r;n)]. ∀[M:Matrix(n;n;r)].  (d M) = 0 ∈ |r| supposing ∃i:ℕn. ∀j:ℕn. (M[i,j] = 0 ∈ |r|)
BY
{ ((Auto THEN ExRepD)
   THEN (DVar `d' THEN Auto)
   THEN (InstHyp [⌜i⌝;⌜0⌝;⌜M⌝] 4⋅ THENA Auto)
   THEN NthHypEq (-1)
   THEN EqCDA
   THEN Auto
   THEN EqCDA) }

1
.....subterm..... T:t
2:n
1. r : Rng
2. n : ℕ
3. d : Matrix(n;n;r) ⟶ |r|
4. ∀i:ℕn. ∀k:|r|. ∀M:Matrix(n;n;r).  ((d matrix-mul-row(r;k;i;M)) = (k * (d M)) ∈ |r|)
5. ∀i:ℕn. ∀row:ℕn ⟶ |r|. ∀M:Matrix(n;n;r).
     ((d matrix(if x=i then (row y) +r M[x,y] else M[x,y]))
     = ((d matrix(if x=i then row y else M[x,y])) +r (d M))
     ∈ |r|)
6. ∀i,j:ℕn.  ((¬(i = j ∈ ℤ)) ⇒ (∀M:Matrix(n;n;r). ((d matrix-swap-rows(M;i;j)) = (-r (d M)) ∈ |r|)))
7. ∀i,j:ℕn.
     ((¬(i = j ∈ ℤ)) ⇒ (∀M:Matrix(n;n;r). ((matrix-swap-rows(M;i;j) = M ∈ Matrix(n;n;r)) ⇒ ((d M) = 0 ∈ |r|))))
8. M : Matrix(n;n;r)
9. i : ℕn
10. ∀j:ℕn. (M[i,j] = 0 ∈ |r|)
11. (d matrix-mul-row(r;0;i;M)) = (0 * (d M)) ∈ |r|
⊢ M = matrix-mul-row(r;0;i;M) ∈ Matrix(n;n;r)

---

Latex:

---

Latex:
\mforall{}[r:Rng].  \mforall{}[n:\mBbbN{}].  \mforall{}[d:det-fun(r;n)].  \mforall{}[M:Matrix(n;n;r)].
    (d  M)  =  0  supposing  \mexists{}i:\mBbbN{}n.  \mforall{}j:\mBbbN{}n.  (M[i,j]  =  0)


By

---

Latex:
((Auto  THEN  ExRepD)
  THEN  (DVar  `d'  THEN  Auto)
  THEN  (InstHyp  [\mkleeneopen{}i\mkleeneclose{};\mkleeneopen{}0\mkleeneclose{};\mkleeneopen{}M\mkleeneclose{}]  4\mcdot{}  THENA  Auto)
  THEN  NthHypEq  (-1)
  THEN  EqCDA
  THEN  Auto
  THEN  EqCDA)

---

Home Index