Theorem psgnfvalfi

Description: Function definition 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	psgnfvalfi	⊢ ( 𝐷 ∈ 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		eqid	⊢ { 𝑝 ∈ 𝐵 ∣ dom ( 𝑝 ∖ I ) ∈ Fin } = { 𝑝 ∈ 𝐵 ∣ dom ( 𝑝 ∖ I ) ∈ Fin }
6	1 2 5 3 4	psgnfval	⊢ 𝑁 = ( 𝑥 ∈ { 𝑝 ∈ 𝐵 ∣ dom ( 𝑝 ∖ I ) ∈ Fin } ↦ ( ℩ 𝑠 ∃ 𝑤 ∈ Word 𝑇 ( 𝑥 = ( 𝐺 Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ) )
7	1 2	sygbasnfpfi	⊢ ( ( 𝐷 ∈ Fin ∧ 𝑝 ∈ 𝐵 ) → dom ( 𝑝 ∖ I ) ∈ Fin )
8	7	ralrimiva	⊢ ( 𝐷 ∈ Fin → ∀ 𝑝 ∈ 𝐵 dom ( 𝑝 ∖ I ) ∈ Fin )
9		rabid2	⊢ ( 𝐵 = { 𝑝 ∈ 𝐵 ∣ dom ( 𝑝 ∖ I ) ∈ Fin } ↔ ∀ 𝑝 ∈ 𝐵 dom ( 𝑝 ∖ I ) ∈ Fin )
10	8 9	sylibr	⊢ ( 𝐷 ∈ Fin → 𝐵 = { 𝑝 ∈ 𝐵 ∣ dom ( 𝑝 ∖ I ) ∈ Fin } )
11	10	eqcomd	⊢ ( 𝐷 ∈ Fin → { 𝑝 ∈ 𝐵 ∣ dom ( 𝑝 ∖ I ) ∈ Fin } = 𝐵 )
12	11	mpteq1d	⊢ ( 𝐷 ∈ Fin → ( 𝑥 ∈ { 𝑝 ∈ 𝐵 ∣ dom ( 𝑝 ∖ I ) ∈ Fin } ↦ ( ℩ 𝑠 ∃ 𝑤 ∈ Word 𝑇 ( 𝑥 = ( 𝐺 Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ) ) = ( 𝑥 ∈ 𝐵 ↦ ( ℩ 𝑠 ∃ 𝑤 ∈ Word 𝑇 ( 𝑥 = ( 𝐺 Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ) ) )
13	6 12	syl5eq	⊢ ( 𝐷 ∈ Fin → 𝑁 = ( 𝑥 ∈ 𝐵 ↦ ( ℩ 𝑠 ∃ 𝑤 ∈ Word 𝑇 ( 𝑥 = ( 𝐺 Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ) ) )