# Metamath Proof Explorer

## Theorem gsmsymgreqlem2

Description: Lemma 2 for gsmsymgreq . (Contributed by AV, 26-Jan-2019)

Ref Expression
Hypotheses gsmsymgrfix.s ${⊢}{S}=\mathrm{SymGrp}\left({N}\right)$
gsmsymgrfix.b ${⊢}{B}={\mathrm{Base}}_{{S}}$
gsmsymgreq.z ${⊢}{Z}=\mathrm{SymGrp}\left({M}\right)$
gsmsymgreq.p ${⊢}{P}={\mathrm{Base}}_{{Z}}$
gsmsymgreq.i ${⊢}{I}={N}\cap {M}$
Assertion gsmsymgreqlem2 ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {M}\in \mathrm{Fin}\right)\wedge \left(\left({X}\in \mathrm{Word}{B}\wedge {C}\in {B}\right)\wedge \left({Y}\in \mathrm{Word}{P}\wedge {R}\in {P}\right)\wedge \left|{X}\right|=\left|{Y}\right|\right)\right)\to \left(\left(\forall {i}\in \left(0..^\left|{X}\right|\right)\phantom{\rule{.4em}{0ex}}\forall {n}\in {I}\phantom{\rule{.4em}{0ex}}{X}\left({i}\right)\left({n}\right)={Y}\left({i}\right)\left({n}\right)\to \forall {n}\in {I}\phantom{\rule{.4em}{0ex}}\left({\sum }_{{S}},{X}\right)\left({n}\right)=\left({\sum }_{{Z}},{Y}\right)\left({n}\right)\right)\to \left(\forall {i}\in \left(0..^\left|{X}\mathrm{++}⟨“{C}”⟩\right|\right)\phantom{\rule{.4em}{0ex}}\forall {n}\in {I}\phantom{\rule{.4em}{0ex}}\left({X}\mathrm{++}⟨“{C}”⟩\right)\left({i}\right)\left({n}\right)=\left({Y}\mathrm{++}⟨“{R}”⟩\right)\left({i}\right)\left({n}\right)\to \forall {n}\in {I}\phantom{\rule{.4em}{0ex}}\left({\sum }_{{S}},\left({X}\mathrm{++}⟨“{C}”⟩\right)\right)\left({n}\right)=\left({\sum }_{{Z}},\left({Y}\mathrm{++}⟨“{R}”⟩\right)\right)\left({n}\right)\right)\right)$

### Proof

Step Hyp Ref Expression
1 gsmsymgrfix.s ${⊢}{S}=\mathrm{SymGrp}\left({N}\right)$
2 gsmsymgrfix.b ${⊢}{B}={\mathrm{Base}}_{{S}}$
3 gsmsymgreq.z ${⊢}{Z}=\mathrm{SymGrp}\left({M}\right)$
4 gsmsymgreq.p ${⊢}{P}={\mathrm{Base}}_{{Z}}$
5 gsmsymgreq.i ${⊢}{I}={N}\cap {M}$
6 ccatws1len ${⊢}{X}\in \mathrm{Word}{B}\to \left|{X}\mathrm{++}⟨“{C}”⟩\right|=\left|{X}\right|+1$
7 6 oveq2d ${⊢}{X}\in \mathrm{Word}{B}\to \left(0..^\left|{X}\mathrm{++}⟨“{C}”⟩\right|\right)=\left(0..^\left|{X}\right|+1\right)$
8 lencl ${⊢}{X}\in \mathrm{Word}{B}\to \left|{X}\right|\in {ℕ}_{0}$
9 elnn0uz ${⊢}\left|{X}\right|\in {ℕ}_{0}↔\left|{X}\right|\in {ℤ}_{\ge 0}$
10 8 9 sylib ${⊢}{X}\in \mathrm{Word}{B}\to \left|{X}\right|\in {ℤ}_{\ge 0}$
11 fzosplitsn ${⊢}\left|{X}\right|\in {ℤ}_{\ge 0}\to \left(0..^\left|{X}\right|+1\right)=\left(0..^\left|{X}\right|\right)\cup \left\{\left|{X}\right|\right\}$
12 10 11 syl ${⊢}{X}\in \mathrm{Word}{B}\to \left(0..^\left|{X}\right|+1\right)=\left(0..^\left|{X}\right|\right)\cup \left\{\left|{X}\right|\right\}$
13 7 12 eqtrd ${⊢}{X}\in \mathrm{Word}{B}\to \left(0..^\left|{X}\mathrm{++}⟨“{C}”⟩\right|\right)=\left(0..^\left|{X}\right|\right)\cup \left\{\left|{X}\right|\right\}$
14 13 adantr ${⊢}\left({X}\in \mathrm{Word}{B}\wedge {C}\in {B}\right)\to \left(0..^\left|{X}\mathrm{++}⟨“{C}”⟩\right|\right)=\left(0..^\left|{X}\right|\right)\cup \left\{\left|{X}\right|\right\}$
15 14 3ad2ant1 ${⊢}\left(\left({X}\in \mathrm{Word}{B}\wedge {C}\in {B}\right)\wedge \left({Y}\in \mathrm{Word}{P}\wedge {R}\in {P}\right)\wedge \left|{X}\right|=\left|{Y}\right|\right)\to \left(0..^\left|{X}\mathrm{++}⟨“{C}”⟩\right|\right)=\left(0..^\left|{X}\right|\right)\cup \left\{\left|{X}\right|\right\}$
16 15 raleqdv ${⊢}\left(\left({X}\in \mathrm{Word}{B}\wedge {C}\in {B}\right)\wedge \left({Y}\in \mathrm{Word}{P}\wedge {R}\in {P}\right)\wedge \left|{X}\right|=\left|{Y}\right|\right)\to \left(\forall {i}\in \left(0..^\left|{X}\mathrm{++}⟨“{C}”⟩\right|\right)\phantom{\rule{.4em}{0ex}}\forall {n}\in {I}\phantom{\rule{.4em}{0ex}}\left({X}\mathrm{++}⟨“{C}”⟩\right)\left({i}\right)\left({n}\right)=\left({Y}\mathrm{++}⟨“{R}”⟩\right)\left({i}\right)\left({n}\right)↔\forall {i}\in \left(\left(0..^\left|{X}\right|\right)\cup \left\{\left|{X}\right|\right\}\right)\phantom{\rule{.4em}{0ex}}\forall {n}\in {I}\phantom{\rule{.4em}{0ex}}\left({X}\mathrm{++}⟨“{C}”⟩\right)\left({i}\right)\left({n}\right)=\left({Y}\mathrm{++}⟨“{R}”⟩\right)\left({i}\right)\left({n}\right)\right)$
17 8 adantr ${⊢}\left({X}\in \mathrm{Word}{B}\wedge {C}\in {B}\right)\to \left|{X}\right|\in {ℕ}_{0}$
18 17 3ad2ant1 ${⊢}\left(\left({X}\in \mathrm{Word}{B}\wedge {C}\in {B}\right)\wedge \left({Y}\in \mathrm{Word}{P}\wedge {R}\in {P}\right)\wedge \left|{X}\right|=\left|{Y}\right|\right)\to \left|{X}\right|\in {ℕ}_{0}$
19 fveq2 ${⊢}{i}=\left|{X}\right|\to \left({X}\mathrm{++}⟨“{C}”⟩\right)\left({i}\right)=\left({X}\mathrm{++}⟨“{C}”⟩\right)\left(\left|{X}\right|\right)$
20 19 fveq1d ${⊢}{i}=\left|{X}\right|\to \left({X}\mathrm{++}⟨“{C}”⟩\right)\left({i}\right)\left({n}\right)=\left({X}\mathrm{++}⟨“{C}”⟩\right)\left(\left|{X}\right|\right)\left({n}\right)$
21 fveq2 ${⊢}{i}=\left|{X}\right|\to \left({Y}\mathrm{++}⟨“{R}”⟩\right)\left({i}\right)=\left({Y}\mathrm{++}⟨“{R}”⟩\right)\left(\left|{X}\right|\right)$
22 21 fveq1d ${⊢}{i}=\left|{X}\right|\to \left({Y}\mathrm{++}⟨“{R}”⟩\right)\left({i}\right)\left({n}\right)=\left({Y}\mathrm{++}⟨“{R}”⟩\right)\left(\left|{X}\right|\right)\left({n}\right)$
23 20 22 eqeq12d ${⊢}{i}=\left|{X}\right|\to \left(\left({X}\mathrm{++}⟨“{C}”⟩\right)\left({i}\right)\left({n}\right)=\left({Y}\mathrm{++}⟨“{R}”⟩\right)\left({i}\right)\left({n}\right)↔\left({X}\mathrm{++}⟨“{C}”⟩\right)\left(\left|{X}\right|\right)\left({n}\right)=\left({Y}\mathrm{++}⟨“{R}”⟩\right)\left(\left|{X}\right|\right)\left({n}\right)\right)$
24 23 ralbidv ${⊢}{i}=\left|{X}\right|\to \left(\forall {n}\in {I}\phantom{\rule{.4em}{0ex}}\left({X}\mathrm{++}⟨“{C}”⟩\right)\left({i}\right)\left({n}\right)=\left({Y}\mathrm{++}⟨“{R}”⟩\right)\left({i}\right)\left({n}\right)↔\forall {n}\in {I}\phantom{\rule{.4em}{0ex}}\left({X}\mathrm{++}⟨“{C}”⟩\right)\left(\left|{X}\right|\right)\left({n}\right)=\left({Y}\mathrm{++}⟨“{R}”⟩\right)\left(\left|{X}\right|\right)\left({n}\right)\right)$
25 24 ralunsn ${⊢}\left|{X}\right|\in {ℕ}_{0}\to \left(\forall {i}\in \left(\left(0..^\left|{X}\right|\right)\cup \left\{\left|{X}\right|\right\}\right)\phantom{\rule{.4em}{0ex}}\forall {n}\in {I}\phantom{\rule{.4em}{0ex}}\left({X}\mathrm{++}⟨“{C}”⟩\right)\left({i}\right)\left({n}\right)=\left({Y}\mathrm{++}⟨“{R}”⟩\right)\left({i}\right)\left({n}\right)↔\left(\forall {i}\in \left(0..^\left|{X}\right|\right)\phantom{\rule{.4em}{0ex}}\forall {n}\in {I}\phantom{\rule{.4em}{0ex}}\left({X}\mathrm{++}⟨“{C}”⟩\right)\left({i}\right)\left({n}\right)=\left({Y}\mathrm{++}⟨“{R}”⟩\right)\left({i}\right)\left({n}\right)\wedge \forall {n}\in {I}\phantom{\rule{.4em}{0ex}}\left({X}\mathrm{++}⟨“{C}”⟩\right)\left(\left|{X}\right|\right)\left({n}\right)=\left({Y}\mathrm{++}⟨“{R}”⟩\right)\left(\left|{X}\right|\right)\left({n}\right)\right)\right)$
26 18 25 syl ${⊢}\left(\left({X}\in \mathrm{Word}{B}\wedge {C}\in {B}\right)\wedge \left({Y}\in \mathrm{Word}{P}\wedge {R}\in {P}\right)\wedge \left|{X}\right|=\left|{Y}\right|\right)\to \left(\forall {i}\in \left(\left(0..^\left|{X}\right|\right)\cup \left\{\left|{X}\right|\right\}\right)\phantom{\rule{.4em}{0ex}}\forall {n}\in {I}\phantom{\rule{.4em}{0ex}}\left({X}\mathrm{++}⟨“{C}”⟩\right)\left({i}\right)\left({n}\right)=\left({Y}\mathrm{++}⟨“{R}”⟩\right)\left({i}\right)\left({n}\right)↔\left(\forall {i}\in \left(0..^\left|{X}\right|\right)\phantom{\rule{.4em}{0ex}}\forall {n}\in {I}\phantom{\rule{.4em}{0ex}}\left({X}\mathrm{++}⟨“{C}”⟩\right)\left({i}\right)\left({n}\right)=\left({Y}\mathrm{++}⟨“{R}”⟩\right)\left({i}\right)\left({n}\right)\wedge \forall {n}\in {I}\phantom{\rule{.4em}{0ex}}\left({X}\mathrm{++}⟨“{C}”⟩\right)\left(\left|{X}\right|\right)\left({n}\right)=\left({Y}\mathrm{++}⟨“{R}”⟩\right)\left(\left|{X}\right|\right)\left({n}\right)\right)\right)$
27 simp1l ${⊢}\left(\left({X}\in \mathrm{Word}{B}\wedge {C}\in {B}\right)\wedge \left({Y}\in \mathrm{Word}{P}\wedge {R}\in {P}\right)\wedge \left|{X}\right|=\left|{Y}\right|\right)\to {X}\in \mathrm{Word}{B}$
28 ccats1val1 ${⊢}\left({X}\in \mathrm{Word}{B}\wedge {i}\in \left(0..^\left|{X}\right|\right)\right)\to \left({X}\mathrm{++}⟨“{C}”⟩\right)\left({i}\right)={X}\left({i}\right)$
29 27 28 sylan ${⊢}\left(\left(\left({X}\in \mathrm{Word}{B}\wedge {C}\in {B}\right)\wedge \left({Y}\in \mathrm{Word}{P}\wedge {R}\in {P}\right)\wedge \left|{X}\right|=\left|{Y}\right|\right)\wedge {i}\in \left(0..^\left|{X}\right|\right)\right)\to \left({X}\mathrm{++}⟨“{C}”⟩\right)\left({i}\right)={X}\left({i}\right)$
30 29 fveq1d ${⊢}\left(\left(\left({X}\in \mathrm{Word}{B}\wedge {C}\in {B}\right)\wedge \left({Y}\in \mathrm{Word}{P}\wedge {R}\in {P}\right)\wedge \left|{X}\right|=\left|{Y}\right|\right)\wedge {i}\in \left(0..^\left|{X}\right|\right)\right)\to \left({X}\mathrm{++}⟨“{C}”⟩\right)\left({i}\right)\left({n}\right)={X}\left({i}\right)\left({n}\right)$
31 simp2l ${⊢}\left(\left({X}\in \mathrm{Word}{B}\wedge {C}\in {B}\right)\wedge \left({Y}\in \mathrm{Word}{P}\wedge {R}\in {P}\right)\wedge \left|{X}\right|=\left|{Y}\right|\right)\to {Y}\in \mathrm{Word}{P}$
32 oveq2 ${⊢}\left|{X}\right|=\left|{Y}\right|\to \left(0..^\left|{X}\right|\right)=\left(0..^\left|{Y}\right|\right)$
33 32 eleq2d ${⊢}\left|{X}\right|=\left|{Y}\right|\to \left({i}\in \left(0..^\left|{X}\right|\right)↔{i}\in \left(0..^\left|{Y}\right|\right)\right)$
34 33 biimpd ${⊢}\left|{X}\right|=\left|{Y}\right|\to \left({i}\in \left(0..^\left|{X}\right|\right)\to {i}\in \left(0..^\left|{Y}\right|\right)\right)$
35 34 3ad2ant3 ${⊢}\left(\left({X}\in \mathrm{Word}{B}\wedge {C}\in {B}\right)\wedge \left({Y}\in \mathrm{Word}{P}\wedge {R}\in {P}\right)\wedge \left|{X}\right|=\left|{Y}\right|\right)\to \left({i}\in \left(0..^\left|{X}\right|\right)\to {i}\in \left(0..^\left|{Y}\right|\right)\right)$
36 35 imp ${⊢}\left(\left(\left({X}\in \mathrm{Word}{B}\wedge {C}\in {B}\right)\wedge \left({Y}\in \mathrm{Word}{P}\wedge {R}\in {P}\right)\wedge \left|{X}\right|=\left|{Y}\right|\right)\wedge {i}\in \left(0..^\left|{X}\right|\right)\right)\to {i}\in \left(0..^\left|{Y}\right|\right)$
37 ccats1val1 ${⊢}\left({Y}\in \mathrm{Word}{P}\wedge {i}\in \left(0..^\left|{Y}\right|\right)\right)\to \left({Y}\mathrm{++}⟨“{R}”⟩\right)\left({i}\right)={Y}\left({i}\right)$
38 31 36 37 syl2an2r ${⊢}\left(\left(\left({X}\in \mathrm{Word}{B}\wedge {C}\in {B}\right)\wedge \left({Y}\in \mathrm{Word}{P}\wedge {R}\in {P}\right)\wedge \left|{X}\right|=\left|{Y}\right|\right)\wedge {i}\in \left(0..^\left|{X}\right|\right)\right)\to \left({Y}\mathrm{++}⟨“{R}”⟩\right)\left({i}\right)={Y}\left({i}\right)$
39 38 fveq1d ${⊢}\left(\left(\left({X}\in \mathrm{Word}{B}\wedge {C}\in {B}\right)\wedge \left({Y}\in \mathrm{Word}{P}\wedge {R}\in {P}\right)\wedge \left|{X}\right|=\left|{Y}\right|\right)\wedge {i}\in \left(0..^\left|{X}\right|\right)\right)\to \left({Y}\mathrm{++}⟨“{R}”⟩\right)\left({i}\right)\left({n}\right)={Y}\left({i}\right)\left({n}\right)$
40 30 39 eqeq12d ${⊢}\left(\left(\left({X}\in \mathrm{Word}{B}\wedge {C}\in {B}\right)\wedge \left({Y}\in \mathrm{Word}{P}\wedge {R}\in {P}\right)\wedge \left|{X}\right|=\left|{Y}\right|\right)\wedge {i}\in \left(0..^\left|{X}\right|\right)\right)\to \left(\left({X}\mathrm{++}⟨“{C}”⟩\right)\left({i}\right)\left({n}\right)=\left({Y}\mathrm{++}⟨“{R}”⟩\right)\left({i}\right)\left({n}\right)↔{X}\left({i}\right)\left({n}\right)={Y}\left({i}\right)\left({n}\right)\right)$
41 40 ralbidv ${⊢}\left(\left(\left({X}\in \mathrm{Word}{B}\wedge {C}\in {B}\right)\wedge \left({Y}\in \mathrm{Word}{P}\wedge {R}\in {P}\right)\wedge \left|{X}\right|=\left|{Y}\right|\right)\wedge {i}\in \left(0..^\left|{X}\right|\right)\right)\to \left(\forall {n}\in {I}\phantom{\rule{.4em}{0ex}}\left({X}\mathrm{++}⟨“{C}”⟩\right)\left({i}\right)\left({n}\right)=\left({Y}\mathrm{++}⟨“{R}”⟩\right)\left({i}\right)\left({n}\right)↔\forall {n}\in {I}\phantom{\rule{.4em}{0ex}}{X}\left({i}\right)\left({n}\right)={Y}\left({i}\right)\left({n}\right)\right)$
42 41 ralbidva ${⊢}\left(\left({X}\in \mathrm{Word}{B}\wedge {C}\in {B}\right)\wedge \left({Y}\in \mathrm{Word}{P}\wedge {R}\in {P}\right)\wedge \left|{X}\right|=\left|{Y}\right|\right)\to \left(\forall {i}\in \left(0..^\left|{X}\right|\right)\phantom{\rule{.4em}{0ex}}\forall {n}\in {I}\phantom{\rule{.4em}{0ex}}\left({X}\mathrm{++}⟨“{C}”⟩\right)\left({i}\right)\left({n}\right)=\left({Y}\mathrm{++}⟨“{R}”⟩\right)\left({i}\right)\left({n}\right)↔\forall {i}\in \left(0..^\left|{X}\right|\right)\phantom{\rule{.4em}{0ex}}\forall {n}\in {I}\phantom{\rule{.4em}{0ex}}{X}\left({i}\right)\left({n}\right)={Y}\left({i}\right)\left({n}\right)\right)$
43 eqidd ${⊢}\left({X}\in \mathrm{Word}{B}\wedge {C}\in {B}\right)\to \left|{X}\right|=\left|{X}\right|$
44 ccats1val2 ${⊢}\left({X}\in \mathrm{Word}{B}\wedge {C}\in {B}\wedge \left|{X}\right|=\left|{X}\right|\right)\to \left({X}\mathrm{++}⟨“{C}”⟩\right)\left(\left|{X}\right|\right)={C}$
45 44 fveq1d ${⊢}\left({X}\in \mathrm{Word}{B}\wedge {C}\in {B}\wedge \left|{X}\right|=\left|{X}\right|\right)\to \left({X}\mathrm{++}⟨“{C}”⟩\right)\left(\left|{X}\right|\right)\left({n}\right)={C}\left({n}\right)$
46 43 45 mpd3an3 ${⊢}\left({X}\in \mathrm{Word}{B}\wedge {C}\in {B}\right)\to \left({X}\mathrm{++}⟨“{C}”⟩\right)\left(\left|{X}\right|\right)\left({n}\right)={C}\left({n}\right)$
47 46 3ad2ant1 ${⊢}\left(\left({X}\in \mathrm{Word}{B}\wedge {C}\in {B}\right)\wedge \left({Y}\in \mathrm{Word}{P}\wedge {R}\in {P}\right)\wedge \left|{X}\right|=\left|{Y}\right|\right)\to \left({X}\mathrm{++}⟨“{C}”⟩\right)\left(\left|{X}\right|\right)\left({n}\right)={C}\left({n}\right)$
48 ccats1val2 ${⊢}\left({Y}\in \mathrm{Word}{P}\wedge {R}\in {P}\wedge \left|{X}\right|=\left|{Y}\right|\right)\to \left({Y}\mathrm{++}⟨“{R}”⟩\right)\left(\left|{X}\right|\right)={R}$
49 48 fveq1d ${⊢}\left({Y}\in \mathrm{Word}{P}\wedge {R}\in {P}\wedge \left|{X}\right|=\left|{Y}\right|\right)\to \left({Y}\mathrm{++}⟨“{R}”⟩\right)\left(\left|{X}\right|\right)\left({n}\right)={R}\left({n}\right)$
50 49 3expa ${⊢}\left(\left({Y}\in \mathrm{Word}{P}\wedge {R}\in {P}\right)\wedge \left|{X}\right|=\left|{Y}\right|\right)\to \left({Y}\mathrm{++}⟨“{R}”⟩\right)\left(\left|{X}\right|\right)\left({n}\right)={R}\left({n}\right)$
51 50 3adant1 ${⊢}\left(\left({X}\in \mathrm{Word}{B}\wedge {C}\in {B}\right)\wedge \left({Y}\in \mathrm{Word}{P}\wedge {R}\in {P}\right)\wedge \left|{X}\right|=\left|{Y}\right|\right)\to \left({Y}\mathrm{++}⟨“{R}”⟩\right)\left(\left|{X}\right|\right)\left({n}\right)={R}\left({n}\right)$
52 47 51 eqeq12d ${⊢}\left(\left({X}\in \mathrm{Word}{B}\wedge {C}\in {B}\right)\wedge \left({Y}\in \mathrm{Word}{P}\wedge {R}\in {P}\right)\wedge \left|{X}\right|=\left|{Y}\right|\right)\to \left(\left({X}\mathrm{++}⟨“{C}”⟩\right)\left(\left|{X}\right|\right)\left({n}\right)=\left({Y}\mathrm{++}⟨“{R}”⟩\right)\left(\left|{X}\right|\right)\left({n}\right)↔{C}\left({n}\right)={R}\left({n}\right)\right)$
53 52 ralbidv ${⊢}\left(\left({X}\in \mathrm{Word}{B}\wedge {C}\in {B}\right)\wedge \left({Y}\in \mathrm{Word}{P}\wedge {R}\in {P}\right)\wedge \left|{X}\right|=\left|{Y}\right|\right)\to \left(\forall {n}\in {I}\phantom{\rule{.4em}{0ex}}\left({X}\mathrm{++}⟨“{C}”⟩\right)\left(\left|{X}\right|\right)\left({n}\right)=\left({Y}\mathrm{++}⟨“{R}”⟩\right)\left(\left|{X}\right|\right)\left({n}\right)↔\forall {n}\in {I}\phantom{\rule{.4em}{0ex}}{C}\left({n}\right)={R}\left({n}\right)\right)$
54 42 53 anbi12d ${⊢}\left(\left({X}\in \mathrm{Word}{B}\wedge {C}\in {B}\right)\wedge \left({Y}\in \mathrm{Word}{P}\wedge {R}\in {P}\right)\wedge \left|{X}\right|=\left|{Y}\right|\right)\to \left(\left(\forall {i}\in \left(0..^\left|{X}\right|\right)\phantom{\rule{.4em}{0ex}}\forall {n}\in {I}\phantom{\rule{.4em}{0ex}}\left({X}\mathrm{++}⟨“{C}”⟩\right)\left({i}\right)\left({n}\right)=\left({Y}\mathrm{++}⟨“{R}”⟩\right)\left({i}\right)\left({n}\right)\wedge \forall {n}\in {I}\phantom{\rule{.4em}{0ex}}\left({X}\mathrm{++}⟨“{C}”⟩\right)\left(\left|{X}\right|\right)\left({n}\right)=\left({Y}\mathrm{++}⟨“{R}”⟩\right)\left(\left|{X}\right|\right)\left({n}\right)\right)↔\left(\forall {i}\in \left(0..^\left|{X}\right|\right)\phantom{\rule{.4em}{0ex}}\forall {n}\in {I}\phantom{\rule{.4em}{0ex}}{X}\left({i}\right)\left({n}\right)={Y}\left({i}\right)\left({n}\right)\wedge \forall {n}\in {I}\phantom{\rule{.4em}{0ex}}{C}\left({n}\right)={R}\left({n}\right)\right)\right)$
55 16 26 54 3bitrd ${⊢}\left(\left({X}\in \mathrm{Word}{B}\wedge {C}\in {B}\right)\wedge \left({Y}\in \mathrm{Word}{P}\wedge {R}\in {P}\right)\wedge \left|{X}\right|=\left|{Y}\right|\right)\to \left(\forall {i}\in \left(0..^\left|{X}\mathrm{++}⟨“{C}”⟩\right|\right)\phantom{\rule{.4em}{0ex}}\forall {n}\in {I}\phantom{\rule{.4em}{0ex}}\left({X}\mathrm{++}⟨“{C}”⟩\right)\left({i}\right)\left({n}\right)=\left({Y}\mathrm{++}⟨“{R}”⟩\right)\left({i}\right)\left({n}\right)↔\left(\forall {i}\in \left(0..^\left|{X}\right|\right)\phantom{\rule{.4em}{0ex}}\forall {n}\in {I}\phantom{\rule{.4em}{0ex}}{X}\left({i}\right)\left({n}\right)={Y}\left({i}\right)\left({n}\right)\wedge \forall {n}\in {I}\phantom{\rule{.4em}{0ex}}{C}\left({n}\right)={R}\left({n}\right)\right)\right)$
56 55 ad2antlr ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {M}\in \mathrm{Fin}\right)\wedge \left(\left({X}\in \mathrm{Word}{B}\wedge {C}\in {B}\right)\wedge \left({Y}\in \mathrm{Word}{P}\wedge {R}\in {P}\right)\wedge \left|{X}\right|=\left|{Y}\right|\right)\right)\wedge \left(\forall {i}\in \left(0..^\left|{X}\right|\right)\phantom{\rule{.4em}{0ex}}\forall {n}\in {I}\phantom{\rule{.4em}{0ex}}{X}\left({i}\right)\left({n}\right)={Y}\left({i}\right)\left({n}\right)\to \forall {n}\in {I}\phantom{\rule{.4em}{0ex}}\left({\sum }_{{S}},{X}\right)\left({n}\right)=\left({\sum }_{{Z}},{Y}\right)\left({n}\right)\right)\right)\to \left(\forall {i}\in \left(0..^\left|{X}\mathrm{++}⟨“{C}”⟩\right|\right)\phantom{\rule{.4em}{0ex}}\forall {n}\in {I}\phantom{\rule{.4em}{0ex}}\left({X}\mathrm{++}⟨“{C}”⟩\right)\left({i}\right)\left({n}\right)=\left({Y}\mathrm{++}⟨“{R}”⟩\right)\left({i}\right)\left({n}\right)↔\left(\forall {i}\in \left(0..^\left|{X}\right|\right)\phantom{\rule{.4em}{0ex}}\forall {n}\in {I}\phantom{\rule{.4em}{0ex}}{X}\left({i}\right)\left({n}\right)={Y}\left({i}\right)\left({n}\right)\wedge \forall {n}\in {I}\phantom{\rule{.4em}{0ex}}{C}\left({n}\right)={R}\left({n}\right)\right)\right)$
57 pm3.35 ${⊢}\left(\forall {i}\in \left(0..^\left|{X}\right|\right)\phantom{\rule{.4em}{0ex}}\forall {n}\in {I}\phantom{\rule{.4em}{0ex}}{X}\left({i}\right)\left({n}\right)={Y}\left({i}\right)\left({n}\right)\wedge \left(\forall {i}\in \left(0..^\left|{X}\right|\right)\phantom{\rule{.4em}{0ex}}\forall {n}\in {I}\phantom{\rule{.4em}{0ex}}{X}\left({i}\right)\left({n}\right)={Y}\left({i}\right)\left({n}\right)\to \forall {n}\in {I}\phantom{\rule{.4em}{0ex}}\left({\sum }_{{S}},{X}\right)\left({n}\right)=\left({\sum }_{{Z}},{Y}\right)\left({n}\right)\right)\right)\to \forall {n}\in {I}\phantom{\rule{.4em}{0ex}}\left({\sum }_{{S}},{X}\right)\left({n}\right)=\left({\sum }_{{Z}},{Y}\right)\left({n}\right)$
58 fveq2 ${⊢}{n}={j}\to \left({\sum }_{{S}},{X}\right)\left({n}\right)=\left({\sum }_{{S}},{X}\right)\left({j}\right)$
59 fveq2 ${⊢}{n}={j}\to \left({\sum }_{{Z}},{Y}\right)\left({n}\right)=\left({\sum }_{{Z}},{Y}\right)\left({j}\right)$
60 58 59 eqeq12d ${⊢}{n}={j}\to \left(\left({\sum }_{{S}},{X}\right)\left({n}\right)=\left({\sum }_{{Z}},{Y}\right)\left({n}\right)↔\left({\sum }_{{S}},{X}\right)\left({j}\right)=\left({\sum }_{{Z}},{Y}\right)\left({j}\right)\right)$
61 60 cbvralvw ${⊢}\forall {n}\in {I}\phantom{\rule{.4em}{0ex}}\left({\sum }_{{S}},{X}\right)\left({n}\right)=\left({\sum }_{{Z}},{Y}\right)\left({n}\right)↔\forall {j}\in {I}\phantom{\rule{.4em}{0ex}}\left({\sum }_{{S}},{X}\right)\left({j}\right)=\left({\sum }_{{Z}},{Y}\right)\left({j}\right)$
62 simp-4l ${⊢}\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {M}\in \mathrm{Fin}\right)\wedge \left(\left({X}\in \mathrm{Word}{B}\wedge {C}\in {B}\right)\wedge \left({Y}\in \mathrm{Word}{P}\wedge {R}\in {P}\right)\wedge \left|{X}\right|=\left|{Y}\right|\right)\right)\wedge \forall {j}\in {I}\phantom{\rule{.4em}{0ex}}\left({\sum }_{{S}},{X}\right)\left({j}\right)=\left({\sum }_{{Z}},{Y}\right)\left({j}\right)\right)\wedge {n}\in {I}\right)\to {N}\in \mathrm{Fin}$
63 simp-4r ${⊢}\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {M}\in \mathrm{Fin}\right)\wedge \left(\left({X}\in \mathrm{Word}{B}\wedge {C}\in {B}\right)\wedge \left({Y}\in \mathrm{Word}{P}\wedge {R}\in {P}\right)\wedge \left|{X}\right|=\left|{Y}\right|\right)\right)\wedge \forall {j}\in {I}\phantom{\rule{.4em}{0ex}}\left({\sum }_{{S}},{X}\right)\left({j}\right)=\left({\sum }_{{Z}},{Y}\right)\left({j}\right)\right)\wedge {n}\in {I}\right)\to {M}\in \mathrm{Fin}$
64 simpr ${⊢}\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {M}\in \mathrm{Fin}\right)\wedge \left(\left({X}\in \mathrm{Word}{B}\wedge {C}\in {B}\right)\wedge \left({Y}\in \mathrm{Word}{P}\wedge {R}\in {P}\right)\wedge \left|{X}\right|=\left|{Y}\right|\right)\right)\wedge \forall {j}\in {I}\phantom{\rule{.4em}{0ex}}\left({\sum }_{{S}},{X}\right)\left({j}\right)=\left({\sum }_{{Z}},{Y}\right)\left({j}\right)\right)\wedge {n}\in {I}\right)\to {n}\in {I}$
65 62 63 64 3jca ${⊢}\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {M}\in \mathrm{Fin}\right)\wedge \left(\left({X}\in \mathrm{Word}{B}\wedge {C}\in {B}\right)\wedge \left({Y}\in \mathrm{Word}{P}\wedge {R}\in {P}\right)\wedge \left|{X}\right|=\left|{Y}\right|\right)\right)\wedge \forall {j}\in {I}\phantom{\rule{.4em}{0ex}}\left({\sum }_{{S}},{X}\right)\left({j}\right)=\left({\sum }_{{Z}},{Y}\right)\left({j}\right)\right)\wedge {n}\in {I}\right)\to \left({N}\in \mathrm{Fin}\wedge {M}\in \mathrm{Fin}\wedge {n}\in {I}\right)$
66 65 adantr ${⊢}\left(\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {M}\in \mathrm{Fin}\right)\wedge \left(\left({X}\in \mathrm{Word}{B}\wedge {C}\in {B}\right)\wedge \left({Y}\in \mathrm{Word}{P}\wedge {R}\in {P}\right)\wedge \left|{X}\right|=\left|{Y}\right|\right)\right)\wedge \forall {j}\in {I}\phantom{\rule{.4em}{0ex}}\left({\sum }_{{S}},{X}\right)\left({j}\right)=\left({\sum }_{{Z}},{Y}\right)\left({j}\right)\right)\wedge {n}\in {I}\right)\wedge {C}\left({n}\right)={R}\left({n}\right)\right)\to \left({N}\in \mathrm{Fin}\wedge {M}\in \mathrm{Fin}\wedge {n}\in {I}\right)$
67 simp-4r ${⊢}\left(\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {M}\in \mathrm{Fin}\right)\wedge \left(\left({X}\in \mathrm{Word}{B}\wedge {C}\in {B}\right)\wedge \left({Y}\in \mathrm{Word}{P}\wedge {R}\in {P}\right)\wedge \left|{X}\right|=\left|{Y}\right|\right)\right)\wedge \forall {j}\in {I}\phantom{\rule{.4em}{0ex}}\left({\sum }_{{S}},{X}\right)\left({j}\right)=\left({\sum }_{{Z}},{Y}\right)\left({j}\right)\right)\wedge {n}\in {I}\right)\wedge {C}\left({n}\right)={R}\left({n}\right)\right)\to \left(\left({X}\in \mathrm{Word}{B}\wedge {C}\in {B}\right)\wedge \left({Y}\in \mathrm{Word}{P}\wedge {R}\in {P}\right)\wedge \left|{X}\right|=\left|{Y}\right|\right)$
68 simplr ${⊢}\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {M}\in \mathrm{Fin}\right)\wedge \left(\left({X}\in \mathrm{Word}{B}\wedge {C}\in {B}\right)\wedge \left({Y}\in \mathrm{Word}{P}\wedge {R}\in {P}\right)\wedge \left|{X}\right|=\left|{Y}\right|\right)\right)\wedge \forall {j}\in {I}\phantom{\rule{.4em}{0ex}}\left({\sum }_{{S}},{X}\right)\left({j}\right)=\left({\sum }_{{Z}},{Y}\right)\left({j}\right)\right)\wedge {n}\in {I}\right)\to \forall {j}\in {I}\phantom{\rule{.4em}{0ex}}\left({\sum }_{{S}},{X}\right)\left({j}\right)=\left({\sum }_{{Z}},{Y}\right)\left({j}\right)$
69 68 anim1i ${⊢}\left(\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {M}\in \mathrm{Fin}\right)\wedge \left(\left({X}\in \mathrm{Word}{B}\wedge {C}\in {B}\right)\wedge \left({Y}\in \mathrm{Word}{P}\wedge {R}\in {P}\right)\wedge \left|{X}\right|=\left|{Y}\right|\right)\right)\wedge \forall {j}\in {I}\phantom{\rule{.4em}{0ex}}\left({\sum }_{{S}},{X}\right)\left({j}\right)=\left({\sum }_{{Z}},{Y}\right)\left({j}\right)\right)\wedge {n}\in {I}\right)\wedge {C}\left({n}\right)={R}\left({n}\right)\right)\to \left(\forall {j}\in {I}\phantom{\rule{.4em}{0ex}}\left({\sum }_{{S}},{X}\right)\left({j}\right)=\left({\sum }_{{Z}},{Y}\right)\left({j}\right)\wedge {C}\left({n}\right)={R}\left({n}\right)\right)$
70 1 2 3 4 5 gsmsymgreqlem1 ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {M}\in \mathrm{Fin}\wedge {n}\in {I}\right)\wedge \left(\left({X}\in \mathrm{Word}{B}\wedge {C}\in {B}\right)\wedge \left({Y}\in \mathrm{Word}{P}\wedge {R}\in {P}\right)\wedge \left|{X}\right|=\left|{Y}\right|\right)\right)\to \left(\left(\forall {j}\in {I}\phantom{\rule{.4em}{0ex}}\left({\sum }_{{S}},{X}\right)\left({j}\right)=\left({\sum }_{{Z}},{Y}\right)\left({j}\right)\wedge {C}\left({n}\right)={R}\left({n}\right)\right)\to \left({\sum }_{{S}},\left({X}\mathrm{++}⟨“{C}”⟩\right)\right)\left({n}\right)=\left({\sum }_{{Z}},\left({Y}\mathrm{++}⟨“{R}”⟩\right)\right)\left({n}\right)\right)$
71 70 imp ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {M}\in \mathrm{Fin}\wedge {n}\in {I}\right)\wedge \left(\left({X}\in \mathrm{Word}{B}\wedge {C}\in {B}\right)\wedge \left({Y}\in \mathrm{Word}{P}\wedge {R}\in {P}\right)\wedge \left|{X}\right|=\left|{Y}\right|\right)\right)\wedge \left(\forall {j}\in {I}\phantom{\rule{.4em}{0ex}}\left({\sum }_{{S}},{X}\right)\left({j}\right)=\left({\sum }_{{Z}},{Y}\right)\left({j}\right)\wedge {C}\left({n}\right)={R}\left({n}\right)\right)\right)\to \left({\sum }_{{S}},\left({X}\mathrm{++}⟨“{C}”⟩\right)\right)\left({n}\right)=\left({\sum }_{{Z}},\left({Y}\mathrm{++}⟨“{R}”⟩\right)\right)\left({n}\right)$
72 66 67 69 71 syl21anc ${⊢}\left(\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {M}\in \mathrm{Fin}\right)\wedge \left(\left({X}\in \mathrm{Word}{B}\wedge {C}\in {B}\right)\wedge \left({Y}\in \mathrm{Word}{P}\wedge {R}\in {P}\right)\wedge \left|{X}\right|=\left|{Y}\right|\right)\right)\wedge \forall {j}\in {I}\phantom{\rule{.4em}{0ex}}\left({\sum }_{{S}},{X}\right)\left({j}\right)=\left({\sum }_{{Z}},{Y}\right)\left({j}\right)\right)\wedge {n}\in {I}\right)\wedge {C}\left({n}\right)={R}\left({n}\right)\right)\to \left({\sum }_{{S}},\left({X}\mathrm{++}⟨“{C}”⟩\right)\right)\left({n}\right)=\left({\sum }_{{Z}},\left({Y}\mathrm{++}⟨“{R}”⟩\right)\right)\left({n}\right)$
73 72 ex ${⊢}\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {M}\in \mathrm{Fin}\right)\wedge \left(\left({X}\in \mathrm{Word}{B}\wedge {C}\in {B}\right)\wedge \left({Y}\in \mathrm{Word}{P}\wedge {R}\in {P}\right)\wedge \left|{X}\right|=\left|{Y}\right|\right)\right)\wedge \forall {j}\in {I}\phantom{\rule{.4em}{0ex}}\left({\sum }_{{S}},{X}\right)\left({j}\right)=\left({\sum }_{{Z}},{Y}\right)\left({j}\right)\right)\wedge {n}\in {I}\right)\to \left({C}\left({n}\right)={R}\left({n}\right)\to \left({\sum }_{{S}},\left({X}\mathrm{++}⟨“{C}”⟩\right)\right)\left({n}\right)=\left({\sum }_{{Z}},\left({Y}\mathrm{++}⟨“{R}”⟩\right)\right)\left({n}\right)\right)$
74 73 ralimdva ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {M}\in \mathrm{Fin}\right)\wedge \left(\left({X}\in \mathrm{Word}{B}\wedge {C}\in {B}\right)\wedge \left({Y}\in \mathrm{Word}{P}\wedge {R}\in {P}\right)\wedge \left|{X}\right|=\left|{Y}\right|\right)\right)\wedge \forall {j}\in {I}\phantom{\rule{.4em}{0ex}}\left({\sum }_{{S}},{X}\right)\left({j}\right)=\left({\sum }_{{Z}},{Y}\right)\left({j}\right)\right)\to \left(\forall {n}\in {I}\phantom{\rule{.4em}{0ex}}{C}\left({n}\right)={R}\left({n}\right)\to \forall {n}\in {I}\phantom{\rule{.4em}{0ex}}\left({\sum }_{{S}},\left({X}\mathrm{++}⟨“{C}”⟩\right)\right)\left({n}\right)=\left({\sum }_{{Z}},\left({Y}\mathrm{++}⟨“{R}”⟩\right)\right)\left({n}\right)\right)$
75 74 expcom ${⊢}\forall {j}\in {I}\phantom{\rule{.4em}{0ex}}\left({\sum }_{{S}},{X}\right)\left({j}\right)=\left({\sum }_{{Z}},{Y}\right)\left({j}\right)\to \left(\left(\left({N}\in \mathrm{Fin}\wedge {M}\in \mathrm{Fin}\right)\wedge \left(\left({X}\in \mathrm{Word}{B}\wedge {C}\in {B}\right)\wedge \left({Y}\in \mathrm{Word}{P}\wedge {R}\in {P}\right)\wedge \left|{X}\right|=\left|{Y}\right|\right)\right)\to \left(\forall {n}\in {I}\phantom{\rule{.4em}{0ex}}{C}\left({n}\right)={R}\left({n}\right)\to \forall {n}\in {I}\phantom{\rule{.4em}{0ex}}\left({\sum }_{{S}},\left({X}\mathrm{++}⟨“{C}”⟩\right)\right)\left({n}\right)=\left({\sum }_{{Z}},\left({Y}\mathrm{++}⟨“{R}”⟩\right)\right)\left({n}\right)\right)\right)$
76 61 75 sylbi ${⊢}\forall {n}\in {I}\phantom{\rule{.4em}{0ex}}\left({\sum }_{{S}},{X}\right)\left({n}\right)=\left({\sum }_{{Z}},{Y}\right)\left({n}\right)\to \left(\left(\left({N}\in \mathrm{Fin}\wedge {M}\in \mathrm{Fin}\right)\wedge \left(\left({X}\in \mathrm{Word}{B}\wedge {C}\in {B}\right)\wedge \left({Y}\in \mathrm{Word}{P}\wedge {R}\in {P}\right)\wedge \left|{X}\right|=\left|{Y}\right|\right)\right)\to \left(\forall {n}\in {I}\phantom{\rule{.4em}{0ex}}{C}\left({n}\right)={R}\left({n}\right)\to \forall {n}\in {I}\phantom{\rule{.4em}{0ex}}\left({\sum }_{{S}},\left({X}\mathrm{++}⟨“{C}”⟩\right)\right)\left({n}\right)=\left({\sum }_{{Z}},\left({Y}\mathrm{++}⟨“{R}”⟩\right)\right)\left({n}\right)\right)\right)$
77 76 com23 ${⊢}\forall {n}\in {I}\phantom{\rule{.4em}{0ex}}\left({\sum }_{{S}},{X}\right)\left({n}\right)=\left({\sum }_{{Z}},{Y}\right)\left({n}\right)\to \left(\forall {n}\in {I}\phantom{\rule{.4em}{0ex}}{C}\left({n}\right)={R}\left({n}\right)\to \left(\left(\left({N}\in \mathrm{Fin}\wedge {M}\in \mathrm{Fin}\right)\wedge \left(\left({X}\in \mathrm{Word}{B}\wedge {C}\in {B}\right)\wedge \left({Y}\in \mathrm{Word}{P}\wedge {R}\in {P}\right)\wedge \left|{X}\right|=\left|{Y}\right|\right)\right)\to \forall {n}\in {I}\phantom{\rule{.4em}{0ex}}\left({\sum }_{{S}},\left({X}\mathrm{++}⟨“{C}”⟩\right)\right)\left({n}\right)=\left({\sum }_{{Z}},\left({Y}\mathrm{++}⟨“{R}”⟩\right)\right)\left({n}\right)\right)\right)$
78 57 77 syl ${⊢}\left(\forall {i}\in \left(0..^\left|{X}\right|\right)\phantom{\rule{.4em}{0ex}}\forall {n}\in {I}\phantom{\rule{.4em}{0ex}}{X}\left({i}\right)\left({n}\right)={Y}\left({i}\right)\left({n}\right)\wedge \left(\forall {i}\in \left(0..^\left|{X}\right|\right)\phantom{\rule{.4em}{0ex}}\forall {n}\in {I}\phantom{\rule{.4em}{0ex}}{X}\left({i}\right)\left({n}\right)={Y}\left({i}\right)\left({n}\right)\to \forall {n}\in {I}\phantom{\rule{.4em}{0ex}}\left({\sum }_{{S}},{X}\right)\left({n}\right)=\left({\sum }_{{Z}},{Y}\right)\left({n}\right)\right)\right)\to \left(\forall {n}\in {I}\phantom{\rule{.4em}{0ex}}{C}\left({n}\right)={R}\left({n}\right)\to \left(\left(\left({N}\in \mathrm{Fin}\wedge {M}\in \mathrm{Fin}\right)\wedge \left(\left({X}\in \mathrm{Word}{B}\wedge {C}\in {B}\right)\wedge \left({Y}\in \mathrm{Word}{P}\wedge {R}\in {P}\right)\wedge \left|{X}\right|=\left|{Y}\right|\right)\right)\to \forall {n}\in {I}\phantom{\rule{.4em}{0ex}}\left({\sum }_{{S}},\left({X}\mathrm{++}⟨“{C}”⟩\right)\right)\left({n}\right)=\left({\sum }_{{Z}},\left({Y}\mathrm{++}⟨“{R}”⟩\right)\right)\left({n}\right)\right)\right)$
79 78 impancom ${⊢}\left(\forall {i}\in \left(0..^\left|{X}\right|\right)\phantom{\rule{.4em}{0ex}}\forall {n}\in {I}\phantom{\rule{.4em}{0ex}}{X}\left({i}\right)\left({n}\right)={Y}\left({i}\right)\left({n}\right)\wedge \forall {n}\in {I}\phantom{\rule{.4em}{0ex}}{C}\left({n}\right)={R}\left({n}\right)\right)\to \left(\left(\forall {i}\in \left(0..^\left|{X}\right|\right)\phantom{\rule{.4em}{0ex}}\forall {n}\in {I}\phantom{\rule{.4em}{0ex}}{X}\left({i}\right)\left({n}\right)={Y}\left({i}\right)\left({n}\right)\to \forall {n}\in {I}\phantom{\rule{.4em}{0ex}}\left({\sum }_{{S}},{X}\right)\left({n}\right)=\left({\sum }_{{Z}},{Y}\right)\left({n}\right)\right)\to \left(\left(\left({N}\in \mathrm{Fin}\wedge {M}\in \mathrm{Fin}\right)\wedge \left(\left({X}\in \mathrm{Word}{B}\wedge {C}\in {B}\right)\wedge \left({Y}\in \mathrm{Word}{P}\wedge {R}\in {P}\right)\wedge \left|{X}\right|=\left|{Y}\right|\right)\right)\to \forall {n}\in {I}\phantom{\rule{.4em}{0ex}}\left({\sum }_{{S}},\left({X}\mathrm{++}⟨“{C}”⟩\right)\right)\left({n}\right)=\left({\sum }_{{Z}},\left({Y}\mathrm{++}⟨“{R}”⟩\right)\right)\left({n}\right)\right)\right)$
80 79 com13 ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {M}\in \mathrm{Fin}\right)\wedge \left(\left({X}\in \mathrm{Word}{B}\wedge {C}\in {B}\right)\wedge \left({Y}\in \mathrm{Word}{P}\wedge {R}\in {P}\right)\wedge \left|{X}\right|=\left|{Y}\right|\right)\right)\to \left(\left(\forall {i}\in \left(0..^\left|{X}\right|\right)\phantom{\rule{.4em}{0ex}}\forall {n}\in {I}\phantom{\rule{.4em}{0ex}}{X}\left({i}\right)\left({n}\right)={Y}\left({i}\right)\left({n}\right)\to \forall {n}\in {I}\phantom{\rule{.4em}{0ex}}\left({\sum }_{{S}},{X}\right)\left({n}\right)=\left({\sum }_{{Z}},{Y}\right)\left({n}\right)\right)\to \left(\left(\forall {i}\in \left(0..^\left|{X}\right|\right)\phantom{\rule{.4em}{0ex}}\forall {n}\in {I}\phantom{\rule{.4em}{0ex}}{X}\left({i}\right)\left({n}\right)={Y}\left({i}\right)\left({n}\right)\wedge \forall {n}\in {I}\phantom{\rule{.4em}{0ex}}{C}\left({n}\right)={R}\left({n}\right)\right)\to \forall {n}\in {I}\phantom{\rule{.4em}{0ex}}\left({\sum }_{{S}},\left({X}\mathrm{++}⟨“{C}”⟩\right)\right)\left({n}\right)=\left({\sum }_{{Z}},\left({Y}\mathrm{++}⟨“{R}”⟩\right)\right)\left({n}\right)\right)\right)$
81 80 imp ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {M}\in \mathrm{Fin}\right)\wedge \left(\left({X}\in \mathrm{Word}{B}\wedge {C}\in {B}\right)\wedge \left({Y}\in \mathrm{Word}{P}\wedge {R}\in {P}\right)\wedge \left|{X}\right|=\left|{Y}\right|\right)\right)\wedge \left(\forall {i}\in \left(0..^\left|{X}\right|\right)\phantom{\rule{.4em}{0ex}}\forall {n}\in {I}\phantom{\rule{.4em}{0ex}}{X}\left({i}\right)\left({n}\right)={Y}\left({i}\right)\left({n}\right)\to \forall {n}\in {I}\phantom{\rule{.4em}{0ex}}\left({\sum }_{{S}},{X}\right)\left({n}\right)=\left({\sum }_{{Z}},{Y}\right)\left({n}\right)\right)\right)\to \left(\left(\forall {i}\in \left(0..^\left|{X}\right|\right)\phantom{\rule{.4em}{0ex}}\forall {n}\in {I}\phantom{\rule{.4em}{0ex}}{X}\left({i}\right)\left({n}\right)={Y}\left({i}\right)\left({n}\right)\wedge \forall {n}\in {I}\phantom{\rule{.4em}{0ex}}{C}\left({n}\right)={R}\left({n}\right)\right)\to \forall {n}\in {I}\phantom{\rule{.4em}{0ex}}\left({\sum }_{{S}},\left({X}\mathrm{++}⟨“{C}”⟩\right)\right)\left({n}\right)=\left({\sum }_{{Z}},\left({Y}\mathrm{++}⟨“{R}”⟩\right)\right)\left({n}\right)\right)$
82 56 81 sylbid ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {M}\in \mathrm{Fin}\right)\wedge \left(\left({X}\in \mathrm{Word}{B}\wedge {C}\in {B}\right)\wedge \left({Y}\in \mathrm{Word}{P}\wedge {R}\in {P}\right)\wedge \left|{X}\right|=\left|{Y}\right|\right)\right)\wedge \left(\forall {i}\in \left(0..^\left|{X}\right|\right)\phantom{\rule{.4em}{0ex}}\forall {n}\in {I}\phantom{\rule{.4em}{0ex}}{X}\left({i}\right)\left({n}\right)={Y}\left({i}\right)\left({n}\right)\to \forall {n}\in {I}\phantom{\rule{.4em}{0ex}}\left({\sum }_{{S}},{X}\right)\left({n}\right)=\left({\sum }_{{Z}},{Y}\right)\left({n}\right)\right)\right)\to \left(\forall {i}\in \left(0..^\left|{X}\mathrm{++}⟨“{C}”⟩\right|\right)\phantom{\rule{.4em}{0ex}}\forall {n}\in {I}\phantom{\rule{.4em}{0ex}}\left({X}\mathrm{++}⟨“{C}”⟩\right)\left({i}\right)\left({n}\right)=\left({Y}\mathrm{++}⟨“{R}”⟩\right)\left({i}\right)\left({n}\right)\to \forall {n}\in {I}\phantom{\rule{.4em}{0ex}}\left({\sum }_{{S}},\left({X}\mathrm{++}⟨“{C}”⟩\right)\right)\left({n}\right)=\left({\sum }_{{Z}},\left({Y}\mathrm{++}⟨“{R}”⟩\right)\right)\left({n}\right)\right)$
83 82 ex ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {M}\in \mathrm{Fin}\right)\wedge \left(\left({X}\in \mathrm{Word}{B}\wedge {C}\in {B}\right)\wedge \left({Y}\in \mathrm{Word}{P}\wedge {R}\in {P}\right)\wedge \left|{X}\right|=\left|{Y}\right|\right)\right)\to \left(\left(\forall {i}\in \left(0..^\left|{X}\right|\right)\phantom{\rule{.4em}{0ex}}\forall {n}\in {I}\phantom{\rule{.4em}{0ex}}{X}\left({i}\right)\left({n}\right)={Y}\left({i}\right)\left({n}\right)\to \forall {n}\in {I}\phantom{\rule{.4em}{0ex}}\left({\sum }_{{S}},{X}\right)\left({n}\right)=\left({\sum }_{{Z}},{Y}\right)\left({n}\right)\right)\to \left(\forall {i}\in \left(0..^\left|{X}\mathrm{++}⟨“{C}”⟩\right|\right)\phantom{\rule{.4em}{0ex}}\forall {n}\in {I}\phantom{\rule{.4em}{0ex}}\left({X}\mathrm{++}⟨“{C}”⟩\right)\left({i}\right)\left({n}\right)=\left({Y}\mathrm{++}⟨“{R}”⟩\right)\left({i}\right)\left({n}\right)\to \forall {n}\in {I}\phantom{\rule{.4em}{0ex}}\left({\sum }_{{S}},\left({X}\mathrm{++}⟨“{C}”⟩\right)\right)\left({n}\right)=\left({\sum }_{{Z}},\left({Y}\mathrm{++}⟨“{R}”⟩\right)\right)\left({n}\right)\right)\right)$