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

Metamath Proof Explorer

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 ∧ 𝐾 ∈ 𝑁 ) → ( 𝑄 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } → ( ( 𝑌 ∘ 𝑍 ) ‘ ( 𝑄 ↾ ( 𝑁 ∖ { 𝐾 } ) ) ) = ( ( 𝑌 ∘ 𝑆 ) ‘ 𝑄 ) ) )