---

Step * 1 of Lemma det-add-row

.....assertion..... 
1. r : CRng
2. n : ℕ
3. M : Matrix(n;n;r)
4. i : ℕn
5. row : ℕn ⟶ |r|
6. f : ℕn →⟶ ℕn
⊢ (Π(r) 0 
        ≤ i@0 
        < n
    if i@0=i then (row (f i@0)) +r M[i@0,f i@0] else M[i@0,f i@0])
= ((Π(r) 0 ≤ i@0 < n. if i@0=i then row (f i@0) else M[i@0,f i@0]) +r (Π(r) 0 ≤ i < n. M[i,f i]))
∈ |r|
BY
{ ((Unfold `rng_prod` 0 THEN (RWH (LemmaWithC [`b',i] `mon_itop_split_el`) 0 THENA Auto))
   THEN Fold `rng_prod` 0
   THEN (Subst' * ~ * 0 THENA (RepUR ``mul_mon_of_rng`` 0 THEN Auto))
   THEN (Reduce 0 THENA Auto)
   THEN (Subst' (Π(r) 0 
                      ≤ i@0 
                      < i
                  if i@0=i then (row (f i@0)) +r M[i@0,f i@0] else M[i@0,f i@0])
         = (Π(r) 0 
                 ≤ i 
                 < i
             M[i,f i])
         ∈ |r| 0
         THENA (Auto THEN EqCDA THEN AutoSplit)
         )
   THEN (Subst' (Π(r) 0 ≤ i@0 < i. if i@0=i then row (f i@0) else M[i@0,f i@0]) = (Π(r) 0 ≤ i < i. M[i,f i]) ∈ |r| 0
         THENA (Auto THEN EqCDA THEN AutoSplit)
         )) }

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

---

Latex:

---

Latex:
.....assertion..... 
1.  r  :  CRng
2.  n  :  \mBbbN{}
3.  M  :  Matrix(n;n;r)
4.  i  :  \mBbbN{}n
5.  row  :  \mBbbN{}n  {}\mrightarrow{}  |r|
6.  f  :  \mBbbN{}n  \mrightarrow{}{}\mrightarrow{}  \mBbbN{}n
\mvdash{}  (\mPi{}(r)  0 
                \mleq{}  i@0 
                <  n
        if  i@0=i  then  (row  (f  i@0))  +r  M[i@0,f  i@0]  else  M[i@0,f  i@0])
=  ((\mPi{}(r)  0  \mleq{}  i@0  <  n.  if  i@0=i  then  row  (f  i@0)  else  M[i@0,f  i@0])  +r  (\mPi{}(r)  0  \mleq{}  i  <  n.  M[i,f  i]))


By

---

Latex:
((Unfold  `rng\_prod`  0  THEN  (RWH  (LemmaWithC  [`b',i]  `mon\_itop\_split\_el`)  0  THENA  Auto))
  THEN  Fold  `rng\_prod`  0
  THEN  (Subst'  *  \msim{}  *  0  THENA  (RepUR  ``mul\_mon\_of\_rng``  0  THEN  Auto))
  THEN  (Reduce  0  THENA  Auto)
  THEN  (Subst'  (\mPi{}(r)  0 
                                        \mleq{}  i@0 
                                        <  i
                                if  i@0=i  then  (row  (f  i@0))  +r  M[i@0,f  i@0]  else  M[i@0,f  i@0])
              =  (\mPi{}(r)  0 
                              \mleq{}  i 
                              <  i
                      M[i,f  i])  0
              THENA  (Auto  THEN  EqCDA  THEN  AutoSplit)
              )
  THEN  (Subst'  (\mPi{}(r)  0 
                                        \mleq{}  i@0 
                                        <  i
                                if  i@0=i  then  row  (f  i@0)  else  M[i@0,f  i@0])
              =  (\mPi{}(r)  0 
                              \mleq{}  i 
                              <  i
                      M[i,f  i])  0
              THENA  (Auto  THEN  EqCDA  THEN  AutoSplit)
              ))

---

Home Index