---

Step * 1 2 of Lemma adj-solution-column


1. r : CRng
2. n : ℕ
3. A : Matrix(n;n;r)
4. c : |r|
5. b : Column(n;r)
6. x : ℕn
7. y : ℕ1
8. i : ℕn
⊢ (if isEven(x + i) then |matrix-minor(i;x;A)| else -r |matrix-minor(i;x;A)| fi  * b[i,y])
= (if isEven(i + x) then b[i,0] else -r b[i,0] fi  * |matrix-minor(i;x;A)|)
∈ |r|
BY
{ ((Subst' x + i ~ i + x 0 THENA Auto) THEN (CaseNat 0 `y' THENL [AutoSplit; Auto])) }

---

Latex:

---

Latex:

1.  r  :  CRng
2.  n  :  \mBbbN{}
3.  A  :  Matrix(n;n;r)
4.  c  :  |r|
5.  b  :  Column(n;r)
6.  x  :  \mBbbN{}n
7.  y  :  \mBbbN{}1
8.  i  :  \mBbbN{}n
\mvdash{}  (if  isEven(x  +  i)  then  |matrix-minor(i;x;A)|  else  -r  |matrix-minor(i;x;A)|  fi    *  b[i,y])
=  (if  isEven(i  +  x)  then  b[i,0]  else  -r  b[i,0]  fi    *  |matrix-minor(i;x;A)|)


By

---

Latex:
((Subst'  x  +  i  \msim{}  i  +  x  0  THENA  Auto)  THEN  (CaseNat  0  `y'  THENL  [AutoSplit;  Auto]))

---

Home Index