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

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 ( 𝑊 ++ ⟨“ 𝑃 ”⟩ ) ) ‘ 𝐾 ) = 𝐾 ) )