Theorem gsummptmhm

Description: Apply a group homomorphism to a group sum expressed with a mapping. (Contributed by Thierry Arnoux, 7-Sep-2018) (Revised by AV, 8-Sep-2019)

	Ref	Expression
Hypotheses	gsummptmhm.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
	gsummptmhm.z	⊢ 0 = ( 0g ‘ 𝐺 )
	gsummptmhm.g	⊢ ( 𝜑 → 𝐺 ∈ CMnd )
	gsummptmhm.h	⊢ ( 𝜑 → 𝐻 ∈ Mnd )
	gsummptmhm.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	gsummptmhm.k	⊢ ( 𝜑 → 𝐾 ∈ ( 𝐺 MndHom 𝐻 ) )
	gsummptmhm.c	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ 𝐵 )
	gsummptmhm.w	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) finSupp 0 )
Assertion	gsummptmhm	⊢ ( 𝜑 → ( 𝐻 Σg ( 𝑥 ∈ 𝐴 ↦ ( 𝐾 ‘ 𝐶 ) ) ) = ( 𝐾 ‘ ( 𝐺 Σg ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		gsummptmhm.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		gsummptmhm.z	⊢ 0 = ( 0g ‘ 𝐺 )
3		gsummptmhm.g	⊢ ( 𝜑 → 𝐺 ∈ CMnd )
4		gsummptmhm.h	⊢ ( 𝜑 → 𝐻 ∈ Mnd )
5		gsummptmhm.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
6		gsummptmhm.k	⊢ ( 𝜑 → 𝐾 ∈ ( 𝐺 MndHom 𝐻 ) )
7		gsummptmhm.c	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ 𝐵 )
8		gsummptmhm.w	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) finSupp 0 )
9		eqidd	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) )
10		eqid	⊢ ( Base ‘ 𝐻 ) = ( Base ‘ 𝐻 )
11	1 10	mhmf	⊢ ( 𝐾 ∈ ( 𝐺 MndHom 𝐻 ) → 𝐾 : 𝐵 ⟶ ( Base ‘ 𝐻 ) )
12		ffn	⊢ ( 𝐾 : 𝐵 ⟶ ( Base ‘ 𝐻 ) → 𝐾 Fn 𝐵 )
13	6 11 12	3syl	⊢ ( 𝜑 → 𝐾 Fn 𝐵 )
14		dffn5	⊢ ( 𝐾 Fn 𝐵 ↔ 𝐾 = ( 𝑦 ∈ 𝐵 ↦ ( 𝐾 ‘ 𝑦 ) ) )
15	13 14	sylib	⊢ ( 𝜑 → 𝐾 = ( 𝑦 ∈ 𝐵 ↦ ( 𝐾 ‘ 𝑦 ) ) )
16		fveq2	⊢ ( 𝑦 = 𝐶 → ( 𝐾 ‘ 𝑦 ) = ( 𝐾 ‘ 𝐶 ) )
17	7 9 15 16	fmptco	⊢ ( 𝜑 → ( 𝐾 ∘ ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ) = ( 𝑥 ∈ 𝐴 ↦ ( 𝐾 ‘ 𝐶 ) ) )
18	17	oveq2d	⊢ ( 𝜑 → ( 𝐻 Σg ( 𝐾 ∘ ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ) ) = ( 𝐻 Σg ( 𝑥 ∈ 𝐴 ↦ ( 𝐾 ‘ 𝐶 ) ) ) )
19	7	fmpttd	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) : 𝐴 ⟶ 𝐵 )
20	1 2 3 4 5 6 19 8	gsummhm	⊢ ( 𝜑 → ( 𝐻 Σg ( 𝐾 ∘ ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ) ) = ( 𝐾 ‘ ( 𝐺 Σg ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ) ) )
21	18 20	eqtr3d	⊢ ( 𝜑 → ( 𝐻 Σg ( 𝑥 ∈ 𝐴 ↦ ( 𝐾 ‘ 𝐶 ) ) ) = ( 𝐾 ‘ ( 𝐺 Σg ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ) ) )