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

Metamath Proof Explorer

Theorem psgndiflemA

Description: Lemma 2 for psgndif . (Contributed by AV, 31-Jan-2019)

Ref Expression
Hypotheses psgnfix.p ⊢ 𝑃 = ( Base ‘ ( SymGrp ‘ 𝑁 ) )
psgnfix.t ⊢ 𝑇 = ran ( pmTrsp ‘ ( 𝑁 ∖ { 𝐾 } ) )
psgnfix.s ⊢ 𝑆 = ( SymGrp ‘ ( 𝑁 ∖ { 𝐾 } ) )
psgnfix.z ⊢ 𝑍 = ( SymGrp ‘ 𝑁 )
psgnfix.r ⊢ 𝑅 = ran ( pmTrsp ‘ 𝑁 )
Assertion psgndiflemA ( ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑄 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ) → ( ( 𝑊 ∈ Word 𝑇 ∧ ( 𝑄 ↾ ( 𝑁 ∖ { 𝐾 } ) ) = ( 𝑆 Σg 𝑊 ) ∧ 𝑈 ∈ Word 𝑅 ) → ( 𝑄 = ( ( SymGrp ‘ 𝑁 ) Σg 𝑈 ) → ( - 1 ↑ ( ♯ ‘ 𝑊 ) ) = ( - 1 ↑ ( ♯ ‘ 𝑈 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 psgnfix.p ⊢ 𝑃 = ( Base ‘ ( SymGrp ‘ 𝑁 ) )
2 psgnfix.t ⊢ 𝑇 = ran ( pmTrsp ‘ ( 𝑁 ∖ { 𝐾 } ) )
3 psgnfix.s ⊢ 𝑆 = ( SymGrp ‘ ( 𝑁 ∖ { 𝐾 } ) )
4 psgnfix.z ⊢ 𝑍 = ( SymGrp ‘ 𝑁 )
5 psgnfix.r ⊢ 𝑅 = ran ( pmTrsp ‘ 𝑁 )
6 fveq2 ⊢ ( 𝑤 = 𝑊 → ( ♯ ‘ 𝑤 ) = ( ♯ ‘ 𝑊 ) )
7 6 eqeq1d ⊢ ( 𝑤 = 𝑊 → ( ( ♯ ‘ 𝑤 ) = ( ♯ ‘ 𝑟 ) ↔ ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑟 ) ) )
8 6 oveq2d ⊢ ( 𝑤 = 𝑊 → ( 0 ..^ ( ♯ ‘ 𝑤 ) ) = ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
9 fveq1 ⊢ ( 𝑤 = 𝑊 → ( 𝑤 ‘ 𝑖 ) = ( 𝑊 ‘ 𝑖 ) )
10 9 fveq1d ⊢ ( 𝑤 = 𝑊 → ( ( 𝑤 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑊 ‘ 𝑖 ) ‘ 𝑛 ) )
11 10 eqeq1d ⊢ ( 𝑤 = 𝑊 → ( ( ( 𝑤 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑟 ‘ 𝑖 ) ‘ 𝑛 ) ↔ ( ( 𝑊 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑟 ‘ 𝑖 ) ‘ 𝑛 ) ) )
12 11 ralbidv ⊢ ( 𝑤 = 𝑊 → ( ∀ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ( ( 𝑤 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑟 ‘ 𝑖 ) ‘ 𝑛 ) ↔ ∀ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ( ( 𝑊 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑟 ‘ 𝑖 ) ‘ 𝑛 ) ) )
13 12 anbi2d ⊢ ( 𝑤 = 𝑊 → ( ( ( ( 𝑟 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ∧ ∀ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ( ( 𝑤 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑟 ‘ 𝑖 ) ‘ 𝑛 ) ) ↔ ( ( ( 𝑟 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ∧ ∀ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ( ( 𝑊 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑟 ‘ 𝑖 ) ‘ 𝑛 ) ) ) )
14 8 13 raleqbidv ⊢ ( 𝑤 = 𝑊 → ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) ( ( ( 𝑟 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ∧ ∀ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ( ( 𝑤 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑟 ‘ 𝑖 ) ‘ 𝑛 ) ) ↔ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( ( 𝑟 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ∧ ∀ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ( ( 𝑊 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑟 ‘ 𝑖 ) ‘ 𝑛 ) ) ) )
15 7 14 anbi12d ⊢ ( 𝑤 = 𝑊 → ( ( ( ♯ ‘ 𝑤 ) = ( ♯ ‘ 𝑟 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) ( ( ( 𝑟 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ∧ ∀ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ( ( 𝑤 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑟 ‘ 𝑖 ) ‘ 𝑛 ) ) ) ↔ ( ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑟 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( ( 𝑟 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ∧ ∀ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ( ( 𝑊 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑟 ‘ 𝑖 ) ‘ 𝑛 ) ) ) ) )
16 15 rexbidv ⊢ ( 𝑤 = 𝑊 → ( ∃ 𝑟 ∈ Word 𝑅 ( ( ♯ ‘ 𝑤 ) = ( ♯ ‘ 𝑟 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) ( ( ( 𝑟 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ∧ ∀ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ( ( 𝑤 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑟 ‘ 𝑖 ) ‘ 𝑛 ) ) ) ↔ ∃ 𝑟 ∈ Word 𝑅 ( ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑟 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( ( 𝑟 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ∧ ∀ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ( ( 𝑊 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑟 ‘ 𝑖 ) ‘ 𝑛 ) ) ) ) )
17 16 rspccv ⊢ ( ∀ 𝑤 ∈ Word 𝑇 ∃ 𝑟 ∈ Word 𝑅 ( ( ♯ ‘ 𝑤 ) = ( ♯ ‘ 𝑟 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) ( ( ( 𝑟 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ∧ ∀ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ( ( 𝑤 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑟 ‘ 𝑖 ) ‘ 𝑛 ) ) ) → ( 𝑊 ∈ Word 𝑇 → ∃ 𝑟 ∈ Word 𝑅 ( ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑟 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( ( 𝑟 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ∧ ∀ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ( ( 𝑊 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑟 ‘ 𝑖 ) ‘ 𝑛 ) ) ) ) )
18 2 5 pmtrdifwrdel2 ⊢ ( 𝐾 ∈ 𝑁 → ∀ 𝑤 ∈ Word 𝑇 ∃ 𝑟 ∈ Word 𝑅 ( ( ♯ ‘ 𝑤 ) = ( ♯ ‘ 𝑟 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) ( ( ( 𝑟 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ∧ ∀ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ( ( 𝑤 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑟 ‘ 𝑖 ) ‘ 𝑛 ) ) ) )
19 17 18 syl11 ⊢ ( 𝑊 ∈ Word 𝑇 → ( 𝐾 ∈ 𝑁 → ∃ 𝑟 ∈ Word 𝑅 ( ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑟 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( ( 𝑟 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ∧ ∀ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ( ( 𝑊 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑟 ‘ 𝑖 ) ‘ 𝑛 ) ) ) ) )
20 19 3ad2ant1 ⊢ ( ( 𝑊 ∈ Word 𝑇 ∧ ( 𝑄 ↾ ( 𝑁 ∖ { 𝐾 } ) ) = ( 𝑆 Σg 𝑊 ) ∧ 𝑈 ∈ Word 𝑅 ) → ( 𝐾 ∈ 𝑁 → ∃ 𝑟 ∈ Word 𝑅 ( ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑟 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( ( 𝑟 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ∧ ∀ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ( ( 𝑊 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑟 ‘ 𝑖 ) ‘ 𝑛 ) ) ) ) )
21 20 com12 ⊢ ( 𝐾 ∈ 𝑁 → ( ( 𝑊 ∈ Word 𝑇 ∧ ( 𝑄 ↾ ( 𝑁 ∖ { 𝐾 } ) ) = ( 𝑆 Σg 𝑊 ) ∧ 𝑈 ∈ Word 𝑅 ) → ∃ 𝑟 ∈ Word 𝑅 ( ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑟 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( ( 𝑟 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ∧ ∀ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ( ( 𝑊 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑟 ‘ 𝑖 ) ‘ 𝑛 ) ) ) ) )
22 21 ad2antlr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑄 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ) → ( ( 𝑊 ∈ Word 𝑇 ∧ ( 𝑄 ↾ ( 𝑁 ∖ { 𝐾 } ) ) = ( 𝑆 Σg 𝑊 ) ∧ 𝑈 ∈ Word 𝑅 ) → ∃ 𝑟 ∈ Word 𝑅 ( ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑟 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( ( 𝑟 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ∧ ∀ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ( ( 𝑊 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑟 ‘ 𝑖 ) ‘ 𝑛 ) ) ) ) )
23 22 imp ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑄 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ) ∧ ( 𝑊 ∈ Word 𝑇 ∧ ( 𝑄 ↾ ( 𝑁 ∖ { 𝐾 } ) ) = ( 𝑆 Σg 𝑊 ) ∧ 𝑈 ∈ Word 𝑅 ) ) → ∃ 𝑟 ∈ Word 𝑅 ( ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑟 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( ( 𝑟 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ∧ ∀ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ( ( 𝑊 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑟 ‘ 𝑖 ) ‘ 𝑛 ) ) ) )
24 oveq2 ⊢ ( ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑟 ) → ( - 1 ↑ ( ♯ ‘ 𝑊 ) ) = ( - 1 ↑ ( ♯ ‘ 𝑟 ) ) )
25 24 adantr ⊢ ( ( ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑟 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( ( 𝑟 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ∧ ∀ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ( ( 𝑊 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑟 ‘ 𝑖 ) ‘ 𝑛 ) ) ) → ( - 1 ↑ ( ♯ ‘ 𝑊 ) ) = ( - 1 ↑ ( ♯ ‘ 𝑟 ) ) )
26 25 ad3antlr ⊢ ( ( ( ( 𝑟 ∈ Word 𝑅 ∧ ( ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑟 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( ( 𝑟 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ∧ ∀ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ( ( 𝑊 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑟 ‘ 𝑖 ) ‘ 𝑛 ) ) ) ) ∧ ( ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑄 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ) ∧ ( 𝑊 ∈ Word 𝑇 ∧ ( 𝑄 ↾ ( 𝑁 ∖ { 𝐾 } ) ) = ( 𝑆 Σg 𝑊 ) ∧ 𝑈 ∈ Word 𝑅 ) ) ) ∧ 𝑄 = ( ( SymGrp ‘ 𝑁 ) Σg 𝑈 ) ) → ( - 1 ↑ ( ♯ ‘ 𝑊 ) ) = ( - 1 ↑ ( ♯ ‘ 𝑟 ) ) )
27 simplll ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑄 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ) ∧ ( 𝑊 ∈ Word 𝑇 ∧ ( 𝑄 ↾ ( 𝑁 ∖ { 𝐾 } ) ) = ( 𝑆 Σg 𝑊 ) ∧ 𝑈 ∈ Word 𝑅 ) ) → 𝑁 ∈ Fin )
28 27 ad2antlr ⊢ ( ( ( ( 𝑟 ∈ Word 𝑅 ∧ ( ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑟 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( ( 𝑟 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ∧ ∀ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ( ( 𝑊 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑟 ‘ 𝑖 ) ‘ 𝑛 ) ) ) ) ∧ ( ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑄 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ) ∧ ( 𝑊 ∈ Word 𝑇 ∧ ( 𝑄 ↾ ( 𝑁 ∖ { 𝐾 } ) ) = ( 𝑆 Σg 𝑊 ) ∧ 𝑈 ∈ Word 𝑅 ) ) ) ∧ 𝑄 = ( ( SymGrp ‘ 𝑁 ) Σg 𝑈 ) ) → 𝑁 ∈ Fin )
29 simplll ⊢ ( ( ( ( 𝑟 ∈ Word 𝑅 ∧ ( ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑟 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( ( 𝑟 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ∧ ∀ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ( ( 𝑊 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑟 ‘ 𝑖 ) ‘ 𝑛 ) ) ) ) ∧ ( ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑄 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ) ∧ ( 𝑊 ∈ Word 𝑇 ∧ ( 𝑄 ↾ ( 𝑁 ∖ { 𝐾 } ) ) = ( 𝑆 Σg 𝑊 ) ∧ 𝑈 ∈ Word 𝑅 ) ) ) ∧ 𝑄 = ( ( SymGrp ‘ 𝑁 ) Σg 𝑈 ) ) → 𝑟 ∈ Word 𝑅 )
30 simprr3 ⊢ ( ( ( 𝑟 ∈ Word 𝑅 ∧ ( ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑟 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( ( 𝑟 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ∧ ∀ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ( ( 𝑊 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑟 ‘ 𝑖 ) ‘ 𝑛 ) ) ) ) ∧ ( ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑄 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ) ∧ ( 𝑊 ∈ Word 𝑇 ∧ ( 𝑄 ↾ ( 𝑁 ∖ { 𝐾 } ) ) = ( 𝑆 Σg 𝑊 ) ∧ 𝑈 ∈ Word 𝑅 ) ) ) → 𝑈 ∈ Word 𝑅 )
31 30 adantr ⊢ ( ( ( ( 𝑟 ∈ Word 𝑅 ∧ ( ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑟 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( ( 𝑟 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ∧ ∀ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ( ( 𝑊 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑟 ‘ 𝑖 ) ‘ 𝑛 ) ) ) ) ∧ ( ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑄 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ) ∧ ( 𝑊 ∈ Word 𝑇 ∧ ( 𝑄 ↾ ( 𝑁 ∖ { 𝐾 } ) ) = ( 𝑆 Σg 𝑊 ) ∧ 𝑈 ∈ Word 𝑅 ) ) ) ∧ 𝑄 = ( ( SymGrp ‘ 𝑁 ) Σg 𝑈 ) ) → 𝑈 ∈ Word 𝑅 )
32 simplrl ⊢ ( ( ( ( 𝑟 ∈ Word 𝑅 ∧ ( ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑟 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( ( 𝑟 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ∧ ∀ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ( ( 𝑊 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑟 ‘ 𝑖 ) ‘ 𝑛 ) ) ) ) ∧ ( ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑄 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ) ∧ ( 𝑊 ∈ Word 𝑇 ∧ ( 𝑄 ↾ ( 𝑁 ∖ { 𝐾 } ) ) = ( 𝑆 Σg 𝑊 ) ∧ 𝑈 ∈ Word 𝑅 ) ) ) ∧ 𝑄 = ( ( SymGrp ‘ 𝑁 ) Σg 𝑈 ) ) → ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑄 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ) )
33 3simpa ⊢ ( ( 𝑊 ∈ Word 𝑇 ∧ ( 𝑄 ↾ ( 𝑁 ∖ { 𝐾 } ) ) = ( 𝑆 Σg 𝑊 ) ∧ 𝑈 ∈ Word 𝑅 ) → ( 𝑊 ∈ Word 𝑇 ∧ ( 𝑄 ↾ ( 𝑁 ∖ { 𝐾 } ) ) = ( 𝑆 Σg 𝑊 ) ) )
34 33 adantl ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑄 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ) ∧ ( 𝑊 ∈ Word 𝑇 ∧ ( 𝑄 ↾ ( 𝑁 ∖ { 𝐾 } ) ) = ( 𝑆 Σg 𝑊 ) ∧ 𝑈 ∈ Word 𝑅 ) ) → ( 𝑊 ∈ Word 𝑇 ∧ ( 𝑄 ↾ ( 𝑁 ∖ { 𝐾 } ) ) = ( 𝑆 Σg 𝑊 ) ) )
35 34 ad2antlr ⊢ ( ( ( ( 𝑟 ∈ Word 𝑅 ∧ ( ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑟 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( ( 𝑟 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ∧ ∀ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ( ( 𝑊 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑟 ‘ 𝑖 ) ‘ 𝑛 ) ) ) ) ∧ ( ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑄 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ) ∧ ( 𝑊 ∈ Word 𝑇 ∧ ( 𝑄 ↾ ( 𝑁 ∖ { 𝐾 } ) ) = ( 𝑆 Σg 𝑊 ) ∧ 𝑈 ∈ Word 𝑅 ) ) ) ∧ 𝑄 = ( ( SymGrp ‘ 𝑁 ) Σg 𝑈 ) ) → ( 𝑊 ∈ Word 𝑇 ∧ ( 𝑄 ↾ ( 𝑁 ∖ { 𝐾 } ) ) = ( 𝑆 Σg 𝑊 ) ) )
36 simplrl ⊢ ( ( ( 𝑟 ∈ Word 𝑅 ∧ ( ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑟 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( ( 𝑟 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ∧ ∀ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ( ( 𝑊 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑟 ‘ 𝑖 ) ‘ 𝑛 ) ) ) ) ∧ ( ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑄 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ) ∧ ( 𝑊 ∈ Word 𝑇 ∧ ( 𝑄 ↾ ( 𝑁 ∖ { 𝐾 } ) ) = ( 𝑆 Σg 𝑊 ) ∧ 𝑈 ∈ Word 𝑅 ) ) ) → ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑟 ) )
37 36 adantr ⊢ ( ( ( ( 𝑟 ∈ Word 𝑅 ∧ ( ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑟 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( ( 𝑟 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ∧ ∀ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ( ( 𝑊 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑟 ‘ 𝑖 ) ‘ 𝑛 ) ) ) ) ∧ ( ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑄 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ) ∧ ( 𝑊 ∈ Word 𝑇 ∧ ( 𝑄 ↾ ( 𝑁 ∖ { 𝐾 } ) ) = ( 𝑆 Σg 𝑊 ) ∧ 𝑈 ∈ Word 𝑅 ) ) ) ∧ 𝑄 = ( ( SymGrp ‘ 𝑁 ) Σg 𝑈 ) ) → ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑟 ) )
38 simplrr ⊢ ( ( ( 𝑟 ∈ Word 𝑅 ∧ ( ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑟 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( ( 𝑟 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ∧ ∀ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ( ( 𝑊 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑟 ‘ 𝑖 ) ‘ 𝑛 ) ) ) ) ∧ ( ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑄 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ) ∧ ( 𝑊 ∈ Word 𝑇 ∧ ( 𝑄 ↾ ( 𝑁 ∖ { 𝐾 } ) ) = ( 𝑆 Σg 𝑊 ) ∧ 𝑈 ∈ Word 𝑅 ) ) ) → ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( ( 𝑟 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ∧ ∀ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ( ( 𝑊 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑟 ‘ 𝑖 ) ‘ 𝑛 ) ) )
39 38 adantr ⊢ ( ( ( ( 𝑟 ∈ Word 𝑅 ∧ ( ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑟 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( ( 𝑟 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ∧ ∀ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ( ( 𝑊 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑟 ‘ 𝑖 ) ‘ 𝑛 ) ) ) ) ∧ ( ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑄 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ) ∧ ( 𝑊 ∈ Word 𝑇 ∧ ( 𝑄 ↾ ( 𝑁 ∖ { 𝐾 } ) ) = ( 𝑆 Σg 𝑊 ) ∧ 𝑈 ∈ Word 𝑅 ) ) ) ∧ 𝑄 = ( ( SymGrp ‘ 𝑁 ) Σg 𝑈 ) ) → ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( ( 𝑟 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ∧ ∀ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ( ( 𝑊 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑟 ‘ 𝑖 ) ‘ 𝑛 ) ) )
40 1 2 3 4 5 psgndiflemB ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑄 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ) → ( ( 𝑊 ∈ Word 𝑇 ∧ ( 𝑄 ↾ ( 𝑁 ∖ { 𝐾 } ) ) = ( 𝑆 Σg 𝑊 ) ) → ( ( 𝑟 ∈ Word 𝑅 ∧ ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑟 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( ( 𝑟 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ∧ ∀ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ( ( 𝑊 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑟 ‘ 𝑖 ) ‘ 𝑛 ) ) ) → 𝑄 = ( 𝑍 Σg 𝑟 ) ) ) )
41 40 imp31 ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑄 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ) ∧ ( 𝑊 ∈ Word 𝑇 ∧ ( 𝑄 ↾ ( 𝑁 ∖ { 𝐾 } ) ) = ( 𝑆 Σg 𝑊 ) ) ) ∧ ( 𝑟 ∈ Word 𝑅 ∧ ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑟 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( ( 𝑟 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ∧ ∀ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ( ( 𝑊 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑟 ‘ 𝑖 ) ‘ 𝑛 ) ) ) ) → 𝑄 = ( 𝑍 Σg 𝑟 ) )
42 41 eqcomd ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑄 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ) ∧ ( 𝑊 ∈ Word 𝑇 ∧ ( 𝑄 ↾ ( 𝑁 ∖ { 𝐾 } ) ) = ( 𝑆 Σg 𝑊 ) ) ) ∧ ( 𝑟 ∈ Word 𝑅 ∧ ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑟 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( ( 𝑟 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ∧ ∀ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ( ( 𝑊 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑟 ‘ 𝑖 ) ‘ 𝑛 ) ) ) ) → ( 𝑍 Σg 𝑟 ) = 𝑄 )
43 32 35 29 37 39 42 syl23anc ⊢ ( ( ( ( 𝑟 ∈ Word 𝑅 ∧ ( ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑟 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( ( 𝑟 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ∧ ∀ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ( ( 𝑊 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑟 ‘ 𝑖 ) ‘ 𝑛 ) ) ) ) ∧ ( ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑄 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ) ∧ ( 𝑊 ∈ Word 𝑇 ∧ ( 𝑄 ↾ ( 𝑁 ∖ { 𝐾 } ) ) = ( 𝑆 Σg 𝑊 ) ∧ 𝑈 ∈ Word 𝑅 ) ) ) ∧ 𝑄 = ( ( SymGrp ‘ 𝑁 ) Σg 𝑈 ) ) → ( 𝑍 Σg 𝑟 ) = 𝑄 )
44 id ⊢ ( 𝑄 = ( ( SymGrp ‘ 𝑁 ) Σg 𝑈 ) → 𝑄 = ( ( SymGrp ‘ 𝑁 ) Σg 𝑈 ) )
45 4 eqcomi ⊢ ( SymGrp ‘ 𝑁 ) = 𝑍
46 45 oveq1i ⊢ ( ( SymGrp ‘ 𝑁 ) Σg 𝑈 ) = ( 𝑍 Σg 𝑈 )
47 44 46 eqtrdi ⊢ ( 𝑄 = ( ( SymGrp ‘ 𝑁 ) Σg 𝑈 ) → 𝑄 = ( 𝑍 Σg 𝑈 ) )
48 47 adantl ⊢ ( ( ( ( 𝑟 ∈ Word 𝑅 ∧ ( ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑟 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( ( 𝑟 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ∧ ∀ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ( ( 𝑊 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑟 ‘ 𝑖 ) ‘ 𝑛 ) ) ) ) ∧ ( ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑄 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ) ∧ ( 𝑊 ∈ Word 𝑇 ∧ ( 𝑄 ↾ ( 𝑁 ∖ { 𝐾 } ) ) = ( 𝑆 Σg 𝑊 ) ∧ 𝑈 ∈ Word 𝑅 ) ) ) ∧ 𝑄 = ( ( SymGrp ‘ 𝑁 ) Σg 𝑈 ) ) → 𝑄 = ( 𝑍 Σg 𝑈 ) )
49 43 48 eqtrd ⊢ ( ( ( ( 𝑟 ∈ Word 𝑅 ∧ ( ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑟 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( ( 𝑟 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ∧ ∀ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ( ( 𝑊 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑟 ‘ 𝑖 ) ‘ 𝑛 ) ) ) ) ∧ ( ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑄 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ) ∧ ( 𝑊 ∈ Word 𝑇 ∧ ( 𝑄 ↾ ( 𝑁 ∖ { 𝐾 } ) ) = ( 𝑆 Σg 𝑊 ) ∧ 𝑈 ∈ Word 𝑅 ) ) ) ∧ 𝑄 = ( ( SymGrp ‘ 𝑁 ) Σg 𝑈 ) ) → ( 𝑍 Σg 𝑟 ) = ( 𝑍 Σg 𝑈 ) )
50 4 5 28 29 31 49 psgnuni ⊢ ( ( ( ( 𝑟 ∈ Word 𝑅 ∧ ( ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑟 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( ( 𝑟 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ∧ ∀ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ( ( 𝑊 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑟 ‘ 𝑖 ) ‘ 𝑛 ) ) ) ) ∧ ( ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑄 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ) ∧ ( 𝑊 ∈ Word 𝑇 ∧ ( 𝑄 ↾ ( 𝑁 ∖ { 𝐾 } ) ) = ( 𝑆 Σg 𝑊 ) ∧ 𝑈 ∈ Word 𝑅 ) ) ) ∧ 𝑄 = ( ( SymGrp ‘ 𝑁 ) Σg 𝑈 ) ) → ( - 1 ↑ ( ♯ ‘ 𝑟 ) ) = ( - 1 ↑ ( ♯ ‘ 𝑈 ) ) )
51 26 50 eqtrd ⊢ ( ( ( ( 𝑟 ∈ Word 𝑅 ∧ ( ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑟 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( ( 𝑟 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ∧ ∀ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ( ( 𝑊 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑟 ‘ 𝑖 ) ‘ 𝑛 ) ) ) ) ∧ ( ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑄 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ) ∧ ( 𝑊 ∈ Word 𝑇 ∧ ( 𝑄 ↾ ( 𝑁 ∖ { 𝐾 } ) ) = ( 𝑆 Σg 𝑊 ) ∧ 𝑈 ∈ Word 𝑅 ) ) ) ∧ 𝑄 = ( ( SymGrp ‘ 𝑁 ) Σg 𝑈 ) ) → ( - 1 ↑ ( ♯ ‘ 𝑊 ) ) = ( - 1 ↑ ( ♯ ‘ 𝑈 ) ) )
52 51 ex ⊢ ( ( ( 𝑟 ∈ Word 𝑅 ∧ ( ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑟 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( ( 𝑟 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ∧ ∀ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ( ( 𝑊 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑟 ‘ 𝑖 ) ‘ 𝑛 ) ) ) ) ∧ ( ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑄 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ) ∧ ( 𝑊 ∈ Word 𝑇 ∧ ( 𝑄 ↾ ( 𝑁 ∖ { 𝐾 } ) ) = ( 𝑆 Σg 𝑊 ) ∧ 𝑈 ∈ Word 𝑅 ) ) ) → ( 𝑄 = ( ( SymGrp ‘ 𝑁 ) Σg 𝑈 ) → ( - 1 ↑ ( ♯ ‘ 𝑊 ) ) = ( - 1 ↑ ( ♯ ‘ 𝑈 ) ) ) )
53 52 ex ⊢ ( ( 𝑟 ∈ Word 𝑅 ∧ ( ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑟 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( ( 𝑟 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ∧ ∀ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ( ( 𝑊 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑟 ‘ 𝑖 ) ‘ 𝑛 ) ) ) ) → ( ( ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑄 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ) ∧ ( 𝑊 ∈ Word 𝑇 ∧ ( 𝑄 ↾ ( 𝑁 ∖ { 𝐾 } ) ) = ( 𝑆 Σg 𝑊 ) ∧ 𝑈 ∈ Word 𝑅 ) ) → ( 𝑄 = ( ( SymGrp ‘ 𝑁 ) Σg 𝑈 ) → ( - 1 ↑ ( ♯ ‘ 𝑊 ) ) = ( - 1 ↑ ( ♯ ‘ 𝑈 ) ) ) ) )
54 53 rexlimiva ⊢ ( ∃ 𝑟 ∈ Word 𝑅 ( ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑟 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( ( 𝑟 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ∧ ∀ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ( ( 𝑊 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑟 ‘ 𝑖 ) ‘ 𝑛 ) ) ) → ( ( ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑄 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ) ∧ ( 𝑊 ∈ Word 𝑇 ∧ ( 𝑄 ↾ ( 𝑁 ∖ { 𝐾 } ) ) = ( 𝑆 Σg 𝑊 ) ∧ 𝑈 ∈ Word 𝑅 ) ) → ( 𝑄 = ( ( SymGrp ‘ 𝑁 ) Σg 𝑈 ) → ( - 1 ↑ ( ♯ ‘ 𝑊 ) ) = ( - 1 ↑ ( ♯ ‘ 𝑈 ) ) ) ) )
55 23 54 mpcom ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑄 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ) ∧ ( 𝑊 ∈ Word 𝑇 ∧ ( 𝑄 ↾ ( 𝑁 ∖ { 𝐾 } ) ) = ( 𝑆 Σg 𝑊 ) ∧ 𝑈 ∈ Word 𝑅 ) ) → ( 𝑄 = ( ( SymGrp ‘ 𝑁 ) Σg 𝑈 ) → ( - 1 ↑ ( ♯ ‘ 𝑊 ) ) = ( - 1 ↑ ( ♯ ‘ 𝑈 ) ) ) )
56 55 ex ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑄 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ) → ( ( 𝑊 ∈ Word 𝑇 ∧ ( 𝑄 ↾ ( 𝑁 ∖ { 𝐾 } ) ) = ( 𝑆 Σg 𝑊 ) ∧ 𝑈 ∈ Word 𝑅 ) → ( 𝑄 = ( ( SymGrp ‘ 𝑁 ) Σg 𝑈 ) → ( - 1 ↑ ( ♯ ‘ 𝑊 ) ) = ( - 1 ↑ ( ♯ ‘ 𝑈 ) ) ) ) )