---

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


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|
9. d - 1 < n
10. ¬((d - 1) = a ∈ ℤ)
⊢ |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 )|
= |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 )|
∈ |r|
BY
{ (InstLemma `det-row-op` [⌜r⌝;⌜n⌝;⌜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 )⌝;⌜d - 1⌝;⌜a⌝;⌜k⌝]⋅
   THENA Auto
   ) }

1
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|
9. d - 1 < n
10. ¬((d - 1) = a ∈ ℤ)
11. |row-op(r;d - 1;a;k;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 ))|
= |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 )|
∈ |r|
⊢ |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 )|
= |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 )|
∈ |r|

---

Latex:

---

Latex:

1.  r  :  CRng
2.  n  :  \mBbbN{}
3.  M  :  Matrix(n;n;r)
4.  a  :  \mBbbN{}n
5.  k  :  |r|
6.  d  :  \mBbbZ{}
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|
9.  d  -  1  <  n
10.  \mneg{}((d  -  1)  =  a)
\mvdash{}  |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  )|
=  |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  )|


By

---

Latex:
(InstLemma  `det-row-op`  [\mkleeneopen{}r\mkleeneclose{};\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}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  )\mkleeneclose{};\mkleeneopen{}d  -  1\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}k\mkleeneclose{}]\mcdot{}
  THENA  Auto
  )

---

Home Index