---

Step * of Lemma det-equal-rows

∀[r:CRng]. ∀[n:ℕ]. ∀[M:Matrix(n;n;r)]. ∀[i,j:ℕn].
  |M| = 0 ∈ |r| supposing (¬(i = j ∈ ℤ)) ∧ (matrix-swap-rows(M;i;j) = M ∈ Matrix(n;n;r))
BY
{ (Auto
   THEN Unfold `matrix-det` 0
   THEN (InstLemma `rng_lsum-split` [⌜ℕn ⟶ ℕn⌝;⌜λf.(permutation-sign(n;f) =z 1)⌝;⌜r⌝;
         ⌜λ2f.let k = Π(r) 0 
                           ≤ i 
                           < n
                       M[i,f i] in
                  if permutation-sign(n;f)=1 then k else (-r k)⌝;⌜permutations-list(n)⌝]⋅
         THENA Auto
         )
   THEN NthHypEqTrans (-1)
   THEN Thin (-1)
   THEN Reduce 0) }

1
1. r : CRng
2. n : ℕ
3. M : Matrix(n;n;r)
4. i : ℕn
5. j : ℕn
6. ¬(i = j ∈ ℤ)
7. matrix-swap-rows(M;i;j) = M ∈ Matrix(n;n;r)
⊢ (Σ{r} x ∈ filter(λf.(permutation-sign(n;f) =z 1);permutations-list(n)). let k = Π(r) 0 
                                                                                       ≤ i 
                                                                                       < n
                                                                                   M[i,x i] in
                                                                              if permutation-sign(n;x)=1
                                                                              then k
                                                                              else (-r k) 
   +r 
   Σ{r} x ∈ filter(λa.(¬b(permutation-sign(n;a) =z 1));permutations-list(n)). let k = Π(r) 0 
                                                                                           ≤ i 
                                                                                           < n
                                                                                       M[i,x i] in
                                                                                  if permutation-sign(n;x)=1
                                                                                  then k
                                                                                  else (-r k))
= 0
∈ |r|

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  Unfold  `matrix-det`  0
  THEN  (InstLemma  `rng\_lsum-split`  [\mkleeneopen{}\mBbbN{}n  {}\mrightarrow{}  \mBbbN{}n\mkleeneclose{};\mkleeneopen{}\mlambda{}f.(permutation-sign(n;f)  =\msubz{}  1)\mkleeneclose{};\mkleeneopen{}r\mkleeneclose{};
              \mkleeneopen{}\mlambda{}\msubtwo{}f.let  k  =  \mPi{}(r)  0 
                                                  \mleq{}  i 
                                                  <  n
                                          M[i,f  i]  in
                                if  permutation-sign(n;f)=1  then  k  else  (-r  k)\mkleeneclose{};\mkleeneopen{}permutations-list(n)\mkleeneclose{}]\mcdot{}
              THENA  Auto
              )
  THEN  NthHypEqTrans  (-1)
  THEN  Thin  (-1)
  THEN  Reduce  0)

---

Home Index