Theorem psgnvali

Description: A finitary permutation has at least one representation for its parity. (Contributed by Stefan O'Rear, 28-Aug-2015)

	Ref	Expression
Hypotheses	psgnval.g	⊢ 𝐺 = ( SymGrp ‘ 𝐷 )
	psgnval.t	⊢ 𝑇 = ran ( pmTrsp ‘ 𝐷 )
	psgnval.n	⊢ 𝑁 = ( pmSgn ‘ 𝐷 )
Assertion	psgnvali	⊢ ( 𝑃 ∈ dom 𝑁 → ∃ 𝑤 ∈ Word 𝑇 ( 𝑃 = ( 𝐺 Σg 𝑤 ) ∧ ( 𝑁 ‘ 𝑃 ) = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		psgnval.g	⊢ 𝐺 = ( SymGrp ‘ 𝐷 )
2		psgnval.t	⊢ 𝑇 = ran ( pmTrsp ‘ 𝐷 )
3		psgnval.n	⊢ 𝑁 = ( pmSgn ‘ 𝐷 )
4	1 2 3	psgnval	⊢ ( 𝑃 ∈ dom 𝑁 → ( 𝑁 ‘ 𝑃 ) = ( ℩ 𝑠 ∃ 𝑤 ∈ Word 𝑇 ( 𝑃 = ( 𝐺 Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ) )
5	1 2 3	psgneu	⊢ ( 𝑃 ∈ dom 𝑁 → ∃! 𝑠 ∃ 𝑤 ∈ Word 𝑇 ( 𝑃 = ( 𝐺 Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) )
6		iotacl	⊢ ( ∃! 𝑠 ∃ 𝑤 ∈ Word 𝑇 ( 𝑃 = ( 𝐺 Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) → ( ℩ 𝑠 ∃ 𝑤 ∈ Word 𝑇 ( 𝑃 = ( 𝐺 Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ) ∈ { 𝑠 ∣ ∃ 𝑤 ∈ Word 𝑇 ( 𝑃 = ( 𝐺 Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) } )
7	5 6	syl	⊢ ( 𝑃 ∈ dom 𝑁 → ( ℩ 𝑠 ∃ 𝑤 ∈ Word 𝑇 ( 𝑃 = ( 𝐺 Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ) ∈ { 𝑠 ∣ ∃ 𝑤 ∈ Word 𝑇 ( 𝑃 = ( 𝐺 Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) } )
8	4 7	eqeltrd	⊢ ( 𝑃 ∈ dom 𝑁 → ( 𝑁 ‘ 𝑃 ) ∈ { 𝑠 ∣ ∃ 𝑤 ∈ Word 𝑇 ( 𝑃 = ( 𝐺 Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) } )
9		fvex	⊢ ( 𝑁 ‘ 𝑃 ) ∈ V
10		eqeq1	⊢ ( 𝑠 = ( 𝑁 ‘ 𝑃 ) → ( 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ↔ ( 𝑁 ‘ 𝑃 ) = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) )
11	10	anbi2d	⊢ ( 𝑠 = ( 𝑁 ‘ 𝑃 ) → ( ( 𝑃 = ( 𝐺 Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ↔ ( 𝑃 = ( 𝐺 Σg 𝑤 ) ∧ ( 𝑁 ‘ 𝑃 ) = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ) )
12	11	rexbidv	⊢ ( 𝑠 = ( 𝑁 ‘ 𝑃 ) → ( ∃ 𝑤 ∈ Word 𝑇 ( 𝑃 = ( 𝐺 Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ↔ ∃ 𝑤 ∈ Word 𝑇 ( 𝑃 = ( 𝐺 Σg 𝑤 ) ∧ ( 𝑁 ‘ 𝑃 ) = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ) )
13	9 12	elab	⊢ ( ( 𝑁 ‘ 𝑃 ) ∈ { 𝑠 ∣ ∃ 𝑤 ∈ Word 𝑇 ( 𝑃 = ( 𝐺 Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) } ↔ ∃ 𝑤 ∈ Word 𝑇 ( 𝑃 = ( 𝐺 Σg 𝑤 ) ∧ ( 𝑁 ‘ 𝑃 ) = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) )
14	8 13	sylib	⊢ ( 𝑃 ∈ dom 𝑁 → ∃ 𝑤 ∈ Word 𝑇 ( 𝑃 = ( 𝐺 Σg 𝑤 ) ∧ ( 𝑁 ‘ 𝑃 ) = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) )