---

Step * 1 1 2 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)
8. Σ{r} x ∈ map(λf.(f o (i, j));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} x ∈ filter(λa.(¬b(permutation-sign(n;a) =z 1));permutations-list(n)). let k = Π(r) 0 
                                                                                          ≤ i@0 
                                                                                          < n
                                                                                      M[i@0,(λf.(f o (i, j))) x i@0] in
                                                                                 if permutation-sign(n;(λf.(f
                                                                                                            o (i, j))) 
                                                                                                       x)=1
                                                                                 then k
                                                                                 else (-r k)
∈ |r|
⊢ Σ{r} x ∈ filter(λa.(¬b(permutation-sign(n;a) =z 1));permutations-list(n)). (-r 
                                                                              let k = Π(r) 0 
                                                                                           ≤ i 
                                                                                           < n
                                                                                       M[i,x i] in
                                                                                  if permutation-sign(n;x)=1
                                                                                  then k
                                                                                  else (-r k))
= Σ{r} x ∈ filter(λa.(¬b(permutation-sign(n;a) =z 1));permutations-list(n)). let k = Π(r) 0 
                                                                                          ≤ i@0 
                                                                                          < n
                                                                                      M[i@0,(λf.(f o (i, j))) x i@0] in
                                                                                 if permutation-sign(n;(λf.(f
                                                                                                            o (i, j))) 
                                                                                                       x)=1
                                                                                 then k
                                                                                 else (-r k)
∈ |r|
BY
{ Assert ⌜filter(λa.(¬b(permutation-sign(n;a) =z 1));permutations-list(n)) ∈ {p:ℕn ⟶ ℕn| Inj(ℕn;ℕn;p)}  List⌝⋅ }

1
.....assertion..... 
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)
8. Σ{r} x ∈ map(λf.(f o (i, j));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} x ∈ filter(λa.(¬b(permutation-sign(n;a) =z 1));permutations-list(n)). let k = Π(r) 0 
                                                                                          ≤ i@0 
                                                                                          < n
                                                                                      M[i@0,(λf.(f o (i, j))) x i@0] in
                                                                                 if permutation-sign(n;(λf.(f
                                                                                                            o (i, j))) 
                                                                                                       x)=1
                                                                                 then k
                                                                                 else (-r k)
∈ |r|
⊢ filter(λa.(¬b(permutation-sign(n;a) =z 1));permutations-list(n)) ∈ {p:ℕn ⟶ ℕn| Inj(ℕn;ℕn;p)}  List

2
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)
8. Σ{r} x ∈ map(λf.(f o (i, j));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} x ∈ filter(λa.(¬b(permutation-sign(n;a) =z 1));permutations-list(n)). let k = Π(r) 0 
                                                                                          ≤ i@0 
                                                                                          < n
                                                                                      M[i@0,(λf.(f o (i, j))) x i@0] in
                                                                                 if permutation-sign(n;(λf.(f
                                                                                                            o (i, j))) 
                                                                                                       x)=1
                                                                                 then k
                                                                                 else (-r k)
∈ |r|
9. filter(λa.(¬b(permutation-sign(n;a) =z 1));permutations-list(n)) ∈ {p:ℕn ⟶ ℕn| Inj(ℕn;ℕn;p)}  List
⊢ Σ{r} x ∈ filter(λa.(¬b(permutation-sign(n;a) =z 1));permutations-list(n)). (-r 
                                                                              let k = Π(r) 0 
                                                                                           ≤ i 
                                                                                           < n
                                                                                       M[i,x i] in
                                                                                  if permutation-sign(n;x)=1
                                                                                  then k
                                                                                  else (-r k))
= Σ{r} x ∈ filter(λa.(¬b(permutation-sign(n;a) =z 1));permutations-list(n)). let k = Π(r) 0 
                                                                                          ≤ i@0 
                                                                                          < n
                                                                                      M[i@0,(λf.(f o (i, j))) x i@0] in
                                                                                 if permutation-sign(n;(λf.(f
                                                                                                            o (i, j))) 
                                                                                                       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
8.  \mSigma{}\{r\}  x  \mmember{}  map(\mlambda{}f.(f  o  (i,  j));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)
=  \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@0 
                                                                                                            <  n
                                                                                                    M[i@0,(\mlambda{}f.(f  o  (i,  j)))  x  i@0]  in
                                                                                          if  permutation-sign(n;(\mlambda{}f.(f  o  (i,  j)))  x)=1
                                                                                          then  k
                                                                                          else  (-r  k)
\mvdash{}  \mSigma{}\{r\}  x  \mmember{}  filter(\mlambda{}a.(\mneg{}\msubb{}(permutation-sign(n;a)  =\msubz{}  1));
                                    permutations-list(n)).  (-r 
                                                                                    let  k  =  \mPi{}(r)  0 
                                                                                                              \mleq{}  i 
                                                                                                              <  n
                                                                                                      M[i,x  i]  in
                                                                                            if  permutation-sign(n;x)=1  then  k  else  (-r  k))
=  \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@0 
                                                                                                            <  n
                                                                                                    M[i@0,(\mlambda{}f.(f  o  (i,  j)))  x  i@0]  in
                                                                                          if  permutation-sign(n;(\mlambda{}f.(f  o  (i,  j)))  x)=1
                                                                                          then  k
                                                                                          else  (-r  k)


By

---

Latex:
Assert  \mkleeneopen{}filter(\mlambda{}a.(\mneg{}\msubb{}(permutation-sign(n;a)  =\msubz{}  1));permutations-list(n))  \mmember{}  \{p:\mBbbN{}n  {}\mrightarrow{}  \mBbbN{}n| 
                                                                                                                                                        Inj(\mBbbN{}n;\mBbbN{}n;p)\}    List\mkleeneclose{}\mcdot{}

---

Home Index