---

Step * of Lemma det-multiple-row-ops

∀[r:CRng]. ∀[n:ℕ]. ∀[M:Matrix(n;n;r)]. ∀[a:ℕn]. ∀[k:|r|].
  (|matrix(if x=a then M[x,y] else (M[x,y] +r (k * M[a,y])))| = |M| ∈ |r|)
BY
{ (Auto
   THEN Assert ⌜∀d:ℕ
                  (|matrix(if x <z d then if x=a then M[x,y] else (M[x,y] +r (k * M[a,y])) else M[x,y] fi )|
                  = |M|
                  ∈ |r|)⌝⋅
   ) }

1
.....assertion..... 
1. r : CRng
2. n : ℕ
3. M : Matrix(n;n;r)
4. a : ℕn
5. k : |r|
⊢ ∀d:ℕ. (|matrix(if x <z d then if x=a then M[x,y] else (M[x,y] +r (k * M[a,y])) else M[x,y] fi )| = |M| ∈ |r|)

2
1. r : CRng
2. n : ℕ
3. M : Matrix(n;n;r)
4. a : ℕn
5. k : |r|
6. ∀d:ℕ. (|matrix(if x <z d then if x=a then M[x,y] else (M[x,y] +r (k * M[a,y])) else M[x,y] fi )| = |M| ∈ |r|)
⊢ |matrix(if x=a then M[x,y] else (M[x,y] +r (k * M[a,y])))| = |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  x=a  then  M[x,y]  else  (M[x,y]  +r  (k  *  M[a,y])))|  =  |M|)


By

---

Latex:
(Auto
  THEN  Assert  \mkleeneopen{}\mforall{}d:\mBbbN{}
                                (|matrix(if  x  <z  d
                                then  if  x=a  then  M[x,y]  else  (M[x,y]  +r  (k  *  M[a,y]))
                                else  M[x,y]
                                fi  )|
                                =  |M|)\mkleeneclose{}\mcdot{}
  )

---

Home Index