---

Step * 1 1 of Lemma det-swap-cols


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|
BY
{ ((MoveToConcl (-1)
    THEN GenConclTerms Auto
          [⌜Π(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)]⌝]⋅
    )
   THEN (D 0 THENA Auto)
   THEN RepUR ``let`` 0) }

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. v : |r|
9. (Π(r) 0 ≤ i@0 < n. matrix-swap-cols(M;i;j)[i@0,f i@0]) = v ∈ |r|
10. v1 : |r|
11. (Π(r) 0 ≤ i@0 < n. M[i@0,(i, j) (f i@0)]) = v1 ∈ |r|
12. v = v1 ∈ |r|
⊢ if permutation-sign(n;f)=1 then v else (-r v) = (-r if permutation-sign(n;(i, j) o f)=1 then v1 else (-r v1)) ∈ |r|

---

Latex:

---

Latex:

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
8.  (\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)])
\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:
((MoveToConcl  (-1)
    THEN  GenConclTerms  Auto
                [\mkleeneopen{}\mPi{}(r)  0 
                              \mleq{}  i@0 
                              <  n
                      matrix-swap-cols(M;i;j)[i@0,f  i@0]\mkleeneclose{};\mkleeneopen{}\mPi{}(r)  0 
                                                                                                          \mleq{}  i@0 
                                                                                                          <  n
                                                                                                  M[i@0,(i,  j)  (f  i@0)]\mkleeneclose{}]\mcdot{}
    )
  THEN  (D  0  THENA  Auto)
  THEN  RepUR  ``let``  0)

---

Home Index