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

Metamath Proof Explorer

Theorem psgndif

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

Ref Expression
Hypotheses psgndif.p ⊢ 𝑃 = ( Base ‘ ( SymGrp ‘ 𝑁 ) )
psgndif.s ⊢ 𝑆 = ( pmSgn ‘ 𝑁 )
psgndif.z ⊢ 𝑍 = ( pmSgn ‘ ( 𝑁 ∖ { 𝐾 } ) )
Assertion psgndif ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) → ( 𝑄 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } → ( 𝑍 ‘ ( 𝑄 ↾ ( 𝑁 ∖ { 𝐾 } ) ) ) = ( 𝑆 ‘ 𝑄 ) ) )

Proof

Step Hyp Ref Expression
1 psgndif.p ⊢ 𝑃 = ( Base ‘ ( SymGrp ‘ 𝑁 ) )
2 psgndif.s ⊢ 𝑆 = ( pmSgn ‘ 𝑁 )
3 psgndif.z ⊢ 𝑍 = ( pmSgn ‘ ( 𝑁 ∖ { 𝐾 } ) )
4 eqid ⊢ ran ( pmTrsp ‘ ( 𝑁 ∖ { 𝐾 } ) ) = ran ( pmTrsp ‘ ( 𝑁 ∖ { 𝐾 } ) )
5 eqid ⊢ ( SymGrp ‘ ( 𝑁 ∖ { 𝐾 } ) ) = ( SymGrp ‘ ( 𝑁 ∖ { 𝐾 } ) )
6 eqid ⊢ ( SymGrp ‘ 𝑁 ) = ( SymGrp ‘ 𝑁 )
7 eqid ⊢ ran ( pmTrsp ‘ 𝑁 ) = ran ( pmTrsp ‘ 𝑁 )
8 1 4 5 6 7 psgnfix2 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) → ( 𝑄 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } → ∃ 𝑟 ∈ Word ran ( pmTrsp ‘ 𝑁 ) 𝑄 = ( ( SymGrp ‘ 𝑁 ) Σg 𝑟 ) ) )
9 8 imp ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑄 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ) → ∃ 𝑟 ∈ Word ran ( pmTrsp ‘ 𝑁 ) 𝑄 = ( ( SymGrp ‘ 𝑁 ) Σg 𝑟 ) )
10 9 ad2antrr ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑄 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ) ∧ 𝑤 ∈ Word ran ( pmTrsp ‘ ( 𝑁 ∖ { 𝐾 } ) ) ) ∧ ( ( 𝑄 ↾ ( 𝑁 ∖ { 𝐾 } ) ) = ( ( SymGrp ‘ ( 𝑁 ∖ { 𝐾 } ) ) Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ) → ∃ 𝑟 ∈ Word ran ( pmTrsp ‘ 𝑁 ) 𝑄 = ( ( SymGrp ‘ 𝑁 ) Σg 𝑟 ) )
11 1 4 5 6 7 psgndiflemA ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑄 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ) → ( ( 𝑤 ∈ Word ran ( pmTrsp ‘ ( 𝑁 ∖ { 𝐾 } ) ) ∧ ( 𝑄 ↾ ( 𝑁 ∖ { 𝐾 } ) ) = ( ( SymGrp ‘ ( 𝑁 ∖ { 𝐾 } ) ) Σg 𝑤 ) ∧ 𝑟 ∈ Word ran ( pmTrsp ‘ 𝑁 ) ) → ( 𝑄 = ( ( SymGrp ‘ 𝑁 ) Σg 𝑟 ) → ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) = ( - 1 ↑ ( ♯ ‘ 𝑟 ) ) ) ) )
12 11 imp ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑄 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ) ∧ ( 𝑤 ∈ Word ran ( pmTrsp ‘ ( 𝑁 ∖ { 𝐾 } ) ) ∧ ( 𝑄 ↾ ( 𝑁 ∖ { 𝐾 } ) ) = ( ( SymGrp ‘ ( 𝑁 ∖ { 𝐾 } ) ) Σg 𝑤 ) ∧ 𝑟 ∈ Word ran ( pmTrsp ‘ 𝑁 ) ) ) → ( 𝑄 = ( ( SymGrp ‘ 𝑁 ) Σg 𝑟 ) → ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) = ( - 1 ↑ ( ♯ ‘ 𝑟 ) ) ) )
13 12 3anassrs ⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑄 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ) ∧ 𝑤 ∈ Word ran ( pmTrsp ‘ ( 𝑁 ∖ { 𝐾 } ) ) ) ∧ ( 𝑄 ↾ ( 𝑁 ∖ { 𝐾 } ) ) = ( ( SymGrp ‘ ( 𝑁 ∖ { 𝐾 } ) ) Σg 𝑤 ) ) ∧ 𝑟 ∈ Word ran ( pmTrsp ‘ 𝑁 ) ) → ( 𝑄 = ( ( SymGrp ‘ 𝑁 ) Σg 𝑟 ) → ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) = ( - 1 ↑ ( ♯ ‘ 𝑟 ) ) ) )
14 13 adantlrr ⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑄 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ) ∧ 𝑤 ∈ Word ran ( pmTrsp ‘ ( 𝑁 ∖ { 𝐾 } ) ) ) ∧ ( ( 𝑄 ↾ ( 𝑁 ∖ { 𝐾 } ) ) = ( ( SymGrp ‘ ( 𝑁 ∖ { 𝐾 } ) ) Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ) ∧ 𝑟 ∈ Word ran ( pmTrsp ‘ 𝑁 ) ) → ( 𝑄 = ( ( SymGrp ‘ 𝑁 ) Σg 𝑟 ) → ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) = ( - 1 ↑ ( ♯ ‘ 𝑟 ) ) ) )
15 eqeq1 ⊢ ( 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) → ( 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑟 ) ) ↔ ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) = ( - 1 ↑ ( ♯ ‘ 𝑟 ) ) ) )
16 15 ad2antll ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑄 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ) ∧ 𝑤 ∈ Word ran ( pmTrsp ‘ ( 𝑁 ∖ { 𝐾 } ) ) ) ∧ ( ( 𝑄 ↾ ( 𝑁 ∖ { 𝐾 } ) ) = ( ( SymGrp ‘ ( 𝑁 ∖ { 𝐾 } ) ) Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ) → ( 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑟 ) ) ↔ ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) = ( - 1 ↑ ( ♯ ‘ 𝑟 ) ) ) )
17 16 adantr ⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑄 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ) ∧ 𝑤 ∈ Word ran ( pmTrsp ‘ ( 𝑁 ∖ { 𝐾 } ) ) ) ∧ ( ( 𝑄 ↾ ( 𝑁 ∖ { 𝐾 } ) ) = ( ( SymGrp ‘ ( 𝑁 ∖ { 𝐾 } ) ) Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ) ∧ 𝑟 ∈ Word ran ( pmTrsp ‘ 𝑁 ) ) → ( 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑟 ) ) ↔ ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) = ( - 1 ↑ ( ♯ ‘ 𝑟 ) ) ) )
18 14 17 sylibrd ⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑄 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ) ∧ 𝑤 ∈ Word ran ( pmTrsp ‘ ( 𝑁 ∖ { 𝐾 } ) ) ) ∧ ( ( 𝑄 ↾ ( 𝑁 ∖ { 𝐾 } ) ) = ( ( SymGrp ‘ ( 𝑁 ∖ { 𝐾 } ) ) Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ) ∧ 𝑟 ∈ Word ran ( pmTrsp ‘ 𝑁 ) ) → ( 𝑄 = ( ( SymGrp ‘ 𝑁 ) Σg 𝑟 ) → 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑟 ) ) ) )
19 18 ralrimiva ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑄 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ) ∧ 𝑤 ∈ Word ran ( pmTrsp ‘ ( 𝑁 ∖ { 𝐾 } ) ) ) ∧ ( ( 𝑄 ↾ ( 𝑁 ∖ { 𝐾 } ) ) = ( ( SymGrp ‘ ( 𝑁 ∖ { 𝐾 } ) ) Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ) → ∀ 𝑟 ∈ Word ran ( pmTrsp ‘ 𝑁 ) ( 𝑄 = ( ( SymGrp ‘ 𝑁 ) Σg 𝑟 ) → 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑟 ) ) ) )
20 10 19 r19.29imd ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑄 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ) ∧ 𝑤 ∈ Word ran ( pmTrsp ‘ ( 𝑁 ∖ { 𝐾 } ) ) ) ∧ ( ( 𝑄 ↾ ( 𝑁 ∖ { 𝐾 } ) ) = ( ( SymGrp ‘ ( 𝑁 ∖ { 𝐾 } ) ) Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ) → ∃ 𝑟 ∈ Word ran ( pmTrsp ‘ 𝑁 ) ( 𝑄 = ( ( SymGrp ‘ 𝑁 ) Σg 𝑟 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑟 ) ) ) )
21 20 rexlimdva2 ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑄 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ) → ( ∃ 𝑤 ∈ Word ran ( pmTrsp ‘ ( 𝑁 ∖ { 𝐾 } ) ) ( ( 𝑄 ↾ ( 𝑁 ∖ { 𝐾 } ) ) = ( ( SymGrp ‘ ( 𝑁 ∖ { 𝐾 } ) ) Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) → ∃ 𝑟 ∈ Word ran ( pmTrsp ‘ 𝑁 ) ( 𝑄 = ( ( SymGrp ‘ 𝑁 ) Σg 𝑟 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑟 ) ) ) ) )
22 1 4 5 psgnfix1 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) → ( 𝑄 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } → ∃ 𝑤 ∈ Word ran ( pmTrsp ‘ ( 𝑁 ∖ { 𝐾 } ) ) ( 𝑄 ↾ ( 𝑁 ∖ { 𝐾 } ) ) = ( ( SymGrp ‘ ( 𝑁 ∖ { 𝐾 } ) ) Σg 𝑤 ) ) )
23 22 imp ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑄 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ) → ∃ 𝑤 ∈ Word ran ( pmTrsp ‘ ( 𝑁 ∖ { 𝐾 } ) ) ( 𝑄 ↾ ( 𝑁 ∖ { 𝐾 } ) ) = ( ( SymGrp ‘ ( 𝑁 ∖ { 𝐾 } ) ) Σg 𝑤 ) )
24 23 ad2antrr ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑄 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ) ∧ 𝑟 ∈ Word ran ( pmTrsp ‘ 𝑁 ) ) ∧ ( 𝑄 = ( ( SymGrp ‘ 𝑁 ) Σg 𝑟 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑟 ) ) ) ) → ∃ 𝑤 ∈ Word ran ( pmTrsp ‘ ( 𝑁 ∖ { 𝐾 } ) ) ( 𝑄 ↾ ( 𝑁 ∖ { 𝐾 } ) ) = ( ( SymGrp ‘ ( 𝑁 ∖ { 𝐾 } ) ) Σg 𝑤 ) )
25 simp-4l ⊢ ( ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑄 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ) ∧ 𝑟 ∈ Word ran ( pmTrsp ‘ 𝑁 ) ) ∧ 𝑄 = ( ( SymGrp ‘ 𝑁 ) Σg 𝑟 ) ) ∧ 𝑤 ∈ Word ran ( pmTrsp ‘ ( 𝑁 ∖ { 𝐾 } ) ) ) ∧ ( 𝑄 ↾ ( 𝑁 ∖ { 𝐾 } ) ) = ( ( SymGrp ‘ ( 𝑁 ∖ { 𝐾 } ) ) Σg 𝑤 ) ) → ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑄 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ) )
26 simpr ⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑄 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ) ∧ 𝑟 ∈ Word ran ( pmTrsp ‘ 𝑁 ) ) ∧ 𝑄 = ( ( SymGrp ‘ 𝑁 ) Σg 𝑟 ) ) ∧ 𝑤 ∈ Word ran ( pmTrsp ‘ ( 𝑁 ∖ { 𝐾 } ) ) ) → 𝑤 ∈ Word ran ( pmTrsp ‘ ( 𝑁 ∖ { 𝐾 } ) ) )
27 26 adantr ⊢ ( ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑄 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ) ∧ 𝑟 ∈ Word ran ( pmTrsp ‘ 𝑁 ) ) ∧ 𝑄 = ( ( SymGrp ‘ 𝑁 ) Σg 𝑟 ) ) ∧ 𝑤 ∈ Word ran ( pmTrsp ‘ ( 𝑁 ∖ { 𝐾 } ) ) ) ∧ ( 𝑄 ↾ ( 𝑁 ∖ { 𝐾 } ) ) = ( ( SymGrp ‘ ( 𝑁 ∖ { 𝐾 } ) ) Σg 𝑤 ) ) → 𝑤 ∈ Word ran ( pmTrsp ‘ ( 𝑁 ∖ { 𝐾 } ) ) )
28 simpr ⊢ ( ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑄 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ) ∧ 𝑟 ∈ Word ran ( pmTrsp ‘ 𝑁 ) ) ∧ 𝑄 = ( ( SymGrp ‘ 𝑁 ) Σg 𝑟 ) ) ∧ 𝑤 ∈ Word ran ( pmTrsp ‘ ( 𝑁 ∖ { 𝐾 } ) ) ) ∧ ( 𝑄 ↾ ( 𝑁 ∖ { 𝐾 } ) ) = ( ( SymGrp ‘ ( 𝑁 ∖ { 𝐾 } ) ) Σg 𝑤 ) ) → ( 𝑄 ↾ ( 𝑁 ∖ { 𝐾 } ) ) = ( ( SymGrp ‘ ( 𝑁 ∖ { 𝐾 } ) ) Σg 𝑤 ) )
29 simp-4r ⊢ ( ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑄 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ) ∧ 𝑟 ∈ Word ran ( pmTrsp ‘ 𝑁 ) ) ∧ 𝑄 = ( ( SymGrp ‘ 𝑁 ) Σg 𝑟 ) ) ∧ 𝑤 ∈ Word ran ( pmTrsp ‘ ( 𝑁 ∖ { 𝐾 } ) ) ) ∧ ( 𝑄 ↾ ( 𝑁 ∖ { 𝐾 } ) ) = ( ( SymGrp ‘ ( 𝑁 ∖ { 𝐾 } ) ) Σg 𝑤 ) ) → 𝑟 ∈ Word ran ( pmTrsp ‘ 𝑁 ) )
30 27 28 29 3jca ⊢ ( ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑄 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ) ∧ 𝑟 ∈ Word ran ( pmTrsp ‘ 𝑁 ) ) ∧ 𝑄 = ( ( SymGrp ‘ 𝑁 ) Σg 𝑟 ) ) ∧ 𝑤 ∈ Word ran ( pmTrsp ‘ ( 𝑁 ∖ { 𝐾 } ) ) ) ∧ ( 𝑄 ↾ ( 𝑁 ∖ { 𝐾 } ) ) = ( ( SymGrp ‘ ( 𝑁 ∖ { 𝐾 } ) ) Σg 𝑤 ) ) → ( 𝑤 ∈ Word ran ( pmTrsp ‘ ( 𝑁 ∖ { 𝐾 } ) ) ∧ ( 𝑄 ↾ ( 𝑁 ∖ { 𝐾 } ) ) = ( ( SymGrp ‘ ( 𝑁 ∖ { 𝐾 } ) ) Σg 𝑤 ) ∧ 𝑟 ∈ Word ran ( pmTrsp ‘ 𝑁 ) ) )
31 simpr ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑄 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ) ∧ 𝑟 ∈ Word ran ( pmTrsp ‘ 𝑁 ) ) ∧ 𝑄 = ( ( SymGrp ‘ 𝑁 ) Σg 𝑟 ) ) → 𝑄 = ( ( SymGrp ‘ 𝑁 ) Σg 𝑟 ) )
32 31 ad2antrr ⊢ ( ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑄 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ) ∧ 𝑟 ∈ Word ran ( pmTrsp ‘ 𝑁 ) ) ∧ 𝑄 = ( ( SymGrp ‘ 𝑁 ) Σg 𝑟 ) ) ∧ 𝑤 ∈ Word ran ( pmTrsp ‘ ( 𝑁 ∖ { 𝐾 } ) ) ) ∧ ( 𝑄 ↾ ( 𝑁 ∖ { 𝐾 } ) ) = ( ( SymGrp ‘ ( 𝑁 ∖ { 𝐾 } ) ) Σg 𝑤 ) ) → 𝑄 = ( ( SymGrp ‘ 𝑁 ) Σg 𝑟 ) )
33 25 30 32 11 syl3c ⊢ ( ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑄 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ) ∧ 𝑟 ∈ Word ran ( pmTrsp ‘ 𝑁 ) ) ∧ 𝑄 = ( ( SymGrp ‘ 𝑁 ) Σg 𝑟 ) ) ∧ 𝑤 ∈ Word ran ( pmTrsp ‘ ( 𝑁 ∖ { 𝐾 } ) ) ) ∧ ( 𝑄 ↾ ( 𝑁 ∖ { 𝐾 } ) ) = ( ( SymGrp ‘ ( 𝑁 ∖ { 𝐾 } ) ) Σg 𝑤 ) ) → ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) = ( - 1 ↑ ( ♯ ‘ 𝑟 ) ) )
34 33 eqcomd ⊢ ( ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑄 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ) ∧ 𝑟 ∈ Word ran ( pmTrsp ‘ 𝑁 ) ) ∧ 𝑄 = ( ( SymGrp ‘ 𝑁 ) Σg 𝑟 ) ) ∧ 𝑤 ∈ Word ran ( pmTrsp ‘ ( 𝑁 ∖ { 𝐾 } ) ) ) ∧ ( 𝑄 ↾ ( 𝑁 ∖ { 𝐾 } ) ) = ( ( SymGrp ‘ ( 𝑁 ∖ { 𝐾 } ) ) Σg 𝑤 ) ) → ( - 1 ↑ ( ♯ ‘ 𝑟 ) ) = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) )
35 34 ex ⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑄 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ) ∧ 𝑟 ∈ Word ran ( pmTrsp ‘ 𝑁 ) ) ∧ 𝑄 = ( ( SymGrp ‘ 𝑁 ) Σg 𝑟 ) ) ∧ 𝑤 ∈ Word ran ( pmTrsp ‘ ( 𝑁 ∖ { 𝐾 } ) ) ) → ( ( 𝑄 ↾ ( 𝑁 ∖ { 𝐾 } ) ) = ( ( SymGrp ‘ ( 𝑁 ∖ { 𝐾 } ) ) Σg 𝑤 ) → ( - 1 ↑ ( ♯ ‘ 𝑟 ) ) = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) )
36 35 adantlrr ⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑄 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ) ∧ 𝑟 ∈ Word ran ( pmTrsp ‘ 𝑁 ) ) ∧ ( 𝑄 = ( ( SymGrp ‘ 𝑁 ) Σg 𝑟 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑟 ) ) ) ) ∧ 𝑤 ∈ Word ran ( pmTrsp ‘ ( 𝑁 ∖ { 𝐾 } ) ) ) → ( ( 𝑄 ↾ ( 𝑁 ∖ { 𝐾 } ) ) = ( ( SymGrp ‘ ( 𝑁 ∖ { 𝐾 } ) ) Σg 𝑤 ) → ( - 1 ↑ ( ♯ ‘ 𝑟 ) ) = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) )
37 eqeq1 ⊢ ( 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑟 ) ) → ( 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ↔ ( - 1 ↑ ( ♯ ‘ 𝑟 ) ) = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) )
38 37 ad2antll ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑄 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ) ∧ 𝑟 ∈ Word ran ( pmTrsp ‘ 𝑁 ) ) ∧ ( 𝑄 = ( ( SymGrp ‘ 𝑁 ) Σg 𝑟 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑟 ) ) ) ) → ( 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ↔ ( - 1 ↑ ( ♯ ‘ 𝑟 ) ) = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) )
39 38 adantr ⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑄 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ) ∧ 𝑟 ∈ Word ran ( pmTrsp ‘ 𝑁 ) ) ∧ ( 𝑄 = ( ( SymGrp ‘ 𝑁 ) Σg 𝑟 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑟 ) ) ) ) ∧ 𝑤 ∈ Word ran ( pmTrsp ‘ ( 𝑁 ∖ { 𝐾 } ) ) ) → ( 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ↔ ( - 1 ↑ ( ♯ ‘ 𝑟 ) ) = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) )
40 36 39 sylibrd ⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑄 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ) ∧ 𝑟 ∈ Word ran ( pmTrsp ‘ 𝑁 ) ) ∧ ( 𝑄 = ( ( SymGrp ‘ 𝑁 ) Σg 𝑟 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑟 ) ) ) ) ∧ 𝑤 ∈ Word ran ( pmTrsp ‘ ( 𝑁 ∖ { 𝐾 } ) ) ) → ( ( 𝑄 ↾ ( 𝑁 ∖ { 𝐾 } ) ) = ( ( SymGrp ‘ ( 𝑁 ∖ { 𝐾 } ) ) Σg 𝑤 ) → 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) )
41 40 ralrimiva ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑄 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ) ∧ 𝑟 ∈ Word ran ( pmTrsp ‘ 𝑁 ) ) ∧ ( 𝑄 = ( ( SymGrp ‘ 𝑁 ) Σg 𝑟 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑟 ) ) ) ) → ∀ 𝑤 ∈ Word ran ( pmTrsp ‘ ( 𝑁 ∖ { 𝐾 } ) ) ( ( 𝑄 ↾ ( 𝑁 ∖ { 𝐾 } ) ) = ( ( SymGrp ‘ ( 𝑁 ∖ { 𝐾 } ) ) Σg 𝑤 ) → 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) )
42 24 41 r19.29imd ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑄 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ) ∧ 𝑟 ∈ Word ran ( pmTrsp ‘ 𝑁 ) ) ∧ ( 𝑄 = ( ( SymGrp ‘ 𝑁 ) Σg 𝑟 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑟 ) ) ) ) → ∃ 𝑤 ∈ Word ran ( pmTrsp ‘ ( 𝑁 ∖ { 𝐾 } ) ) ( ( 𝑄 ↾ ( 𝑁 ∖ { 𝐾 } ) ) = ( ( SymGrp ‘ ( 𝑁 ∖ { 𝐾 } ) ) Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) )
43 42 rexlimdva2 ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑄 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ) → ( ∃ 𝑟 ∈ Word ran ( pmTrsp ‘ 𝑁 ) ( 𝑄 = ( ( SymGrp ‘ 𝑁 ) Σg 𝑟 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑟 ) ) ) → ∃ 𝑤 ∈ Word ran ( pmTrsp ‘ ( 𝑁 ∖ { 𝐾 } ) ) ( ( 𝑄 ↾ ( 𝑁 ∖ { 𝐾 } ) ) = ( ( SymGrp ‘ ( 𝑁 ∖ { 𝐾 } ) ) Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ) )
44 21 43 impbid ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑄 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ) → ( ∃ 𝑤 ∈ Word ran ( pmTrsp ‘ ( 𝑁 ∖ { 𝐾 } ) ) ( ( 𝑄 ↾ ( 𝑁 ∖ { 𝐾 } ) ) = ( ( SymGrp ‘ ( 𝑁 ∖ { 𝐾 } ) ) Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ↔ ∃ 𝑟 ∈ Word ran ( pmTrsp ‘ 𝑁 ) ( 𝑄 = ( ( SymGrp ‘ 𝑁 ) Σg 𝑟 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑟 ) ) ) ) )
45 44 iotabidv ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑄 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ) → ( ℩ 𝑠 ∃ 𝑤 ∈ Word ran ( pmTrsp ‘ ( 𝑁 ∖ { 𝐾 } ) ) ( ( 𝑄 ↾ ( 𝑁 ∖ { 𝐾 } ) ) = ( ( SymGrp ‘ ( 𝑁 ∖ { 𝐾 } ) ) Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ) = ( ℩ 𝑠 ∃ 𝑟 ∈ Word ran ( pmTrsp ‘ 𝑁 ) ( 𝑄 = ( ( SymGrp ‘ 𝑁 ) Σg 𝑟 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑟 ) ) ) ) )
46 diffi ⊢ ( 𝑁 ∈ Fin → ( 𝑁 ∖ { 𝐾 } ) ∈ Fin )
47 46 ad2antrr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑄 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ) → ( 𝑁 ∖ { 𝐾 } ) ∈ Fin )
48 eqid ⊢ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } = { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 }
49 eqid ⊢ ( Base ‘ ( SymGrp ‘ ( 𝑁 ∖ { 𝐾 } ) ) ) = ( Base ‘ ( SymGrp ‘ ( 𝑁 ∖ { 𝐾 } ) ) )
50 eqid ⊢ ( 𝑁 ∖ { 𝐾 } ) = ( 𝑁 ∖ { 𝐾 } )
51 1 48 49 50 symgfixelsi ⊢ ( ( 𝐾 ∈ 𝑁 ∧ 𝑄 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ) → ( 𝑄 ↾ ( 𝑁 ∖ { 𝐾 } ) ) ∈ ( Base ‘ ( SymGrp ‘ ( 𝑁 ∖ { 𝐾 } ) ) ) )
52 51 adantll ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑄 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ) → ( 𝑄 ↾ ( 𝑁 ∖ { 𝐾 } ) ) ∈ ( Base ‘ ( SymGrp ‘ ( 𝑁 ∖ { 𝐾 } ) ) ) )
53 5 49 4 3 psgnvalfi ⊢ ( ( ( 𝑁 ∖ { 𝐾 } ) ∈ Fin ∧ ( 𝑄 ↾ ( 𝑁 ∖ { 𝐾 } ) ) ∈ ( Base ‘ ( SymGrp ‘ ( 𝑁 ∖ { 𝐾 } ) ) ) ) → ( 𝑍 ‘ ( 𝑄 ↾ ( 𝑁 ∖ { 𝐾 } ) ) ) = ( ℩ 𝑠 ∃ 𝑤 ∈ Word ran ( pmTrsp ‘ ( 𝑁 ∖ { 𝐾 } ) ) ( ( 𝑄 ↾ ( 𝑁 ∖ { 𝐾 } ) ) = ( ( SymGrp ‘ ( 𝑁 ∖ { 𝐾 } ) ) Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ) )
54 47 52 53 syl2anc ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑄 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ) → ( 𝑍 ‘ ( 𝑄 ↾ ( 𝑁 ∖ { 𝐾 } ) ) ) = ( ℩ 𝑠 ∃ 𝑤 ∈ Word ran ( pmTrsp ‘ ( 𝑁 ∖ { 𝐾 } ) ) ( ( 𝑄 ↾ ( 𝑁 ∖ { 𝐾 } ) ) = ( ( SymGrp ‘ ( 𝑁 ∖ { 𝐾 } ) ) Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ) )
55 simpl ⊢ ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) → 𝑁 ∈ Fin )
56 elrabi ⊢ ( 𝑄 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } → 𝑄 ∈ 𝑃 )
57 6 1 7 2 psgnvalfi ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑄 ∈ 𝑃 ) → ( 𝑆 ‘ 𝑄 ) = ( ℩ 𝑠 ∃ 𝑟 ∈ Word ran ( pmTrsp ‘ 𝑁 ) ( 𝑄 = ( ( SymGrp ‘ 𝑁 ) Σg 𝑟 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑟 ) ) ) ) )
58 55 56 57 syl2an ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑄 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ) → ( 𝑆 ‘ 𝑄 ) = ( ℩ 𝑠 ∃ 𝑟 ∈ Word ran ( pmTrsp ‘ 𝑁 ) ( 𝑄 = ( ( SymGrp ‘ 𝑁 ) Σg 𝑟 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑟 ) ) ) ) )
59 45 54 58 3eqtr4d ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑄 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ) → ( 𝑍 ‘ ( 𝑄 ↾ ( 𝑁 ∖ { 𝐾 } ) ) ) = ( 𝑆 ‘ 𝑄 ) )
60 59 ex ⊢ ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) → ( 𝑄 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } → ( 𝑍 ‘ ( 𝑄 ↾ ( 𝑁 ∖ { 𝐾 } ) ) ) = ( 𝑆 ‘ 𝑄 ) ) )