---

Step * 2 1 2 2 1 1 1 1 of Lemma adjugate-property

.....equality..... 
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
⊢ |matrix-minor(0;i;matrix(M[if x@0=0 then x else if x@0=x then 0 else x@0,y]))|
= if isOdd(x) then |matrix-minor(x;i;M)| else -r |matrix-minor(x;i;M)| fi 
∈ |r|
BY
{ ((Assert ⌜∀d:ℕ. ∀b:ℕn. ∀a:ℕb.
              (((b - a) ≤ (d + 1))
              ⇒ (|matrix-minor(a;i;matrix(M[if x=a then b else if x=b then a else x,y]))|
                 = if isOdd(b - a) then |matrix-minor(b;i;M)| else -r |matrix-minor(b;i;M)| fi 
                 ∈ |r|))⌝⋅
   THENM ((InstHyp [⌜x⌝;⌜x⌝;⌜0⌝] (-1)⋅ THENA Auto) THEN Subst' x - 0 ~ x -1 THEN Auto)
   )
   THEN ThinVar `x'
   THEN Thin (-3)
   THEN InductionOnNat
   THEN Auto) }

1
1. r : CRng
2. n : ℕ
3. ¬(n = 0 ∈ ℤ)
4. M : Matrix(n;n;r)@i
5. i : ℕn@i
6. d : ℤ
7. b : ℕn@i
8. a : ℕb@i
9. (b - a) ≤ (0 + 1)
⊢ |matrix-minor(a;i;matrix(M[if x=a then b else if x=b then a else x,y]))|
= if isOdd(b - a) then |matrix-minor(b;i;M)| else -r |matrix-minor(b;i;M)| fi 
∈ |r|

2
1. r : CRng
2. n : ℕ
3. ¬(n = 0 ∈ ℤ)
4. M : Matrix(n;n;r)@i
5. i : ℕn@i
6. d : ℤ
7. 0 < d
8. ∀b:ℕn. ∀a:ℕb.
     (((b - a) ≤ ((d - 1) + 1))
     ⇒ (|matrix-minor(a;i;matrix(M[if x=a then b else if x=b then a else x,y]))|
        = if isOdd(b - a) then |matrix-minor(b;i;M)| else -r |matrix-minor(b;i;M)| fi 
        ∈ |r|))
9. b : ℕn@i
10. a : ℕb@i
11. (b - a) ≤ (d + 1)
⊢ |matrix-minor(a;i;matrix(M[if x=a then b else if x=b then a else x,y]))|
= if isOdd(b - a) then |matrix-minor(b;i;M)| else -r |matrix-minor(b;i;M)| fi 
∈ |r|

---

Latex:

---

Latex:
.....equality..... 
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{}  |matrix-minor(0;i;matrix(M[if  x@0=0  then  x  else  if  x@0=x  then  0  else  x@0,y]))|
=  if  isOdd(x)  then  |matrix-minor(x;i;M)|  else  -r  |matrix-minor(x;i;M)|  fi 


By

---

Latex:
((Assert  \mkleeneopen{}\mforall{}d:\mBbbN{}.  \mforall{}b:\mBbbN{}n.  \mforall{}a:\mBbbN{}b.
                        (((b  -  a)  \mleq{}  (d  +  1))
                        {}\mRightarrow{}  (|matrix-minor(a;i;matrix(M[if  x=a  then  b  else  if  x=b  then  a  else  x,y]))|
                              =  if  isOdd(b  -  a)  then  |matrix-minor(b;i;M)|  else  -r  |matrix-minor(b;i;M)|  fi  ))\mkleeneclose{}\mcdot{}
  THENM  ((InstHyp  [\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}0\mkleeneclose{}]  (-1)\mcdot{}  THENA  Auto)  THEN  Subst'  x  -  0  \msim{}  x  -1  THEN  Auto)
  )
  THEN  ThinVar  `x'
  THEN  Thin  (-3)
  THEN  InductionOnNat
  THEN  Auto)

---

Home Index