---

Step * of Lemma det-swap-cols

∀[r:CRng]. ∀[n:ℕ]. ∀[M:Matrix(n;n;r)]. ∀[i,j:ℕn].  |matrix-swap-cols(M;i;j)| = (-r |M|) ∈ |r| supposing ¬(i = j ∈ ℤ)
BY
{ (Auto
   THEN (Assert |M|
               = Σ{r} f ∈ map(λf.((i, j) o f);permutations-list(n)). let k = Π(r) 0 
                                                                                  ≤ i 
                                                                                  < n
                                                                              M[i,f i] in
                                                                         if permutation-sign(n;f)=1 then k else (-r k)
               ∈ |r| BY
               (Unfold `matrix-det` 0
                THEN (InstLemma `rng_lsum_functionality_wrt_permutation` [⌜r⌝;⌜{p:ℕn ⟶ ℕn| Inj(ℕn;ℕn;p)} ⌝]⋅ THENA Auto\000C)
                THEN BHyp -1 
                THEN Auto))
   THEN (RWO "rng_lsum_map" (-1) THENA Auto)
   THEN Reduce -1
   THEN (RWO "-1" 0 THENA Auto)
   THEN Thin (-1)
   THEN (RWO "rng_minus_lsum" 0 THENA Auto)
   THEN Unfold `matrix-det` 0
   THEN EqCDA) }

1
.....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|

---

Latex:

---

Latex:
\mforall{}[r:CRng].  \mforall{}[n:\mBbbN{}].  \mforall{}[M:Matrix(n;n;r)].  \mforall{}[i,j:\mBbbN{}n].
    |matrix-swap-cols(M;i;j)|  =  (-r  |M|)  supposing  \mneg{}(i  =  j)


By

---

Latex:
(Auto
  THEN  (Assert  |M|
                          =  \mSigma{}\{r\}  f  \mmember{}  map(\mlambda{}f.((i,  j)  o  f);permutations-list(n)).  let  k  =  \mPi{}(r)  0 
                                                                                                                                                                \mleq{}  i 
                                                                                                                                                                <  n
                                                                                                                                                        M[i,f  i]  in
                                                                                                                                              if  permutation-sign(n;f)=1
                                                                                                                                              then  k
                                                                                                                                              else  (-r  k)  BY
                          (Unfold  `matrix-det`  0
                            THEN  (InstLemma  `rng\_lsum\_functionality\_wrt\_permutation`  [\mkleeneopen{}r\mkleeneclose{};\mkleeneopen{}\{p:\mBbbN{}n  {}\mrightarrow{}  \mBbbN{}n| 
                                                                                                                                                            Inj(\mBbbN{}n;\mBbbN{}n;p)\}  \mkleeneclose{}]\mcdot{}
                                        THENA  Auto
                                        )
                            THEN  BHyp  -1 
                            THEN  Auto))
  THEN  (RWO  "rng\_lsum\_map"  (-1)  THENA  Auto)
  THEN  Reduce  -1
  THEN  (RWO  "-1"  0  THENA  Auto)
  THEN  Thin  (-1)
  THEN  (RWO  "rng\_minus\_lsum"  0  THENA  Auto)
  THEN  Unfold  `matrix-det`  0
  THEN  EqCDA)

---

Home Index