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

Metamath Proof Explorer

Theorem psgnfvalfi

Description: Function definition 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 psgnfvalfi ( 𝐷 ∈ 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 eqid ⊢ { 𝑝 ∈ 𝐵 ∣ dom ( 𝑝 ∖ I ) ∈ Fin } = { 𝑝 ∈ 𝐵 ∣ dom ( 𝑝 ∖ I ) ∈ Fin }
6 1 2 5 3 4 psgnfval ⊢ 𝑁 = ( 𝑥 ∈ { 𝑝 ∈ 𝐵 ∣ dom ( 𝑝 ∖ I ) ∈ Fin } ↦ ( ℩ 𝑠 ∃ 𝑤 ∈ Word 𝑇 ( 𝑥 = ( 𝐺 Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ) )
7 1 2 sygbasnfpfi ⊢ ( ( 𝐷 ∈ Fin ∧ 𝑝 ∈ 𝐵 ) → dom ( 𝑝 ∖ I ) ∈ Fin )
8 7 ralrimiva ⊢ ( 𝐷 ∈ Fin → ∀ 𝑝 ∈ 𝐵 dom ( 𝑝 ∖ I ) ∈ Fin )
9 rabid2 ⊢ ( 𝐵 = { 𝑝 ∈ 𝐵 ∣ dom ( 𝑝 ∖ I ) ∈ Fin } ↔ ∀ 𝑝 ∈ 𝐵 dom ( 𝑝 ∖ I ) ∈ Fin )
10 8 9 sylibr ⊢ ( 𝐷 ∈ Fin → 𝐵 = { 𝑝 ∈ 𝐵 ∣ dom ( 𝑝 ∖ I ) ∈ Fin } )
11 10 eqcomd ⊢ ( 𝐷 ∈ Fin → { 𝑝 ∈ 𝐵 ∣ dom ( 𝑝 ∖ I ) ∈ Fin } = 𝐵 )
12 11 mpteq1d ⊢ ( 𝐷 ∈ Fin → ( 𝑥 ∈ { 𝑝 ∈ 𝐵 ∣ dom ( 𝑝 ∖ I ) ∈ Fin } ↦ ( ℩ 𝑠 ∃ 𝑤 ∈ Word 𝑇 ( 𝑥 = ( 𝐺 Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ) ) = ( 𝑥 ∈ 𝐵 ↦ ( ℩ 𝑠 ∃ 𝑤 ∈ Word 𝑇 ( 𝑥 = ( 𝐺 Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ) ) )
13 6 12 eqtrid ⊢ ( 𝐷 ∈ Fin → 𝑁 = ( 𝑥 ∈ 𝐵 ↦ ( ℩ 𝑠 ∃ 𝑤 ∈ Word 𝑇 ( 𝑥 = ( 𝐺 Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ) ) )