---

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

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

---

Latex:

---

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


By

---

Latex:
Assert  \mkleeneopen{}(\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]))
                =  (\mSigma{}(r)  0 
                                \mleq{}  i 
                                <  n
                        M[0,i]  *  (d  matrix(if  x=0  then  if  y=i  then  1  else  0  else  M[x,y])))\mkleeneclose{}\mcdot{}

---

Home Index