---

Step * 1 of Lemma sign-inverse


1. n : ℕ
2. f : {p:ℕn ⟶ ℕn| Inj(ℕn;ℕn;p)} 
3. ∀[g:{p:ℕn ⟶ ℕn| Inj(ℕn;ℕn;p)} ]
     (permutation-sign(n;f o g) = (permutation-sign(n;f) * permutation-sign(n;g)) ∈ {s:ℤ| |s| = 1 ∈ ℤ} )
4. permutation-sign(n;f o inv(f)) = (permutation-sign(n;f) * permutation-sign(n;inv(f))) ∈ {s:ℤ| |s| = 1 ∈ ℤ} 
⊢ permutation-sign(n;inv(f)) = permutation-sign(n;f) ∈ {s:ℤ| |s| = 1 ∈ ℤ} 
BY
{ ((Subst' (f o inv(f)) = (λx.x) ∈ (ℕn ⟶ ℕn) -1
    THENA (Auto THEN FunExt THEN Reduce 0 THEN Auto THEN RWO "funinv-property.1" 0 THEN Auto)
    )
   THEN (RWO "permutation-sign-id" (-1) THENA Auto)
   ) }

1
1. n : ℕ
2. f : {p:ℕn ⟶ ℕn| Inj(ℕn;ℕn;p)} 
3. ∀[g:{p:ℕn ⟶ ℕn| Inj(ℕn;ℕn;p)} ]
     (permutation-sign(n;f o g) = (permutation-sign(n;f) * permutation-sign(n;g)) ∈ {s:ℤ| |s| = 1 ∈ ℤ} )
4. 1 = (permutation-sign(n;f) * permutation-sign(n;inv(f))) ∈ {s:ℤ| |s| = 1 ∈ ℤ} 
⊢ permutation-sign(n;inv(f)) = permutation-sign(n;f) ∈ {s:ℤ| |s| = 1 ∈ ℤ} 

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  f  :  \{p:\mBbbN{}n  {}\mrightarrow{}  \mBbbN{}n|  Inj(\mBbbN{}n;\mBbbN{}n;p)\} 
3.  \mforall{}[g:\{p:\mBbbN{}n  {}\mrightarrow{}  \mBbbN{}n|  Inj(\mBbbN{}n;\mBbbN{}n;p)\}  ]
          (permutation-sign(n;f  o  g)  =  (permutation-sign(n;f)  *  permutation-sign(n;g)))
4.  permutation-sign(n;f  o  inv(f))  =  (permutation-sign(n;f)  *  permutation-sign(n;inv(f)))
\mvdash{}  permutation-sign(n;inv(f))  =  permutation-sign(n;f)


By

---

Latex:
((Subst'  (f  o  inv(f))  =  (\mlambda{}x.x)  -1
    THENA  (Auto  THEN  FunExt  THEN  Reduce  0  THEN  Auto  THEN  RWO  "funinv-property.1"  0  THEN  Auto)
    )
  THEN  (RWO  "permutation-sign-id"  (-1)  THENA  Auto)
  )

---

Home Index