---

Step * of Lemma det-transpose

∀[r:CRng]. ∀[n:ℕ]. ∀[M:Matrix(n;n;r)].  (|M'| = |M| ∈ |r|)
BY
{ (Auto
   THEN (Assert |M|
               = Σ{r} f ∈ map(λf.inv(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 NthHypEqTrans (-1)) }

1
.....assertion..... 
1. r : CRng
2. n : ℕ
3. M : Matrix(n;n;r)
4. |M|
= Σ{r} f ∈ permutations-list(n). let k = Π(r) 0 
                                              ≤ i 
                                              < n
                                          M[i,inv(f) i] in
                                     if permutation-sign(n;inv(f))=1 then k else (-r k)
∈ |r|
⊢ Σ{r} f ∈ permutations-list(n). let k = Π(r) 0 
                                              ≤ i 
                                              < n
                                          M[i,inv(f) i] in
                                     if permutation-sign(n;inv(f))=1 then k else (-r k)
= |M'|
∈ |r|

---

Latex:

---

Latex:
\mforall{}[r:CRng].  \mforall{}[n:\mBbbN{}].  \mforall{}[M:Matrix(n;n;r)].    (|M'|  =  |M|)


By

---

Latex:
(Auto
  THEN  (Assert  |M|
                          =  \mSigma{}\{r\}  f  \mmember{}  map(\mlambda{}f.inv(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  NthHypEqTrans  (-1))

---

Home Index