---

Step * 1 1 of Lemma det-add-row


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|
BY
{ ((Subst' (Π(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) i + 1 
            ≤ i 
            < n
        M[i,f i])
    ∈ |r| 0
    THENA (Auto THEN EqCDA THEN AutoSplit)
    )
   THEN (Subst' (Π(r) i + 1 
                      ≤ i@0 
                      < n
                  if i@0=i then row (f i@0) else M[i@0,f i@0])
         = (Π(r) i + 1 
                 ≤ i 
                 < n
             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 < n. M[i,f i])))
= (((Π(r) 0 ≤ i < i. M[i,f i]) * ((row (f i)) * (Π(r) i + 1 ≤ i < n. M[i,f i]))) 
   +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:

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 
                  <  i
          M[i,f  i]) 
      * 
      (((row  (f  i))  +r  M[i,f  i]) 
        * 
        (\mPi{}(r)  i  +  1 
                    \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 
                    <  i
            M[i,f  i]) 
        * 
        ((row  (f  i))  *  (\mPi{}(r)  i  +  1  \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  <  i.  M[i,f  i])  *  (M[i,f  i]  *  (\mPi{}(r)  i  +  1  \mleq{}  i  <  n.  M[i,f  i]))))


By

---

Latex:
((Subst'  (\mPi{}(r)  i  +  1 
                              \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)  i  +  1 
                    \mleq{}  i 
                    <  n
            M[i,f  i])  0
    THENA  (Auto  THEN  EqCDA  THEN  AutoSplit)
    )
  THEN  (Subst'  (\mPi{}(r)  i  +  1 
                                        \mleq{}  i@0 
                                        <  n
                                if  i@0=i  then  row  (f  i@0)  else  M[i@0,f  i@0])
              =  (\mPi{}(r)  i  +  1 
                              \mleq{}  i 
                              <  n
                      M[i,f  i])  0
              THENA  (Auto  THEN  EqCDA  THEN  AutoSplit)
              )
  )

---

Home Index