---

Step * 1 1 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|
13. v2 : ℤ
14. |v2| = 1 ∈ ℤ
15. 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|
BY
{ ((RWO "absval_cases" (-2) THENA Auto) THEN D -2 THEN HypSubst' (-2)0 THEN Reduce 0 THEN Auto) }

---

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
13.  v2  :  \mBbbZ{}
14.  |v2|  =  1
15.  permutation-sign(n;f)  =  v2
\mvdash{}  if  v2=1  then  v  else  (-r  v)  =  (-r  if  (-1)  *  v2=1  then  v1  else  (-r  v1))


By

---

Latex:
((RWO  "absval\_cases"  (-2)  THENA  Auto)  THEN  D  -2  THEN  HypSubst'  (-2)0  THEN  Reduce  0  THEN  Auto)

---

Home Index