---

Step * 1 of Lemma det-swap-cols

.....subterm..... T:t
3:n
1. r : CRng
2. n : ℕ
3. M : Matrix(n;n;r)
4. i : ℕn
5. j : ℕn
6. ¬(i = j ∈ ℤ)
7. f : ℕn →⟶ ℕn
⊢ let k = Π(r) 0 
               ≤ i@0 
               < n
           matrix-swap-cols(M;i;j)[i@0,f i@0] in
      if permutation-sign(n;f)=1 then k else (-r k)
= (-r let k = Π(r) 0 ≤ i@0 < n. M[i@0,(i, j) (f i@0)] in if permutation-sign(n;(i, j) o f)=1 then k else (-r k))
∈ |r|
BY
{ (Assert (Π(r) 0 ≤ i@0 < n. matrix-swap-cols(M;i;j)[i@0,f i@0]) = (Π(r) 0 ≤ i@0 < n. M[i@0,(i, j) (f i@0)]) ∈ |r| BY
         (EqCDA
          THEN RepUR ``matrix-swap-cols mx matrix-ap`` 0
          THEN Fold `matrix-ap` 0
          THEN EqCDA
          THEN RepUR ``flip`` 0
          THEN AutoSplit)) }

1
1. r : CRng
2. n : ℕ
3. M : Matrix(n;n;r)
4. i : ℕn
5. j : ℕn
6. ¬(i = j ∈ ℤ)
7. f : ℕn →⟶ ℕn
8. (Π(r) 0 ≤ i@0 < n. matrix-swap-cols(M;i;j)[i@0,f i@0]) = (Π(r) 0 ≤ i@0 < n. M[i@0,(i, j) (f i@0)]) ∈ |r|
⊢ let k = Π(r) 0 
               ≤ i@0 
               < n
           matrix-swap-cols(M;i;j)[i@0,f i@0] in
      if permutation-sign(n;f)=1 then k else (-r k)
= (-r let k = Π(r) 0 ≤ i@0 < n. M[i@0,(i, j) (f i@0)] in if permutation-sign(n;(i, j) o f)=1 then k else (-r k))
∈ |r|

---

Latex:

---

Latex:
.....subterm.....  T:t
3:n
1.  r  :  CRng
2.  n  :  \mBbbN{}
3.  M  :  Matrix(n;n;r)
4.  i  :  \mBbbN{}n
5.  j  :  \mBbbN{}n
6.  \mneg{}(i  =  j)
7.  f  :  \mBbbN{}n  \mrightarrow{}{}\mrightarrow{}  \mBbbN{}n
\mvdash{}  let  k  =  \mPi{}(r)  0 
                              \mleq{}  i@0 
                              <  n
                      matrix-swap-cols(M;i;j)[i@0,f  i@0]  in
            if  permutation-sign(n;f)=1  then  k  else  (-r  k)
=  (-r 
      let  k  =  \mPi{}(r)  0 
                                \mleq{}  i@0 
                                <  n
                        M[i@0,(i,  j)  (f  i@0)]  in
              if  permutation-sign(n;(i,  j)  o  f)=1  then  k  else  (-r  k))


By

---

Latex:
(Assert  (\mPi{}(r)  0 
                            \mleq{}  i@0 
                            <  n
                    matrix-swap-cols(M;i;j)[i@0,f  i@0])
              =  (\mPi{}(r)  0 
                              \mleq{}  i@0 
                              <  n
                      M[i@0,(i,  j)  (f  i@0)])  BY
              (EqCDA
                THEN  RepUR  ``matrix-swap-cols  mx  matrix-ap``  0
                THEN  Fold  `matrix-ap`  0
                THEN  EqCDA
                THEN  RepUR  ``flip``  0
                THEN  AutoSplit))

---

Home Index