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

Metamath Proof Explorer

Theorem psgnval

Description: Value of the permutation sign function. (Contributed by Stefan O'Rear, 28-Aug-2015)

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

Proof

Step Hyp Ref Expression
1 psgnval.g ⊢ 𝐺 = ( SymGrp ‘ 𝐷 )
2 psgnval.t ⊢ 𝑇 = ran ( pmTrsp ‘ 𝐷 )
3 psgnval.n ⊢ 𝑁 = ( pmSgn ‘ 𝐷 )
4 eqeq1 ⊢ ( 𝑡 = 𝑃 → ( 𝑡 = ( 𝐺 Σg 𝑤 ) ↔ 𝑃 = ( 𝐺 Σg 𝑤 ) ) )
5 4 anbi1d ⊢ ( 𝑡 = 𝑃 → ( ( 𝑡 = ( 𝐺 Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ↔ ( 𝑃 = ( 𝐺 Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ) )
6 5 rexbidv ⊢ ( 𝑡 = 𝑃 → ( ∃ 𝑤 ∈ Word 𝑇 ( 𝑡 = ( 𝐺 Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ↔ ∃ 𝑤 ∈ Word 𝑇 ( 𝑃 = ( 𝐺 Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ) )
7 6 iotabidv ⊢ ( 𝑡 = 𝑃 → ( ℩ 𝑠 ∃ 𝑤 ∈ Word 𝑇 ( 𝑡 = ( 𝐺 Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ) = ( ℩ 𝑠 ∃ 𝑤 ∈ Word 𝑇 ( 𝑃 = ( 𝐺 Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ) )
8 eqid ⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
9 eqid ⊢ { 𝑥 ∈ ( Base ‘ 𝐺 ) ∣ dom ( 𝑥 ∖ I ) ∈ Fin } = { 𝑥 ∈ ( Base ‘ 𝐺 ) ∣ dom ( 𝑥 ∖ I ) ∈ Fin }
10 1 8 9 3 psgnfn ⊢ 𝑁 Fn { 𝑥 ∈ ( Base ‘ 𝐺 ) ∣ dom ( 𝑥 ∖ I ) ∈ Fin }
11 10 fndmi ⊢ dom 𝑁 = { 𝑥 ∈ ( Base ‘ 𝐺 ) ∣ dom ( 𝑥 ∖ I ) ∈ Fin }
12 1 8 11 2 3 psgnfval ⊢ 𝑁 = ( 𝑡 ∈ dom 𝑁 ↦ ( ℩ 𝑠 ∃ 𝑤 ∈ Word 𝑇 ( 𝑡 = ( 𝐺 Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ) )
13 iotaex ⊢ ( ℩ 𝑠 ∃ 𝑤 ∈ Word 𝑇 ( 𝑃 = ( 𝐺 Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ) ∈ V
14 7 12 13 fvmpt ⊢ ( 𝑃 ∈ dom 𝑁 → ( 𝑁 ‘ 𝑃 ) = ( ℩ 𝑠 ∃ 𝑤 ∈ Word 𝑇 ( 𝑃 = ( 𝐺 Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ) )