---

Step * 1 1 of Lemma det-mul-row


1. r : CRng
2. n : ℕ
3. M : Matrix(n;n;r)
4. i : ℕn
5. k : |r|
6. f : ℕn →⟶ ℕn
⊢ ((Π 0 ≤ i@0 < i. matrix-mul-row(r;k;i;M)[i@0,f i@0]) 
   * 
   (matrix-mul-row(r;k;i;M)[i,f i] * (Π i + 1 ≤ i@0 < n. matrix-mul-row(r;k;i;M)[i@0,f i@0])))
= (k * ((Π 0 ≤ i < i. M[i,f i]) * (M[i,f i] * (Π i + 1 ≤ i < n. M[i,f i]))))
∈ |r|
BY
{ ((Subst' (Π 0 ≤ i@0 < i. matrix-mul-row(r;k;i;M)[i@0,f i@0]) = (Π 0 ≤ i < i. M[i,f i]) ∈ |r| 0
    THENA (Auto THEN EqCDA THEN RepUR ``matrix-mul-row mx matrix-ap`` 0 THEN Fold `matrix-ap` 0 THEN AutoSplit)
    )
   THEN (Subst' (Π i + 1 ≤ i@0 < n. matrix-mul-row(r;k;i;M)[i@0,f i@0]) = (Π i + 1 ≤ i < n. M[i,f i]) ∈ |r| 0
         THENA (Auto THEN EqCDA THEN RepUR ``matrix-mul-row mx matrix-ap`` 0 THEN Fold `matrix-ap` 0 THEN AutoSplit)
         )
   THEN (Subst' matrix-mul-row(r;k;i;M)[i,f i] ~ k * M[i,f i] 0
         THENA (RepUR ``matrix-mul-row mx matrix-ap`` 0 THEN Auto)
         )) }

1
1. r : CRng
2. n : ℕ
3. M : Matrix(n;n;r)
4. i : ℕn
5. k : |r|
6. f : ℕn →⟶ ℕn
⊢ ((Π 0 ≤ i < i. M[i,f i]) * ((k * M[i,f i]) * (Π i + 1 ≤ i < n. M[i,f i])))
= (k * ((Π 0 ≤ i < i. M[i,f i]) * (M[i,f i] * (Π i + 1 ≤ i < n. M[i,f i]))))
∈ |r|

---

Latex:

---

Latex:

1.  r  :  CRng
2.  n  :  \mBbbN{}
3.  M  :  Matrix(n;n;r)
4.  i  :  \mBbbN{}n
5.  k  :  |r|
6.  f  :  \mBbbN{}n  \mrightarrow{}{}\mrightarrow{}  \mBbbN{}n
\mvdash{}  ((\mPi{}  0  \mleq{}  i@0  <  i.  matrix-mul-row(r;k;i;M)[i@0,f  i@0]) 
      * 
      (matrix-mul-row(r;k;i;M)[i,f  i]  *  (\mPi{}  i  +  1  \mleq{}  i@0  <  n.  matrix-mul-row(r;k;i;M)[i@0,f  i@0])))
=  (k  *  ((\mPi{}  0  \mleq{}  i  <  i.  M[i,f  i])  *  (M[i,f  i]  *  (\mPi{}  i  +  1  \mleq{}  i  <  n.  M[i,f  i]))))


By

---

Latex:
((Subst'  (\mPi{}  0  \mleq{}  i@0  <  i.  matrix-mul-row(r;k;i;M)[i@0,f  i@0])  =  (\mPi{}  0  \mleq{}  i  <  i.  M[i,f  i])  0
    THENA  (Auto
                  THEN  EqCDA
                  THEN  RepUR  ``matrix-mul-row  mx  matrix-ap``  0
                  THEN  Fold  `matrix-ap`  0
                  THEN  AutoSplit)
    )
  THEN  (Subst'  (\mPi{}  i  +  1  \mleq{}  i@0  <  n.  matrix-mul-row(r;k;i;M)[i@0,f  i@0])
              =  (\mPi{}  i  +  1  \mleq{}  i  <  n.  M[i,f  i])  0
              THENA  (Auto
                            THEN  EqCDA
                            THEN  RepUR  ``matrix-mul-row  mx  matrix-ap``  0
                            THEN  Fold  `matrix-ap`  0
                            THEN  AutoSplit)
              )
  THEN  (Subst'  matrix-mul-row(r;k;i;M)[i,f  i]  \msim{}  k  *  M[i,f  i]  0
              THENA  (RepUR  ``matrix-mul-row  mx  matrix-ap``  0  THEN  Auto)
              ))

---

Home Index