Theorem cofipsgn

Description: Composition of any class Y and the sign function for a finite permutation. (Contributed by AV, 27-Dec-2018) (Revised by AV, 3-Jul-2022)

	Ref	Expression
Hypotheses	cofipsgn.p	⊢ 𝑃 = ( Base ‘ ( SymGrp ‘ 𝑁 ) )
	cofipsgn.s	⊢ 𝑆 = ( pmSgn ‘ 𝑁 )
Assertion	cofipsgn	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑄 ∈ 𝑃 ) → ( ( 𝑌 ∘ 𝑆 ) ‘ 𝑄 ) = ( 𝑌 ‘ ( 𝑆 ‘ 𝑄 ) ) )

Proof

Step	Hyp	Ref	Expression
1		cofipsgn.p	⊢ 𝑃 = ( Base ‘ ( SymGrp ‘ 𝑁 ) )
2		cofipsgn.s	⊢ 𝑆 = ( pmSgn ‘ 𝑁 )
3		eqid	⊢ ( SymGrp ‘ 𝑁 ) = ( SymGrp ‘ 𝑁 )
4		eqid	⊢ { 𝑝 ∈ 𝑃 ∣ dom ( 𝑝 ∖ I ) ∈ Fin } = { 𝑝 ∈ 𝑃 ∣ dom ( 𝑝 ∖ I ) ∈ Fin }
5	3 1 4 2	psgnfn	⊢ 𝑆 Fn { 𝑝 ∈ 𝑃 ∣ dom ( 𝑝 ∖ I ) ∈ Fin }
6		difeq1	⊢ ( 𝑝 = 𝑄 → ( 𝑝 ∖ I ) = ( 𝑄 ∖ I ) )
7	6	dmeqd	⊢ ( 𝑝 = 𝑄 → dom ( 𝑝 ∖ I ) = dom ( 𝑄 ∖ I ) )
8	7	eleq1d	⊢ ( 𝑝 = 𝑄 → ( dom ( 𝑝 ∖ I ) ∈ Fin ↔ dom ( 𝑄 ∖ I ) ∈ Fin ) )
9		simpr	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑄 ∈ 𝑃 ) → 𝑄 ∈ 𝑃 )
10	3 1	sygbasnfpfi	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑄 ∈ 𝑃 ) → dom ( 𝑄 ∖ I ) ∈ Fin )
11	8 9 10	elrabd	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑄 ∈ 𝑃 ) → 𝑄 ∈ { 𝑝 ∈ 𝑃 ∣ dom ( 𝑝 ∖ I ) ∈ Fin } )
12		fvco2	⊢ ( ( 𝑆 Fn { 𝑝 ∈ 𝑃 ∣ dom ( 𝑝 ∖ I ) ∈ Fin } ∧ 𝑄 ∈ { 𝑝 ∈ 𝑃 ∣ dom ( 𝑝 ∖ I ) ∈ Fin } ) → ( ( 𝑌 ∘ 𝑆 ) ‘ 𝑄 ) = ( 𝑌 ‘ ( 𝑆 ‘ 𝑄 ) ) )
13	5 11 12	sylancr	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑄 ∈ 𝑃 ) → ( ( 𝑌 ∘ 𝑆 ) ‘ 𝑄 ) = ( 𝑌 ‘ ( 𝑆 ‘ 𝑄 ) ) )