---

Step * of Lemma permutation-sign-compose

∀[n:ℕ]. ∀[f,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 ∈ ℤ} )
BY
{ (Intros
   THEN (RepeatFor 2 (MoveToConcl (-1))
         THEN (Assert ∀x,y:{s:ℤ| |s| = 1 ∈ ℤ} .  (x * y ∈ {s:ℤ| |s| = 1 ∈ ℤ} ) BY
                     (Auto
                      THEN D -2
                      THEN D -1
                      THEN MemTypeCD
                      THEN Auto
                      THEN (RWO  "absval_mul" 0 THEN Auto)
                      THEN RWO "-3 -1" 0
                      THEN Auto))
         )
   THEN InstLemma `permutation-generators3` [⌜n⌝;⌜λ2f.∀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 ∈ ℤ} )⌝]⋅
   THEN Auto) }

1
1. n : ℕ
2. ∀x,y:{s:ℤ| |s| = 1 ∈ ℤ} .  (x * y ∈ {s:ℤ| |s| = 1 ∈ ℤ} )
3. g : {p:ℕn ⟶ ℕn| Inj(ℕn;ℕn;p)} 
⊢ permutation-sign(n;(λx.x) o g) = (permutation-sign(n;λx.x) * permutation-sign(n;g)) ∈ {s:ℤ| |s| = 1 ∈ ℤ} 

2
1. n : ℕ
2. ∀x,y:{s:ℤ| |s| = 1 ∈ ℤ} .  (x * y ∈ {s:ℤ| |s| = 1 ∈ ℤ} )
3. f : {f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} 
4. i : ℕn
5. j : ℕn
6. i < j
7. ∀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 ∈ ℤ} )
8. g : {p:ℕn ⟶ ℕn| Inj(ℕn;ℕn;p)} 
⊢ permutation-sign(n;(f o (i, j)) o g) = (permutation-sign(n;f o (i, j)) * permutation-sign(n;g)) ∈ {s:ℤ| |s| = 1 ∈ ℤ} 

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[f,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)))


By

---

Latex:
(Intros
  THEN  (RepeatFor  2  (MoveToConcl  (-1))
              THEN  (Assert  \mforall{}x,y:\{s:\mBbbZ{}|  |s|  =  1\}  .    (x  *  y  \mmember{}  \{s:\mBbbZ{}|  |s|  =  1\}  )  BY
                                      (Auto
                                        THEN  D  -2
                                        THEN  D  -1
                                        THEN  MemTypeCD
                                        THEN  Auto
                                        THEN  (RWO    "absval\_mul"  0  THEN  Auto)
                                        THEN  RWO  "-3  -1"  0
                                        THEN  Auto))
              )
  THEN  InstLemma  `permutation-generators3`  [\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}f.\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)))\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index