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 ↑ ( ♯ ‘ 𝑤 ) ) ) )