# Metamath Proof Explorer

## Theorem gsmsymgrfixlem1

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

Ref Expression
Hypotheses gsmsymgrfix.s ${⊢}{S}=\mathrm{SymGrp}\left({N}\right)$
gsmsymgrfix.b ${⊢}{B}={\mathrm{Base}}_{{S}}$
Assertion gsmsymgrfixlem1 ${⊢}\left(\left({W}\in \mathrm{Word}{B}\wedge {P}\in {B}\right)\wedge \left({N}\in \mathrm{Fin}\wedge {K}\in {N}\right)\wedge \left(\forall {i}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}{W}\left({i}\right)\left({K}\right)={K}\to \left({\sum }_{{S}},{W}\right)\left({K}\right)={K}\right)\right)\to \left(\forall {i}\in \left(0..^\left|{W}\right|+1\right)\phantom{\rule{.4em}{0ex}}\left({W}\mathrm{++}⟨“{P}”⟩\right)\left({i}\right)\left({K}\right)={K}\to \left({\sum }_{{S}},\left({W}\mathrm{++}⟨“{P}”⟩\right)\right)\left({K}\right)={K}\right)$

### Proof

Step Hyp Ref Expression
1 gsmsymgrfix.s ${⊢}{S}=\mathrm{SymGrp}\left({N}\right)$
2 gsmsymgrfix.b ${⊢}{B}={\mathrm{Base}}_{{S}}$
3 lencl ${⊢}{W}\in \mathrm{Word}{B}\to \left|{W}\right|\in {ℕ}_{0}$
4 elnn0uz ${⊢}\left|{W}\right|\in {ℕ}_{0}↔\left|{W}\right|\in {ℤ}_{\ge 0}$
5 3 4 sylib ${⊢}{W}\in \mathrm{Word}{B}\to \left|{W}\right|\in {ℤ}_{\ge 0}$
6 5 adantr ${⊢}\left({W}\in \mathrm{Word}{B}\wedge {P}\in {B}\right)\to \left|{W}\right|\in {ℤ}_{\ge 0}$
7 6 3ad2ant1 ${⊢}\left(\left({W}\in \mathrm{Word}{B}\wedge {P}\in {B}\right)\wedge \left({N}\in \mathrm{Fin}\wedge {K}\in {N}\right)\wedge \left(\forall {i}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}{W}\left({i}\right)\left({K}\right)={K}\to \left({\sum }_{{S}},{W}\right)\left({K}\right)={K}\right)\right)\to \left|{W}\right|\in {ℤ}_{\ge 0}$
8 fzosplitsn ${⊢}\left|{W}\right|\in {ℤ}_{\ge 0}\to \left(0..^\left|{W}\right|+1\right)=\left(0..^\left|{W}\right|\right)\cup \left\{\left|{W}\right|\right\}$
9 7 8 syl ${⊢}\left(\left({W}\in \mathrm{Word}{B}\wedge {P}\in {B}\right)\wedge \left({N}\in \mathrm{Fin}\wedge {K}\in {N}\right)\wedge \left(\forall {i}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}{W}\left({i}\right)\left({K}\right)={K}\to \left({\sum }_{{S}},{W}\right)\left({K}\right)={K}\right)\right)\to \left(0..^\left|{W}\right|+1\right)=\left(0..^\left|{W}\right|\right)\cup \left\{\left|{W}\right|\right\}$
10 9 raleqdv ${⊢}\left(\left({W}\in \mathrm{Word}{B}\wedge {P}\in {B}\right)\wedge \left({N}\in \mathrm{Fin}\wedge {K}\in {N}\right)\wedge \left(\forall {i}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}{W}\left({i}\right)\left({K}\right)={K}\to \left({\sum }_{{S}},{W}\right)\left({K}\right)={K}\right)\right)\to \left(\forall {i}\in \left(0..^\left|{W}\right|+1\right)\phantom{\rule{.4em}{0ex}}\left({W}\mathrm{++}⟨“{P}”⟩\right)\left({i}\right)\left({K}\right)={K}↔\forall {i}\in \left(\left(0..^\left|{W}\right|\right)\cup \left\{\left|{W}\right|\right\}\right)\phantom{\rule{.4em}{0ex}}\left({W}\mathrm{++}⟨“{P}”⟩\right)\left({i}\right)\left({K}\right)={K}\right)$
11 3 adantr ${⊢}\left({W}\in \mathrm{Word}{B}\wedge {P}\in {B}\right)\to \left|{W}\right|\in {ℕ}_{0}$
12 11 3ad2ant1 ${⊢}\left(\left({W}\in \mathrm{Word}{B}\wedge {P}\in {B}\right)\wedge \left({N}\in \mathrm{Fin}\wedge {K}\in {N}\right)\wedge \left(\forall {i}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}{W}\left({i}\right)\left({K}\right)={K}\to \left({\sum }_{{S}},{W}\right)\left({K}\right)={K}\right)\right)\to \left|{W}\right|\in {ℕ}_{0}$
13 fveq2 ${⊢}{i}=\left|{W}\right|\to \left({W}\mathrm{++}⟨“{P}”⟩\right)\left({i}\right)=\left({W}\mathrm{++}⟨“{P}”⟩\right)\left(\left|{W}\right|\right)$
14 13 fveq1d ${⊢}{i}=\left|{W}\right|\to \left({W}\mathrm{++}⟨“{P}”⟩\right)\left({i}\right)\left({K}\right)=\left({W}\mathrm{++}⟨“{P}”⟩\right)\left(\left|{W}\right|\right)\left({K}\right)$
15 14 eqeq1d ${⊢}{i}=\left|{W}\right|\to \left(\left({W}\mathrm{++}⟨“{P}”⟩\right)\left({i}\right)\left({K}\right)={K}↔\left({W}\mathrm{++}⟨“{P}”⟩\right)\left(\left|{W}\right|\right)\left({K}\right)={K}\right)$
16 15 ralunsn ${⊢}\left|{W}\right|\in {ℕ}_{0}\to \left(\forall {i}\in \left(\left(0..^\left|{W}\right|\right)\cup \left\{\left|{W}\right|\right\}\right)\phantom{\rule{.4em}{0ex}}\left({W}\mathrm{++}⟨“{P}”⟩\right)\left({i}\right)\left({K}\right)={K}↔\left(\forall {i}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}\left({W}\mathrm{++}⟨“{P}”⟩\right)\left({i}\right)\left({K}\right)={K}\wedge \left({W}\mathrm{++}⟨“{P}”⟩\right)\left(\left|{W}\right|\right)\left({K}\right)={K}\right)\right)$
17 12 16 syl ${⊢}\left(\left({W}\in \mathrm{Word}{B}\wedge {P}\in {B}\right)\wedge \left({N}\in \mathrm{Fin}\wedge {K}\in {N}\right)\wedge \left(\forall {i}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}{W}\left({i}\right)\left({K}\right)={K}\to \left({\sum }_{{S}},{W}\right)\left({K}\right)={K}\right)\right)\to \left(\forall {i}\in \left(\left(0..^\left|{W}\right|\right)\cup \left\{\left|{W}\right|\right\}\right)\phantom{\rule{.4em}{0ex}}\left({W}\mathrm{++}⟨“{P}”⟩\right)\left({i}\right)\left({K}\right)={K}↔\left(\forall {i}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}\left({W}\mathrm{++}⟨“{P}”⟩\right)\left({i}\right)\left({K}\right)={K}\wedge \left({W}\mathrm{++}⟨“{P}”⟩\right)\left(\left|{W}\right|\right)\left({K}\right)={K}\right)\right)$
18 10 17 bitrd ${⊢}\left(\left({W}\in \mathrm{Word}{B}\wedge {P}\in {B}\right)\wedge \left({N}\in \mathrm{Fin}\wedge {K}\in {N}\right)\wedge \left(\forall {i}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}{W}\left({i}\right)\left({K}\right)={K}\to \left({\sum }_{{S}},{W}\right)\left({K}\right)={K}\right)\right)\to \left(\forall {i}\in \left(0..^\left|{W}\right|+1\right)\phantom{\rule{.4em}{0ex}}\left({W}\mathrm{++}⟨“{P}”⟩\right)\left({i}\right)\left({K}\right)={K}↔\left(\forall {i}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}\left({W}\mathrm{++}⟨“{P}”⟩\right)\left({i}\right)\left({K}\right)={K}\wedge \left({W}\mathrm{++}⟨“{P}”⟩\right)\left(\left|{W}\right|\right)\left({K}\right)={K}\right)\right)$
19 eqidd ${⊢}\left({W}\in \mathrm{Word}{B}\wedge {P}\in {B}\right)\to \left|{W}\right|=\left|{W}\right|$
20 ccats1val2 ${⊢}\left({W}\in \mathrm{Word}{B}\wedge {P}\in {B}\wedge \left|{W}\right|=\left|{W}\right|\right)\to \left({W}\mathrm{++}⟨“{P}”⟩\right)\left(\left|{W}\right|\right)={P}$
21 20 fveq1d ${⊢}\left({W}\in \mathrm{Word}{B}\wedge {P}\in {B}\wedge \left|{W}\right|=\left|{W}\right|\right)\to \left({W}\mathrm{++}⟨“{P}”⟩\right)\left(\left|{W}\right|\right)\left({K}\right)={P}\left({K}\right)$
22 21 eqeq1d ${⊢}\left({W}\in \mathrm{Word}{B}\wedge {P}\in {B}\wedge \left|{W}\right|=\left|{W}\right|\right)\to \left(\left({W}\mathrm{++}⟨“{P}”⟩\right)\left(\left|{W}\right|\right)\left({K}\right)={K}↔{P}\left({K}\right)={K}\right)$
23 19 22 mpd3an3 ${⊢}\left({W}\in \mathrm{Word}{B}\wedge {P}\in {B}\right)\to \left(\left({W}\mathrm{++}⟨“{P}”⟩\right)\left(\left|{W}\right|\right)\left({K}\right)={K}↔{P}\left({K}\right)={K}\right)$
24 23 3ad2ant1 ${⊢}\left(\left({W}\in \mathrm{Word}{B}\wedge {P}\in {B}\right)\wedge \left({N}\in \mathrm{Fin}\wedge {K}\in {N}\right)\wedge \left(\forall {i}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}{W}\left({i}\right)\left({K}\right)={K}\to \left({\sum }_{{S}},{W}\right)\left({K}\right)={K}\right)\right)\to \left(\left({W}\mathrm{++}⟨“{P}”⟩\right)\left(\left|{W}\right|\right)\left({K}\right)={K}↔{P}\left({K}\right)={K}\right)$
25 simprl ${⊢}\left(\left({W}\in \mathrm{Word}{B}\wedge {P}\in {B}\right)\wedge \left({N}\in \mathrm{Fin}\wedge {K}\in {N}\right)\right)\to {N}\in \mathrm{Fin}$
26 simpll ${⊢}\left(\left({W}\in \mathrm{Word}{B}\wedge {P}\in {B}\right)\wedge \left({N}\in \mathrm{Fin}\wedge {K}\in {N}\right)\right)\to {W}\in \mathrm{Word}{B}$
27 simplr ${⊢}\left(\left({W}\in \mathrm{Word}{B}\wedge {P}\in {B}\right)\wedge \left({N}\in \mathrm{Fin}\wedge {K}\in {N}\right)\right)\to {P}\in {B}$
28 1 2 gsumccatsymgsn ${⊢}\left({N}\in \mathrm{Fin}\wedge {W}\in \mathrm{Word}{B}\wedge {P}\in {B}\right)\to {\sum }_{{S}}\left({W}\mathrm{++}⟨“{P}”⟩\right)=\left({\sum }_{{S}},{W}\right)\circ {P}$
29 28 fveq1d ${⊢}\left({N}\in \mathrm{Fin}\wedge {W}\in \mathrm{Word}{B}\wedge {P}\in {B}\right)\to \left({\sum }_{{S}},\left({W}\mathrm{++}⟨“{P}”⟩\right)\right)\left({K}\right)=\left(\left({\sum }_{{S}},{W}\right)\circ {P}\right)\left({K}\right)$
30 25 26 27 29 syl3anc ${⊢}\left(\left({W}\in \mathrm{Word}{B}\wedge {P}\in {B}\right)\wedge \left({N}\in \mathrm{Fin}\wedge {K}\in {N}\right)\right)\to \left({\sum }_{{S}},\left({W}\mathrm{++}⟨“{P}”⟩\right)\right)\left({K}\right)=\left(\left({\sum }_{{S}},{W}\right)\circ {P}\right)\left({K}\right)$
31 30 3adant3 ${⊢}\left(\left({W}\in \mathrm{Word}{B}\wedge {P}\in {B}\right)\wedge \left({N}\in \mathrm{Fin}\wedge {K}\in {N}\right)\wedge \left(\forall {i}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}{W}\left({i}\right)\left({K}\right)={K}\to \left({\sum }_{{S}},{W}\right)\left({K}\right)={K}\right)\right)\to \left({\sum }_{{S}},\left({W}\mathrm{++}⟨“{P}”⟩\right)\right)\left({K}\right)=\left(\left({\sum }_{{S}},{W}\right)\circ {P}\right)\left({K}\right)$
32 31 adantr ${⊢}\left(\left(\left({W}\in \mathrm{Word}{B}\wedge {P}\in {B}\right)\wedge \left({N}\in \mathrm{Fin}\wedge {K}\in {N}\right)\wedge \left(\forall {i}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}{W}\left({i}\right)\left({K}\right)={K}\to \left({\sum }_{{S}},{W}\right)\left({K}\right)={K}\right)\right)\wedge \left({P}\left({K}\right)={K}\wedge \forall {i}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}\left({W}\mathrm{++}⟨“{P}”⟩\right)\left({i}\right)\left({K}\right)={K}\right)\right)\to \left({\sum }_{{S}},\left({W}\mathrm{++}⟨“{P}”⟩\right)\right)\left({K}\right)=\left(\left({\sum }_{{S}},{W}\right)\circ {P}\right)\left({K}\right)$
33 1 2 symgbasf ${⊢}{P}\in {B}\to {P}:{N}⟶{N}$
34 33 ffnd ${⊢}{P}\in {B}\to {P}Fn{N}$
35 34 adantl ${⊢}\left({W}\in \mathrm{Word}{B}\wedge {P}\in {B}\right)\to {P}Fn{N}$
36 simpr ${⊢}\left({N}\in \mathrm{Fin}\wedge {K}\in {N}\right)\to {K}\in {N}$
37 fvco2 ${⊢}\left({P}Fn{N}\wedge {K}\in {N}\right)\to \left(\left({\sum }_{{S}},{W}\right)\circ {P}\right)\left({K}\right)=\left({\sum }_{{S}},{W}\right)\left({P}\left({K}\right)\right)$
38 35 36 37 syl2an ${⊢}\left(\left({W}\in \mathrm{Word}{B}\wedge {P}\in {B}\right)\wedge \left({N}\in \mathrm{Fin}\wedge {K}\in {N}\right)\right)\to \left(\left({\sum }_{{S}},{W}\right)\circ {P}\right)\left({K}\right)=\left({\sum }_{{S}},{W}\right)\left({P}\left({K}\right)\right)$
39 38 3adant3 ${⊢}\left(\left({W}\in \mathrm{Word}{B}\wedge {P}\in {B}\right)\wedge \left({N}\in \mathrm{Fin}\wedge {K}\in {N}\right)\wedge \left(\forall {i}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}{W}\left({i}\right)\left({K}\right)={K}\to \left({\sum }_{{S}},{W}\right)\left({K}\right)={K}\right)\right)\to \left(\left({\sum }_{{S}},{W}\right)\circ {P}\right)\left({K}\right)=\left({\sum }_{{S}},{W}\right)\left({P}\left({K}\right)\right)$
40 39 adantr ${⊢}\left(\left(\left({W}\in \mathrm{Word}{B}\wedge {P}\in {B}\right)\wedge \left({N}\in \mathrm{Fin}\wedge {K}\in {N}\right)\wedge \left(\forall {i}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}{W}\left({i}\right)\left({K}\right)={K}\to \left({\sum }_{{S}},{W}\right)\left({K}\right)={K}\right)\right)\wedge \left({P}\left({K}\right)={K}\wedge \forall {i}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}\left({W}\mathrm{++}⟨“{P}”⟩\right)\left({i}\right)\left({K}\right)={K}\right)\right)\to \left(\left({\sum }_{{S}},{W}\right)\circ {P}\right)\left({K}\right)=\left({\sum }_{{S}},{W}\right)\left({P}\left({K}\right)\right)$
41 fveq2 ${⊢}{P}\left({K}\right)={K}\to \left({\sum }_{{S}},{W}\right)\left({P}\left({K}\right)\right)=\left({\sum }_{{S}},{W}\right)\left({K}\right)$
42 41 ad2antrl ${⊢}\left(\left(\left({W}\in \mathrm{Word}{B}\wedge {P}\in {B}\right)\wedge \left({N}\in \mathrm{Fin}\wedge {K}\in {N}\right)\wedge \left(\forall {i}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}{W}\left({i}\right)\left({K}\right)={K}\to \left({\sum }_{{S}},{W}\right)\left({K}\right)={K}\right)\right)\wedge \left({P}\left({K}\right)={K}\wedge \forall {i}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}\left({W}\mathrm{++}⟨“{P}”⟩\right)\left({i}\right)\left({K}\right)={K}\right)\right)\to \left({\sum }_{{S}},{W}\right)\left({P}\left({K}\right)\right)=\left({\sum }_{{S}},{W}\right)\left({K}\right)$
43 ccats1val1 ${⊢}\left({W}\in \mathrm{Word}{B}\wedge {i}\in \left(0..^\left|{W}\right|\right)\right)\to \left({W}\mathrm{++}⟨“{P}”⟩\right)\left({i}\right)={W}\left({i}\right)$
44 43 ad4ant14 ${⊢}\left(\left(\left({W}\in \mathrm{Word}{B}\wedge {P}\in {B}\right)\wedge \left({N}\in \mathrm{Fin}\wedge {K}\in {N}\right)\right)\wedge {i}\in \left(0..^\left|{W}\right|\right)\right)\to \left({W}\mathrm{++}⟨“{P}”⟩\right)\left({i}\right)={W}\left({i}\right)$
45 44 fveq1d ${⊢}\left(\left(\left({W}\in \mathrm{Word}{B}\wedge {P}\in {B}\right)\wedge \left({N}\in \mathrm{Fin}\wedge {K}\in {N}\right)\right)\wedge {i}\in \left(0..^\left|{W}\right|\right)\right)\to \left({W}\mathrm{++}⟨“{P}”⟩\right)\left({i}\right)\left({K}\right)={W}\left({i}\right)\left({K}\right)$
46 45 eqeq1d ${⊢}\left(\left(\left({W}\in \mathrm{Word}{B}\wedge {P}\in {B}\right)\wedge \left({N}\in \mathrm{Fin}\wedge {K}\in {N}\right)\right)\wedge {i}\in \left(0..^\left|{W}\right|\right)\right)\to \left(\left({W}\mathrm{++}⟨“{P}”⟩\right)\left({i}\right)\left({K}\right)={K}↔{W}\left({i}\right)\left({K}\right)={K}\right)$
47 46 ralbidva ${⊢}\left(\left({W}\in \mathrm{Word}{B}\wedge {P}\in {B}\right)\wedge \left({N}\in \mathrm{Fin}\wedge {K}\in {N}\right)\right)\to \left(\forall {i}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}\left({W}\mathrm{++}⟨“{P}”⟩\right)\left({i}\right)\left({K}\right)={K}↔\forall {i}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}{W}\left({i}\right)\left({K}\right)={K}\right)$
48 47 biimpd ${⊢}\left(\left({W}\in \mathrm{Word}{B}\wedge {P}\in {B}\right)\wedge \left({N}\in \mathrm{Fin}\wedge {K}\in {N}\right)\right)\to \left(\forall {i}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}\left({W}\mathrm{++}⟨“{P}”⟩\right)\left({i}\right)\left({K}\right)={K}\to \forall {i}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}{W}\left({i}\right)\left({K}\right)={K}\right)$
49 48 adantld ${⊢}\left(\left({W}\in \mathrm{Word}{B}\wedge {P}\in {B}\right)\wedge \left({N}\in \mathrm{Fin}\wedge {K}\in {N}\right)\right)\to \left(\left({P}\left({K}\right)={K}\wedge \forall {i}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}\left({W}\mathrm{++}⟨“{P}”⟩\right)\left({i}\right)\left({K}\right)={K}\right)\to \forall {i}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}{W}\left({i}\right)\left({K}\right)={K}\right)$
50 49 3adant3 ${⊢}\left(\left({W}\in \mathrm{Word}{B}\wedge {P}\in {B}\right)\wedge \left({N}\in \mathrm{Fin}\wedge {K}\in {N}\right)\wedge \left(\forall {i}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}{W}\left({i}\right)\left({K}\right)={K}\to \left({\sum }_{{S}},{W}\right)\left({K}\right)={K}\right)\right)\to \left(\left({P}\left({K}\right)={K}\wedge \forall {i}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}\left({W}\mathrm{++}⟨“{P}”⟩\right)\left({i}\right)\left({K}\right)={K}\right)\to \forall {i}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}{W}\left({i}\right)\left({K}\right)={K}\right)$
51 simp3 ${⊢}\left(\left({W}\in \mathrm{Word}{B}\wedge {P}\in {B}\right)\wedge \left({N}\in \mathrm{Fin}\wedge {K}\in {N}\right)\wedge \left(\forall {i}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}{W}\left({i}\right)\left({K}\right)={K}\to \left({\sum }_{{S}},{W}\right)\left({K}\right)={K}\right)\right)\to \left(\forall {i}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}{W}\left({i}\right)\left({K}\right)={K}\to \left({\sum }_{{S}},{W}\right)\left({K}\right)={K}\right)$
52 50 51 syld ${⊢}\left(\left({W}\in \mathrm{Word}{B}\wedge {P}\in {B}\right)\wedge \left({N}\in \mathrm{Fin}\wedge {K}\in {N}\right)\wedge \left(\forall {i}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}{W}\left({i}\right)\left({K}\right)={K}\to \left({\sum }_{{S}},{W}\right)\left({K}\right)={K}\right)\right)\to \left(\left({P}\left({K}\right)={K}\wedge \forall {i}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}\left({W}\mathrm{++}⟨“{P}”⟩\right)\left({i}\right)\left({K}\right)={K}\right)\to \left({\sum }_{{S}},{W}\right)\left({K}\right)={K}\right)$
53 52 imp ${⊢}\left(\left(\left({W}\in \mathrm{Word}{B}\wedge {P}\in {B}\right)\wedge \left({N}\in \mathrm{Fin}\wedge {K}\in {N}\right)\wedge \left(\forall {i}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}{W}\left({i}\right)\left({K}\right)={K}\to \left({\sum }_{{S}},{W}\right)\left({K}\right)={K}\right)\right)\wedge \left({P}\left({K}\right)={K}\wedge \forall {i}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}\left({W}\mathrm{++}⟨“{P}”⟩\right)\left({i}\right)\left({K}\right)={K}\right)\right)\to \left({\sum }_{{S}},{W}\right)\left({K}\right)={K}$
54 42 53 eqtrd ${⊢}\left(\left(\left({W}\in \mathrm{Word}{B}\wedge {P}\in {B}\right)\wedge \left({N}\in \mathrm{Fin}\wedge {K}\in {N}\right)\wedge \left(\forall {i}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}{W}\left({i}\right)\left({K}\right)={K}\to \left({\sum }_{{S}},{W}\right)\left({K}\right)={K}\right)\right)\wedge \left({P}\left({K}\right)={K}\wedge \forall {i}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}\left({W}\mathrm{++}⟨“{P}”⟩\right)\left({i}\right)\left({K}\right)={K}\right)\right)\to \left({\sum }_{{S}},{W}\right)\left({P}\left({K}\right)\right)={K}$
55 32 40 54 3eqtrd ${⊢}\left(\left(\left({W}\in \mathrm{Word}{B}\wedge {P}\in {B}\right)\wedge \left({N}\in \mathrm{Fin}\wedge {K}\in {N}\right)\wedge \left(\forall {i}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}{W}\left({i}\right)\left({K}\right)={K}\to \left({\sum }_{{S}},{W}\right)\left({K}\right)={K}\right)\right)\wedge \left({P}\left({K}\right)={K}\wedge \forall {i}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}\left({W}\mathrm{++}⟨“{P}”⟩\right)\left({i}\right)\left({K}\right)={K}\right)\right)\to \left({\sum }_{{S}},\left({W}\mathrm{++}⟨“{P}”⟩\right)\right)\left({K}\right)={K}$
56 55 exp32 ${⊢}\left(\left({W}\in \mathrm{Word}{B}\wedge {P}\in {B}\right)\wedge \left({N}\in \mathrm{Fin}\wedge {K}\in {N}\right)\wedge \left(\forall {i}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}{W}\left({i}\right)\left({K}\right)={K}\to \left({\sum }_{{S}},{W}\right)\left({K}\right)={K}\right)\right)\to \left({P}\left({K}\right)={K}\to \left(\forall {i}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}\left({W}\mathrm{++}⟨“{P}”⟩\right)\left({i}\right)\left({K}\right)={K}\to \left({\sum }_{{S}},\left({W}\mathrm{++}⟨“{P}”⟩\right)\right)\left({K}\right)={K}\right)\right)$
57 24 56 sylbid ${⊢}\left(\left({W}\in \mathrm{Word}{B}\wedge {P}\in {B}\right)\wedge \left({N}\in \mathrm{Fin}\wedge {K}\in {N}\right)\wedge \left(\forall {i}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}{W}\left({i}\right)\left({K}\right)={K}\to \left({\sum }_{{S}},{W}\right)\left({K}\right)={K}\right)\right)\to \left(\left({W}\mathrm{++}⟨“{P}”⟩\right)\left(\left|{W}\right|\right)\left({K}\right)={K}\to \left(\forall {i}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}\left({W}\mathrm{++}⟨“{P}”⟩\right)\left({i}\right)\left({K}\right)={K}\to \left({\sum }_{{S}},\left({W}\mathrm{++}⟨“{P}”⟩\right)\right)\left({K}\right)={K}\right)\right)$
58 57 impcomd ${⊢}\left(\left({W}\in \mathrm{Word}{B}\wedge {P}\in {B}\right)\wedge \left({N}\in \mathrm{Fin}\wedge {K}\in {N}\right)\wedge \left(\forall {i}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}{W}\left({i}\right)\left({K}\right)={K}\to \left({\sum }_{{S}},{W}\right)\left({K}\right)={K}\right)\right)\to \left(\left(\forall {i}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}\left({W}\mathrm{++}⟨“{P}”⟩\right)\left({i}\right)\left({K}\right)={K}\wedge \left({W}\mathrm{++}⟨“{P}”⟩\right)\left(\left|{W}\right|\right)\left({K}\right)={K}\right)\to \left({\sum }_{{S}},\left({W}\mathrm{++}⟨“{P}”⟩\right)\right)\left({K}\right)={K}\right)$
59 18 58 sylbid ${⊢}\left(\left({W}\in \mathrm{Word}{B}\wedge {P}\in {B}\right)\wedge \left({N}\in \mathrm{Fin}\wedge {K}\in {N}\right)\wedge \left(\forall {i}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}{W}\left({i}\right)\left({K}\right)={K}\to \left({\sum }_{{S}},{W}\right)\left({K}\right)={K}\right)\right)\to \left(\forall {i}\in \left(0..^\left|{W}\right|+1\right)\phantom{\rule{.4em}{0ex}}\left({W}\mathrm{++}⟨“{P}”⟩\right)\left({i}\right)\left({K}\right)={K}\to \left({\sum }_{{S}},\left({W}\mathrm{++}⟨“{P}”⟩\right)\right)\left({K}\right)={K}\right)$