---

Step * 1 1 1 of Lemma det-times

.....assertion..... 
1. r : CRng
2. n : ℕ
3. A : Matrix(n;n;r)
4. B : Matrix(n;n;r)
5. i : ℕn
6. k : |r|
7. M : Matrix(n;n;r)
8. |matrix-mul-row(r;k;i;(M*B))| = (k * |(M*B)|) ∈ |r|
⊢ |matrix-mul-row(r;k;i;(M*B))| = |(matrix-mul-row(r;k;i;M)*B)| ∈ |r|
BY
{ (EqCDA
   THEN RepUR ``matrix-mul-row matrix-times`` 0
   THEN EqCDA
   THEN AutoSplit
   THEN RWO "rng_times_sum_l" 0
   THEN Auto
   THEN EqCDA
   THEN Auto) }

---

Latex:

---

Latex:
.....assertion..... 
1.  r  :  CRng
2.  n  :  \mBbbN{}
3.  A  :  Matrix(n;n;r)
4.  B  :  Matrix(n;n;r)
5.  i  :  \mBbbN{}n
6.  k  :  |r|
7.  M  :  Matrix(n;n;r)
8.  |matrix-mul-row(r;k;i;(M*B))|  =  (k  *  |(M*B)|)
\mvdash{}  |matrix-mul-row(r;k;i;(M*B))|  =  |(matrix-mul-row(r;k;i;M)*B)|


By

---

Latex:
(EqCDA
  THEN  RepUR  ``matrix-mul-row  matrix-times``  0
  THEN  EqCDA
  THEN  AutoSplit
  THEN  RWO  "rng\_times\_sum\_l"  0
  THEN  Auto
  THEN  EqCDA
  THEN  Auto)

---

Home Index