This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem psgnfieu

Description: A permutation of a finite set has exactly one parity. (Contributed by AV, 13-Jan-2019)

Ref Expression
Hypotheses psgnfitr.g ⊢ 𝐺 = ( SymGrp ‘ 𝑁 )
psgnfitr.p ⊢ 𝐵 = ( Base ‘ 𝐺 )
psgnfitr.t ⊢ 𝑇 = ran ( pmTrsp ‘ 𝑁 )
Assertion psgnfieu ( ( 𝑁 ∈ Fin ∧ 𝑄 ∈ 𝐵 ) → ∃! 𝑠 ∃ 𝑤 ∈ Word 𝑇 ( 𝑄 = ( 𝐺 Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) )

Proof

Step Hyp Ref Expression
1 psgnfitr.g ⊢ 𝐺 = ( SymGrp ‘ 𝑁 )
2 psgnfitr.p ⊢ 𝐵 = ( Base ‘ 𝐺 )
3 psgnfitr.t ⊢ 𝑇 = ran ( pmTrsp ‘ 𝑁 )
4 simpr ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑄 ∈ 𝐵 ) → 𝑄 ∈ 𝐵 )
5 1 2 sygbasnfpfi ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑄 ∈ 𝐵 ) → dom ( 𝑄 ∖ I ) ∈ Fin )
6 eqid ⊢ ( pmSgn ‘ 𝑁 ) = ( pmSgn ‘ 𝑁 )
7 1 6 2 psgneldm ⊢ ( 𝑄 ∈ dom ( pmSgn ‘ 𝑁 ) ↔ ( 𝑄 ∈ 𝐵 ∧ dom ( 𝑄 ∖ I ) ∈ Fin ) )
8 4 5 7 sylanbrc ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑄 ∈ 𝐵 ) → 𝑄 ∈ dom ( pmSgn ‘ 𝑁 ) )
9 1 3 6 psgneu ⊢ ( 𝑄 ∈ dom ( pmSgn ‘ 𝑁 ) → ∃! 𝑠 ∃ 𝑤 ∈ Word 𝑇 ( 𝑄 = ( 𝐺 Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) )
10 8 9 syl ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑄 ∈ 𝐵 ) → ∃! 𝑠 ∃ 𝑤 ∈ Word 𝑇 ( 𝑄 = ( 𝐺 Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) )