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	syl5eq	⊢ ( ¬ 𝐷 ∈ V → 𝐺 = ∅ )
32	31	fveq2d	⊢ ( ¬ 𝐷 ∈ V → ( Base ‘ 𝐺 ) = ( Base ‘ ∅ ) )
33		base0	⊢ ∅ = ( Base ‘ ∅ )
34	32 33	eqtr4di	⊢ ( ¬ 𝐷 ∈ V → ( Base ‘ 𝐺 ) = ∅ )
35	2 34	syl5eq	⊢ ( ¬ 𝐷 ∈ 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	syl5eq	⊢ ( ¬ 𝐷 ∈ 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 ↑ ( ♯ ‘ 𝑤 ) ) ) ) )