---

Step * 1 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;matrix(if y=x then b[x@0,0] else A[x@0,y]))|)
∈ |r|
BY
{ (Subst' |matrix-minor(i;x;matrix(if y=x then b[x@0,0] else A[x@0,y]))| = |matrix-minor(i;x;A)| ∈ |r| 0 THENA Auto) }

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

2
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|

---

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


By

---

Latex:
(Subst'  |matrix-minor(i;x;matrix(if  y=x  then  b[x@0,0]  else  A[x@0,y]))|  =  |matrix-minor(i;x;A)|  0
  THENA  Auto
  )

---

Home Index