Metamath Proof Explorer


Theorem gsmsymgrfixlem1

Description: Lemma 1 for gsmsymgrfix . (Contributed by AV, 20-Jan-2019)

Ref Expression
Hypotheses gsmsymgrfix.s 𝑆 = ( SymGrp ‘ 𝑁 )
gsmsymgrfix.b 𝐵 = ( Base ‘ 𝑆 )
Assertion gsmsymgrfixlem1 ( ( ( 𝑊 ∈ Word 𝐵𝑃𝐵 ) ∧ ( 𝑁 ∈ Fin ∧ 𝐾𝑁 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( 𝑊𝑖 ) ‘ 𝐾 ) = 𝐾 → ( ( 𝑆 Σg 𝑊 ) ‘ 𝐾 ) = 𝐾 ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) + 1 ) ) ( ( ( 𝑊 ++ ⟨“ 𝑃 ”⟩ ) ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 → ( ( 𝑆 Σg ( 𝑊 ++ ⟨“ 𝑃 ”⟩ ) ) ‘ 𝐾 ) = 𝐾 ) )

Proof

Step Hyp Ref Expression
1 gsmsymgrfix.s 𝑆 = ( SymGrp ‘ 𝑁 )
2 gsmsymgrfix.b 𝐵 = ( Base ‘ 𝑆 )
3 lencl ( 𝑊 ∈ Word 𝐵 → ( ♯ ‘ 𝑊 ) ∈ ℕ0 )
4 elnn0uz ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 ↔ ( ♯ ‘ 𝑊 ) ∈ ( ℤ ‘ 0 ) )
5 3 4 sylib ( 𝑊 ∈ Word 𝐵 → ( ♯ ‘ 𝑊 ) ∈ ( ℤ ‘ 0 ) )
6 5 adantr ( ( 𝑊 ∈ Word 𝐵𝑃𝐵 ) → ( ♯ ‘ 𝑊 ) ∈ ( ℤ ‘ 0 ) )
7 6 3ad2ant1 ( ( ( 𝑊 ∈ Word 𝐵𝑃𝐵 ) ∧ ( 𝑁 ∈ Fin ∧ 𝐾𝑁 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( 𝑊𝑖 ) ‘ 𝐾 ) = 𝐾 → ( ( 𝑆 Σg 𝑊 ) ‘ 𝐾 ) = 𝐾 ) ) → ( ♯ ‘ 𝑊 ) ∈ ( ℤ ‘ 0 ) )
8 fzosplitsn ( ( ♯ ‘ 𝑊 ) ∈ ( ℤ ‘ 0 ) → ( 0 ..^ ( ( ♯ ‘ 𝑊 ) + 1 ) ) = ( ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ∪ { ( ♯ ‘ 𝑊 ) } ) )
9 7 8 syl ( ( ( 𝑊 ∈ Word 𝐵𝑃𝐵 ) ∧ ( 𝑁 ∈ Fin ∧ 𝐾𝑁 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( 𝑊𝑖 ) ‘ 𝐾 ) = 𝐾 → ( ( 𝑆 Σg 𝑊 ) ‘ 𝐾 ) = 𝐾 ) ) → ( 0 ..^ ( ( ♯ ‘ 𝑊 ) + 1 ) ) = ( ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ∪ { ( ♯ ‘ 𝑊 ) } ) )
10 9 raleqdv ( ( ( 𝑊 ∈ Word 𝐵𝑃𝐵 ) ∧ ( 𝑁 ∈ Fin ∧ 𝐾𝑁 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( 𝑊𝑖 ) ‘ 𝐾 ) = 𝐾 → ( ( 𝑆 Σg 𝑊 ) ‘ 𝐾 ) = 𝐾 ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) + 1 ) ) ( ( ( 𝑊 ++ ⟨“ 𝑃 ”⟩ ) ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ↔ ∀ 𝑖 ∈ ( ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ∪ { ( ♯ ‘ 𝑊 ) } ) ( ( ( 𝑊 ++ ⟨“ 𝑃 ”⟩ ) ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ) )
11 3 adantr ( ( 𝑊 ∈ Word 𝐵𝑃𝐵 ) → ( ♯ ‘ 𝑊 ) ∈ ℕ0 )
12 11 3ad2ant1 ( ( ( 𝑊 ∈ Word 𝐵𝑃𝐵 ) ∧ ( 𝑁 ∈ Fin ∧ 𝐾𝑁 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( 𝑊𝑖 ) ‘ 𝐾 ) = 𝐾 → ( ( 𝑆 Σg 𝑊 ) ‘ 𝐾 ) = 𝐾 ) ) → ( ♯ ‘ 𝑊 ) ∈ ℕ0 )
13 fveq2 ( 𝑖 = ( ♯ ‘ 𝑊 ) → ( ( 𝑊 ++ ⟨“ 𝑃 ”⟩ ) ‘ 𝑖 ) = ( ( 𝑊 ++ ⟨“ 𝑃 ”⟩ ) ‘ ( ♯ ‘ 𝑊 ) ) )
14 13 fveq1d ( 𝑖 = ( ♯ ‘ 𝑊 ) → ( ( ( 𝑊 ++ ⟨“ 𝑃 ”⟩ ) ‘ 𝑖 ) ‘ 𝐾 ) = ( ( ( 𝑊 ++ ⟨“ 𝑃 ”⟩ ) ‘ ( ♯ ‘ 𝑊 ) ) ‘ 𝐾 ) )
15 14 eqeq1d ( 𝑖 = ( ♯ ‘ 𝑊 ) → ( ( ( ( 𝑊 ++ ⟨“ 𝑃 ”⟩ ) ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ↔ ( ( ( 𝑊 ++ ⟨“ 𝑃 ”⟩ ) ‘ ( ♯ ‘ 𝑊 ) ) ‘ 𝐾 ) = 𝐾 ) )
16 15 ralunsn ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 → ( ∀ 𝑖 ∈ ( ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ∪ { ( ♯ ‘ 𝑊 ) } ) ( ( ( 𝑊 ++ ⟨“ 𝑃 ”⟩ ) ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ↔ ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( ( 𝑊 ++ ⟨“ 𝑃 ”⟩ ) ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ∧ ( ( ( 𝑊 ++ ⟨“ 𝑃 ”⟩ ) ‘ ( ♯ ‘ 𝑊 ) ) ‘ 𝐾 ) = 𝐾 ) ) )
17 12 16 syl ( ( ( 𝑊 ∈ Word 𝐵𝑃𝐵 ) ∧ ( 𝑁 ∈ Fin ∧ 𝐾𝑁 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( 𝑊𝑖 ) ‘ 𝐾 ) = 𝐾 → ( ( 𝑆 Σg 𝑊 ) ‘ 𝐾 ) = 𝐾 ) ) → ( ∀ 𝑖 ∈ ( ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ∪ { ( ♯ ‘ 𝑊 ) } ) ( ( ( 𝑊 ++ ⟨“ 𝑃 ”⟩ ) ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ↔ ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( ( 𝑊 ++ ⟨“ 𝑃 ”⟩ ) ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ∧ ( ( ( 𝑊 ++ ⟨“ 𝑃 ”⟩ ) ‘ ( ♯ ‘ 𝑊 ) ) ‘ 𝐾 ) = 𝐾 ) ) )
18 10 17 bitrd ( ( ( 𝑊 ∈ Word 𝐵𝑃𝐵 ) ∧ ( 𝑁 ∈ Fin ∧ 𝐾𝑁 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( 𝑊𝑖 ) ‘ 𝐾 ) = 𝐾 → ( ( 𝑆 Σg 𝑊 ) ‘ 𝐾 ) = 𝐾 ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) + 1 ) ) ( ( ( 𝑊 ++ ⟨“ 𝑃 ”⟩ ) ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ↔ ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( ( 𝑊 ++ ⟨“ 𝑃 ”⟩ ) ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ∧ ( ( ( 𝑊 ++ ⟨“ 𝑃 ”⟩ ) ‘ ( ♯ ‘ 𝑊 ) ) ‘ 𝐾 ) = 𝐾 ) ) )
19 eqidd ( ( 𝑊 ∈ Word 𝐵𝑃𝐵 ) → ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑊 ) )
20 ccats1val2 ( ( 𝑊 ∈ Word 𝐵𝑃𝐵 ∧ ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑊 ) ) → ( ( 𝑊 ++ ⟨“ 𝑃 ”⟩ ) ‘ ( ♯ ‘ 𝑊 ) ) = 𝑃 )
21 20 fveq1d ( ( 𝑊 ∈ Word 𝐵𝑃𝐵 ∧ ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑊 ) ) → ( ( ( 𝑊 ++ ⟨“ 𝑃 ”⟩ ) ‘ ( ♯ ‘ 𝑊 ) ) ‘ 𝐾 ) = ( 𝑃𝐾 ) )
22 21 eqeq1d ( ( 𝑊 ∈ Word 𝐵𝑃𝐵 ∧ ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑊 ) ) → ( ( ( ( 𝑊 ++ ⟨“ 𝑃 ”⟩ ) ‘ ( ♯ ‘ 𝑊 ) ) ‘ 𝐾 ) = 𝐾 ↔ ( 𝑃𝐾 ) = 𝐾 ) )
23 19 22 mpd3an3 ( ( 𝑊 ∈ Word 𝐵𝑃𝐵 ) → ( ( ( ( 𝑊 ++ ⟨“ 𝑃 ”⟩ ) ‘ ( ♯ ‘ 𝑊 ) ) ‘ 𝐾 ) = 𝐾 ↔ ( 𝑃𝐾 ) = 𝐾 ) )
24 23 3ad2ant1 ( ( ( 𝑊 ∈ Word 𝐵𝑃𝐵 ) ∧ ( 𝑁 ∈ Fin ∧ 𝐾𝑁 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( 𝑊𝑖 ) ‘ 𝐾 ) = 𝐾 → ( ( 𝑆 Σg 𝑊 ) ‘ 𝐾 ) = 𝐾 ) ) → ( ( ( ( 𝑊 ++ ⟨“ 𝑃 ”⟩ ) ‘ ( ♯ ‘ 𝑊 ) ) ‘ 𝐾 ) = 𝐾 ↔ ( 𝑃𝐾 ) = 𝐾 ) )
25 simprl ( ( ( 𝑊 ∈ Word 𝐵𝑃𝐵 ) ∧ ( 𝑁 ∈ Fin ∧ 𝐾𝑁 ) ) → 𝑁 ∈ Fin )
26 simpll ( ( ( 𝑊 ∈ Word 𝐵𝑃𝐵 ) ∧ ( 𝑁 ∈ Fin ∧ 𝐾𝑁 ) ) → 𝑊 ∈ Word 𝐵 )
27 simplr ( ( ( 𝑊 ∈ Word 𝐵𝑃𝐵 ) ∧ ( 𝑁 ∈ Fin ∧ 𝐾𝑁 ) ) → 𝑃𝐵 )
28 1 2 gsumccatsymgsn ( ( 𝑁 ∈ Fin ∧ 𝑊 ∈ Word 𝐵𝑃𝐵 ) → ( 𝑆 Σg ( 𝑊 ++ ⟨“ 𝑃 ”⟩ ) ) = ( ( 𝑆 Σg 𝑊 ) ∘ 𝑃 ) )
29 28 fveq1d ( ( 𝑁 ∈ Fin ∧ 𝑊 ∈ Word 𝐵𝑃𝐵 ) → ( ( 𝑆 Σg ( 𝑊 ++ ⟨“ 𝑃 ”⟩ ) ) ‘ 𝐾 ) = ( ( ( 𝑆 Σg 𝑊 ) ∘ 𝑃 ) ‘ 𝐾 ) )
30 25 26 27 29 syl3anc ( ( ( 𝑊 ∈ Word 𝐵𝑃𝐵 ) ∧ ( 𝑁 ∈ Fin ∧ 𝐾𝑁 ) ) → ( ( 𝑆 Σg ( 𝑊 ++ ⟨“ 𝑃 ”⟩ ) ) ‘ 𝐾 ) = ( ( ( 𝑆 Σg 𝑊 ) ∘ 𝑃 ) ‘ 𝐾 ) )
31 30 3adant3 ( ( ( 𝑊 ∈ Word 𝐵𝑃𝐵 ) ∧ ( 𝑁 ∈ Fin ∧ 𝐾𝑁 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( 𝑊𝑖 ) ‘ 𝐾 ) = 𝐾 → ( ( 𝑆 Σg 𝑊 ) ‘ 𝐾 ) = 𝐾 ) ) → ( ( 𝑆 Σg ( 𝑊 ++ ⟨“ 𝑃 ”⟩ ) ) ‘ 𝐾 ) = ( ( ( 𝑆 Σg 𝑊 ) ∘ 𝑃 ) ‘ 𝐾 ) )
32 31 adantr ( ( ( ( 𝑊 ∈ Word 𝐵𝑃𝐵 ) ∧ ( 𝑁 ∈ Fin ∧ 𝐾𝑁 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( 𝑊𝑖 ) ‘ 𝐾 ) = 𝐾 → ( ( 𝑆 Σg 𝑊 ) ‘ 𝐾 ) = 𝐾 ) ) ∧ ( ( 𝑃𝐾 ) = 𝐾 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( ( 𝑊 ++ ⟨“ 𝑃 ”⟩ ) ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ) ) → ( ( 𝑆 Σg ( 𝑊 ++ ⟨“ 𝑃 ”⟩ ) ) ‘ 𝐾 ) = ( ( ( 𝑆 Σg 𝑊 ) ∘ 𝑃 ) ‘ 𝐾 ) )
33 1 2 symgbasf ( 𝑃𝐵𝑃 : 𝑁𝑁 )
34 33 ffnd ( 𝑃𝐵𝑃 Fn 𝑁 )
35 34 adantl ( ( 𝑊 ∈ Word 𝐵𝑃𝐵 ) → 𝑃 Fn 𝑁 )
36 simpr ( ( 𝑁 ∈ Fin ∧ 𝐾𝑁 ) → 𝐾𝑁 )
37 fvco2 ( ( 𝑃 Fn 𝑁𝐾𝑁 ) → ( ( ( 𝑆 Σg 𝑊 ) ∘ 𝑃 ) ‘ 𝐾 ) = ( ( 𝑆 Σg 𝑊 ) ‘ ( 𝑃𝐾 ) ) )
38 35 36 37 syl2an ( ( ( 𝑊 ∈ Word 𝐵𝑃𝐵 ) ∧ ( 𝑁 ∈ Fin ∧ 𝐾𝑁 ) ) → ( ( ( 𝑆 Σg 𝑊 ) ∘ 𝑃 ) ‘ 𝐾 ) = ( ( 𝑆 Σg 𝑊 ) ‘ ( 𝑃𝐾 ) ) )
39 38 3adant3 ( ( ( 𝑊 ∈ Word 𝐵𝑃𝐵 ) ∧ ( 𝑁 ∈ Fin ∧ 𝐾𝑁 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( 𝑊𝑖 ) ‘ 𝐾 ) = 𝐾 → ( ( 𝑆 Σg 𝑊 ) ‘ 𝐾 ) = 𝐾 ) ) → ( ( ( 𝑆 Σg 𝑊 ) ∘ 𝑃 ) ‘ 𝐾 ) = ( ( 𝑆 Σg 𝑊 ) ‘ ( 𝑃𝐾 ) ) )
40 39 adantr ( ( ( ( 𝑊 ∈ Word 𝐵𝑃𝐵 ) ∧ ( 𝑁 ∈ Fin ∧ 𝐾𝑁 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( 𝑊𝑖 ) ‘ 𝐾 ) = 𝐾 → ( ( 𝑆 Σg 𝑊 ) ‘ 𝐾 ) = 𝐾 ) ) ∧ ( ( 𝑃𝐾 ) = 𝐾 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( ( 𝑊 ++ ⟨“ 𝑃 ”⟩ ) ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ) ) → ( ( ( 𝑆 Σg 𝑊 ) ∘ 𝑃 ) ‘ 𝐾 ) = ( ( 𝑆 Σg 𝑊 ) ‘ ( 𝑃𝐾 ) ) )
41 fveq2 ( ( 𝑃𝐾 ) = 𝐾 → ( ( 𝑆 Σg 𝑊 ) ‘ ( 𝑃𝐾 ) ) = ( ( 𝑆 Σg 𝑊 ) ‘ 𝐾 ) )
42 41 ad2antrl ( ( ( ( 𝑊 ∈ Word 𝐵𝑃𝐵 ) ∧ ( 𝑁 ∈ Fin ∧ 𝐾𝑁 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( 𝑊𝑖 ) ‘ 𝐾 ) = 𝐾 → ( ( 𝑆 Σg 𝑊 ) ‘ 𝐾 ) = 𝐾 ) ) ∧ ( ( 𝑃𝐾 ) = 𝐾 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( ( 𝑊 ++ ⟨“ 𝑃 ”⟩ ) ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ) ) → ( ( 𝑆 Σg 𝑊 ) ‘ ( 𝑃𝐾 ) ) = ( ( 𝑆 Σg 𝑊 ) ‘ 𝐾 ) )
43 ccats1val1 ( ( 𝑊 ∈ Word 𝐵𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝑊 ++ ⟨“ 𝑃 ”⟩ ) ‘ 𝑖 ) = ( 𝑊𝑖 ) )
44 43 ad4ant14 ( ( ( ( 𝑊 ∈ Word 𝐵𝑃𝐵 ) ∧ ( 𝑁 ∈ Fin ∧ 𝐾𝑁 ) ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝑊 ++ ⟨“ 𝑃 ”⟩ ) ‘ 𝑖 ) = ( 𝑊𝑖 ) )
45 44 fveq1d ( ( ( ( 𝑊 ∈ Word 𝐵𝑃𝐵 ) ∧ ( 𝑁 ∈ Fin ∧ 𝐾𝑁 ) ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( ( 𝑊 ++ ⟨“ 𝑃 ”⟩ ) ‘ 𝑖 ) ‘ 𝐾 ) = ( ( 𝑊𝑖 ) ‘ 𝐾 ) )
46 45 eqeq1d ( ( ( ( 𝑊 ∈ Word 𝐵𝑃𝐵 ) ∧ ( 𝑁 ∈ Fin ∧ 𝐾𝑁 ) ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( ( ( 𝑊 ++ ⟨“ 𝑃 ”⟩ ) ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ↔ ( ( 𝑊𝑖 ) ‘ 𝐾 ) = 𝐾 ) )
47 46 ralbidva ( ( ( 𝑊 ∈ Word 𝐵𝑃𝐵 ) ∧ ( 𝑁 ∈ Fin ∧ 𝐾𝑁 ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( ( 𝑊 ++ ⟨“ 𝑃 ”⟩ ) ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ↔ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( 𝑊𝑖 ) ‘ 𝐾 ) = 𝐾 ) )
48 47 biimpd ( ( ( 𝑊 ∈ Word 𝐵𝑃𝐵 ) ∧ ( 𝑁 ∈ Fin ∧ 𝐾𝑁 ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( ( 𝑊 ++ ⟨“ 𝑃 ”⟩ ) ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 → ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( 𝑊𝑖 ) ‘ 𝐾 ) = 𝐾 ) )
49 48 adantld ( ( ( 𝑊 ∈ Word 𝐵𝑃𝐵 ) ∧ ( 𝑁 ∈ Fin ∧ 𝐾𝑁 ) ) → ( ( ( 𝑃𝐾 ) = 𝐾 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( ( 𝑊 ++ ⟨“ 𝑃 ”⟩ ) ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ) → ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( 𝑊𝑖 ) ‘ 𝐾 ) = 𝐾 ) )
50 49 3adant3 ( ( ( 𝑊 ∈ Word 𝐵𝑃𝐵 ) ∧ ( 𝑁 ∈ Fin ∧ 𝐾𝑁 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( 𝑊𝑖 ) ‘ 𝐾 ) = 𝐾 → ( ( 𝑆 Σg 𝑊 ) ‘ 𝐾 ) = 𝐾 ) ) → ( ( ( 𝑃𝐾 ) = 𝐾 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( ( 𝑊 ++ ⟨“ 𝑃 ”⟩ ) ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ) → ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( 𝑊𝑖 ) ‘ 𝐾 ) = 𝐾 ) )
51 simp3 ( ( ( 𝑊 ∈ Word 𝐵𝑃𝐵 ) ∧ ( 𝑁 ∈ Fin ∧ 𝐾𝑁 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( 𝑊𝑖 ) ‘ 𝐾 ) = 𝐾 → ( ( 𝑆 Σg 𝑊 ) ‘ 𝐾 ) = 𝐾 ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( 𝑊𝑖 ) ‘ 𝐾 ) = 𝐾 → ( ( 𝑆 Σg 𝑊 ) ‘ 𝐾 ) = 𝐾 ) )
52 50 51 syld ( ( ( 𝑊 ∈ Word 𝐵𝑃𝐵 ) ∧ ( 𝑁 ∈ Fin ∧ 𝐾𝑁 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( 𝑊𝑖 ) ‘ 𝐾 ) = 𝐾 → ( ( 𝑆 Σg 𝑊 ) ‘ 𝐾 ) = 𝐾 ) ) → ( ( ( 𝑃𝐾 ) = 𝐾 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( ( 𝑊 ++ ⟨“ 𝑃 ”⟩ ) ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ) → ( ( 𝑆 Σg 𝑊 ) ‘ 𝐾 ) = 𝐾 ) )
53 52 imp ( ( ( ( 𝑊 ∈ Word 𝐵𝑃𝐵 ) ∧ ( 𝑁 ∈ Fin ∧ 𝐾𝑁 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( 𝑊𝑖 ) ‘ 𝐾 ) = 𝐾 → ( ( 𝑆 Σg 𝑊 ) ‘ 𝐾 ) = 𝐾 ) ) ∧ ( ( 𝑃𝐾 ) = 𝐾 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( ( 𝑊 ++ ⟨“ 𝑃 ”⟩ ) ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ) ) → ( ( 𝑆 Σg 𝑊 ) ‘ 𝐾 ) = 𝐾 )
54 42 53 eqtrd ( ( ( ( 𝑊 ∈ Word 𝐵𝑃𝐵 ) ∧ ( 𝑁 ∈ Fin ∧ 𝐾𝑁 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( 𝑊𝑖 ) ‘ 𝐾 ) = 𝐾 → ( ( 𝑆 Σg 𝑊 ) ‘ 𝐾 ) = 𝐾 ) ) ∧ ( ( 𝑃𝐾 ) = 𝐾 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( ( 𝑊 ++ ⟨“ 𝑃 ”⟩ ) ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ) ) → ( ( 𝑆 Σg 𝑊 ) ‘ ( 𝑃𝐾 ) ) = 𝐾 )
55 32 40 54 3eqtrd ( ( ( ( 𝑊 ∈ Word 𝐵𝑃𝐵 ) ∧ ( 𝑁 ∈ Fin ∧ 𝐾𝑁 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( 𝑊𝑖 ) ‘ 𝐾 ) = 𝐾 → ( ( 𝑆 Σg 𝑊 ) ‘ 𝐾 ) = 𝐾 ) ) ∧ ( ( 𝑃𝐾 ) = 𝐾 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( ( 𝑊 ++ ⟨“ 𝑃 ”⟩ ) ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ) ) → ( ( 𝑆 Σg ( 𝑊 ++ ⟨“ 𝑃 ”⟩ ) ) ‘ 𝐾 ) = 𝐾 )
56 55 exp32 ( ( ( 𝑊 ∈ Word 𝐵𝑃𝐵 ) ∧ ( 𝑁 ∈ Fin ∧ 𝐾𝑁 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( 𝑊𝑖 ) ‘ 𝐾 ) = 𝐾 → ( ( 𝑆 Σg 𝑊 ) ‘ 𝐾 ) = 𝐾 ) ) → ( ( 𝑃𝐾 ) = 𝐾 → ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( ( 𝑊 ++ ⟨“ 𝑃 ”⟩ ) ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 → ( ( 𝑆 Σg ( 𝑊 ++ ⟨“ 𝑃 ”⟩ ) ) ‘ 𝐾 ) = 𝐾 ) ) )
57 24 56 sylbid ( ( ( 𝑊 ∈ Word 𝐵𝑃𝐵 ) ∧ ( 𝑁 ∈ Fin ∧ 𝐾𝑁 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( 𝑊𝑖 ) ‘ 𝐾 ) = 𝐾 → ( ( 𝑆 Σg 𝑊 ) ‘ 𝐾 ) = 𝐾 ) ) → ( ( ( ( 𝑊 ++ ⟨“ 𝑃 ”⟩ ) ‘ ( ♯ ‘ 𝑊 ) ) ‘ 𝐾 ) = 𝐾 → ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( ( 𝑊 ++ ⟨“ 𝑃 ”⟩ ) ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 → ( ( 𝑆 Σg ( 𝑊 ++ ⟨“ 𝑃 ”⟩ ) ) ‘ 𝐾 ) = 𝐾 ) ) )
58 57 impcomd ( ( ( 𝑊 ∈ Word 𝐵𝑃𝐵 ) ∧ ( 𝑁 ∈ Fin ∧ 𝐾𝑁 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( 𝑊𝑖 ) ‘ 𝐾 ) = 𝐾 → ( ( 𝑆 Σg 𝑊 ) ‘ 𝐾 ) = 𝐾 ) ) → ( ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( ( 𝑊 ++ ⟨“ 𝑃 ”⟩ ) ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ∧ ( ( ( 𝑊 ++ ⟨“ 𝑃 ”⟩ ) ‘ ( ♯ ‘ 𝑊 ) ) ‘ 𝐾 ) = 𝐾 ) → ( ( 𝑆 Σg ( 𝑊 ++ ⟨“ 𝑃 ”⟩ ) ) ‘ 𝐾 ) = 𝐾 ) )
59 18 58 sylbid ( ( ( 𝑊 ∈ Word 𝐵𝑃𝐵 ) ∧ ( 𝑁 ∈ Fin ∧ 𝐾𝑁 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( 𝑊𝑖 ) ‘ 𝐾 ) = 𝐾 → ( ( 𝑆 Σg 𝑊 ) ‘ 𝐾 ) = 𝐾 ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) + 1 ) ) ( ( ( 𝑊 ++ ⟨“ 𝑃 ”⟩ ) ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 → ( ( 𝑆 Σg ( 𝑊 ++ ⟨“ 𝑃 ”⟩ ) ) ‘ 𝐾 ) = 𝐾 ) )