# Metamath Proof Explorer

## Theorem gsmsymgreqlem1

Description: Lemma 1 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 gsmsymgreqlem1 ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {M}\in \mathrm{Fin}\wedge {J}\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 {n}\in {I}\phantom{\rule{.4em}{0ex}}\left({\sum }_{{S}},{X}\right)\left({n}\right)=\left({\sum }_{{Z}},{Y}\right)\left({n}\right)\wedge {C}\left({J}\right)={R}\left({J}\right)\right)\to \left({\sum }_{{S}},\left({X}\mathrm{++}⟨“{C}”⟩\right)\right)\left({J}\right)=\left({\sum }_{{Z}},\left({Y}\mathrm{++}⟨“{R}”⟩\right)\right)\left({J}\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 simpr ${⊢}\left({X}\in \mathrm{Word}{B}\wedge {C}\in {B}\right)\to {C}\in {B}$
7 simpr ${⊢}\left({Y}\in \mathrm{Word}{P}\wedge {R}\in {P}\right)\to {R}\in {P}$
8 6 7 anim12i ${⊢}\left(\left({X}\in \mathrm{Word}{B}\wedge {C}\in {B}\right)\wedge \left({Y}\in \mathrm{Word}{P}\wedge {R}\in {P}\right)\right)\to \left({C}\in {B}\wedge {R}\in {P}\right)$
9 8 3adant3 ${⊢}\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({C}\in {B}\wedge {R}\in {P}\right)$
10 9 adantl ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {M}\in \mathrm{Fin}\wedge {J}\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({C}\in {B}\wedge {R}\in {P}\right)$
11 10 adantr ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {M}\in \mathrm{Fin}\wedge {J}\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 {n}\in {I}\phantom{\rule{.4em}{0ex}}\left({\sum }_{{S}},{X}\right)\left({n}\right)=\left({\sum }_{{Z}},{Y}\right)\left({n}\right)\wedge {C}\left({J}\right)={R}\left({J}\right)\right)\right)\to \left({C}\in {B}\wedge {R}\in {P}\right)$
12 simpll3 ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {M}\in \mathrm{Fin}\wedge {J}\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 {n}\in {I}\phantom{\rule{.4em}{0ex}}\left({\sum }_{{S}},{X}\right)\left({n}\right)=\left({\sum }_{{Z}},{Y}\right)\left({n}\right)\wedge {C}\left({J}\right)={R}\left({J}\right)\right)\right)\to {J}\in {I}$
13 simpr ${⊢}\left(\forall {n}\in {I}\phantom{\rule{.4em}{0ex}}\left({\sum }_{{S}},{X}\right)\left({n}\right)=\left({\sum }_{{Z}},{Y}\right)\left({n}\right)\wedge {C}\left({J}\right)={R}\left({J}\right)\right)\to {C}\left({J}\right)={R}\left({J}\right)$
14 13 adantl ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {M}\in \mathrm{Fin}\wedge {J}\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 {n}\in {I}\phantom{\rule{.4em}{0ex}}\left({\sum }_{{S}},{X}\right)\left({n}\right)=\left({\sum }_{{Z}},{Y}\right)\left({n}\right)\wedge {C}\left({J}\right)={R}\left({J}\right)\right)\right)\to {C}\left({J}\right)={R}\left({J}\right)$
15 simprl ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {M}\in \mathrm{Fin}\wedge {J}\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 {n}\in {I}\phantom{\rule{.4em}{0ex}}\left({\sum }_{{S}},{X}\right)\left({n}\right)=\left({\sum }_{{Z}},{Y}\right)\left({n}\right)\wedge {C}\left({J}\right)={R}\left({J}\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)$
16 12 14 15 3jca ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {M}\in \mathrm{Fin}\wedge {J}\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 {n}\in {I}\phantom{\rule{.4em}{0ex}}\left({\sum }_{{S}},{X}\right)\left({n}\right)=\left({\sum }_{{Z}},{Y}\right)\left({n}\right)\wedge {C}\left({J}\right)={R}\left({J}\right)\right)\right)\to \left({J}\in {I}\wedge {C}\left({J}\right)={R}\left({J}\right)\wedge \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)$
17 1 2 3 4 5 fvcosymgeq ${⊢}\left({C}\in {B}\wedge {R}\in {P}\right)\to \left(\left({J}\in {I}\wedge {C}\left({J}\right)={R}\left({J}\right)\wedge \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({\sum }_{{S}},{X}\right)\circ {C}\right)\left({J}\right)=\left(\left({\sum }_{{Z}},{Y}\right)\circ {R}\right)\left({J}\right)\right)$
18 11 16 17 sylc ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {M}\in \mathrm{Fin}\wedge {J}\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 {n}\in {I}\phantom{\rule{.4em}{0ex}}\left({\sum }_{{S}},{X}\right)\left({n}\right)=\left({\sum }_{{Z}},{Y}\right)\left({n}\right)\wedge {C}\left({J}\right)={R}\left({J}\right)\right)\right)\to \left(\left({\sum }_{{S}},{X}\right)\circ {C}\right)\left({J}\right)=\left(\left({\sum }_{{Z}},{Y}\right)\circ {R}\right)\left({J}\right)$
19 simpl1 ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {M}\in \mathrm{Fin}\wedge {J}\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 {N}\in \mathrm{Fin}$
20 simpr1l ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {M}\in \mathrm{Fin}\wedge {J}\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 {X}\in \mathrm{Word}{B}$
21 simpr1r ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {M}\in \mathrm{Fin}\wedge {J}\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 {C}\in {B}$
22 19 20 21 3jca ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {M}\in \mathrm{Fin}\wedge {J}\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({N}\in \mathrm{Fin}\wedge {X}\in \mathrm{Word}{B}\wedge {C}\in {B}\right)$
23 22 adantr ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {M}\in \mathrm{Fin}\wedge {J}\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 {n}\in {I}\phantom{\rule{.4em}{0ex}}\left({\sum }_{{S}},{X}\right)\left({n}\right)=\left({\sum }_{{Z}},{Y}\right)\left({n}\right)\wedge {C}\left({J}\right)={R}\left({J}\right)\right)\right)\to \left({N}\in \mathrm{Fin}\wedge {X}\in \mathrm{Word}{B}\wedge {C}\in {B}\right)$
24 1 2 gsumccatsymgsn ${⊢}\left({N}\in \mathrm{Fin}\wedge {X}\in \mathrm{Word}{B}\wedge {C}\in {B}\right)\to {\sum }_{{S}}\left({X}\mathrm{++}⟨“{C}”⟩\right)=\left({\sum }_{{S}},{X}\right)\circ {C}$
25 23 24 syl ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {M}\in \mathrm{Fin}\wedge {J}\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 {n}\in {I}\phantom{\rule{.4em}{0ex}}\left({\sum }_{{S}},{X}\right)\left({n}\right)=\left({\sum }_{{Z}},{Y}\right)\left({n}\right)\wedge {C}\left({J}\right)={R}\left({J}\right)\right)\right)\to {\sum }_{{S}}\left({X}\mathrm{++}⟨“{C}”⟩\right)=\left({\sum }_{{S}},{X}\right)\circ {C}$
26 25 fveq1d ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {M}\in \mathrm{Fin}\wedge {J}\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 {n}\in {I}\phantom{\rule{.4em}{0ex}}\left({\sum }_{{S}},{X}\right)\left({n}\right)=\left({\sum }_{{Z}},{Y}\right)\left({n}\right)\wedge {C}\left({J}\right)={R}\left({J}\right)\right)\right)\to \left({\sum }_{{S}},\left({X}\mathrm{++}⟨“{C}”⟩\right)\right)\left({J}\right)=\left(\left({\sum }_{{S}},{X}\right)\circ {C}\right)\left({J}\right)$
27 simpl2 ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {M}\in \mathrm{Fin}\wedge {J}\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 {M}\in \mathrm{Fin}$
28 simpr2l ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {M}\in \mathrm{Fin}\wedge {J}\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 {Y}\in \mathrm{Word}{P}$
29 simpr2r ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {M}\in \mathrm{Fin}\wedge {J}\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 {R}\in {P}$
30 27 28 29 3jca ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {M}\in \mathrm{Fin}\wedge {J}\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({M}\in \mathrm{Fin}\wedge {Y}\in \mathrm{Word}{P}\wedge {R}\in {P}\right)$
31 30 adantr ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {M}\in \mathrm{Fin}\wedge {J}\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 {n}\in {I}\phantom{\rule{.4em}{0ex}}\left({\sum }_{{S}},{X}\right)\left({n}\right)=\left({\sum }_{{Z}},{Y}\right)\left({n}\right)\wedge {C}\left({J}\right)={R}\left({J}\right)\right)\right)\to \left({M}\in \mathrm{Fin}\wedge {Y}\in \mathrm{Word}{P}\wedge {R}\in {P}\right)$
32 3 4 gsumccatsymgsn ${⊢}\left({M}\in \mathrm{Fin}\wedge {Y}\in \mathrm{Word}{P}\wedge {R}\in {P}\right)\to {\sum }_{{Z}}\left({Y}\mathrm{++}⟨“{R}”⟩\right)=\left({\sum }_{{Z}},{Y}\right)\circ {R}$
33 31 32 syl ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {M}\in \mathrm{Fin}\wedge {J}\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 {n}\in {I}\phantom{\rule{.4em}{0ex}}\left({\sum }_{{S}},{X}\right)\left({n}\right)=\left({\sum }_{{Z}},{Y}\right)\left({n}\right)\wedge {C}\left({J}\right)={R}\left({J}\right)\right)\right)\to {\sum }_{{Z}}\left({Y}\mathrm{++}⟨“{R}”⟩\right)=\left({\sum }_{{Z}},{Y}\right)\circ {R}$
34 33 fveq1d ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {M}\in \mathrm{Fin}\wedge {J}\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 {n}\in {I}\phantom{\rule{.4em}{0ex}}\left({\sum }_{{S}},{X}\right)\left({n}\right)=\left({\sum }_{{Z}},{Y}\right)\left({n}\right)\wedge {C}\left({J}\right)={R}\left({J}\right)\right)\right)\to \left({\sum }_{{Z}},\left({Y}\mathrm{++}⟨“{R}”⟩\right)\right)\left({J}\right)=\left(\left({\sum }_{{Z}},{Y}\right)\circ {R}\right)\left({J}\right)$
35 18 26 34 3eqtr4d ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {M}\in \mathrm{Fin}\wedge {J}\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 {n}\in {I}\phantom{\rule{.4em}{0ex}}\left({\sum }_{{S}},{X}\right)\left({n}\right)=\left({\sum }_{{Z}},{Y}\right)\left({n}\right)\wedge {C}\left({J}\right)={R}\left({J}\right)\right)\right)\to \left({\sum }_{{S}},\left({X}\mathrm{++}⟨“{C}”⟩\right)\right)\left({J}\right)=\left({\sum }_{{Z}},\left({Y}\mathrm{++}⟨“{R}”⟩\right)\right)\left({J}\right)$
36 35 ex ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {M}\in \mathrm{Fin}\wedge {J}\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 {n}\in {I}\phantom{\rule{.4em}{0ex}}\left({\sum }_{{S}},{X}\right)\left({n}\right)=\left({\sum }_{{Z}},{Y}\right)\left({n}\right)\wedge {C}\left({J}\right)={R}\left({J}\right)\right)\to \left({\sum }_{{S}},\left({X}\mathrm{++}⟨“{C}”⟩\right)\right)\left({J}\right)=\left({\sum }_{{Z}},\left({Y}\mathrm{++}⟨“{R}”⟩\right)\right)\left({J}\right)\right)$