---

Step * of Lemma adj-solution-column

∀[r:CRng]. ∀[n:ℕ]. ∀[A:Matrix(n;n;r)]. ∀[c:|r|]. ∀[b:Column(n;r)].
  (adj-solution(r;n;A;c;b) = c*matrix(|matrix(if y=j then b[x,0] else A[x,y])|) ∈ Column(n;r))
BY
{ (Auto
   THEN Unfold `adj-solution` 0
   THEN EqCDA
   THEN Unfold `matrix-times` 0
   THEN EqCDA
   THEN RepUR ``adjugate`` 0
   THEN (InstLemma `expand-det-by-column` [⌜n⌝;⌜x⌝]⋅ THENA Auto)
   THEN (RW (AddrC [3] (HypC (-1))) 0 THENA Auto)
   THEN Thin (-1)
   THEN EqCDA
   THEN (Reduce 0 THENA Auto)) }

1
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;matrix(if y=x then b[x@0,0] else A[x@0,y]))|)
∈ |r|

---

Latex:

---

Latex:
\mforall{}[r:CRng].  \mforall{}[n:\mBbbN{}].  \mforall{}[A:Matrix(n;n;r)].  \mforall{}[c:|r|].  \mforall{}[b:Column(n;r)].
    (adj-solution(r;n;A;c;b)  =  c*matrix(|matrix(if  y=j  then  b[x,0]  else  A[x,y])|))


By

---

Latex:
(Auto
  THEN  Unfold  `adj-solution`  0
  THEN  EqCDA
  THEN  Unfold  `matrix-times`  0
  THEN  EqCDA
  THEN  RepUR  ``adjugate``  0
  THEN  (InstLemma  `expand-det-by-column`  [\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (RW  (AddrC  [3]  (HypC  (-1)))  0  THENA  Auto)
  THEN  Thin  (-1)
  THEN  EqCDA
  THEN  (Reduce  0  THENA  Auto))

---

Home Index