---

Step * 2 1 2 2 1 1 1 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 ∈ ℤ)
8. |matrix-swap-rows(M;0;x)| = (-r |M|) ∈ |r|
9. (-r |matrix-swap-rows(M;0;x)|) = |M| ∈ |r|
10. i : ℕn@i
⊢ (-r 
   (if isEven(i + 0) then M[x,i] else -r M[x,i] fi  
    * 
    if isOdd(x) then |matrix-minor(x;i;M)| else -r |matrix-minor(x;i;M)| fi ))
= (if isEven(i + x) then M[x,i] else -r M[x,i] fi  * |matrix-minor(x;i;M)|)
∈ |r|
BY
{ ((Subst' i + 0 ~ i 0 THENA Auto)
   THEN (BoolCase ⌜isEven(i + x)⌝⋅ THENA Auto)
   THEN (RWO "isEven-add" (-1) THENA Auto)
   THEN MoveToConcl (-1)
   THEN Unfold `same-parity` 0
   THEN (BoolCase ⌜isEven(i)⌝⋅ THENA Auto)
   THEN (D 0 THENA Auto)
   THEN Try ((((FLemma `even-implies` [-1] THENA Auto) ORELSE (FLemma `odd-implies` [-1] THENA Auto))
              THEN AutoSplit
              THEN RW RngNormC 0
              THEN Auto))
   THEN (InstLemma `odd-or-even` [⌜x⌝]⋅ THENA Auto)
   THEN (RW assert_pushdownC (-1) THENA Auto)
   THEN D -1
   THEN Try (Trivial)
   THEN AutoSplit) }

---

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)
8.  |matrix-swap-rows(M;0;x)|  =  (-r  |M|)
9.  (-r  |matrix-swap-rows(M;0;x)|)  =  |M|
10.  i  :  \mBbbN{}n@i
\mvdash{}  (-r 
      (if  isEven(i  +  0)  then  M[x,i]  else  -r  M[x,i]  fi   
        * 
        if  isOdd(x)  then  |matrix-minor(x;i;M)|  else  -r  |matrix-minor(x;i;M)|  fi  ))
=  (if  isEven(i  +  x)  then  M[x,i]  else  -r  M[x,i]  fi    *  |matrix-minor(x;i;M)|)


By

---

Latex:
((Subst'  i  +  0  \msim{}  i  0  THENA  Auto)
  THEN  (BoolCase  \mkleeneopen{}isEven(i  +  x)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (RWO  "isEven-add"  (-1)  THENA  Auto)
  THEN  MoveToConcl  (-1)
  THEN  Unfold  `same-parity`  0
  THEN  (BoolCase  \mkleeneopen{}isEven(i)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (D  0  THENA  Auto)
  THEN  Try  ((((FLemma  `even-implies`  [-1]  THENA  Auto)  ORELSE  (FLemma  `odd-implies`  [-1]  THENA  Auto))
                        THEN  AutoSplit
                        THEN  RW  RngNormC  0
                        THEN  Auto))
  THEN  (InstLemma  `odd-or-even`  [\mkleeneopen{}x\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (RW  assert\_pushdownC  (-1)  THENA  Auto)
  THEN  D  -1
  THEN  Try  (Trivial)
  THEN  AutoSplit)

---

Home Index