---

Step * 1 of Lemma det-equal-rows


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|
BY
{ ((Subst' Σ{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))
    ∈ |r| 0
    THENA Auto
    )
THENM (RW RngNormC 0 THEN Auto)
) }

1
.....equality..... 
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))
∈ |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.  matrix-swap-rows(M;i;j)  =  M
\mvdash{}  (\mSigma{}\{r\}  x  \mmember{}  filter(\mlambda{}f.(permutation-sign(n;f)  =\msubz{}  1);
                                      permutations-list(n)).  let  k  =  \mPi{}(r)  0 
                                                                                                              \mleq{}  i 
                                                                                                              <  n
                                                                                                      M[i,x  i]  in
                                                                                            if  permutation-sign(n;x)=1  then  k  else  (-r  k) 
      +r 
      \mSigma{}\{r\}  x  \mmember{}  filter(\mlambda{}a.(\mneg{}\msubb{}(permutation-sign(n;a)  =\msubz{}  1));
                                      permutations-list(n)).  let  k  =  \mPi{}(r)  0 
                                                                                                              \mleq{}  i 
                                                                                                              <  n
                                                                                                      M[i,x  i]  in
                                                                                            if  permutation-sign(n;x)=1  then  k  else  (-r  k))
=  0


By

---

Latex:
((Subst'  \mSigma{}\{r\}  x  \mmember{}  filter(\mlambda{}f.(permutation-sign(n;f)  =\msubz{}  1);
                                                  permutations-list(n)).  let  k  =  \mPi{}(r)  0 
                                                                                                                          \mleq{}  i 
                                                                                                                          <  n
                                                                                                                  M[i,x  i]  in
                                                                                                        if  permutation-sign(n;x)=1  then  k  else  (-r  k)
    =  (-r 
          \mSigma{}\{r\}  x  \mmember{}  filter(\mlambda{}a.(\mneg{}\msubb{}(permutation-sign(n;a)  =\msubz{}  1));
                                          permutations-list(n)).  let  k  =  \mPi{}(r)  0 
                                                                                                                  \mleq{}  i 
                                                                                                                  <  n
                                                                                                          M[i,x  i]  in
                                                                                                if  permutation-sign(n;x)=1  then  k  else  (-r  k))  0
    THENA  Auto
    )
THENM  (RW  RngNormC  0  THEN  Auto)
)

---

Home Index