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 \in Fin \land Q \in P) \to (Y \circ 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 \in P \| dom (p ∖ I) \in Fin\} = \{p \in P \| dom (p ∖ I) \in Fin\}$
5	3 1 4 2	psgnfn	$⊢ S Fn \{p \in P \| dom (p ∖ I) \in Fin\}$
6		difeq1	$⊢ p = Q \to p ∖ I = Q ∖ I$
7	6	dmeqd	$⊢ p = Q \to dom (p ∖ I) = dom (Q ∖ I)$
8	7	eleq1d	$⊢ p = Q \to (dom (p ∖ I) \in Fin \leftrightarrow dom (Q ∖ I) \in Fin)$
9		simpr	$⊢ (N \in Fin \land Q \in P) \to Q \in P$
10	3 1	sygbasnfpfi	$⊢ (N \in Fin \land Q \in P) \to dom (Q ∖ I) \in Fin$
11	8 9 10	elrabd	$⊢ (N \in Fin \land Q \in P) \to Q \in \{p \in P \| dom (p ∖ I) \in Fin\}$
12		fvco2	$⊢ (S Fn \{p \in P \| dom (p ∖ I) \in Fin\} \land Q \in \{p \in P \| dom (p ∖ I) \in Fin\}) \to (Y \circ S) (Q) = Y (S (Q))$
13	5 11 12	sylancr	$⊢ (N \in Fin \land Q \in P) \to (Y \circ S) (Q) = Y (S (Q))$