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