---

Step * of Lemma det-add-row

∀[r:CRng]. ∀[n:ℕ]. ∀[M:Matrix(n;n;r)]. ∀[i:ℕn]. ∀[row:ℕn ⟶ |r|].
  (|matrix(if x=i then (row y) +r M[x,y] else M[x,y])| = (|matrix(if x=i then row y else M[x,y])| +r |M|) ∈ |r|)
BY
{ (Auto
   THEN Unfold `matrix-det` 0
   THEN (RWO "rng_lsum_plus<" 0 THENA Auto)
   THEN EqCDA
   THEN RepUR ``let`` 0
   THEN (Assert ⌜(Π(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|⌝⋅
   THENM (AutoSplit THEN RWO "-1" 0 THEN Auto)
   )) }

1
.....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|

---

Latex:

---

Latex:
\mforall{}[r:CRng].  \mforall{}[n:\mBbbN{}].  \mforall{}[M:Matrix(n;n;r)].  \mforall{}[i:\mBbbN{}n].  \mforall{}[row:\mBbbN{}n  {}\mrightarrow{}  |r|].
    (|matrix(if  x=i  then  (row  y)  +r  M[x,y]  else  M[x,y])|
    =  (|matrix(if  x=i  then  row  y  else  M[x,y])|  +r  |M|))


By

---

Latex:
(Auto
  THEN  Unfold  `matrix-det`  0
  THEN  (RWO  "rng\_lsum\_plus<"  0  THENA  Auto)
  THEN  EqCDA
  THEN  RepUR  ``let``  0
  THEN  (Assert  \mkleeneopen{}(\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]))\mkleeneclose{}\mcdot{}
  THENM  (AutoSplit  THEN  RWO  "-1"  0  THEN  Auto)
  ))

---

Home Index