---

Step * 1 2 of Lemma adjugate-property


1. r : CRng
2. n : ℕ
3. M : Matrix(n;n;r)
4. ¬(n = 0 ∈ ℤ)
5. x : ℕn@i
6. y : ℕn@i
7. ¬(x = y ∈ ℤ)
⊢ |matrix(if a=y then M[x,b] else M[a,b])| = 0 ∈ |r|
BY
{ ((BLemma `equal-rows-det` THEN Auto) THEN InstConcl [⌜x⌝;⌜y⌝]⋅ THEN Auto) }

1
1. r : CRng
2. n : ℕ
3. M : Matrix(n;n;r)
4. ¬(n = 0 ∈ ℤ)
5. x : ℕn@i
6. y : ℕn@i
7. ¬(x = y ∈ ℤ)
8. ¬(x = y ∈ ℤ)
⊢ matrix-swap-rows(matrix(if a=y then M[x,b] else M[a,b]);x;y) = matrix(if a=y then M[x,b] else M[a,b]) ∈ Matrix(n;n;r)

---

Latex:

---

Latex:

1.  r  :  CRng
2.  n  :  \mBbbN{}
3.  M  :  Matrix(n;n;r)
4.  \mneg{}(n  =  0)
5.  x  :  \mBbbN{}n@i
6.  y  :  \mBbbN{}n@i
7.  \mneg{}(x  =  y)
\mvdash{}  |matrix(if  a=y  then  M[x,b]  else  M[a,b])|  =  0


By

---

Latex:
((BLemma  `equal-rows-det`  THEN  Auto)  THEN  InstConcl  [\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index