---

Step * 1 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. 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 ∈ ℤ} 
BY
{ (MoveToConcl (-1)
   THEN GenConclTerms Auto [⌜permutation-sign(n;f)⌝;⌜permutation-sign(n;inv(f))⌝]⋅
   THEN All Thin
   THEN Auto
   THEN DSetVars) }

1
1. v : ℤ
2. |v| = 1 ∈ ℤ
3. v1 : ℤ
4. |v1| = 1 ∈ ℤ
5. 1 = (v * v1) ∈ {s:ℤ| |s| = 1 ∈ ℤ} 
⊢ v1 = v ∈ {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.  1  =  (permutation-sign(n;f)  *  permutation-sign(n;inv(f)))
\mvdash{}  permutation-sign(n;inv(f))  =  permutation-sign(n;f)


By

---

Latex:
(MoveToConcl  (-1)
  THEN  GenConclTerms  Auto  [\mkleeneopen{}permutation-sign(n;f)\mkleeneclose{};\mkleeneopen{}permutation-sign(n;inv(f))\mkleeneclose{}]\mcdot{}
  THEN  All  Thin
  THEN  Auto
  THEN  DSetVars)

---

Home Index