---

Step * 1 2 1 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 ∈ ℤ)
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)
BY
{ (Unfold `matrix-swap-rows` 0 THEN EqCDA THEN Reduce 0 THEN AutoSplit) }

---

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)
8.  \mneg{}(x  =  y)
\mvdash{}  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])


By

---

Latex:
(Unfold  `matrix-swap-rows`  0  THEN  EqCDA  THEN  Reduce  0  THEN  AutoSplit)

---

Home Index