---

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

.....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|
BY
{ (Subst' matrix(if x=a then M'[x,y] else (M'[x,y] +r (k * M'[a,y])))
   = matrix(if y=a then M[x,y] else (M[x,y] +r (k * M[x,a])))'
   ∈ Matrix(n;n;r) 0
   THEN Auto
   ) }

1
.....equality..... 
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 x=a then M'[x,y] else (M'[x,y] +r (k * M'[a,y])))
= matrix(if y=a then M[x,y] else (M[x,y] +r (k * M[x,a])))'
∈ Matrix(n;n;r)

---

Latex:

---

Latex:
.....subterm.....  T:t
2:n
1.  r  :  CRng
2.  n  :  \mBbbN{}
3.  M  :  Matrix(n;n;r)
4.  a  :  \mBbbN{}n
5.  k  :  |r|
6.  |matrix(if  x=a  then  M'[x,y]  else  (M'[x,y]  +r  (k  *  M'[a,y])))|  =  |M'|
\mvdash{}  |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])))|


By

---

Latex:
(Subst'  matrix(if  x=a  then  M'[x,y]  else  (M'[x,y]  +r  (k  *  M'[a,y])))
  =  matrix(if  y=a  then  M[x,y]  else  (M[x,y]  +r  (k  *  M[x,a])))'  0
  THEN  Auto
  )

---

Home Index