Theorem 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	⊢ 𝑃 = ( Base ‘ ( SymGrp ‘ 𝑁 ) )
	copsgndif.s	⊢ 𝑆 = ( pmSgn ‘ 𝑁 )
	copsgndif.z	⊢ 𝑍 = ( pmSgn ‘ ( 𝑁 ∖ { 𝐾 } ) )
Assertion	copsgndif	⊢ ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) → ( 𝑄 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } → ( ( 𝑌 ∘ 𝑍 ) ‘ ( 𝑄 ↾ ( 𝑁 ∖ { 𝐾 } ) ) ) = ( ( 𝑌 ∘ 𝑆 ) ‘ 𝑄 ) ) )

Proof

Step	Hyp	Ref	Expression
1		copsgndif.p	⊢ 𝑃 = ( Base ‘ ( SymGrp ‘ 𝑁 ) )
2		copsgndif.s	⊢ 𝑆 = ( pmSgn ‘ 𝑁 )
3		copsgndif.z	⊢ 𝑍 = ( pmSgn ‘ ( 𝑁 ∖ { 𝐾 } ) )
4	1 2 3	psgndif	⊢ ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) → ( 𝑄 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } → ( 𝑍 ‘ ( 𝑄 ↾ ( 𝑁 ∖ { 𝐾 } ) ) ) = ( 𝑆 ‘ 𝑄 ) ) )
5	4	imp	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑄 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ) → ( 𝑍 ‘ ( 𝑄 ↾ ( 𝑁 ∖ { 𝐾 } ) ) ) = ( 𝑆 ‘ 𝑄 ) )
6	5	fveq2d	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑄 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ) → ( 𝑌 ‘ ( 𝑍 ‘ ( 𝑄 ↾ ( 𝑁 ∖ { 𝐾 } ) ) ) ) = ( 𝑌 ‘ ( 𝑆 ‘ 𝑄 ) ) )
7		diffi	⊢ ( 𝑁 ∈ Fin → ( 𝑁 ∖ { 𝐾 } ) ∈ Fin )
8	7	ad2antrr	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑄 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ) → ( 𝑁 ∖ { 𝐾 } ) ∈ Fin )
9		eqid	⊢ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } = { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 }
10		eqid	⊢ ( Base ‘ ( SymGrp ‘ ( 𝑁 ∖ { 𝐾 } ) ) ) = ( Base ‘ ( SymGrp ‘ ( 𝑁 ∖ { 𝐾 } ) ) )
11		eqid	⊢ ( 𝑁 ∖ { 𝐾 } ) = ( 𝑁 ∖ { 𝐾 } )
12	1 9 10 11	symgfixelsi	⊢ ( ( 𝐾 ∈ 𝑁 ∧ 𝑄 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ) → ( 𝑄 ↾ ( 𝑁 ∖ { 𝐾 } ) ) ∈ ( Base ‘ ( SymGrp ‘ ( 𝑁 ∖ { 𝐾 } ) ) ) )
13	12	adantll	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑄 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ) → ( 𝑄 ↾ ( 𝑁 ∖ { 𝐾 } ) ) ∈ ( Base ‘ ( SymGrp ‘ ( 𝑁 ∖ { 𝐾 } ) ) ) )
14	10 3	cofipsgn	⊢ ( ( ( 𝑁 ∖ { 𝐾 } ) ∈ Fin ∧ ( 𝑄 ↾ ( 𝑁 ∖ { 𝐾 } ) ) ∈ ( Base ‘ ( SymGrp ‘ ( 𝑁 ∖ { 𝐾 } ) ) ) ) → ( ( 𝑌 ∘ 𝑍 ) ‘ ( 𝑄 ↾ ( 𝑁 ∖ { 𝐾 } ) ) ) = ( 𝑌 ‘ ( 𝑍 ‘ ( 𝑄 ↾ ( 𝑁 ∖ { 𝐾 } ) ) ) ) )
15	8 13 14	syl2anc	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑄 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ) → ( ( 𝑌 ∘ 𝑍 ) ‘ ( 𝑄 ↾ ( 𝑁 ∖ { 𝐾 } ) ) ) = ( 𝑌 ‘ ( 𝑍 ‘ ( 𝑄 ↾ ( 𝑁 ∖ { 𝐾 } ) ) ) ) )
16		elrabi	⊢ ( 𝑄 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } → 𝑄 ∈ 𝑃 )
17	1 2	cofipsgn	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑄 ∈ 𝑃 ) → ( ( 𝑌 ∘ 𝑆 ) ‘ 𝑄 ) = ( 𝑌 ‘ ( 𝑆 ‘ 𝑄 ) ) )
18	16 17	sylan2	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑄 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ) → ( ( 𝑌 ∘ 𝑆 ) ‘ 𝑄 ) = ( 𝑌 ‘ ( 𝑆 ‘ 𝑄 ) ) )
19	18	adantlr	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑄 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ) → ( ( 𝑌 ∘ 𝑆 ) ‘ 𝑄 ) = ( 𝑌 ‘ ( 𝑆 ‘ 𝑄 ) ) )
20	6 15 19	3eqtr4d	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑄 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ) → ( ( 𝑌 ∘ 𝑍 ) ‘ ( 𝑄 ↾ ( 𝑁 ∖ { 𝐾 } ) ) ) = ( ( 𝑌 ∘ 𝑆 ) ‘ 𝑄 ) )
21	20	ex	⊢ ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) → ( 𝑄 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } → ( ( 𝑌 ∘ 𝑍 ) ‘ ( 𝑄 ↾ ( 𝑁 ∖ { 𝐾 } ) ) ) = ( ( 𝑌 ∘ 𝑆 ) ‘ 𝑄 ) ) )