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

Metamath Proof Explorer

Theorem psgnfval

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

Ref Expression
Hypotheses psgnfval.g ⊢ 𝐺 = ( SymGrp ‘ 𝐷 )
psgnfval.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
psgnfval.f ⊢ 𝐹 = { 𝑝 ∈ 𝐵 ∣ dom ( 𝑝 ∖ I ) ∈ Fin }
psgnfval.t ⊢ 𝑇 = ran ( pmTrsp ‘ 𝐷 )
psgnfval.n ⊢ 𝑁 = ( pmSgn ‘ 𝐷 )
Assertion psgnfval 𝑁 = ( 𝑥 ∈ 𝐹 ↦ ( ℩ 𝑠 ∃ 𝑤 ∈ Word 𝑇 ( 𝑥 = ( 𝐺 Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 psgnfval.g ⊢ 𝐺 = ( SymGrp ‘ 𝐷 )
2 psgnfval.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
3 psgnfval.f ⊢ 𝐹 = { 𝑝 ∈ 𝐵 ∣ dom ( 𝑝 ∖ I ) ∈ Fin }
4 psgnfval.t ⊢ 𝑇 = ran ( pmTrsp ‘ 𝐷 )
5 psgnfval.n ⊢ 𝑁 = ( pmSgn ‘ 𝐷 )
6 fveq2 ⊢ ( 𝑑 = 𝐷 → ( SymGrp ‘ 𝑑 ) = ( SymGrp ‘ 𝐷 ) )
7 6 1 eqtr4di ⊢ ( 𝑑 = 𝐷 → ( SymGrp ‘ 𝑑 ) = 𝐺 )
8 7 fveq2d ⊢ ( 𝑑 = 𝐷 → ( Base ‘ ( SymGrp ‘ 𝑑 ) ) = ( Base ‘ 𝐺 ) )
9 8 2 eqtr4di ⊢ ( 𝑑 = 𝐷 → ( Base ‘ ( SymGrp ‘ 𝑑 ) ) = 𝐵 )
10 rabeq ⊢ ( ( Base ‘ ( SymGrp ‘ 𝑑 ) ) = 𝐵 → { 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑑 ) ) ∣ dom ( 𝑝 ∖ I ) ∈ Fin } = { 𝑝 ∈ 𝐵 ∣ dom ( 𝑝 ∖ I ) ∈ Fin } )
11 9 10 syl ⊢ ( 𝑑 = 𝐷 → { 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑑 ) ) ∣ dom ( 𝑝 ∖ I ) ∈ Fin } = { 𝑝 ∈ 𝐵 ∣ dom ( 𝑝 ∖ I ) ∈ Fin } )
12 11 3 eqtr4di ⊢ ( 𝑑 = 𝐷 → { 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑑 ) ) ∣ dom ( 𝑝 ∖ I ) ∈ Fin } = 𝐹 )
13 fveq2 ⊢ ( 𝑑 = 𝐷 → ( pmTrsp ‘ 𝑑 ) = ( pmTrsp ‘ 𝐷 ) )
14 13 rneqd ⊢ ( 𝑑 = 𝐷 → ran ( pmTrsp ‘ 𝑑 ) = ran ( pmTrsp ‘ 𝐷 ) )
15 14 4 eqtr4di ⊢ ( 𝑑 = 𝐷 → ran ( pmTrsp ‘ 𝑑 ) = 𝑇 )
16 wrdeq ⊢ ( ran ( pmTrsp ‘ 𝑑 ) = 𝑇 → Word ran ( pmTrsp ‘ 𝑑 ) = Word 𝑇 )
17 15 16 syl ⊢ ( 𝑑 = 𝐷 → Word ran ( pmTrsp ‘ 𝑑 ) = Word 𝑇 )
18 7 oveq1d ⊢ ( 𝑑 = 𝐷 → ( ( SymGrp ‘ 𝑑 ) Σg 𝑤 ) = ( 𝐺 Σg 𝑤 ) )
19 18 eqeq2d ⊢ ( 𝑑 = 𝐷 → ( 𝑥 = ( ( SymGrp ‘ 𝑑 ) Σg 𝑤 ) ↔ 𝑥 = ( 𝐺 Σg 𝑤 ) ) )
20 19 anbi1d ⊢ ( 𝑑 = 𝐷 → ( ( 𝑥 = ( ( SymGrp ‘ 𝑑 ) Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ↔ ( 𝑥 = ( 𝐺 Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ) )
21 17 20 rexeqbidv ⊢ ( 𝑑 = 𝐷 → ( ∃ 𝑤 ∈ Word ran ( pmTrsp ‘ 𝑑 ) ( 𝑥 = ( ( SymGrp ‘ 𝑑 ) Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ↔ ∃ 𝑤 ∈ Word 𝑇 ( 𝑥 = ( 𝐺 Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ) )
22 21 iotabidv ⊢ ( 𝑑 = 𝐷 → ( ℩ 𝑠 ∃ 𝑤 ∈ Word ran ( pmTrsp ‘ 𝑑 ) ( 𝑥 = ( ( SymGrp ‘ 𝑑 ) Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ) = ( ℩ 𝑠 ∃ 𝑤 ∈ Word 𝑇 ( 𝑥 = ( 𝐺 Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ) )
23 12 22 mpteq12dv ⊢ ( 𝑑 = 𝐷 → ( 𝑥 ∈ { 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑑 ) ) ∣ dom ( 𝑝 ∖ I ) ∈ Fin } ↦ ( ℩ 𝑠 ∃ 𝑤 ∈ Word ran ( pmTrsp ‘ 𝑑 ) ( 𝑥 = ( ( SymGrp ‘ 𝑑 ) Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ) ) = ( 𝑥 ∈ 𝐹 ↦ ( ℩ 𝑠 ∃ 𝑤 ∈ Word 𝑇 ( 𝑥 = ( 𝐺 Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ) ) )
24 df-psgn ⊢ pmSgn = ( 𝑑 ∈ V ↦ ( 𝑥 ∈ { 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑑 ) ) ∣ dom ( 𝑝 ∖ I ) ∈ Fin } ↦ ( ℩ 𝑠 ∃ 𝑤 ∈ Word ran ( pmTrsp ‘ 𝑑 ) ( 𝑥 = ( ( SymGrp ‘ 𝑑 ) Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ) ) )
25 2 fvexi ⊢ 𝐵 ∈ V
26 3 25 rabex2 ⊢ 𝐹 ∈ V
27 26 mptex ⊢ ( 𝑥 ∈ 𝐹 ↦ ( ℩ 𝑠 ∃ 𝑤 ∈ Word 𝑇 ( 𝑥 = ( 𝐺 Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ) ) ∈ V
28 23 24 27 fvmpt ⊢ ( 𝐷 ∈ V → ( pmSgn ‘ 𝐷 ) = ( 𝑥 ∈ 𝐹 ↦ ( ℩ 𝑠 ∃ 𝑤 ∈ Word 𝑇 ( 𝑥 = ( 𝐺 Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ) ) )
29 fvprc ⊢ ( ¬ 𝐷 ∈ V → ( pmSgn ‘ 𝐷 ) = ∅ )
30 fvprc ⊢ ( ¬ 𝐷 ∈ V → ( SymGrp ‘ 𝐷 ) = ∅ )
31 1 30 eqtrid ⊢ ( ¬ 𝐷 ∈ V → 𝐺 = ∅ )
32 31 fveq2d ⊢ ( ¬ 𝐷 ∈ V → ( Base ‘ 𝐺 ) = ( Base ‘ ∅ ) )
33 base0 ⊢ ∅ = ( Base ‘ ∅ )
34 32 33 eqtr4di ⊢ ( ¬ 𝐷 ∈ V → ( Base ‘ 𝐺 ) = ∅ )
35 2 34 eqtrid ⊢ ( ¬ 𝐷 ∈ V → 𝐵 = ∅ )
36 rabeq ⊢ ( 𝐵 = ∅ → { 𝑝 ∈ 𝐵 ∣ dom ( 𝑝 ∖ I ) ∈ Fin } = { 𝑝 ∈ ∅ ∣ dom ( 𝑝 ∖ I ) ∈ Fin } )
37 35 36 syl ⊢ ( ¬ 𝐷 ∈ V → { 𝑝 ∈ 𝐵 ∣ dom ( 𝑝 ∖ I ) ∈ Fin } = { 𝑝 ∈ ∅ ∣ dom ( 𝑝 ∖ I ) ∈ Fin } )
38 rab0 ⊢ { 𝑝 ∈ ∅ ∣ dom ( 𝑝 ∖ I ) ∈ Fin } = ∅
39 37 38 eqtrdi ⊢ ( ¬ 𝐷 ∈ V → { 𝑝 ∈ 𝐵 ∣ dom ( 𝑝 ∖ I ) ∈ Fin } = ∅ )
40 3 39 eqtrid ⊢ ( ¬ 𝐷 ∈ V → 𝐹 = ∅ )
41 40 mpteq1d ⊢ ( ¬ 𝐷 ∈ V → ( 𝑥 ∈ 𝐹 ↦ ( ℩ 𝑠 ∃ 𝑤 ∈ Word 𝑇 ( 𝑥 = ( 𝐺 Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ) ) = ( 𝑥 ∈ ∅ ↦ ( ℩ 𝑠 ∃ 𝑤 ∈ Word 𝑇 ( 𝑥 = ( 𝐺 Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ) ) )
42 mpt0 ⊢ ( 𝑥 ∈ ∅ ↦ ( ℩ 𝑠 ∃ 𝑤 ∈ Word 𝑇 ( 𝑥 = ( 𝐺 Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ) ) = ∅
43 41 42 eqtrdi ⊢ ( ¬ 𝐷 ∈ V → ( 𝑥 ∈ 𝐹 ↦ ( ℩ 𝑠 ∃ 𝑤 ∈ Word 𝑇 ( 𝑥 = ( 𝐺 Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ) ) = ∅ )
44 29 43 eqtr4d ⊢ ( ¬ 𝐷 ∈ V → ( pmSgn ‘ 𝐷 ) = ( 𝑥 ∈ 𝐹 ↦ ( ℩ 𝑠 ∃ 𝑤 ∈ Word 𝑇 ( 𝑥 = ( 𝐺 Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ) ) )
45 28 44 pm2.61i ⊢ ( pmSgn ‘ 𝐷 ) = ( 𝑥 ∈ 𝐹 ↦ ( ℩ 𝑠 ∃ 𝑤 ∈ Word 𝑇 ( 𝑥 = ( 𝐺 Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ) )
46 5 45 eqtri ⊢ 𝑁 = ( 𝑥 ∈ 𝐹 ↦ ( ℩ 𝑠 ∃ 𝑤 ∈ Word 𝑇 ( 𝑥 = ( 𝐺 Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ) )