---

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


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|
BY
{ ((Decide ⌜(b - a) ≤ d⌝⋅ THENA Auto) THENL [(BackThruSomeHyp THEN Auto); (InstHyp [⌜b⌝;⌜a + 1⌝] (-5)⋅ THENA Auto)]) }

1
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)
12. ¬((b - a) ≤ d)
13. |matrix-minor(a + 1;i;matrix(M[if x=a + 1 then b else if x=b then a + 1 else x,y]))|
= if isOdd(b - a + 1) then |matrix-minor(b;i;M)| else -r |matrix-minor(b;i;M)| fi 
∈ |r|
⊢ |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:

1.  r  :  CRng
2.  n  :  \mBbbN{}
3.  \mneg{}(n  =  0)
4.  M  :  Matrix(n;n;r)@i
5.  i  :  \mBbbN{}n@i
6.  d  :  \mBbbZ{}
7.  0  <  d
8.  \mforall{}b:\mBbbN{}n.  \mforall{}a:\mBbbN{}b.
          (((b  -  a)  \mleq{}  ((d  -  1)  +  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  ))
9.  b  :  \mBbbN{}n@i
10.  a  :  \mBbbN{}b@i
11.  (b  -  a)  \mleq{}  (d  +  1)
\mvdash{}  |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 


By

---

Latex:
((Decide  \mkleeneopen{}(b  -  a)  \mleq{}  d\mkleeneclose{}\mcdot{}  THENA  Auto)
  THENL  [(BackThruSomeHyp  THEN  Auto);  (InstHyp  [\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}a  +  1\mkleeneclose{}]  (-5)\mcdot{}  THENA  Auto)]
)

---

Home Index