---

Step * 2 of Lemma expand-det-by-row

.....subterm..... T:t
3:n
1. n : ℕ
2. i : ℕn
3. r : CRng
4. M : Matrix(n;n;r)
5. |M'| = (Σ(r) 0 ≤ i@0 < n. if isEven(i@0 + i) then M'[i@0,i] else -r M'[i@0,i] fi  * |matrix-minor(i@0;i;M')|) ∈ |r|
⊢ (Σ(r) 0 
        ≤ j 
        < n
    if isEven(i + j) then M[i,j] else -r M[i,j] fi  * |matrix-minor(i;j;M)|)
= (Σ(r) 0 
        ≤ i@0 
        < n
    if isEven(i@0 + i) then M'[i@0,i] else -r M'[i@0,i] fi  * |matrix-minor(i@0;i;M')|)
∈ |r|
BY
{ RepeatFor 2 (EqCDA) }

1
.....subterm..... T:t
2:n
1. n : ℕ
2. i : ℕn
3. r : CRng
4. M : Matrix(n;n;r)
5. |M'| = (Σ(r) 0 ≤ i@0 < n. if isEven(i@0 + i) then M'[i@0,i] else -r M'[i@0,i] fi  * |matrix-minor(i@0;i;M')|) ∈ |r|
6. j : ℕn
⊢ if isEven(i + j) then M[i,j] else -r M[i,j] fi  = if isEven(j + i) then M'[j,i] else -r M'[j,i] fi  ∈ |r|

2
.....subterm..... T:t
3:n
1. n : ℕ
2. i : ℕn
3. r : CRng
4. M : Matrix(n;n;r)
5. |M'| = (Σ(r) 0 ≤ i@0 < n. if isEven(i@0 + i) then M'[i@0,i] else -r M'[i@0,i] fi  * |matrix-minor(i@0;i;M')|) ∈ |r|
6. j : ℕn
⊢ |matrix-minor(i;j;M)| = |matrix-minor(j;i;M')| ∈ |r|

---

Latex:

---

Latex:
.....subterm.....  T:t
3:n
1.  n  :  \mBbbN{}
2.  i  :  \mBbbN{}n
3.  r  :  CRng
4.  M  :  Matrix(n;n;r)
5.  |M'|
=  (\mSigma{}(r)  0 
                \mleq{}  i@0 
                <  n
        if  isEven(i@0  +  i)  then  M'[i@0,i]  else  -r  M'[i@0,i]  fi    *  |matrix-minor(i@0;i;M')|)
\mvdash{}  (\mSigma{}(r)  0 
                \mleq{}  j 
                <  n
        if  isEven(i  +  j)  then  M[i,j]  else  -r  M[i,j]  fi    *  |matrix-minor(i;j;M)|)
=  (\mSigma{}(r)  0 
                \mleq{}  i@0 
                <  n
        if  isEven(i@0  +  i)  then  M'[i@0,i]  else  -r  M'[i@0,i]  fi    *  |matrix-minor(i@0;i;M')|)


By

---

Latex:
RepeatFor  2  (EqCDA)

---

Home Index