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