---

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

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

---

Latex:

---

Latex:
.....subterm.....  T:t
3:n
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.  (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])))
8.  i  :  \mBbbN{}n
\mvdash{}  (d  matrix(if  x=0  then  if  y=i  then  1  else  0  else  M[x,y]))  =  (d  matrix+(r;i;matrix-minor(0;i;M)))


By

---

Latex:
Assert  \mkleeneopen{}\mforall{}j:\mBbbN{}
                    ((d 
                        matrix(if  x=0
                                      then  if  y=i  then  1  else  0
                                      else  if  (j)  <  (x)    then  if  y=i  then  0  else  M[x,y]    else  M[x,y]))
                    =  (d  matrix+(r;i;matrix-minor(0;i;M))))\mkleeneclose{}\mcdot{}

---

Home Index