---

Step * 1 1 1 of Lemma det-swap-cols


1. r : CRng
2. n : ℕ
3. M : Matrix(n;n;r)
4. i : ℕn
5. j : ℕn
6. ¬(i = j ∈ ℤ)
7. f : ℕn →⟶ ℕn
8. v : |r|
9. (Π(r) 0 ≤ i@0 < n. matrix-swap-cols(M;i;j)[i@0,f i@0]) = v ∈ |r|
10. v1 : |r|
11. (Π(r) 0 ≤ i@0 < n. M[i@0,(i, j) (f i@0)]) = v1 ∈ |r|
12. v = v1 ∈ |r|
⊢ if permutation-sign(n;f)=1 then v else (-r v) = (-r if permutation-sign(n;(i, j) o f)=1 then v1 else (-r v1)) ∈ |r|
BY
{ ((RWO "permutation-sign-compose" 0 THENA Auto)
   THEN (RWO "sign-flip" 0 THENA Auto)
   THEN (GenConclTerm ⌜permutation-sign(n;f)⌝⋅ THENA Auto)) }

1
1. r : CRng
2. n : ℕ
3. M : Matrix(n;n;r)
4. i : ℕn
5. j : ℕn
6. ¬(i = j ∈ ℤ)
7. f : ℕn →⟶ ℕn
8. v : |r|
9. (Π(r) 0 ≤ i@0 < n. matrix-swap-cols(M;i;j)[i@0,f i@0]) = v ∈ |r|
10. v1 : |r|
11. (Π(r) 0 ≤ i@0 < n. M[i@0,(i, j) (f i@0)]) = v1 ∈ |r|
12. v = v1 ∈ |r|
13. v2 : {s:ℤ| |s| = 1 ∈ ℤ} 
14. permutation-sign(n;f) = v2 ∈ {s:ℤ| |s| = 1 ∈ ℤ} 
⊢ if v2=1 then v else (-r v) = (-r if (-1) * v2=1 then v1 else (-r v1)) ∈ |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.  f  :  \mBbbN{}n  \mrightarrow{}{}\mrightarrow{}  \mBbbN{}n
8.  v  :  |r|
9.  (\mPi{}(r)  0  \mleq{}  i@0  <  n.  matrix-swap-cols(M;i;j)[i@0,f  i@0])  =  v
10.  v1  :  |r|
11.  (\mPi{}(r)  0  \mleq{}  i@0  <  n.  M[i@0,(i,  j)  (f  i@0)])  =  v1
12.  v  =  v1
\mvdash{}  if  permutation-sign(n;f)=1  then  v  else  (-r  v)
=  (-r  if  permutation-sign(n;(i,  j)  o  f)=1  then  v1  else  (-r  v1))


By

---

Latex:
((RWO  "permutation-sign-compose"  0  THENA  Auto)
  THEN  (RWO  "sign-flip"  0  THENA  Auto)
  THEN  (GenConclTerm  \mkleeneopen{}permutation-sign(n;f)\mkleeneclose{}\mcdot{}  THENA  Auto))

---

Home Index