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