---

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


1. r : CRng
2. n : ℤ
3. ¬n < 1
4. 0 < n
5. d : det-fun(r;n)
6. M : Matrix(n;n;r)
⊢ (Σ(r) 0 ≤ i < n. d matrix(if x=0 then if y=i then M[0,i] else 0 else M[x,y])) = (d M) ∈ |r|
BY
{ Assert ⌜∀j:ℕ
            (((Σ(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|)⌝⋅ }

1
.....assertion..... 
1. r : CRng
2. n : ℤ
3. ¬n < 1
4. 0 < n
5. d : det-fun(r;n)
6. M : Matrix(n;n;r)
⊢ ∀j:ℕ
    (((Σ(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|)

2
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:ℕ
     (((Σ(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|)
⊢ (Σ(r) 0 ≤ i < n. d matrix(if x=0 then if y=i then M[0,i] else 0 else M[x,y])) = (d M) ∈ |r|

---

Latex:

---

Latex:

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)
\mvdash{}  (\mSigma{}(r)  0  \mleq{}  i  <  n.  d  matrix(if  x=0  then  if  y=i  then  M[0,i]  else  0  else  M[x,y]))  =  (d  M)


By

---

Latex:
Assert  \mkleeneopen{}\mforall{}j:\mBbbN{}
                    (((\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))\mkleeneclose{}\mcdot{}

---

Home Index