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	⊢ 𝐵 = ( Base ‘ 𝐺 )
	gsummhm2.z	⊢ 0 = ( 0g ‘ 𝐺 )
	gsummhm2.g	⊢ ( 𝜑 → 𝐺 ∈ CMnd )
	gsummhm2.h	⊢ ( 𝜑 → 𝐻 ∈ Mnd )
	gsummhm2.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	gsummhm2.k	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) ∈ ( 𝐺 MndHom 𝐻 ) )
	gsummhm2.f	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝑋 ∈ 𝐵 )
	gsummhm2.w	⊢ ( 𝜑 → ( 𝑘 ∈ 𝐴 ↦ 𝑋 ) finSupp 0 )
	gsummhm2.1	⊢ ( 𝑥 = 𝑋 → 𝐶 = 𝐷 )
	gsummhm2.2	⊢ ( 𝑥 = ( 𝐺 Σg ( 𝑘 ∈ 𝐴 ↦ 𝑋 ) ) → 𝐶 = 𝐸 )
Assertion	gsummhm2	⊢ ( 𝜑 → ( 𝐻 Σg ( 𝑘 ∈ 𝐴 ↦ 𝐷 ) ) = 𝐸 )

Proof

Step	Hyp	Ref	Expression
1		gsummhm2.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		gsummhm2.z	⊢ 0 = ( 0g ‘ 𝐺 )
3		gsummhm2.g	⊢ ( 𝜑 → 𝐺 ∈ CMnd )
4		gsummhm2.h	⊢ ( 𝜑 → 𝐻 ∈ Mnd )
5		gsummhm2.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
6		gsummhm2.k	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) ∈ ( 𝐺 MndHom 𝐻 ) )
7		gsummhm2.f	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝑋 ∈ 𝐵 )
8		gsummhm2.w	⊢ ( 𝜑 → ( 𝑘 ∈ 𝐴 ↦ 𝑋 ) finSupp 0 )
9		gsummhm2.1	⊢ ( 𝑥 = 𝑋 → 𝐶 = 𝐷 )
10		gsummhm2.2	⊢ ( 𝑥 = ( 𝐺 Σg ( 𝑘 ∈ 𝐴 ↦ 𝑋 ) ) → 𝐶 = 𝐸 )
11	7	fmpttd	⊢ ( 𝜑 → ( 𝑘 ∈ 𝐴 ↦ 𝑋 ) : 𝐴 ⟶ 𝐵 )
12	1 2 3 4 5 6 11 8	gsummhm	⊢ ( 𝜑 → ( 𝐻 Σg ( ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) ∘ ( 𝑘 ∈ 𝐴 ↦ 𝑋 ) ) ) = ( ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) ‘ ( 𝐺 Σg ( 𝑘 ∈ 𝐴 ↦ 𝑋 ) ) ) )
13		eqidd	⊢ ( 𝜑 → ( 𝑘 ∈ 𝐴 ↦ 𝑋 ) = ( 𝑘 ∈ 𝐴 ↦ 𝑋 ) )
14		eqidd	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) = ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) )
15	7 13 14 9	fmptco	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) ∘ ( 𝑘 ∈ 𝐴 ↦ 𝑋 ) ) = ( 𝑘 ∈ 𝐴 ↦ 𝐷 ) )
16	15	oveq2d	⊢ ( 𝜑 → ( 𝐻 Σg ( ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) ∘ ( 𝑘 ∈ 𝐴 ↦ 𝑋 ) ) ) = ( 𝐻 Σg ( 𝑘 ∈ 𝐴 ↦ 𝐷 ) ) )
17		eqid	⊢ ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) = ( 𝑥 ∈ 𝐵 ↦ 𝐶 )
18	1 2 3 5 11 8	gsumcl	⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑘 ∈ 𝐴 ↦ 𝑋 ) ) ∈ 𝐵 )
19	10	eleq1d	⊢ ( 𝑥 = ( 𝐺 Σg ( 𝑘 ∈ 𝐴 ↦ 𝑋 ) ) → ( 𝐶 ∈ ( Base ‘ 𝐻 ) ↔ 𝐸 ∈ ( Base ‘ 𝐻 ) ) )
20		eqid	⊢ ( Base ‘ 𝐻 ) = ( Base ‘ 𝐻 )
21	1 20	mhmf	⊢ ( ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) ∈ ( 𝐺 MndHom 𝐻 ) → ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) : 𝐵 ⟶ ( Base ‘ 𝐻 ) )
22	6 21	syl	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) : 𝐵 ⟶ ( Base ‘ 𝐻 ) )
23	17	fmpt	⊢ ( ∀ 𝑥 ∈ 𝐵 𝐶 ∈ ( Base ‘ 𝐻 ) ↔ ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) : 𝐵 ⟶ ( Base ‘ 𝐻 ) )
24	22 23	sylibr	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 𝐶 ∈ ( Base ‘ 𝐻 ) )
25	19 24 18	rspcdva	⊢ ( 𝜑 → 𝐸 ∈ ( Base ‘ 𝐻 ) )
26	17 10 18 25	fvmptd3	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) ‘ ( 𝐺 Σg ( 𝑘 ∈ 𝐴 ↦ 𝑋 ) ) ) = 𝐸 )
27	12 16 26	3eqtr3d	⊢ ( 𝜑 → ( 𝐻 Σg ( 𝑘 ∈ 𝐴 ↦ 𝐷 ) ) = 𝐸 )