This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ∧ 𝑄 ∈ 𝑃 ) → ( ( 𝑌 ∘ 𝑆 ) ‘ 𝑄 ) = ( 𝑌 ‘ ( 𝑆 ‘ 𝑄 ) ) )