Metamath Proof Explorer

Theorem psgneu

Description: A finitary permutation has exactly one parity. (Contributed by Stefan O'Rear, 28-Aug-2015)

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

Proof

Step Hyp Ref Expression
1 psgnval.g ⊢ 𝐺 = ( SymGrp ‘ 𝐷 )
2 psgnval.t ⊢ 𝑇 = ran ( pmTrsp ‘ 𝐷 )
3 psgnval.n ⊢ 𝑁 = ( pmSgn ‘ 𝐷 )
4 eqid ⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
5 1 3 4 psgneldm ⊢ ( 𝑃 ∈ dom 𝑁 ↔ ( 𝑃 ∈ ( Base ‘ 𝐺 ) ∧ dom ( 𝑃 ∖ I ) ∈ Fin ) )
6 5 simplbi ⊢ ( 𝑃 ∈ dom 𝑁 → 𝑃 ∈ ( Base ‘ 𝐺 ) )
7 1 4 elbasfv ⊢ ( 𝑃 ∈ ( Base ‘ 𝐺 ) → 𝐷 ∈ V )
8 6 7 syl ⊢ ( 𝑃 ∈ dom 𝑁 → 𝐷 ∈ V )
9 1 2 3 psgneldm2 ⊢ ( 𝐷 ∈ V → ( 𝑃 ∈ dom 𝑁 ↔ ∃ 𝑤 ∈ Word 𝑇 𝑃 = ( 𝐺 Σg 𝑤 ) ) )
10 8 9 syl ⊢ ( 𝑃 ∈ dom 𝑁 → ( 𝑃 ∈ dom 𝑁 ↔ ∃ 𝑤 ∈ Word 𝑇 𝑃 = ( 𝐺 Σg 𝑤 ) ) )
11 10 ibi ⊢ ( 𝑃 ∈ dom 𝑁 → ∃ 𝑤 ∈ Word 𝑇 𝑃 = ( 𝐺 Σg 𝑤 ) )
12 simpr ⊢ ( ( ( 𝑃 ∈ dom 𝑁 ∧ 𝑤 ∈ Word 𝑇 ) ∧ 𝑃 = ( 𝐺 Σg 𝑤 ) ) → 𝑃 = ( 𝐺 Σg 𝑤 ) )
13 eqid ⊢ ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) = ( - 1 ↑ ( ♯ ‘ 𝑤 ) )
14 ovex ⊢ ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ∈ V
15 eqeq1 ⊢ ( 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) → ( 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ↔ ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) )
16 15 anbi2d ⊢ ( 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) → ( ( 𝑃 = ( 𝐺 Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ↔ ( 𝑃 = ( 𝐺 Σg 𝑤 ) ∧ ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ) )
17 14 16 spcev ⊢ ( ( 𝑃 = ( 𝐺 Σg 𝑤 ) ∧ ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) → ∃ 𝑠 ( 𝑃 = ( 𝐺 Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) )
18 12 13 17 sylancl ⊢ ( ( ( 𝑃 ∈ dom 𝑁 ∧ 𝑤 ∈ Word 𝑇 ) ∧ 𝑃 = ( 𝐺 Σg 𝑤 ) ) → ∃ 𝑠 ( 𝑃 = ( 𝐺 Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) )
19 18 ex ⊢ ( ( 𝑃 ∈ dom 𝑁 ∧ 𝑤 ∈ Word 𝑇 ) → ( 𝑃 = ( 𝐺 Σg 𝑤 ) → ∃ 𝑠 ( 𝑃 = ( 𝐺 Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ) )
20 19 reximdva ⊢ ( 𝑃 ∈ dom 𝑁 → ( ∃ 𝑤 ∈ Word 𝑇 𝑃 = ( 𝐺 Σg 𝑤 ) → ∃ 𝑤 ∈ Word 𝑇 ∃ 𝑠 ( 𝑃 = ( 𝐺 Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ) )
21 11 20 mpd ⊢ ( 𝑃 ∈ dom 𝑁 → ∃ 𝑤 ∈ Word 𝑇 ∃ 𝑠 ( 𝑃 = ( 𝐺 Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) )
22 rexcom4 ⊢ ( ∃ 𝑤 ∈ Word 𝑇 ∃ 𝑠 ( 𝑃 = ( 𝐺 Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ↔ ∃ 𝑠 ∃ 𝑤 ∈ Word 𝑇 ( 𝑃 = ( 𝐺 Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) )
23 21 22 sylib ⊢ ( 𝑃 ∈ dom 𝑁 → ∃ 𝑠 ∃ 𝑤 ∈ Word 𝑇 ( 𝑃 = ( 𝐺 Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) )
24 reeanv ⊢ ( ∃ 𝑤 ∈ Word 𝑇 ∃ 𝑥 ∈ Word 𝑇 ( ( 𝑃 = ( 𝐺 Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ∧ ( 𝑃 = ( 𝐺 Σg 𝑥 ) ∧ 𝑡 = ( - 1 ↑ ( ♯ ‘ 𝑥 ) ) ) ) ↔ ( ∃ 𝑤 ∈ Word 𝑇 ( 𝑃 = ( 𝐺 Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ∧ ∃ 𝑥 ∈ Word 𝑇 ( 𝑃 = ( 𝐺 Σg 𝑥 ) ∧ 𝑡 = ( - 1 ↑ ( ♯ ‘ 𝑥 ) ) ) ) )
25 8 ad2antrr ⊢ ( ( ( 𝑃 ∈ dom 𝑁 ∧ ( 𝑤 ∈ Word 𝑇 ∧ 𝑥 ∈ Word 𝑇 ) ) ∧ ( ( 𝑃 = ( 𝐺 Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ∧ ( 𝑃 = ( 𝐺 Σg 𝑥 ) ∧ 𝑡 = ( - 1 ↑ ( ♯ ‘ 𝑥 ) ) ) ) ) → 𝐷 ∈ V )
26 simplrl ⊢ ( ( ( 𝑃 ∈ dom 𝑁 ∧ ( 𝑤 ∈ Word 𝑇 ∧ 𝑥 ∈ Word 𝑇 ) ) ∧ ( ( 𝑃 = ( 𝐺 Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ∧ ( 𝑃 = ( 𝐺 Σg 𝑥 ) ∧ 𝑡 = ( - 1 ↑ ( ♯ ‘ 𝑥 ) ) ) ) ) → 𝑤 ∈ Word 𝑇 )
27 simplrr ⊢ ( ( ( 𝑃 ∈ dom 𝑁 ∧ ( 𝑤 ∈ Word 𝑇 ∧ 𝑥 ∈ Word 𝑇 ) ) ∧ ( ( 𝑃 = ( 𝐺 Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ∧ ( 𝑃 = ( 𝐺 Σg 𝑥 ) ∧ 𝑡 = ( - 1 ↑ ( ♯ ‘ 𝑥 ) ) ) ) ) → 𝑥 ∈ Word 𝑇 )
28 simprll ⊢ ( ( ( 𝑃 ∈ dom 𝑁 ∧ ( 𝑤 ∈ Word 𝑇 ∧ 𝑥 ∈ Word 𝑇 ) ) ∧ ( ( 𝑃 = ( 𝐺 Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ∧ ( 𝑃 = ( 𝐺 Σg 𝑥 ) ∧ 𝑡 = ( - 1 ↑ ( ♯ ‘ 𝑥 ) ) ) ) ) → 𝑃 = ( 𝐺 Σg 𝑤 ) )
29 simprrl ⊢ ( ( ( 𝑃 ∈ dom 𝑁 ∧ ( 𝑤 ∈ Word 𝑇 ∧ 𝑥 ∈ Word 𝑇 ) ) ∧ ( ( 𝑃 = ( 𝐺 Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ∧ ( 𝑃 = ( 𝐺 Σg 𝑥 ) ∧ 𝑡 = ( - 1 ↑ ( ♯ ‘ 𝑥 ) ) ) ) ) → 𝑃 = ( 𝐺 Σg 𝑥 ) )
30 28 29 eqtr3d ⊢ ( ( ( 𝑃 ∈ dom 𝑁 ∧ ( 𝑤 ∈ Word 𝑇 ∧ 𝑥 ∈ Word 𝑇 ) ) ∧ ( ( 𝑃 = ( 𝐺 Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ∧ ( 𝑃 = ( 𝐺 Σg 𝑥 ) ∧ 𝑡 = ( - 1 ↑ ( ♯ ‘ 𝑥 ) ) ) ) ) → ( 𝐺 Σg 𝑤 ) = ( 𝐺 Σg 𝑥 ) )
31 1 2 25 26 27 30 psgnuni ⊢ ( ( ( 𝑃 ∈ dom 𝑁 ∧ ( 𝑤 ∈ Word 𝑇 ∧ 𝑥 ∈ Word 𝑇 ) ) ∧ ( ( 𝑃 = ( 𝐺 Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ∧ ( 𝑃 = ( 𝐺 Σg 𝑥 ) ∧ 𝑡 = ( - 1 ↑ ( ♯ ‘ 𝑥 ) ) ) ) ) → ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) = ( - 1 ↑ ( ♯ ‘ 𝑥 ) ) )
32 simprlr ⊢ ( ( ( 𝑃 ∈ dom 𝑁 ∧ ( 𝑤 ∈ Word 𝑇 ∧ 𝑥 ∈ Word 𝑇 ) ) ∧ ( ( 𝑃 = ( 𝐺 Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ∧ ( 𝑃 = ( 𝐺 Σg 𝑥 ) ∧ 𝑡 = ( - 1 ↑ ( ♯ ‘ 𝑥 ) ) ) ) ) → 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) )
33 simprrr ⊢ ( ( ( 𝑃 ∈ dom 𝑁 ∧ ( 𝑤 ∈ Word 𝑇 ∧ 𝑥 ∈ Word 𝑇 ) ) ∧ ( ( 𝑃 = ( 𝐺 Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ∧ ( 𝑃 = ( 𝐺 Σg 𝑥 ) ∧ 𝑡 = ( - 1 ↑ ( ♯ ‘ 𝑥 ) ) ) ) ) → 𝑡 = ( - 1 ↑ ( ♯ ‘ 𝑥 ) ) )
34 31 32 33 3eqtr4d ⊢ ( ( ( 𝑃 ∈ dom 𝑁 ∧ ( 𝑤 ∈ Word 𝑇 ∧ 𝑥 ∈ Word 𝑇 ) ) ∧ ( ( 𝑃 = ( 𝐺 Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ∧ ( 𝑃 = ( 𝐺 Σg 𝑥 ) ∧ 𝑡 = ( - 1 ↑ ( ♯ ‘ 𝑥 ) ) ) ) ) → 𝑠 = 𝑡 )
35 34 ex ⊢ ( ( 𝑃 ∈ dom 𝑁 ∧ ( 𝑤 ∈ Word 𝑇 ∧ 𝑥 ∈ Word 𝑇 ) ) → ( ( ( 𝑃 = ( 𝐺 Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ∧ ( 𝑃 = ( 𝐺 Σg 𝑥 ) ∧ 𝑡 = ( - 1 ↑ ( ♯ ‘ 𝑥 ) ) ) ) → 𝑠 = 𝑡 ) )
36 35 rexlimdvva ⊢ ( 𝑃 ∈ dom 𝑁 → ( ∃ 𝑤 ∈ Word 𝑇 ∃ 𝑥 ∈ Word 𝑇 ( ( 𝑃 = ( 𝐺 Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ∧ ( 𝑃 = ( 𝐺 Σg 𝑥 ) ∧ 𝑡 = ( - 1 ↑ ( ♯ ‘ 𝑥 ) ) ) ) → 𝑠 = 𝑡 ) )
37 24 36 syl5bir ⊢ ( 𝑃 ∈ dom 𝑁 → ( ( ∃ 𝑤 ∈ Word 𝑇 ( 𝑃 = ( 𝐺 Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ∧ ∃ 𝑥 ∈ Word 𝑇 ( 𝑃 = ( 𝐺 Σg 𝑥 ) ∧ 𝑡 = ( - 1 ↑ ( ♯ ‘ 𝑥 ) ) ) ) → 𝑠 = 𝑡 ) )
38 37 alrimivv ⊢ ( 𝑃 ∈ dom 𝑁 → ∀ 𝑠 ∀ 𝑡 ( ( ∃ 𝑤 ∈ Word 𝑇 ( 𝑃 = ( 𝐺 Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ∧ ∃ 𝑥 ∈ Word 𝑇 ( 𝑃 = ( 𝐺 Σg 𝑥 ) ∧ 𝑡 = ( - 1 ↑ ( ♯ ‘ 𝑥 ) ) ) ) → 𝑠 = 𝑡 ) )
39 eqeq1 ⊢ ( 𝑠 = 𝑡 → ( 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ↔ 𝑡 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) )
40 39 anbi2d ⊢ ( 𝑠 = 𝑡 → ( ( 𝑃 = ( 𝐺 Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ↔ ( 𝑃 = ( 𝐺 Σg 𝑤 ) ∧ 𝑡 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ) )
41 40 rexbidv ⊢ ( 𝑠 = 𝑡 → ( ∃ 𝑤 ∈ Word 𝑇 ( 𝑃 = ( 𝐺 Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ↔ ∃ 𝑤 ∈ Word 𝑇 ( 𝑃 = ( 𝐺 Σg 𝑤 ) ∧ 𝑡 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ) )
42 oveq2 ⊢ ( 𝑤 = 𝑥 → ( 𝐺 Σg 𝑤 ) = ( 𝐺 Σg 𝑥 ) )
43 42 eqeq2d ⊢ ( 𝑤 = 𝑥 → ( 𝑃 = ( 𝐺 Σg 𝑤 ) ↔ 𝑃 = ( 𝐺 Σg 𝑥 ) ) )
44 fveq2 ⊢ ( 𝑤 = 𝑥 → ( ♯ ‘ 𝑤 ) = ( ♯ ‘ 𝑥 ) )
45 44 oveq2d ⊢ ( 𝑤 = 𝑥 → ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) = ( - 1 ↑ ( ♯ ‘ 𝑥 ) ) )
46 45 eqeq2d ⊢ ( 𝑤 = 𝑥 → ( 𝑡 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ↔ 𝑡 = ( - 1 ↑ ( ♯ ‘ 𝑥 ) ) ) )
47 43 46 anbi12d ⊢ ( 𝑤 = 𝑥 → ( ( 𝑃 = ( 𝐺 Σg 𝑤 ) ∧ 𝑡 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ↔ ( 𝑃 = ( 𝐺 Σg 𝑥 ) ∧ 𝑡 = ( - 1 ↑ ( ♯ ‘ 𝑥 ) ) ) ) )
48 47 cbvrexvw ⊢ ( ∃ 𝑤 ∈ Word 𝑇 ( 𝑃 = ( 𝐺 Σg 𝑤 ) ∧ 𝑡 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ↔ ∃ 𝑥 ∈ Word 𝑇 ( 𝑃 = ( 𝐺 Σg 𝑥 ) ∧ 𝑡 = ( - 1 ↑ ( ♯ ‘ 𝑥 ) ) ) )
49 41 48 bitrdi ⊢ ( 𝑠 = 𝑡 → ( ∃ 𝑤 ∈ Word 𝑇 ( 𝑃 = ( 𝐺 Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ↔ ∃ 𝑥 ∈ Word 𝑇 ( 𝑃 = ( 𝐺 Σg 𝑥 ) ∧ 𝑡 = ( - 1 ↑ ( ♯ ‘ 𝑥 ) ) ) ) )
50 49 eu4 ⊢ ( ∃! 𝑠 ∃ 𝑤 ∈ Word 𝑇 ( 𝑃 = ( 𝐺 Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ↔ ( ∃ 𝑠 ∃ 𝑤 ∈ Word 𝑇 ( 𝑃 = ( 𝐺 Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ∧ ∀ 𝑠 ∀ 𝑡 ( ( ∃ 𝑤 ∈ Word 𝑇 ( 𝑃 = ( 𝐺 Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ∧ ∃ 𝑥 ∈ Word 𝑇 ( 𝑃 = ( 𝐺 Σg 𝑥 ) ∧ 𝑡 = ( - 1 ↑ ( ♯ ‘ 𝑥 ) ) ) ) → 𝑠 = 𝑡 ) ) )
51 23 38 50 sylanbrc ⊢ ( 𝑃 ∈ dom 𝑁 → ∃! 𝑠 ∃ 𝑤 ∈ Word 𝑇 ( 𝑃 = ( 𝐺 Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) )