Theorem psgnval

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

	Ref	Expression
Hypotheses	psgnval.g	⊢ 𝐺 = ( SymGrp ‘ 𝐷 )
	psgnval.t	⊢ 𝑇 = ran ( pmTrsp ‘ 𝐷 )
	psgnval.n	⊢ 𝑁 = ( pmSgn ‘ 𝐷 )
Assertion	psgnval	⊢ ( 𝑃 ∈ dom 𝑁 → ( 𝑁 ‘ 𝑃 ) = ( ℩ 𝑠 ∃ 𝑤 ∈ Word 𝑇 ( 𝑃 = ( 𝐺 Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		psgnval.g	⊢ 𝐺 = ( SymGrp ‘ 𝐷 )
2		psgnval.t	⊢ 𝑇 = ran ( pmTrsp ‘ 𝐷 )
3		psgnval.n	⊢ 𝑁 = ( pmSgn ‘ 𝐷 )
4		eqeq1	⊢ ( 𝑡 = 𝑃 → ( 𝑡 = ( 𝐺 Σg 𝑤 ) ↔ 𝑃 = ( 𝐺 Σg 𝑤 ) ) )
5	4	anbi1d	⊢ ( 𝑡 = 𝑃 → ( ( 𝑡 = ( 𝐺 Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ↔ ( 𝑃 = ( 𝐺 Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ) )
6	5	rexbidv	⊢ ( 𝑡 = 𝑃 → ( ∃ 𝑤 ∈ Word 𝑇 ( 𝑡 = ( 𝐺 Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ↔ ∃ 𝑤 ∈ Word 𝑇 ( 𝑃 = ( 𝐺 Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ) )
7	6	iotabidv	⊢ ( 𝑡 = 𝑃 → ( ℩ 𝑠 ∃ 𝑤 ∈ Word 𝑇 ( 𝑡 = ( 𝐺 Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ) = ( ℩ 𝑠 ∃ 𝑤 ∈ Word 𝑇 ( 𝑃 = ( 𝐺 Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ) )
8		eqid	⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
9		eqid	⊢ { 𝑥 ∈ ( Base ‘ 𝐺 ) ∣ dom ( 𝑥 ∖ I ) ∈ Fin } = { 𝑥 ∈ ( Base ‘ 𝐺 ) ∣ dom ( 𝑥 ∖ I ) ∈ Fin }
10	1 8 9 3	psgnfn	⊢ 𝑁 Fn { 𝑥 ∈ ( Base ‘ 𝐺 ) ∣ dom ( 𝑥 ∖ I ) ∈ Fin }
11	10	fndmi	⊢ dom 𝑁 = { 𝑥 ∈ ( Base ‘ 𝐺 ) ∣ dom ( 𝑥 ∖ I ) ∈ Fin }
12	1 8 11 2 3	psgnfval	⊢ 𝑁 = ( 𝑡 ∈ dom 𝑁 ↦ ( ℩ 𝑠 ∃ 𝑤 ∈ Word 𝑇 ( 𝑡 = ( 𝐺 Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ) )
13		iotaex	⊢ ( ℩ 𝑠 ∃ 𝑤 ∈ Word 𝑇 ( 𝑃 = ( 𝐺 Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ) ∈ V
14	7 12 13	fvmpt	⊢ ( 𝑃 ∈ dom 𝑁 → ( 𝑁 ‘ 𝑃 ) = ( ℩ 𝑠 ∃ 𝑤 ∈ Word 𝑇 ( 𝑃 = ( 𝐺 Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ) )