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

Metamath Proof Explorer

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