Theorem gsuminv

Description: Inverse of a group sum. (Contributed by Mario Carneiro, 15-Dec-2014) (Revised by Mario Carneiro, 4-May-2015) (Revised by AV, 6-Jun-2019)

	Ref	Expression
Hypotheses	gsuminv.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
	gsuminv.z	⊢ 0 = ( 0g ‘ 𝐺 )
	gsuminv.p	⊢ 𝐼 = ( invg ‘ 𝐺 )
	gsuminv.g	⊢ ( 𝜑 → 𝐺 ∈ Abel )
	gsuminv.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	gsuminv.f	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
	gsuminv.n	⊢ ( 𝜑 → 𝐹 finSupp 0 )
Assertion	gsuminv	⊢ ( 𝜑 → ( 𝐺 Σg ( 𝐼 ∘ 𝐹 ) ) = ( 𝐼 ‘ ( 𝐺 Σg 𝐹 ) ) )

Proof

Step	Hyp	Ref	Expression
1		gsuminv.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		gsuminv.z	⊢ 0 = ( 0g ‘ 𝐺 )
3		gsuminv.p	⊢ 𝐼 = ( invg ‘ 𝐺 )
4		gsuminv.g	⊢ ( 𝜑 → 𝐺 ∈ Abel )
5		gsuminv.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
6		gsuminv.f	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
7		gsuminv.n	⊢ ( 𝜑 → 𝐹 finSupp 0 )
8		ablcmn	⊢ ( 𝐺 ∈ Abel → 𝐺 ∈ CMnd )
9	4 8	syl	⊢ ( 𝜑 → 𝐺 ∈ CMnd )
10		cmnmnd	⊢ ( 𝐺 ∈ CMnd → 𝐺 ∈ Mnd )
11	9 10	syl	⊢ ( 𝜑 → 𝐺 ∈ Mnd )
12	1 3	invghm	⊢ ( 𝐺 ∈ Abel ↔ 𝐼 ∈ ( 𝐺 GrpHom 𝐺 ) )
13	4 12	sylib	⊢ ( 𝜑 → 𝐼 ∈ ( 𝐺 GrpHom 𝐺 ) )
14		ghmmhm	⊢ ( 𝐼 ∈ ( 𝐺 GrpHom 𝐺 ) → 𝐼 ∈ ( 𝐺 MndHom 𝐺 ) )
15	13 14	syl	⊢ ( 𝜑 → 𝐼 ∈ ( 𝐺 MndHom 𝐺 ) )
16	1 2 9 11 5 15 6 7	gsummhm	⊢ ( 𝜑 → ( 𝐺 Σg ( 𝐼 ∘ 𝐹 ) ) = ( 𝐼 ‘ ( 𝐺 Σg 𝐹 ) ) )