---

Step * 1 of Lemma det-multiple-row-ops

.....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|)
BY
{ InductionOnNat }

1
.....basecase..... 
1. r : CRng
2. n : ℕ
3. M : Matrix(n;n;r)
4. a : ℕn
5. k : |r|
6. d : ℤ
⊢ |matrix(if x <z 0 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
.....upcase..... 
1. r : CRng
2. n : ℕ
3. M : Matrix(n;n;r)
4. a : ℕn
5. k : |r|
6. d : ℤ
7. 0 < d
8. |matrix(if x <z d - 1 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 <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|

---

Latex:

---

Latex:
.....assertion..... 
1.  r  :  CRng
2.  n  :  \mBbbN{}
3.  M  :  Matrix(n;n;r)
4.  a  :  \mBbbN{}n
5.  k  :  |r|
\mvdash{}  \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|)


By

---

Latex:
InductionOnNat

---

Home Index