copsgndif

Description: Embedding of permutation signs restricted to a set without a single element into a ring. (Contributed by AV, 31-Jan-2019) (Revised by AV, 5-Jul-2022)

	Ref	Expression
Hypotheses	copsgndif.p	$⊢ P = {Base}_{SymGrp (N)}$
	copsgndif.s	$⊢ S = pmSgn (N)$
	copsgndif.z	$⊢ Z = pmSgn (N ∖ \{K\})$
Assertion	copsgndif	$⊢ (N \in Fin \land K \in N) \to (Q \in \{q \in P \| q (K) = K\} \to (Y \circ Z) ({Q ↾}_{(N ∖ \{K\})}) = (Y \circ S) (Q))$

Proof

Step	Hyp	Ref	Expression
1		copsgndif.p	$⊢ P = {Base}_{SymGrp (N)}$
2		copsgndif.s	$⊢ S = pmSgn (N)$
3		copsgndif.z	$⊢ Z = pmSgn (N ∖ \{K\})$
4	1 2 3	psgndif	$⊢ (N \in Fin \land K \in N) \to (Q \in \{q \in P \| q (K) = K\} \to Z ({Q ↾}_{(N ∖ \{K\})}) = S (Q))$
5	4	imp	$⊢ ((N \in Fin \land K \in N) \land Q \in \{q \in P \| q (K) = K\}) \to Z ({Q ↾}_{(N ∖ \{K\})}) = S (Q)$
6	5	fveq2d	$⊢ ((N \in Fin \land K \in N) \land Q \in \{q \in P \| q (K) = K\}) \to Y (Z ({Q ↾}_{(N ∖ \{K\})})) = Y (S (Q))$
7		diffi	$⊢ N \in Fin \to N ∖ \{K\} \in Fin$
8	7	ad2antrr	$⊢ ((N \in Fin \land K \in N) \land Q \in \{q \in P \| q (K) = K\}) \to N ∖ \{K\} \in Fin$
9		eqid	$⊢ \{q \in P \| q (K) = K\} = \{q \in P \| q (K) = K\}$
10		eqid	$⊢ {Base}_{SymGrp (N ∖ \{K\})} = {Base}_{SymGrp (N ∖ \{K\})}$
11		eqid	$⊢ N ∖ \{K\} = N ∖ \{K\}$
12	1 9 10 11	symgfixelsi	$⊢ (K \in N \land Q \in \{q \in P \| q (K) = K\}) \to {Q ↾}_{(N ∖ \{K\})} \in {Base}_{SymGrp (N ∖ \{K\})}$
13	12	adantll	$⊢ ((N \in Fin \land K \in N) \land Q \in \{q \in P \| q (K) = K\}) \to {Q ↾}_{(N ∖ \{K\})} \in {Base}_{SymGrp (N ∖ \{K\})}$
14	10 3	cofipsgn	$⊢ (N ∖ \{K\} \in Fin \land {Q ↾}_{(N ∖ \{K\})} \in {Base}_{SymGrp (N ∖ \{K\})}) \to (Y \circ Z) ({Q ↾}_{(N ∖ \{K\})}) = Y (Z ({Q ↾}_{(N ∖ \{K\})}))$
15	8 13 14	syl2anc	$⊢ ((N \in Fin \land K \in N) \land Q \in \{q \in P \| q (K) = K\}) \to (Y \circ Z) ({Q ↾}_{(N ∖ \{K\})}) = Y (Z ({Q ↾}_{(N ∖ \{K\})}))$
16		elrabi	$⊢ Q \in \{q \in P \| q (K) = K\} \to Q \in P$
17	1 2	cofipsgn	$⊢ (N \in Fin \land Q \in P) \to (Y \circ S) (Q) = Y (S (Q))$
18	16 17	sylan2	$⊢ (N \in Fin \land Q \in \{q \in P \| q (K) = K\}) \to (Y \circ S) (Q) = Y (S (Q))$
19	18	adantlr	$⊢ ((N \in Fin \land K \in N) \land Q \in \{q \in P \| q (K) = K\}) \to (Y \circ S) (Q) = Y (S (Q))$
20	6 15 19	3eqtr4d	$⊢ ((N \in Fin \land K \in N) \land Q \in \{q \in P \| q (K) = K\}) \to (Y \circ Z) ({Q ↾}_{(N ∖ \{K\})}) = (Y \circ S) (Q)$
21	20	ex	$⊢ (N \in Fin \land K \in N) \to (Q \in \{q \in P \| q (K) = K\} \to (Y \circ Z) ({Q ↾}_{(N ∖ \{K\})}) = (Y \circ S) (Q))$

Metamath Proof Explorer

Theorem copsgndif

Proof