---

Step * 1 1 of Lemma adj-solution-column

.....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|
BY
{ (EqCDA THEN RepUR ``matrix-minor`` 0 THEN Fold `mx` 0 THEN EqCDA) }

1
.....subterm..... T:t
1:n
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
9. x@0 : ℕn - 1
10. y1 : ℕn - 1
⊢ if if (y1) < (x)  then y1  else (y1 + 1)=x
  then b[if (x@0) < (i)  then x@0  else (x@0 + 1),0]
  else A[if (x@0) < (i)  then x@0  else (x@0 + 1),if (y1) < (x)  then y1  else (y1 + 1)]
= A[if (x@0) < (i)  then x@0  else (x@0 + 1),if (y1) < (x)  then y1  else (y1 + 1)]
∈ |r|

---

Latex:

---

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


By

---

Latex:
(EqCDA  THEN  RepUR  ``matrix-minor``  0  THEN  Fold  `mx`  0  THEN  EqCDA)

---

Home Index