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 ⊢ P = Base SymGrp ⁡ N
cofipsgn.s ⊢ S = pmSgn ⁡ N
Assertion cofipsgn ⊢ N ∈ Fin ∧ Q ∈ P → Y ∘ S ⁡ Q = Y ⁡ S ⁡ Q

Proof

Step Hyp Ref Expression
1 cofipsgn.p ⊢ P = Base SymGrp ⁡ N
2 cofipsgn.s ⊢ S = pmSgn ⁡ N
3 eqid ⊢ SymGrp ⁡ N = SymGrp ⁡ N
4 eqid ⊢ p ∈ P | dom ⁡ p ∖ I ∈ Fin = p ∈ P | dom ⁡ p ∖ I ∈ Fin
5 3 1 4 2 psgnfn ⊢ S Fn p ∈ P | dom ⁡ p ∖ I ∈ Fin
6 difeq1 ⊢ p = Q → p ∖ I = Q ∖ I
7 6 dmeqd ⊢ p = Q → dom ⁡ p ∖ I = dom ⁡ Q ∖ I
8 7 eleq1d ⊢ p = Q → dom ⁡ p ∖ I ∈ Fin ↔ dom ⁡ Q ∖ I ∈ Fin
9 simpr ⊢ N ∈ Fin ∧ Q ∈ P → Q ∈ P
10 3 1 sygbasnfpfi ⊢ N ∈ Fin ∧ Q ∈ P → dom ⁡ Q ∖ I ∈ Fin
11 8 9 10 elrabd ⊢ N ∈ Fin ∧ Q ∈ P → Q ∈ p ∈ P | dom ⁡ p ∖ I ∈ Fin
12 fvco2 ⊢ S Fn p ∈ P | dom ⁡ p ∖ I ∈ Fin ∧ Q ∈ p ∈ P | dom ⁡ p ∖ I ∈ Fin → Y ∘ S ⁡ Q = Y ⁡ S ⁡ Q
13 5 11 12 sylancr ⊢ N ∈ Fin ∧ Q ∈ P → Y ∘ S ⁡ Q = Y ⁡ S ⁡ Q