---

Step * 2 1 of Lemma adjugate-property

.....assertion..... 
1. r : CRng
2. n : ℕ
3. M : Matrix(n;n;r)
4. ¬(n = 0 ∈ ℤ)
5. x : ℕn@i
6. y : ℕn@i
7. |matrix(if a=y then M[x,b] else M[a,b])| = (|M| * if x=y then 1 else 0) ∈ |r|
⊢ ∀M:Matrix(n;n;r). ∀x:ℕn.
    (|M| = (Σ(r) 0 ≤ i < n. if isEven(i + x) then M[x,i] else -r M[x,i] fi  * |matrix-minor(x;i;M)|) ∈ |r|)
BY
{ (ThinVar `M'
   THEN RepeatFor 2 (Thin (-1))
   THEN Assert ⌜∀M:Matrix(n;n;r)
                  (|M|
                  = (Σ(r) 0 
                          ≤ i 
                          < n
                      if isEven(i + 0) then M[0,i] else -r M[0,i] fi  * |matrix-minor(0;i;M)|)
                  ∈ |r|)⌝⋅) }

1
.....assertion..... 
1. r : CRng
2. n : ℕ
3. ¬(n = 0 ∈ ℤ)
⊢ ∀M:Matrix(n;n;r)
    (|M| = (Σ(r) 0 ≤ i < n. if isEven(i + 0) then M[0,i] else -r M[0,i] fi  * |matrix-minor(0;i;M)|) ∈ |r|)

2
1. r : CRng
2. n : ℕ
3. ¬(n = 0 ∈ ℤ)
4. ∀M:Matrix(n;n;r)
     (|M| = (Σ(r) 0 ≤ i < n. if isEven(i + 0) then M[0,i] else -r M[0,i] fi  * |matrix-minor(0;i;M)|) ∈ |r|)
⊢ ∀M:Matrix(n;n;r). ∀x:ℕn.
    (|M| = (Σ(r) 0 ≤ i < n. if isEven(i + x) then M[x,i] else -r M[x,i] fi  * |matrix-minor(x;i;M)|) ∈ |r|)

---

Latex:

---

Latex:
.....assertion..... 
1.  r  :  CRng
2.  n  :  \mBbbN{}
3.  M  :  Matrix(n;n;r)
4.  \mneg{}(n  =  0)
5.  x  :  \mBbbN{}n@i
6.  y  :  \mBbbN{}n@i
7.  |matrix(if  a=y  then  M[x,b]  else  M[a,b])|  =  (|M|  *  if  x=y  then  1  else  0)
\mvdash{}  \mforall{}M:Matrix(n;n;r).  \mforall{}x:\mBbbN{}n.
        (|M|
        =  (\mSigma{}(r)  0 
                        \mleq{}  i 
                        <  n
                if  isEven(i  +  x)  then  M[x,i]  else  -r  M[x,i]  fi    *  |matrix-minor(x;i;M)|))


By

---

Latex:
(ThinVar  `M'
  THEN  RepeatFor  2  (Thin  (-1))
  THEN  Assert  \mkleeneopen{}\mforall{}M:Matrix(n;n;r)
                                (|M|
                                =  (\mSigma{}(r)  0 
                                                \mleq{}  i 
                                                <  n
                                        if  isEven(i  +  0)  then  M[0,i]  else  -r  M[0,i]  fi    *  |matrix-minor(0;i;M)|))\mkleeneclose{}\mcdot{})

---

Home Index