---

Step * of Lemma det-multiple-col-ops

∀[r:CRng]. ∀[n:ℕ]. ∀[M:Matrix(n;n;r)]. ∀[a:ℕn]. ∀[k:|r|].
  (|matrix(if y=a then M[x,y] else (M[x,y] +r (k * M[x,a])))| = |M| ∈ |r|)
BY
{ (Auto THEN (InstLemma `det-multiple-row-ops` [⌜r⌝;⌜n⌝;⌜M'⌝;⌜a⌝;⌜k⌝]⋅ THENA Auto) THEN NthHypEq (-1) THEN EqCDA) }

1
.....subterm..... T:t
2:n
1. r : CRng
2. n : ℕ
3. M : Matrix(n;n;r)
4. a : ℕn
5. k : |r|
6. |matrix(if x=a then M'[x,y] else (M'[x,y] +r (k * M'[a,y])))| = |M'| ∈ |r|
⊢ |matrix(if y=a then M[x,y] else (M[x,y] +r (k * M[x,a])))|
= |matrix(if x=a then M'[x,y] else (M'[x,y] +r (k * M'[a,y])))|
∈ |r|

2
.....subterm..... T:t
3:n
1. r : CRng
2. n : ℕ
3. M : Matrix(n;n;r)
4. a : ℕn
5. k : |r|
6. |matrix(if x=a then M'[x,y] else (M'[x,y] +r (k * M'[a,y])))| = |M'| ∈ |r|
⊢ |M| = |M'| ∈ |r|

---

Latex:

---

Latex:
\mforall{}[r:CRng].  \mforall{}[n:\mBbbN{}].  \mforall{}[M:Matrix(n;n;r)].  \mforall{}[a:\mBbbN{}n].  \mforall{}[k:|r|].
    (|matrix(if  y=a  then  M[x,y]  else  (M[x,y]  +r  (k  *  M[x,a])))|  =  |M|)


By

---

Latex:
(Auto
  THEN  (InstLemma  `det-multiple-row-ops`  [\mkleeneopen{}r\mkleeneclose{};\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}M'\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}k\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  NthHypEq  (-1)
  THEN  EqCDA)

---

Home Index