Theorem psgnvalfi

Description: Value of the permutation sign function for permutations of finite sets. (Contributed by AV, 13-Jan-2019)

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

Proof

Step	Hyp	Ref	Expression
1		psgnfvalfi.g	⊢ 𝐺 = ( SymGrp ‘ 𝐷 )
2		psgnfvalfi.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
3		psgnfvalfi.t	⊢ 𝑇 = ran ( pmTrsp ‘ 𝐷 )
4		psgnfvalfi.n	⊢ 𝑁 = ( pmSgn ‘ 𝐷 )
5		simpr	⊢ ( ( 𝐷 ∈ Fin ∧ 𝑃 ∈ 𝐵 ) → 𝑃 ∈ 𝐵 )
6	1 2	sygbasnfpfi	⊢ ( ( 𝐷 ∈ Fin ∧ 𝑃 ∈ 𝐵 ) → dom ( 𝑃 ∖ I ) ∈ Fin )
7	1 4 2	psgneldm	⊢ ( 𝑃 ∈ dom 𝑁 ↔ ( 𝑃 ∈ 𝐵 ∧ dom ( 𝑃 ∖ I ) ∈ Fin ) )
8	5 6 7	sylanbrc	⊢ ( ( 𝐷 ∈ Fin ∧ 𝑃 ∈ 𝐵 ) → 𝑃 ∈ dom 𝑁 )
9	1 3 4	psgnval	⊢ ( 𝑃 ∈ dom 𝑁 → ( 𝑁 ‘ 𝑃 ) = ( ℩ 𝑠 ∃ 𝑤 ∈ Word 𝑇 ( 𝑃 = ( 𝐺 Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ) )
10	8 9	syl	⊢ ( ( 𝐷 ∈ Fin ∧ 𝑃 ∈ 𝐵 ) → ( 𝑁 ‘ 𝑃 ) = ( ℩ 𝑠 ∃ 𝑤 ∈ Word 𝑇 ( 𝑃 = ( 𝐺 Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ) )