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

Metamath Proof Explorer

Theorem psgnvalfi

Description: Value of the permutation sign function for permutations of finite sets. (Contributed by AV, 13-Jan-2019)

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

Proof

Step Hyp Ref Expression
1 psgnfvalfi.g ⊢ 𝐺 = ( SymGrp ‘ 𝐷 )
2 psgnfvalfi.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
3 psgnfvalfi.t ⊢ 𝑇 = ran ( pmTrsp ‘ 𝐷 )
4 psgnfvalfi.n ⊢ 𝑁 = ( pmSgn ‘ 𝐷 )
5 simpr ⊢ ( ( 𝐷 ∈ Fin ∧ 𝑃 ∈ 𝐵 ) → 𝑃 ∈ 𝐵 )
6 1 2 sygbasnfpfi ⊢ ( ( 𝐷 ∈ Fin ∧ 𝑃 ∈ 𝐵 ) → dom ( 𝑃 ∖ I ) ∈ Fin )
7 1 4 2 psgneldm ⊢ ( 𝑃 ∈ dom 𝑁 ↔ ( 𝑃 ∈ 𝐵 ∧ dom ( 𝑃 ∖ I ) ∈ Fin ) )
8 5 6 7 sylanbrc ⊢ ( ( 𝐷 ∈ Fin ∧ 𝑃 ∈ 𝐵 ) → 𝑃 ∈ dom 𝑁 )
9 1 3 4 psgnval ⊢ ( 𝑃 ∈ dom 𝑁 → ( 𝑁 ‘ 𝑃 ) = ( ℩ 𝑠 ∃ 𝑤 ∈ Word 𝑇 ( 𝑃 = ( 𝐺 Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ) )
10 8 9 syl ⊢ ( ( 𝐷 ∈ Fin ∧ 𝑃 ∈ 𝐵 ) → ( 𝑁 ‘ 𝑃 ) = ( ℩ 𝑠 ∃ 𝑤 ∈ Word 𝑇 ( 𝑃 = ( 𝐺 Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ) )