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

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

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

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


By


Latex:
(Subst'  (d  matrix(if  x=0  then  if  (y)  <  (n)    then  0    else  M[x,y]  else  M[x,y]))  =  0  0  THENA  Auto)




Home Index