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

Metamath Proof Explorer

Theorem psgnvalii

Description: Any representation of a permutation is length matching the permutation sign. (Contributed by Stefan O'Rear, 28-Aug-2015)

Ref Expression
Hypotheses psgnval.g ⊢ 𝐺 = ( SymGrp ‘ 𝐷 )
psgnval.t ⊢ 𝑇 = ran ( pmTrsp ‘ 𝐷 )
psgnval.n ⊢ 𝑁 = ( pmSgn ‘ 𝐷 )
Assertion psgnvalii ( ( 𝐷 ∈ 𝑉 ∧ 𝑊 ∈ 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 psgneldm2i ⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝑊 ∈ Word 𝑇 ) → ( 𝐺 Σg 𝑊 ) ∈ dom 𝑁 )
5 1 2 3 psgnval ⊢ ( ( 𝐺 Σg 𝑊 ) ∈ dom 𝑁 → ( 𝑁 ‘ ( 𝐺 Σg 𝑊 ) ) = ( ℩ 𝑠 ∃ 𝑤 ∈ Word 𝑇 ( ( 𝐺 Σg 𝑊 ) = ( 𝐺 Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ) )
6 4 5 syl ⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝑊 ∈ Word 𝑇 ) → ( 𝑁 ‘ ( 𝐺 Σg 𝑊 ) ) = ( ℩ 𝑠 ∃ 𝑤 ∈ Word 𝑇 ( ( 𝐺 Σg 𝑊 ) = ( 𝐺 Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ) )
7 simpr ⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝑊 ∈ Word 𝑇 ) → 𝑊 ∈ Word 𝑇 )
8 eqidd ⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝑊 ∈ Word 𝑇 ) → ( 𝐺 Σg 𝑊 ) = ( 𝐺 Σg 𝑊 ) )
9 eqidd ⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝑊 ∈ Word 𝑇 ) → ( - 1 ↑ ( ♯ ‘ 𝑊 ) ) = ( - 1 ↑ ( ♯ ‘ 𝑊 ) ) )
10 oveq2 ⊢ ( 𝑤 = 𝑊 → ( 𝐺 Σg 𝑤 ) = ( 𝐺 Σg 𝑊 ) )
11 10 eqeq2d ⊢ ( 𝑤 = 𝑊 → ( ( 𝐺 Σg 𝑊 ) = ( 𝐺 Σg 𝑤 ) ↔ ( 𝐺 Σg 𝑊 ) = ( 𝐺 Σg 𝑊 ) ) )
12 fveq2 ⊢ ( 𝑤 = 𝑊 → ( ♯ ‘ 𝑤 ) = ( ♯ ‘ 𝑊 ) )
13 12 oveq2d ⊢ ( 𝑤 = 𝑊 → ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) = ( - 1 ↑ ( ♯ ‘ 𝑊 ) ) )
14 13 eqeq2d ⊢ ( 𝑤 = 𝑊 → ( ( - 1 ↑ ( ♯ ‘ 𝑊 ) ) = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ↔ ( - 1 ↑ ( ♯ ‘ 𝑊 ) ) = ( - 1 ↑ ( ♯ ‘ 𝑊 ) ) ) )
15 11 14 anbi12d ⊢ ( 𝑤 = 𝑊 → ( ( ( 𝐺 Σg 𝑊 ) = ( 𝐺 Σg 𝑤 ) ∧ ( - 1 ↑ ( ♯ ‘ 𝑊 ) ) = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ↔ ( ( 𝐺 Σg 𝑊 ) = ( 𝐺 Σg 𝑊 ) ∧ ( - 1 ↑ ( ♯ ‘ 𝑊 ) ) = ( - 1 ↑ ( ♯ ‘ 𝑊 ) ) ) ) )
16 15 rspcev ⊢ ( ( 𝑊 ∈ Word 𝑇 ∧ ( ( 𝐺 Σg 𝑊 ) = ( 𝐺 Σg 𝑊 ) ∧ ( - 1 ↑ ( ♯ ‘ 𝑊 ) ) = ( - 1 ↑ ( ♯ ‘ 𝑊 ) ) ) ) → ∃ 𝑤 ∈ Word 𝑇 ( ( 𝐺 Σg 𝑊 ) = ( 𝐺 Σg 𝑤 ) ∧ ( - 1 ↑ ( ♯ ‘ 𝑊 ) ) = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) )
17 7 8 9 16 syl12anc ⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝑊 ∈ Word 𝑇 ) → ∃ 𝑤 ∈ Word 𝑇 ( ( 𝐺 Σg 𝑊 ) = ( 𝐺 Σg 𝑤 ) ∧ ( - 1 ↑ ( ♯ ‘ 𝑊 ) ) = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) )
18 ovexd ⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝑊 ∈ Word 𝑇 ) → ( - 1 ↑ ( ♯ ‘ 𝑊 ) ) ∈ V )
19 1 2 3 psgneu ⊢ ( ( 𝐺 Σg 𝑊 ) ∈ dom 𝑁 → ∃! 𝑠 ∃ 𝑤 ∈ Word 𝑇 ( ( 𝐺 Σg 𝑊 ) = ( 𝐺 Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) )
20 4 19 syl ⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝑊 ∈ Word 𝑇 ) → ∃! 𝑠 ∃ 𝑤 ∈ Word 𝑇 ( ( 𝐺 Σg 𝑊 ) = ( 𝐺 Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) )
21 eqeq1 ⊢ ( 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑊 ) ) → ( 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ↔ ( - 1 ↑ ( ♯ ‘ 𝑊 ) ) = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) )
22 21 anbi2d ⊢ ( 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑊 ) ) → ( ( ( 𝐺 Σg 𝑊 ) = ( 𝐺 Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ↔ ( ( 𝐺 Σg 𝑊 ) = ( 𝐺 Σg 𝑤 ) ∧ ( - 1 ↑ ( ♯ ‘ 𝑊 ) ) = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ) )
23 22 rexbidv ⊢ ( 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑊 ) ) → ( ∃ 𝑤 ∈ Word 𝑇 ( ( 𝐺 Σg 𝑊 ) = ( 𝐺 Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ↔ ∃ 𝑤 ∈ Word 𝑇 ( ( 𝐺 Σg 𝑊 ) = ( 𝐺 Σg 𝑤 ) ∧ ( - 1 ↑ ( ♯ ‘ 𝑊 ) ) = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ) )
24 23 adantl ⊢ ( ( ( 𝐷 ∈ 𝑉 ∧ 𝑊 ∈ Word 𝑇 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑊 ) ) ) → ( ∃ 𝑤 ∈ Word 𝑇 ( ( 𝐺 Σg 𝑊 ) = ( 𝐺 Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ↔ ∃ 𝑤 ∈ Word 𝑇 ( ( 𝐺 Σg 𝑊 ) = ( 𝐺 Σg 𝑤 ) ∧ ( - 1 ↑ ( ♯ ‘ 𝑊 ) ) = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ) )
25 18 20 24 iota2d ⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝑊 ∈ Word 𝑇 ) → ( ∃ 𝑤 ∈ Word 𝑇 ( ( 𝐺 Σg 𝑊 ) = ( 𝐺 Σg 𝑤 ) ∧ ( - 1 ↑ ( ♯ ‘ 𝑊 ) ) = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ↔ ( ℩ 𝑠 ∃ 𝑤 ∈ Word 𝑇 ( ( 𝐺 Σg 𝑊 ) = ( 𝐺 Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ) = ( - 1 ↑ ( ♯ ‘ 𝑊 ) ) ) )
26 17 25 mpbid ⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝑊 ∈ Word 𝑇 ) → ( ℩ 𝑠 ∃ 𝑤 ∈ Word 𝑇 ( ( 𝐺 Σg 𝑊 ) = ( 𝐺 Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ) = ( - 1 ↑ ( ♯ ‘ 𝑊 ) ) )
27 6 26 eqtrd ⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝑊 ∈ Word 𝑇 ) → ( 𝑁 ‘ ( 𝐺 Σg 𝑊 ) ) = ( - 1 ↑ ( ♯ ‘ 𝑊 ) ) )