Metamath Proof Explorer

Theorem psgndiflemB

Description: Lemma 1 for psgndif . (Contributed by AV, 27-Jan-2019)

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

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 elrabi ⊢ ( 𝑄 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } → 𝑄 ∈ 𝑃 )
7 eqid ⊢ ( SymGrp ‘ 𝑁 ) = ( SymGrp ‘ 𝑁 )
8 7 1 symgbasf ⊢ ( 𝑄 ∈ 𝑃 → 𝑄 : 𝑁 ⟶ 𝑁 )
9 ffn ⊢ ( 𝑄 : 𝑁 ⟶ 𝑁 → 𝑄 Fn 𝑁 )
10 6 8 9 3syl ⊢ ( 𝑄 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } → 𝑄 Fn 𝑁 )
11 10 ad3antlr ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑄 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ) ∧ ( 𝑊 ∈ Word 𝑇 ∧ ( 𝑄 ↾ ( 𝑁 ∖ { 𝐾 } ) ) = ( 𝑆 Σg 𝑊 ) ) ) ∧ ( 𝑈 ∈ Word 𝑅 ∧ ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑈 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( ( 𝑈 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ∧ ∀ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ( ( 𝑊 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑈 ‘ 𝑖 ) ‘ 𝑛 ) ) ) ) → 𝑄 Fn 𝑁 )
12 simpl ⊢ ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) → 𝑁 ∈ Fin )
13 12 adantr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑄 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ) → 𝑁 ∈ Fin )
14 13 adantr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑄 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ) ∧ ( 𝑊 ∈ Word 𝑇 ∧ ( 𝑄 ↾ ( 𝑁 ∖ { 𝐾 } ) ) = ( 𝑆 Σg 𝑊 ) ) ) → 𝑁 ∈ Fin )
15 simp1 ⊢ ( ( 𝑈 ∈ Word 𝑅 ∧ ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑈 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( ( 𝑈 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ∧ ∀ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ( ( 𝑊 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑈 ‘ 𝑖 ) ‘ 𝑛 ) ) ) → 𝑈 ∈ Word 𝑅 )
16 4 eqcomi ⊢ ( SymGrp ‘ 𝑁 ) = 𝑍
17 16 fveq2i ⊢ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) = ( Base ‘ 𝑍 )
18 1 17 eqtri ⊢ 𝑃 = ( Base ‘ 𝑍 )
19 4 18 5 gsmtrcl ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑈 ∈ Word 𝑅 ) → ( 𝑍 Σg 𝑈 ) ∈ 𝑃 )
20 14 15 19 syl2an ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑄 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ) ∧ ( 𝑊 ∈ Word 𝑇 ∧ ( 𝑄 ↾ ( 𝑁 ∖ { 𝐾 } ) ) = ( 𝑆 Σg 𝑊 ) ) ) ∧ ( 𝑈 ∈ Word 𝑅 ∧ ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑈 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( ( 𝑈 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ∧ ∀ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ( ( 𝑊 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑈 ‘ 𝑖 ) ‘ 𝑛 ) ) ) ) → ( 𝑍 Σg 𝑈 ) ∈ 𝑃 )
21 7 1 symgbasf ⊢ ( ( 𝑍 Σg 𝑈 ) ∈ 𝑃 → ( 𝑍 Σg 𝑈 ) : 𝑁 ⟶ 𝑁 )
22 ffn ⊢ ( ( 𝑍 Σg 𝑈 ) : 𝑁 ⟶ 𝑁 → ( 𝑍 Σg 𝑈 ) Fn 𝑁 )
23 20 21 22 3syl ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑄 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ) ∧ ( 𝑊 ∈ Word 𝑇 ∧ ( 𝑄 ↾ ( 𝑁 ∖ { 𝐾 } ) ) = ( 𝑆 Σg 𝑊 ) ) ) ∧ ( 𝑈 ∈ Word 𝑅 ∧ ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑈 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( ( 𝑈 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ∧ ∀ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ( ( 𝑊 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑈 ‘ 𝑖 ) ‘ 𝑛 ) ) ) ) → ( 𝑍 Σg 𝑈 ) Fn 𝑁 )
24 12 ad3antrrr ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑄 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ) ∧ ( 𝑊 ∈ Word 𝑇 ∧ ( 𝑄 ↾ ( 𝑁 ∖ { 𝐾 } ) ) = ( 𝑆 Σg 𝑊 ) ) ) ∧ ( 𝑈 ∈ Word 𝑅 ∧ ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑈 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( ( 𝑈 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ∧ ∀ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ( ( 𝑊 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑈 ‘ 𝑖 ) ‘ 𝑛 ) ) ) ) → 𝑁 ∈ Fin )
25 simpr ⊢ ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) → 𝐾 ∈ 𝑁 )
26 25 ad3antrrr ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑄 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ) ∧ ( 𝑊 ∈ Word 𝑇 ∧ ( 𝑄 ↾ ( 𝑁 ∖ { 𝐾 } ) ) = ( 𝑆 Σg 𝑊 ) ) ) ∧ ( 𝑈 ∈ Word 𝑅 ∧ ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑈 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( ( 𝑈 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ∧ ∀ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ( ( 𝑊 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑈 ‘ 𝑖 ) ‘ 𝑛 ) ) ) ) → 𝐾 ∈ 𝑁 )
27 eqid ⊢ ( Base ‘ 𝑍 ) = ( Base ‘ 𝑍 )
28 5 4 27 symgtrf ⊢ 𝑅 ⊆ ( Base ‘ 𝑍 )
29 sswrd ⊢ ( 𝑅 ⊆ ( Base ‘ 𝑍 ) → Word 𝑅 ⊆ Word ( Base ‘ 𝑍 ) )
30 29 sseld ⊢ ( 𝑅 ⊆ ( Base ‘ 𝑍 ) → ( 𝑈 ∈ Word 𝑅 → 𝑈 ∈ Word ( Base ‘ 𝑍 ) ) )
31 28 30 ax-mp ⊢ ( 𝑈 ∈ Word 𝑅 → 𝑈 ∈ Word ( Base ‘ 𝑍 ) )
32 31 3ad2ant1 ⊢ ( ( 𝑈 ∈ Word 𝑅 ∧ ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑈 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( ( 𝑈 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ∧ ∀ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ( ( 𝑊 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑈 ‘ 𝑖 ) ‘ 𝑛 ) ) ) → 𝑈 ∈ Word ( Base ‘ 𝑍 ) )
33 32 adantl ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑄 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ) ∧ ( 𝑊 ∈ Word 𝑇 ∧ ( 𝑄 ↾ ( 𝑁 ∖ { 𝐾 } ) ) = ( 𝑆 Σg 𝑊 ) ) ) ∧ ( 𝑈 ∈ Word 𝑅 ∧ ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑈 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( ( 𝑈 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ∧ ∀ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ( ( 𝑊 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑈 ‘ 𝑖 ) ‘ 𝑛 ) ) ) ) → 𝑈 ∈ Word ( Base ‘ 𝑍 ) )
34 24 26 33 3jca ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑄 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ) ∧ ( 𝑊 ∈ Word 𝑇 ∧ ( 𝑄 ↾ ( 𝑁 ∖ { 𝐾 } ) ) = ( 𝑆 Σg 𝑊 ) ) ) ∧ ( 𝑈 ∈ Word 𝑅 ∧ ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑈 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( ( 𝑈 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ∧ ∀ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ( ( 𝑊 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑈 ‘ 𝑖 ) ‘ 𝑛 ) ) ) ) → ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ∧ 𝑈 ∈ Word ( Base ‘ 𝑍 ) ) )
35 simpl ⊢ ( ( ( ( 𝑈 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ∧ ∀ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ( ( 𝑊 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑈 ‘ 𝑖 ) ‘ 𝑛 ) ) → ( ( 𝑈 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 )
36 35 ralimi ⊢ ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( ( 𝑈 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ∧ ∀ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ( ( 𝑊 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑈 ‘ 𝑖 ) ‘ 𝑛 ) ) → ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( 𝑈 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 )
37 36 3ad2ant3 ⊢ ( ( 𝑈 ∈ Word 𝑅 ∧ ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑈 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( ( 𝑈 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ∧ ∀ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ( ( 𝑊 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑈 ‘ 𝑖 ) ‘ 𝑛 ) ) ) → ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( 𝑈 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 )
38 37 adantl ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑄 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ) ∧ ( 𝑊 ∈ Word 𝑇 ∧ ( 𝑄 ↾ ( 𝑁 ∖ { 𝐾 } ) ) = ( 𝑆 Σg 𝑊 ) ) ) ∧ ( 𝑈 ∈ Word 𝑅 ∧ ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑈 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( ( 𝑈 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ∧ ∀ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ( ( 𝑊 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑈 ‘ 𝑖 ) ‘ 𝑛 ) ) ) ) → ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( 𝑈 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 )
39 oveq2 ⊢ ( ( ♯ ‘ 𝑈 ) = ( ♯ ‘ 𝑊 ) → ( 0 ..^ ( ♯ ‘ 𝑈 ) ) = ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
40 39 eqcoms ⊢ ( ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑈 ) → ( 0 ..^ ( ♯ ‘ 𝑈 ) ) = ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
41 40 raleqdv ⊢ ( ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑈 ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑈 ) ) ( ( 𝑈 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ↔ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( 𝑈 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ) )
42 41 3ad2ant2 ⊢ ( ( 𝑈 ∈ Word 𝑅 ∧ ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑈 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( ( 𝑈 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ∧ ∀ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ( ( 𝑊 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑈 ‘ 𝑖 ) ‘ 𝑛 ) ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑈 ) ) ( ( 𝑈 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ↔ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( 𝑈 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ) )
43 42 adantl ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑄 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ) ∧ ( 𝑊 ∈ Word 𝑇 ∧ ( 𝑄 ↾ ( 𝑁 ∖ { 𝐾 } ) ) = ( 𝑆 Σg 𝑊 ) ) ) ∧ ( 𝑈 ∈ Word 𝑅 ∧ ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑈 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( ( 𝑈 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ∧ ∀ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ( ( 𝑊 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑈 ‘ 𝑖 ) ‘ 𝑛 ) ) ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑈 ) ) ( ( 𝑈 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ↔ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( 𝑈 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ) )
44 38 43 mpbird ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑄 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ) ∧ ( 𝑊 ∈ Word 𝑇 ∧ ( 𝑄 ↾ ( 𝑁 ∖ { 𝐾 } ) ) = ( 𝑆 Σg 𝑊 ) ) ) ∧ ( 𝑈 ∈ Word 𝑅 ∧ ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑈 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( ( 𝑈 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ∧ ∀ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ( ( 𝑊 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑈 ‘ 𝑖 ) ‘ 𝑛 ) ) ) ) → ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑈 ) ) ( ( 𝑈 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 )
45 4 27 gsmsymgrfix ⊢ ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ∧ 𝑈 ∈ Word ( Base ‘ 𝑍 ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑈 ) ) ( ( 𝑈 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 → ( ( 𝑍 Σg 𝑈 ) ‘ 𝐾 ) = 𝐾 ) )
46 34 44 45 sylc ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑄 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ) ∧ ( 𝑊 ∈ Word 𝑇 ∧ ( 𝑄 ↾ ( 𝑁 ∖ { 𝐾 } ) ) = ( 𝑆 Σg 𝑊 ) ) ) ∧ ( 𝑈 ∈ Word 𝑅 ∧ ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑈 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( ( 𝑈 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ∧ ∀ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ( ( 𝑊 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑈 ‘ 𝑖 ) ‘ 𝑛 ) ) ) ) → ( ( 𝑍 Σg 𝑈 ) ‘ 𝐾 ) = 𝐾 )
47 46 eqcomd ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑄 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ) ∧ ( 𝑊 ∈ Word 𝑇 ∧ ( 𝑄 ↾ ( 𝑁 ∖ { 𝐾 } ) ) = ( 𝑆 Σg 𝑊 ) ) ) ∧ ( 𝑈 ∈ Word 𝑅 ∧ ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑈 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( ( 𝑈 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ∧ ∀ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ( ( 𝑊 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑈 ‘ 𝑖 ) ‘ 𝑛 ) ) ) ) → 𝐾 = ( ( 𝑍 Σg 𝑈 ) ‘ 𝐾 ) )
48 47 adantr ⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑄 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ) ∧ ( 𝑊 ∈ Word 𝑇 ∧ ( 𝑄 ↾ ( 𝑁 ∖ { 𝐾 } ) ) = ( 𝑆 Σg 𝑊 ) ) ) ∧ ( 𝑈 ∈ Word 𝑅 ∧ ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑈 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( ( 𝑈 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ∧ ∀ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ( ( 𝑊 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑈 ‘ 𝑖 ) ‘ 𝑛 ) ) ) ) ∧ 𝑘 = 𝐾 ) → 𝐾 = ( ( 𝑍 Σg 𝑈 ) ‘ 𝐾 ) )
49 fveq2 ⊢ ( 𝑘 = 𝐾 → ( 𝑄 ‘ 𝑘 ) = ( 𝑄 ‘ 𝐾 ) )
50 fveq1 ⊢ ( 𝑞 = 𝑄 → ( 𝑞 ‘ 𝐾 ) = ( 𝑄 ‘ 𝐾 ) )
51 50 eqeq1d ⊢ ( 𝑞 = 𝑄 → ( ( 𝑞 ‘ 𝐾 ) = 𝐾 ↔ ( 𝑄 ‘ 𝐾 ) = 𝐾 ) )
52 51 elrab ⊢ ( 𝑄 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ↔ ( 𝑄 ∈ 𝑃 ∧ ( 𝑄 ‘ 𝐾 ) = 𝐾 ) )
53 52 simprbi ⊢ ( 𝑄 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } → ( 𝑄 ‘ 𝐾 ) = 𝐾 )
54 53 ad3antlr ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑄 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ) ∧ ( 𝑊 ∈ Word 𝑇 ∧ ( 𝑄 ↾ ( 𝑁 ∖ { 𝐾 } ) ) = ( 𝑆 Σg 𝑊 ) ) ) ∧ ( 𝑈 ∈ Word 𝑅 ∧ ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑈 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( ( 𝑈 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ∧ ∀ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ( ( 𝑊 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑈 ‘ 𝑖 ) ‘ 𝑛 ) ) ) ) → ( 𝑄 ‘ 𝐾 ) = 𝐾 )
55 49 54 sylan9eqr ⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑄 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ) ∧ ( 𝑊 ∈ Word 𝑇 ∧ ( 𝑄 ↾ ( 𝑁 ∖ { 𝐾 } ) ) = ( 𝑆 Σg 𝑊 ) ) ) ∧ ( 𝑈 ∈ Word 𝑅 ∧ ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑈 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( ( 𝑈 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ∧ ∀ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ( ( 𝑊 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑈 ‘ 𝑖 ) ‘ 𝑛 ) ) ) ) ∧ 𝑘 = 𝐾 ) → ( 𝑄 ‘ 𝑘 ) = 𝐾 )
56 fveq2 ⊢ ( 𝑘 = 𝐾 → ( ( 𝑍 Σg 𝑈 ) ‘ 𝑘 ) = ( ( 𝑍 Σg 𝑈 ) ‘ 𝐾 ) )
57 56 adantl ⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑄 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ) ∧ ( 𝑊 ∈ Word 𝑇 ∧ ( 𝑄 ↾ ( 𝑁 ∖ { 𝐾 } ) ) = ( 𝑆 Σg 𝑊 ) ) ) ∧ ( 𝑈 ∈ Word 𝑅 ∧ ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑈 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( ( 𝑈 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ∧ ∀ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ( ( 𝑊 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑈 ‘ 𝑖 ) ‘ 𝑛 ) ) ) ) ∧ 𝑘 = 𝐾 ) → ( ( 𝑍 Σg 𝑈 ) ‘ 𝑘 ) = ( ( 𝑍 Σg 𝑈 ) ‘ 𝐾 ) )
58 48 55 57 3eqtr4d ⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑄 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ) ∧ ( 𝑊 ∈ Word 𝑇 ∧ ( 𝑄 ↾ ( 𝑁 ∖ { 𝐾 } ) ) = ( 𝑆 Σg 𝑊 ) ) ) ∧ ( 𝑈 ∈ Word 𝑅 ∧ ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑈 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( ( 𝑈 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ∧ ∀ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ( ( 𝑊 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑈 ‘ 𝑖 ) ‘ 𝑛 ) ) ) ) ∧ 𝑘 = 𝐾 ) → ( 𝑄 ‘ 𝑘 ) = ( ( 𝑍 Σg 𝑈 ) ‘ 𝑘 ) )
59 58 ex ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑄 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ) ∧ ( 𝑊 ∈ Word 𝑇 ∧ ( 𝑄 ↾ ( 𝑁 ∖ { 𝐾 } ) ) = ( 𝑆 Σg 𝑊 ) ) ) ∧ ( 𝑈 ∈ Word 𝑅 ∧ ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑈 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( ( 𝑈 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ∧ ∀ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ( ( 𝑊 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑈 ‘ 𝑖 ) ‘ 𝑛 ) ) ) ) → ( 𝑘 = 𝐾 → ( 𝑄 ‘ 𝑘 ) = ( ( 𝑍 Σg 𝑈 ) ‘ 𝑘 ) ) )
60 59 adantr ⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑄 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ) ∧ ( 𝑊 ∈ Word 𝑇 ∧ ( 𝑄 ↾ ( 𝑁 ∖ { 𝐾 } ) ) = ( 𝑆 Σg 𝑊 ) ) ) ∧ ( 𝑈 ∈ Word 𝑅 ∧ ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑈 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( ( 𝑈 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ∧ ∀ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ( ( 𝑊 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑈 ‘ 𝑖 ) ‘ 𝑛 ) ) ) ) ∧ 𝑘 ∈ 𝑁 ) → ( 𝑘 = 𝐾 → ( 𝑄 ‘ 𝑘 ) = ( ( 𝑍 Σg 𝑈 ) ‘ 𝑘 ) ) )
61 60 com12 ⊢ ( 𝑘 = 𝐾 → ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑄 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ) ∧ ( 𝑊 ∈ Word 𝑇 ∧ ( 𝑄 ↾ ( 𝑁 ∖ { 𝐾 } ) ) = ( 𝑆 Σg 𝑊 ) ) ) ∧ ( 𝑈 ∈ Word 𝑅 ∧ ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑈 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( ( 𝑈 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ∧ ∀ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ( ( 𝑊 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑈 ‘ 𝑖 ) ‘ 𝑛 ) ) ) ) ∧ 𝑘 ∈ 𝑁 ) → ( 𝑄 ‘ 𝑘 ) = ( ( 𝑍 Σg 𝑈 ) ‘ 𝑘 ) ) )
62 fveq1 ⊢ ( ( 𝑄 ↾ ( 𝑁 ∖ { 𝐾 } ) ) = ( 𝑆 Σg 𝑊 ) → ( ( 𝑄 ↾ ( 𝑁 ∖ { 𝐾 } ) ) ‘ 𝑘 ) = ( ( 𝑆 Σg 𝑊 ) ‘ 𝑘 ) )
63 62 adantl ⊢ ( ( 𝑊 ∈ Word 𝑇 ∧ ( 𝑄 ↾ ( 𝑁 ∖ { 𝐾 } ) ) = ( 𝑆 Σg 𝑊 ) ) → ( ( 𝑄 ↾ ( 𝑁 ∖ { 𝐾 } ) ) ‘ 𝑘 ) = ( ( 𝑆 Σg 𝑊 ) ‘ 𝑘 ) )
64 63 ad3antlr ⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑄 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ) ∧ ( 𝑊 ∈ Word 𝑇 ∧ ( 𝑄 ↾ ( 𝑁 ∖ { 𝐾 } ) ) = ( 𝑆 Σg 𝑊 ) ) ) ∧ ( 𝑈 ∈ Word 𝑅 ∧ ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑈 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( ( 𝑈 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ∧ ∀ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ( ( 𝑊 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑈 ‘ 𝑖 ) ‘ 𝑛 ) ) ) ) ∧ 𝑘 ∈ 𝑁 ) → ( ( 𝑄 ↾ ( 𝑁 ∖ { 𝐾 } ) ) ‘ 𝑘 ) = ( ( 𝑆 Σg 𝑊 ) ‘ 𝑘 ) )
65 64 adantl ⊢ ( ( ¬ 𝑘 = 𝐾 ∧ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑄 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ) ∧ ( 𝑊 ∈ Word 𝑇 ∧ ( 𝑄 ↾ ( 𝑁 ∖ { 𝐾 } ) ) = ( 𝑆 Σg 𝑊 ) ) ) ∧ ( 𝑈 ∈ Word 𝑅 ∧ ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑈 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( ( 𝑈 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ∧ ∀ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ( ( 𝑊 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑈 ‘ 𝑖 ) ‘ 𝑛 ) ) ) ) ∧ 𝑘 ∈ 𝑁 ) ) → ( ( 𝑄 ↾ ( 𝑁 ∖ { 𝐾 } ) ) ‘ 𝑘 ) = ( ( 𝑆 Σg 𝑊 ) ‘ 𝑘 ) )
66 simpr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑘 ∈ 𝑁 ) → 𝑘 ∈ 𝑁 )
67 neqne ⊢ ( ¬ 𝑘 = 𝐾 → 𝑘 ≠ 𝐾 )
68 66 67 anim12i ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑘 ∈ 𝑁 ) ∧ ¬ 𝑘 = 𝐾 ) → ( 𝑘 ∈ 𝑁 ∧ 𝑘 ≠ 𝐾 ) )
69 eldifsn ⊢ ( 𝑘 ∈ ( 𝑁 ∖ { 𝐾 } ) ↔ ( 𝑘 ∈ 𝑁 ∧ 𝑘 ≠ 𝐾 ) )
70 68 69 sylibr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑘 ∈ 𝑁 ) ∧ ¬ 𝑘 = 𝐾 ) → 𝑘 ∈ ( 𝑁 ∖ { 𝐾 } ) )
71 70 fvresd ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑘 ∈ 𝑁 ) ∧ ¬ 𝑘 = 𝐾 ) → ( ( 𝑄 ↾ ( 𝑁 ∖ { 𝐾 } ) ) ‘ 𝑘 ) = ( 𝑄 ‘ 𝑘 ) )
72 71 exp31 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) → ( 𝑘 ∈ 𝑁 → ( ¬ 𝑘 = 𝐾 → ( ( 𝑄 ↾ ( 𝑁 ∖ { 𝐾 } ) ) ‘ 𝑘 ) = ( 𝑄 ‘ 𝑘 ) ) ) )
73 72 ad3antrrr ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑄 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ) ∧ ( 𝑊 ∈ Word 𝑇 ∧ ( 𝑄 ↾ ( 𝑁 ∖ { 𝐾 } ) ) = ( 𝑆 Σg 𝑊 ) ) ) ∧ ( 𝑈 ∈ Word 𝑅 ∧ ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑈 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( ( 𝑈 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ∧ ∀ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ( ( 𝑊 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑈 ‘ 𝑖 ) ‘ 𝑛 ) ) ) ) → ( 𝑘 ∈ 𝑁 → ( ¬ 𝑘 = 𝐾 → ( ( 𝑄 ↾ ( 𝑁 ∖ { 𝐾 } ) ) ‘ 𝑘 ) = ( 𝑄 ‘ 𝑘 ) ) ) )
74 73 imp ⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑄 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ) ∧ ( 𝑊 ∈ Word 𝑇 ∧ ( 𝑄 ↾ ( 𝑁 ∖ { 𝐾 } ) ) = ( 𝑆 Σg 𝑊 ) ) ) ∧ ( 𝑈 ∈ Word 𝑅 ∧ ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑈 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( ( 𝑈 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ∧ ∀ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ( ( 𝑊 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑈 ‘ 𝑖 ) ‘ 𝑛 ) ) ) ) ∧ 𝑘 ∈ 𝑁 ) → ( ¬ 𝑘 = 𝐾 → ( ( 𝑄 ↾ ( 𝑁 ∖ { 𝐾 } ) ) ‘ 𝑘 ) = ( 𝑄 ‘ 𝑘 ) ) )
75 74 impcom ⊢ ( ( ¬ 𝑘 = 𝐾 ∧ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑄 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ) ∧ ( 𝑊 ∈ Word 𝑇 ∧ ( 𝑄 ↾ ( 𝑁 ∖ { 𝐾 } ) ) = ( 𝑆 Σg 𝑊 ) ) ) ∧ ( 𝑈 ∈ Word 𝑅 ∧ ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑈 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( ( 𝑈 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ∧ ∀ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ( ( 𝑊 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑈 ‘ 𝑖 ) ‘ 𝑛 ) ) ) ) ∧ 𝑘 ∈ 𝑁 ) ) → ( ( 𝑄 ↾ ( 𝑁 ∖ { 𝐾 } ) ) ‘ 𝑘 ) = ( 𝑄 ‘ 𝑘 ) )
76 fveq2 ⊢ ( 𝑛 = 𝑘 → ( ( 𝑆 Σg 𝑊 ) ‘ 𝑛 ) = ( ( 𝑆 Σg 𝑊 ) ‘ 𝑘 ) )
77 fveq2 ⊢ ( 𝑛 = 𝑘 → ( ( 𝑍 Σg 𝑈 ) ‘ 𝑛 ) = ( ( 𝑍 Σg 𝑈 ) ‘ 𝑘 ) )
78 76 77 eqeq12d ⊢ ( 𝑛 = 𝑘 → ( ( ( 𝑆 Σg 𝑊 ) ‘ 𝑛 ) = ( ( 𝑍 Σg 𝑈 ) ‘ 𝑛 ) ↔ ( ( 𝑆 Σg 𝑊 ) ‘ 𝑘 ) = ( ( 𝑍 Σg 𝑈 ) ‘ 𝑘 ) ) )
79 diffi ⊢ ( 𝑁 ∈ Fin → ( 𝑁 ∖ { 𝐾 } ) ∈ Fin )
80 79 ancri ⊢ ( 𝑁 ∈ Fin → ( ( 𝑁 ∖ { 𝐾 } ) ∈ Fin ∧ 𝑁 ∈ Fin ) )
81 80 adantr ⊢ ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) → ( ( 𝑁 ∖ { 𝐾 } ) ∈ Fin ∧ 𝑁 ∈ Fin ) )
82 81 ad3antrrr ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑄 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ) ∧ ( 𝑊 ∈ Word 𝑇 ∧ ( 𝑄 ↾ ( 𝑁 ∖ { 𝐾 } ) ) = ( 𝑆 Σg 𝑊 ) ) ) ∧ ( 𝑈 ∈ Word 𝑅 ∧ ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑈 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( ( 𝑈 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ∧ ∀ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ( ( 𝑊 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑈 ‘ 𝑖 ) ‘ 𝑛 ) ) ) ) → ( ( 𝑁 ∖ { 𝐾 } ) ∈ Fin ∧ 𝑁 ∈ Fin ) )
83 eqid ⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
84 2 3 83 symgtrf ⊢ 𝑇 ⊆ ( Base ‘ 𝑆 )
85 sswrd ⊢ ( 𝑇 ⊆ ( Base ‘ 𝑆 ) → Word 𝑇 ⊆ Word ( Base ‘ 𝑆 ) )
86 85 sseld ⊢ ( 𝑇 ⊆ ( Base ‘ 𝑆 ) → ( 𝑊 ∈ Word 𝑇 → 𝑊 ∈ Word ( Base ‘ 𝑆 ) ) )
87 84 86 ax-mp ⊢ ( 𝑊 ∈ Word 𝑇 → 𝑊 ∈ Word ( Base ‘ 𝑆 ) )
88 87 ad2antrl ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑄 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ) ∧ ( 𝑊 ∈ Word 𝑇 ∧ ( 𝑄 ↾ ( 𝑁 ∖ { 𝐾 } ) ) = ( 𝑆 Σg 𝑊 ) ) ) → 𝑊 ∈ Word ( Base ‘ 𝑆 ) )
89 88 adantr ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑄 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ) ∧ ( 𝑊 ∈ Word 𝑇 ∧ ( 𝑄 ↾ ( 𝑁 ∖ { 𝐾 } ) ) = ( 𝑆 Σg 𝑊 ) ) ) ∧ ( 𝑈 ∈ Word 𝑅 ∧ ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑈 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( ( 𝑈 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ∧ ∀ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ( ( 𝑊 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑈 ‘ 𝑖 ) ‘ 𝑛 ) ) ) ) → 𝑊 ∈ Word ( Base ‘ 𝑆 ) )
90 simpr2 ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑄 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ) ∧ ( 𝑊 ∈ Word 𝑇 ∧ ( 𝑄 ↾ ( 𝑁 ∖ { 𝐾 } ) ) = ( 𝑆 Σg 𝑊 ) ) ) ∧ ( 𝑈 ∈ Word 𝑅 ∧ ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑈 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( ( 𝑈 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ∧ ∀ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ( ( 𝑊 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑈 ‘ 𝑖 ) ‘ 𝑛 ) ) ) ) → ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑈 ) )
91 89 33 90 3jca ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑄 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ) ∧ ( 𝑊 ∈ Word 𝑇 ∧ ( 𝑄 ↾ ( 𝑁 ∖ { 𝐾 } ) ) = ( 𝑆 Σg 𝑊 ) ) ) ∧ ( 𝑈 ∈ Word 𝑅 ∧ ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑈 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( ( 𝑈 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ∧ ∀ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ( ( 𝑊 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑈 ‘ 𝑖 ) ‘ 𝑛 ) ) ) ) → ( 𝑊 ∈ Word ( Base ‘ 𝑆 ) ∧ 𝑈 ∈ Word ( Base ‘ 𝑍 ) ∧ ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑈 ) ) )
92 82 91 jca ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑄 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ) ∧ ( 𝑊 ∈ Word 𝑇 ∧ ( 𝑄 ↾ ( 𝑁 ∖ { 𝐾 } ) ) = ( 𝑆 Σg 𝑊 ) ) ) ∧ ( 𝑈 ∈ Word 𝑅 ∧ ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑈 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( ( 𝑈 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ∧ ∀ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ( ( 𝑊 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑈 ‘ 𝑖 ) ‘ 𝑛 ) ) ) ) → ( ( ( 𝑁 ∖ { 𝐾 } ) ∈ Fin ∧ 𝑁 ∈ Fin ) ∧ ( 𝑊 ∈ Word ( Base ‘ 𝑆 ) ∧ 𝑈 ∈ Word ( Base ‘ 𝑍 ) ∧ ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑈 ) ) ) )
93 92 ad2antrl ⊢ ( ( ¬ 𝑘 = 𝐾 ∧ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑄 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ) ∧ ( 𝑊 ∈ Word 𝑇 ∧ ( 𝑄 ↾ ( 𝑁 ∖ { 𝐾 } ) ) = ( 𝑆 Σg 𝑊 ) ) ) ∧ ( 𝑈 ∈ Word 𝑅 ∧ ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑈 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( ( 𝑈 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ∧ ∀ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ( ( 𝑊 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑈 ‘ 𝑖 ) ‘ 𝑛 ) ) ) ) ∧ 𝑘 ∈ 𝑁 ) ) → ( ( ( 𝑁 ∖ { 𝐾 } ) ∈ Fin ∧ 𝑁 ∈ Fin ) ∧ ( 𝑊 ∈ Word ( Base ‘ 𝑆 ) ∧ 𝑈 ∈ Word ( Base ‘ 𝑍 ) ∧ ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑈 ) ) ) )
94 simpr ⊢ ( ( ( ( 𝑈 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ∧ ∀ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ( ( 𝑊 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑈 ‘ 𝑖 ) ‘ 𝑛 ) ) → ∀ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ( ( 𝑊 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑈 ‘ 𝑖 ) ‘ 𝑛 ) )
95 94 ralimi ⊢ ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( ( 𝑈 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ∧ ∀ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ( ( 𝑊 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑈 ‘ 𝑖 ) ‘ 𝑛 ) ) → ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ∀ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ( ( 𝑊 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑈 ‘ 𝑖 ) ‘ 𝑛 ) )
96 95 3ad2ant3 ⊢ ( ( 𝑈 ∈ Word 𝑅 ∧ ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑈 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( ( 𝑈 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ∧ ∀ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ( ( 𝑊 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑈 ‘ 𝑖 ) ‘ 𝑛 ) ) ) → ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ∀ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ( ( 𝑊 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑈 ‘ 𝑖 ) ‘ 𝑛 ) )
97 96 adantl ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑄 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ) ∧ ( 𝑊 ∈ Word 𝑇 ∧ ( 𝑄 ↾ ( 𝑁 ∖ { 𝐾 } ) ) = ( 𝑆 Σg 𝑊 ) ) ) ∧ ( 𝑈 ∈ Word 𝑅 ∧ ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑈 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( ( 𝑈 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ∧ ∀ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ( ( 𝑊 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑈 ‘ 𝑖 ) ‘ 𝑛 ) ) ) ) → ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ∀ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ( ( 𝑊 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑈 ‘ 𝑖 ) ‘ 𝑛 ) )
98 97 ad2antrl ⊢ ( ( ¬ 𝑘 = 𝐾 ∧ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑄 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ) ∧ ( 𝑊 ∈ Word 𝑇 ∧ ( 𝑄 ↾ ( 𝑁 ∖ { 𝐾 } ) ) = ( 𝑆 Σg 𝑊 ) ) ) ∧ ( 𝑈 ∈ Word 𝑅 ∧ ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑈 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( ( 𝑈 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ∧ ∀ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ( ( 𝑊 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑈 ‘ 𝑖 ) ‘ 𝑛 ) ) ) ) ∧ 𝑘 ∈ 𝑁 ) ) → ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ∀ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ( ( 𝑊 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑈 ‘ 𝑖 ) ‘ 𝑛 ) )
99 incom ⊢ ( ( 𝑁 ∖ { 𝐾 } ) ∩ 𝑁 ) = ( 𝑁 ∩ ( 𝑁 ∖ { 𝐾 } ) )
100 indif ⊢ ( 𝑁 ∩ ( 𝑁 ∖ { 𝐾 } ) ) = ( 𝑁 ∖ { 𝐾 } )
101 99 100 eqtri ⊢ ( ( 𝑁 ∖ { 𝐾 } ) ∩ 𝑁 ) = ( 𝑁 ∖ { 𝐾 } )
102 101 eqcomi ⊢ ( 𝑁 ∖ { 𝐾 } ) = ( ( 𝑁 ∖ { 𝐾 } ) ∩ 𝑁 )
103 3 83 4 27 102 gsmsymgreq ⊢ ( ( ( ( 𝑁 ∖ { 𝐾 } ) ∈ Fin ∧ 𝑁 ∈ Fin ) ∧ ( 𝑊 ∈ Word ( Base ‘ 𝑆 ) ∧ 𝑈 ∈ Word ( Base ‘ 𝑍 ) ∧ ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑈 ) ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ∀ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ( ( 𝑊 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑈 ‘ 𝑖 ) ‘ 𝑛 ) → ∀ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ( ( 𝑆 Σg 𝑊 ) ‘ 𝑛 ) = ( ( 𝑍 Σg 𝑈 ) ‘ 𝑛 ) ) )
104 93 98 103 sylc ⊢ ( ( ¬ 𝑘 = 𝐾 ∧ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑄 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ) ∧ ( 𝑊 ∈ Word 𝑇 ∧ ( 𝑄 ↾ ( 𝑁 ∖ { 𝐾 } ) ) = ( 𝑆 Σg 𝑊 ) ) ) ∧ ( 𝑈 ∈ Word 𝑅 ∧ ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑈 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( ( 𝑈 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ∧ ∀ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ( ( 𝑊 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑈 ‘ 𝑖 ) ‘ 𝑛 ) ) ) ) ∧ 𝑘 ∈ 𝑁 ) ) → ∀ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ( ( 𝑆 Σg 𝑊 ) ‘ 𝑛 ) = ( ( 𝑍 Σg 𝑈 ) ‘ 𝑛 ) )
105 67 anim2i ⊢ ( ( 𝑘 ∈ 𝑁 ∧ ¬ 𝑘 = 𝐾 ) → ( 𝑘 ∈ 𝑁 ∧ 𝑘 ≠ 𝐾 ) )
106 105 69 sylibr ⊢ ( ( 𝑘 ∈ 𝑁 ∧ ¬ 𝑘 = 𝐾 ) → 𝑘 ∈ ( 𝑁 ∖ { 𝐾 } ) )
107 106 ex ⊢ ( 𝑘 ∈ 𝑁 → ( ¬ 𝑘 = 𝐾 → 𝑘 ∈ ( 𝑁 ∖ { 𝐾 } ) ) )
108 107 adantl ⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑄 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ) ∧ ( 𝑊 ∈ Word 𝑇 ∧ ( 𝑄 ↾ ( 𝑁 ∖ { 𝐾 } ) ) = ( 𝑆 Σg 𝑊 ) ) ) ∧ ( 𝑈 ∈ Word 𝑅 ∧ ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑈 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( ( 𝑈 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ∧ ∀ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ( ( 𝑊 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑈 ‘ 𝑖 ) ‘ 𝑛 ) ) ) ) ∧ 𝑘 ∈ 𝑁 ) → ( ¬ 𝑘 = 𝐾 → 𝑘 ∈ ( 𝑁 ∖ { 𝐾 } ) ) )
109 108 impcom ⊢ ( ( ¬ 𝑘 = 𝐾 ∧ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑄 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ) ∧ ( 𝑊 ∈ Word 𝑇 ∧ ( 𝑄 ↾ ( 𝑁 ∖ { 𝐾 } ) ) = ( 𝑆 Σg 𝑊 ) ) ) ∧ ( 𝑈 ∈ Word 𝑅 ∧ ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑈 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( ( 𝑈 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ∧ ∀ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ( ( 𝑊 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑈 ‘ 𝑖 ) ‘ 𝑛 ) ) ) ) ∧ 𝑘 ∈ 𝑁 ) ) → 𝑘 ∈ ( 𝑁 ∖ { 𝐾 } ) )
110 78 104 109 rspcdva ⊢ ( ( ¬ 𝑘 = 𝐾 ∧ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑄 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ) ∧ ( 𝑊 ∈ Word 𝑇 ∧ ( 𝑄 ↾ ( 𝑁 ∖ { 𝐾 } ) ) = ( 𝑆 Σg 𝑊 ) ) ) ∧ ( 𝑈 ∈ Word 𝑅 ∧ ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑈 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( ( 𝑈 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ∧ ∀ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ( ( 𝑊 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑈 ‘ 𝑖 ) ‘ 𝑛 ) ) ) ) ∧ 𝑘 ∈ 𝑁 ) ) → ( ( 𝑆 Σg 𝑊 ) ‘ 𝑘 ) = ( ( 𝑍 Σg 𝑈 ) ‘ 𝑘 ) )
111 65 75 110 3eqtr3d ⊢ ( ( ¬ 𝑘 = 𝐾 ∧ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑄 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ) ∧ ( 𝑊 ∈ Word 𝑇 ∧ ( 𝑄 ↾ ( 𝑁 ∖ { 𝐾 } ) ) = ( 𝑆 Σg 𝑊 ) ) ) ∧ ( 𝑈 ∈ Word 𝑅 ∧ ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑈 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( ( 𝑈 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ∧ ∀ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ( ( 𝑊 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑈 ‘ 𝑖 ) ‘ 𝑛 ) ) ) ) ∧ 𝑘 ∈ 𝑁 ) ) → ( 𝑄 ‘ 𝑘 ) = ( ( 𝑍 Σg 𝑈 ) ‘ 𝑘 ) )
112 111 ex ⊢ ( ¬ 𝑘 = 𝐾 → ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑄 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ) ∧ ( 𝑊 ∈ Word 𝑇 ∧ ( 𝑄 ↾ ( 𝑁 ∖ { 𝐾 } ) ) = ( 𝑆 Σg 𝑊 ) ) ) ∧ ( 𝑈 ∈ Word 𝑅 ∧ ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑈 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( ( 𝑈 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ∧ ∀ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ( ( 𝑊 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑈 ‘ 𝑖 ) ‘ 𝑛 ) ) ) ) ∧ 𝑘 ∈ 𝑁 ) → ( 𝑄 ‘ 𝑘 ) = ( ( 𝑍 Σg 𝑈 ) ‘ 𝑘 ) ) )
113 61 112 pm2.61i ⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑄 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ) ∧ ( 𝑊 ∈ Word 𝑇 ∧ ( 𝑄 ↾ ( 𝑁 ∖ { 𝐾 } ) ) = ( 𝑆 Σg 𝑊 ) ) ) ∧ ( 𝑈 ∈ Word 𝑅 ∧ ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑈 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( ( 𝑈 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ∧ ∀ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ( ( 𝑊 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑈 ‘ 𝑖 ) ‘ 𝑛 ) ) ) ) ∧ 𝑘 ∈ 𝑁 ) → ( 𝑄 ‘ 𝑘 ) = ( ( 𝑍 Σg 𝑈 ) ‘ 𝑘 ) )
114 11 23 113 eqfnfvd ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑄 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ) ∧ ( 𝑊 ∈ Word 𝑇 ∧ ( 𝑄 ↾ ( 𝑁 ∖ { 𝐾 } ) ) = ( 𝑆 Σg 𝑊 ) ) ) ∧ ( 𝑈 ∈ Word 𝑅 ∧ ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑈 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( ( 𝑈 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ∧ ∀ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ( ( 𝑊 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑈 ‘ 𝑖 ) ‘ 𝑛 ) ) ) ) → 𝑄 = ( 𝑍 Σg 𝑈 ) )
115 114 exp31 ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑄 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ) → ( ( 𝑊 ∈ Word 𝑇 ∧ ( 𝑄 ↾ ( 𝑁 ∖ { 𝐾 } ) ) = ( 𝑆 Σg 𝑊 ) ) → ( ( 𝑈 ∈ Word 𝑅 ∧ ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑈 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( ( 𝑈 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ∧ ∀ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ( ( 𝑊 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑈 ‘ 𝑖 ) ‘ 𝑛 ) ) ) → 𝑄 = ( 𝑍 Σg 𝑈 ) ) ) )