This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem gsummhm

Description: Apply a group homomorphism to a group sum. (Contributed by Mario Carneiro, 15-Dec-2014) (Revised by Mario Carneiro, 24-Apr-2016) (Revised by AV, 6-Jun-2019)

		Ref	Expression
	Hypotheses	gsummhm.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
		gsummhm.z	⊢ 0 = ( 0_g ‘ 𝐺 )
		gsummhm.g	⊢ ( 𝜑 → 𝐺 ∈ CMnd )
		gsummhm.h	⊢ ( 𝜑 → 𝐻 ∈ Mnd )
		gsummhm.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
		gsummhm.k	⊢ ( 𝜑 → 𝐾 ∈ ( 𝐺 MndHom 𝐻 ) )
		gsummhm.f	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
		gsummhm.w	⊢ ( 𝜑 → 𝐹 finSupp 0 )
	Assertion	gsummhm	⊢ ( 𝜑 → ( 𝐻 Σ_g ( 𝐾 ∘ 𝐹 ) ) = ( 𝐾 ‘ ( 𝐺 Σ_g 𝐹 ) ) )

Proof

Step	Hyp	Ref	Expression
1		gsummhm.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		gsummhm.z	⊢ 0 = ( 0_g ‘ 𝐺 )
3		gsummhm.g	⊢ ( 𝜑 → 𝐺 ∈ CMnd )
4		gsummhm.h	⊢ ( 𝜑 → 𝐻 ∈ Mnd )
5		gsummhm.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
6		gsummhm.k	⊢ ( 𝜑 → 𝐾 ∈ ( 𝐺 MndHom 𝐻 ) )
7		gsummhm.f	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
8		gsummhm.w	⊢ ( 𝜑 → 𝐹 finSupp 0 )
9		eqid	⊢ ( Cntz ‘ 𝐺 ) = ( Cntz ‘ 𝐺 )
10		cmnmnd	⊢ ( 𝐺 ∈ CMnd → 𝐺 ∈ Mnd )
11	3 10	syl	⊢ ( 𝜑 → 𝐺 ∈ Mnd )
12	1 9 3 7	cntzcmnf	⊢ ( 𝜑 → ran 𝐹 ⊆ ( ( Cntz ‘ 𝐺 ) ‘ ran 𝐹 ) )
13	1 9 11 4 5 6 7 12 2 8	gsumzmhm	⊢ ( 𝜑 → ( 𝐻 Σ_g ( 𝐾 ∘ 𝐹 ) ) = ( 𝐾 ‘ ( 𝐺 Σ_g 𝐹 ) ) )