---

Step * of Lemma det-fun-row-op

∀[r:Rng]. ∀[n:ℕ]. ∀[d:det-fun(r;n)]. ∀[M:Matrix(n;n;r)]. ∀[a,b:ℕn]. ∀[k:|r|].
  (d row-op(r;a;b;k;M)) = (d M) ∈ |r| supposing ¬(a = b ∈ ℤ)
BY
{ (Auto
   THEN DVar `d'
   THEN Auto
   THEN (InstHyp [⌜a⌝;⌜λy.(k * M[b,y])⌝;⌜M⌝] 5⋅ THENA Auto)
   THEN Reduce -1
   THEN NthHypEq (-1)
   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. a : ℕn
10. b : ℕn
11. k : |r|
12. ¬(a = b ∈ ℤ)
13. (d matrix(if x=a then (k * M[b,y]) +r M[x,y] else M[x,y]))
= ((d matrix(if x=a then k * M[b,y] else M[x,y])) +r (d M))
∈ |r|
⊢ (d row-op(r;a;b;k;M)) = (d matrix(if x=a then (k * M[b,y]) +r M[x,y] else M[x,y])) ∈ |r|

2
.....subterm..... T:t
3: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. a : ℕn
10. b : ℕn
11. k : |r|
12. ¬(a = b ∈ ℤ)
13. (d matrix(if x=a then (k * M[b,y]) +r M[x,y] else M[x,y]))
= ((d matrix(if x=a then k * M[b,y] else M[x,y])) +r (d M))
∈ |r|
⊢ (d M) = ((d matrix(if x=a then k * M[b,y] else M[x,y])) +r (d M)) ∈ |r|

---

Latex:

---

Latex:
\mforall{}[r:Rng].  \mforall{}[n:\mBbbN{}].  \mforall{}[d:det-fun(r;n)].  \mforall{}[M:Matrix(n;n;r)].  \mforall{}[a,b:\mBbbN{}n].  \mforall{}[k:|r|].
    (d  row-op(r;a;b;k;M))  =  (d  M)  supposing  \mneg{}(a  =  b)


By

---

Latex:
(Auto
  THEN  DVar  `d'
  THEN  Auto
  THEN  (InstHyp  [\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}\mlambda{}y.(k  *  M[b,y])\mkleeneclose{};\mkleeneopen{}M\mkleeneclose{}]  5\mcdot{}  THENA  Auto)
  THEN  Reduce  -1
  THEN  NthHypEq  (-1)
  THEN  EqCDA)

---

Home Index