---

Step * 1 of Lemma equal-rows-det


1. r : CRng
2. n : ℕ
3. M : Matrix(n;n;r)
4. ∀[i,j:ℕn].  |M| = 0 ∈ |r| supposing (¬(i = j ∈ ℤ)) ∧ (matrix-swap-rows(M;i;j) = M ∈ Matrix(n;n;r))
5. i : ℕn
6. j : ℕn
7. ¬(i = j ∈ ℤ)
8. matrix-swap-rows(M;i;j) = M ∈ Matrix(n;n;r)
⊢ |M| = 0 ∈ |r|
BY
{ (InstHyp [⌜i⌝;⌜j⌝] 4⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  r  :  CRng
2.  n  :  \mBbbN{}
3.  M  :  Matrix(n;n;r)
4.  \mforall{}[i,j:\mBbbN{}n].    |M|  =  0  supposing  (\mneg{}(i  =  j))  \mwedge{}  (matrix-swap-rows(M;i;j)  =  M)
5.  i  :  \mBbbN{}n
6.  j  :  \mBbbN{}n
7.  \mneg{}(i  =  j)
8.  matrix-swap-rows(M;i;j)  =  M
\mvdash{}  |M|  =  0


By

---

Latex:
(InstHyp  [\mkleeneopen{}i\mkleeneclose{};\mkleeneopen{}j\mkleeneclose{}]  4\mcdot{}  THEN  Auto)

---

Home Index