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