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

Metamath Proof Explorer

Definition df-psgn

Description: Define a function which takes the value 1 for even permutations and -u 1 for odd. (Contributed by Stefan O'Rear, 28-Aug-2015)

Ref Expression
Assertion df-psgn pmSgn = ( 𝑑 ∈ V ↦ ( 𝑥 ∈ { 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑑 ) ) ∣ dom ( 𝑝 ∖ I ) ∈ Fin } ↦ ( ℩ 𝑠 ∃ 𝑤 ∈ Word ran ( pmTrsp ‘ 𝑑 ) ( 𝑥 = ( ( SymGrp ‘ 𝑑 ) Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cpsgn ⊢ pmSgn
1 vd ⊢ 𝑑
2 cvv ⊢ V
3 vx ⊢ 𝑥
4 vp ⊢ 𝑝
5 cbs ⊢ Base
6 csymg ⊢ SymGrp
7 1 cv ⊢ 𝑑
8 7 6 cfv ⊢ ( SymGrp ‘ 𝑑 )
9 8 5 cfv ⊢ ( Base ‘ ( SymGrp ‘ 𝑑 ) )
10 4 cv ⊢ 𝑝
11 cid ⊢ I
12 10 11 cdif ⊢ ( 𝑝 ∖ I )
13 12 cdm ⊢ dom ( 𝑝 ∖ I )
14 cfn ⊢ Fin
15 13 14 wcel ⊢ dom ( 𝑝 ∖ I ) ∈ Fin
16 15 4 9 crab ⊢ { 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑑 ) ) ∣ dom ( 𝑝 ∖ I ) ∈ Fin }
17 vs ⊢ 𝑠
18 vw ⊢ 𝑤
19 cpmtr ⊢ pmTrsp
20 7 19 cfv ⊢ ( pmTrsp ‘ 𝑑 )
21 20 crn ⊢ ran ( pmTrsp ‘ 𝑑 )
22 21 cword ⊢ Word ran ( pmTrsp ‘ 𝑑 )
23 3 cv ⊢ 𝑥
24 cgsu ⊢ Σg
25 18 cv ⊢ 𝑤
26 8 25 24 co ⊢ ( ( SymGrp ‘ 𝑑 ) Σg 𝑤 )
27 23 26 wceq ⊢ 𝑥 = ( ( SymGrp ‘ 𝑑 ) Σg 𝑤 )
28 17 cv ⊢ 𝑠
29 c1 ⊢ 1
30 29 cneg ⊢ - 1
31 cexp ⊢ ↑
32 chash ⊢ ♯
33 25 32 cfv ⊢ ( ♯ ‘ 𝑤 )
34 30 33 31 co ⊢ ( - 1 ↑ ( ♯ ‘ 𝑤 ) )
35 28 34 wceq ⊢ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) )
36 27 35 wa ⊢ ( 𝑥 = ( ( SymGrp ‘ 𝑑 ) Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) )
37 36 18 22 wrex ⊢ ∃ 𝑤 ∈ Word ran ( pmTrsp ‘ 𝑑 ) ( 𝑥 = ( ( SymGrp ‘ 𝑑 ) Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) )
38 37 17 cio ⊢ ( ℩ 𝑠 ∃ 𝑤 ∈ Word ran ( pmTrsp ‘ 𝑑 ) ( 𝑥 = ( ( SymGrp ‘ 𝑑 ) Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) )
39 3 16 38 cmpt ⊢ ( 𝑥 ∈ { 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑑 ) ) ∣ dom ( 𝑝 ∖ I ) ∈ Fin } ↦ ( ℩ 𝑠 ∃ 𝑤 ∈ Word ran ( pmTrsp ‘ 𝑑 ) ( 𝑥 = ( ( SymGrp ‘ 𝑑 ) Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ) )
40 1 2 39 cmpt ⊢ ( 𝑑 ∈ V ↦ ( 𝑥 ∈ { 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑑 ) ) ∣ dom ( 𝑝 ∖ I ) ∈ Fin } ↦ ( ℩ 𝑠 ∃ 𝑤 ∈ Word ran ( pmTrsp ‘ 𝑑 ) ( 𝑥 = ( ( SymGrp ‘ 𝑑 ) Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ) ) )
41 0 40 wceq ⊢ pmSgn = ( 𝑑 ∈ V ↦ ( 𝑥 ∈ { 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑑 ) ) ∣ dom ( 𝑝 ∖ I ) ∈ Fin } ↦ ( ℩ 𝑠 ∃ 𝑤 ∈ Word ran ( pmTrsp ‘ 𝑑 ) ( 𝑥 = ( ( SymGrp ‘ 𝑑 ) Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ) ) )