# Metamath Proof Explorer

## Theorem gsummhm2

Description: Apply a group homomorphism to a group sum, mapping version with implicit substitution. (Contributed by Mario Carneiro, 5-May-2015) (Revised by AV, 6-Jun-2019)

Ref Expression
Hypotheses gsummhm2.b ${⊢}{B}={\mathrm{Base}}_{{G}}$
gsummhm2.z
gsummhm2.g ${⊢}{\phi }\to {G}\in \mathrm{CMnd}$
gsummhm2.h ${⊢}{\phi }\to {H}\in \mathrm{Mnd}$
gsummhm2.a ${⊢}{\phi }\to {A}\in {V}$
gsummhm2.k ${⊢}{\phi }\to \left({x}\in {B}⟼{C}\right)\in \left({G}\mathrm{MndHom}{H}\right)$
gsummhm2.f ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to {X}\in {B}$
gsummhm2.w
gsummhm2.1 ${⊢}{x}={X}\to {C}={D}$
gsummhm2.2 ${⊢}{x}=\underset{{k}\in {A}}{{\sum }_{{G}}}{X}\to {C}={E}$
Assertion gsummhm2 ${⊢}{\phi }\to \underset{{k}\in {A}}{{\sum }_{{H}}}{D}={E}$

### Proof

Step Hyp Ref Expression
1 gsummhm2.b ${⊢}{B}={\mathrm{Base}}_{{G}}$
2 gsummhm2.z
3 gsummhm2.g ${⊢}{\phi }\to {G}\in \mathrm{CMnd}$
4 gsummhm2.h ${⊢}{\phi }\to {H}\in \mathrm{Mnd}$
5 gsummhm2.a ${⊢}{\phi }\to {A}\in {V}$
6 gsummhm2.k ${⊢}{\phi }\to \left({x}\in {B}⟼{C}\right)\in \left({G}\mathrm{MndHom}{H}\right)$
7 gsummhm2.f ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to {X}\in {B}$
8 gsummhm2.w
9 gsummhm2.1 ${⊢}{x}={X}\to {C}={D}$
10 gsummhm2.2 ${⊢}{x}=\underset{{k}\in {A}}{{\sum }_{{G}}}{X}\to {C}={E}$
11 7 fmpttd ${⊢}{\phi }\to \left({k}\in {A}⟼{X}\right):{A}⟶{B}$
12 1 2 3 4 5 6 11 8 gsummhm ${⊢}{\phi }\to {\sum }_{{H}}\left(\left({x}\in {B}⟼{C}\right)\circ \left({k}\in {A}⟼{X}\right)\right)=\left({x}\in {B}⟼{C}\right)\left(\underset{{k}\in {A}}{{\sum }_{{G}}}{X}\right)$
13 eqidd ${⊢}{\phi }\to \left({k}\in {A}⟼{X}\right)=\left({k}\in {A}⟼{X}\right)$
14 eqidd ${⊢}{\phi }\to \left({x}\in {B}⟼{C}\right)=\left({x}\in {B}⟼{C}\right)$
15 7 13 14 9 fmptco ${⊢}{\phi }\to \left({x}\in {B}⟼{C}\right)\circ \left({k}\in {A}⟼{X}\right)=\left({k}\in {A}⟼{D}\right)$
16 15 oveq2d ${⊢}{\phi }\to {\sum }_{{H}}\left(\left({x}\in {B}⟼{C}\right)\circ \left({k}\in {A}⟼{X}\right)\right)=\underset{{k}\in {A}}{{\sum }_{{H}}}{D}$
17 eqid ${⊢}\left({x}\in {B}⟼{C}\right)=\left({x}\in {B}⟼{C}\right)$
18 1 2 3 5 11 8 gsumcl ${⊢}{\phi }\to \underset{{k}\in {A}}{{\sum }_{{G}}}{X}\in {B}$
19 10 eleq1d ${⊢}{x}=\underset{{k}\in {A}}{{\sum }_{{G}}}{X}\to \left({C}\in {\mathrm{Base}}_{{H}}↔{E}\in {\mathrm{Base}}_{{H}}\right)$
20 eqid ${⊢}{\mathrm{Base}}_{{H}}={\mathrm{Base}}_{{H}}$
21 1 20 mhmf ${⊢}\left({x}\in {B}⟼{C}\right)\in \left({G}\mathrm{MndHom}{H}\right)\to \left({x}\in {B}⟼{C}\right):{B}⟶{\mathrm{Base}}_{{H}}$
22 6 21 syl ${⊢}{\phi }\to \left({x}\in {B}⟼{C}\right):{B}⟶{\mathrm{Base}}_{{H}}$
23 17 fmpt ${⊢}\forall {x}\in {B}\phantom{\rule{.4em}{0ex}}{C}\in {\mathrm{Base}}_{{H}}↔\left({x}\in {B}⟼{C}\right):{B}⟶{\mathrm{Base}}_{{H}}$
24 22 23 sylibr ${⊢}{\phi }\to \forall {x}\in {B}\phantom{\rule{.4em}{0ex}}{C}\in {\mathrm{Base}}_{{H}}$
25 19 24 18 rspcdva ${⊢}{\phi }\to {E}\in {\mathrm{Base}}_{{H}}$
26 17 10 18 25 fvmptd3 ${⊢}{\phi }\to \left({x}\in {B}⟼{C}\right)\left(\underset{{k}\in {A}}{{\sum }_{{G}}}{X}\right)={E}$
27 12 16 26 3eqtr3d ${⊢}{\phi }\to \underset{{k}\in {A}}{{\sum }_{{H}}}{D}={E}$