---

Step * 2 1 2 2 of Lemma adjugate-property


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|)
5. M : Matrix(n;n;r)@i
6. x : ℕn@i
7. ¬(x = 0 ∈ ℤ)
⊢ |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
{ ((InstLemma `det-swap-rows` [⌜r⌝;⌜n⌝;⌜M⌝;⌜0⌝;⌜x⌝]⋅ THENA Auto)
   THEN (ApFunToHypEquands `Z' ⌜-r Z⌝ ⌜|r|⌝ (-1)⋅ THENA Auto)
   THEN (RW  RngNormC  (-1) THENA Auto)
   THEN NthHypEqTrans (-1)) }

1
.....assertion..... 
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|)
5. M : Matrix(n;n;r)@i
6. x : ℕn@i
7. ¬(x = 0 ∈ ℤ)
8. |matrix-swap-rows(M;0;x)| = (-r |M|) ∈ |r|
9. (-r |matrix-swap-rows(M;0;x)|) = |M| ∈ |r|
⊢ (-r |matrix-swap-rows(M;0;x)|)
= (Σ(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:

1.  r  :  CRng
2.  n  :  \mBbbN{}
3.  \mneg{}(n  =  0)
4.  \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)|))
5.  M  :  Matrix(n;n;r)@i
6.  x  :  \mBbbN{}n@i
7.  \mneg{}(x  =  0)
\mvdash{}  |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:
((InstLemma  `det-swap-rows`  [\mkleeneopen{}r\mkleeneclose{};\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}M\mkleeneclose{};\mkleeneopen{}0\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (ApFunToHypEquands  `Z'  \mkleeneopen{}-r  Z\mkleeneclose{}  \mkleeneopen{}|r|\mkleeneclose{}  (-1)\mcdot{}  THENA  Auto)
  THEN  (RW    RngNormC    (-1)  THENA  Auto)
  THEN  NthHypEqTrans  (-1))

---

Home Index