---

Step * 2 1 1 1 1 2 1 1 2 of Lemma det-fun-is-determinant

.....upcase..... 
1. r : CRng
2. n : ℤ
3. ¬n < 1
4. 0 < n
5. d : det-fun(r;n)
6. M : Matrix(n;n;r)
7. j : ℤ
8. 0 < j
9. ((Σ(r) 0 
          ≤ i 
          < j - 1
      d matrix(if x=0 then if y=i then M[0,i] else 0 else M[x,y])) 
    +r 
    (d matrix(if x=0 then if (y) < (j - 1)  then 0  else M[x,y] else M[x,y])))
= (d M)
∈ |r|
⊢ ((Σ(r) 0 
         ≤ i 
         < j
     d matrix(if x=0 then if y=i then M[0,i] else 0 else M[x,y])) 
   +r 
   (d matrix(if x=0 then if (y) < (j)  then 0  else M[x,y] else M[x,y])))
= (d M)
∈ |r|
BY
{ (NthHypEqTrans (-1)
   THEN Thin (-1)
   THEN skip{((Subst' (j - 1) + 1 ~ j 0 THENA Auto)
              THEN (RW (AddrC [3] (LemmaC `rng_sum_unroll_hi`)) 0 THENA Auto)
              THEN (Subst' (j + 1) - 1 ~ j 0 THENA Auto)
              THEN skip{((RW (AddrC [3;2] (LemmaC `rng_sum_unroll_hi`)) 0 THENA Auto)
                         THEN (RW (AddrC [2] (LemmaC `rng_sum_unroll_hi`)) 0 THENA Auto)
                         )})}) }

1
1. r : CRng
2. n : ℤ
3. ¬n < 1
4. 0 < n
5. d : det-fun(r;n)
6. M : Matrix(n;n;r)
7. j : ℤ
8. 0 < j
⊢ ((Σ(r) 0 
         ≤ i 
         < j - 1
     d matrix(if x=0 then if y=i then M[0,i] else 0 else M[x,y])) 
   +r 
   (d matrix(if x=0 then if (y) < (j - 1)  then 0  else M[x,y] else M[x,y])))
= ((Σ(r) 0 
         ≤ i 
         < j
     d matrix(if x=0 then if y=i then M[0,i] else 0 else M[x,y])) 
   +r 
   (d matrix(if x=0 then if (y) < (j)  then 0  else M[x,y] else M[x,y])))
∈ |r|

---

Latex:

---

Latex:
.....upcase..... 
1.  r  :  CRng
2.  n  :  \mBbbZ{}
3.  \mneg{}n  <  1
4.  0  <  n
5.  d  :  det-fun(r;n)
6.  M  :  Matrix(n;n;r)
7.  j  :  \mBbbZ{}
8.  0  <  j
9.  ((\mSigma{}(r)  0 
                    \mleq{}  i 
                    <  j  -  1
            d  matrix(if  x=0  then  if  y=i  then  M[0,i]  else  0  else  M[x,y])) 
        +r 
        (d  matrix(if  x=0  then  if  (y)  <  (j  -  1)    then  0    else  M[x,y]  else  M[x,y])))
=  (d  M)
\mvdash{}  ((\mSigma{}(r)  0 
                  \mleq{}  i 
                  <  j
          d  matrix(if  x=0  then  if  y=i  then  M[0,i]  else  0  else  M[x,y])) 
      +r 
      (d  matrix(if  x=0  then  if  (y)  <  (j)    then  0    else  M[x,y]  else  M[x,y])))
=  (d  M)


By

---

Latex:
(NthHypEqTrans  (-1)
  THEN  Thin  (-1)
  THEN  skip\{((Subst'  (j  -  1)  +  1  \msim{}  j  0  THENA  Auto)
                        THEN  (RW  (AddrC  [3]  (LemmaC  `rng\_sum\_unroll\_hi`))  0  THENA  Auto)
                        THEN  (Subst'  (j  +  1)  -  1  \msim{}  j  0  THENA  Auto)
                        THEN  skip\{((RW  (AddrC  [3;2]  (LemmaC  `rng\_sum\_unroll\_hi`))  0  THENA  Auto)
                                              THEN  (RW  (AddrC  [2]  (LemmaC  `rng\_sum\_unroll\_hi`))  0  THENA  Auto)
                                              )\})\})

---

Home Index