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	$$⊢\underset{\dot{}}{0}=0_G$$
	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	$$⊢\phi \to {finSupp}_{\underset{\dot{}}{0}}\left(\left(k\in A⟼X\right)\right)$$
	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	$$⊢\underset{\dot{}}{0}=0_G$$
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	$$⊢\phi \to {finSupp}_{\underset{\dot{}}{0}}\left(\left(k\in A⟼X\right)\right)$$
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\leftrightarrow 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 BC\in {\mathrm{Base}}_H\leftrightarrow \left(x\in B⟼C\right):B⟶{\mathrm{Base}}_H$$
24	22 23	sylibr	$$⊢\phi \to \forall x\in BC\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$$