Theorem gsumadd

Description: The sum of two group sums. (Contributed by Mario Carneiro, 19-Dec-2014) (Revised by Mario Carneiro, 25-Apr-2016) (Revised by AV, 5-Jun-2019)

	Ref	Expression
Hypotheses	gsumadd.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
	gsumadd.z	⊢ 0 = ( 0g ‘ 𝐺 )
	gsumadd.p	⊢ + = ( +g ‘ 𝐺 )
	gsumadd.g	⊢ ( 𝜑 → 𝐺 ∈ CMnd )
	gsumadd.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	gsumadd.f	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
	gsumadd.h	⊢ ( 𝜑 → 𝐻 : 𝐴 ⟶ 𝐵 )
	gsumadd.fn	⊢ ( 𝜑 → 𝐹 finSupp 0 )
	gsumadd.hn	⊢ ( 𝜑 → 𝐻 finSupp 0 )
Assertion	gsumadd	⊢ ( 𝜑 → ( 𝐺 Σg ( 𝐹 ∘f + 𝐻 ) ) = ( ( 𝐺 Σg 𝐹 ) + ( 𝐺 Σg 𝐻 ) ) )

Proof

Step	Hyp	Ref	Expression
1		gsumadd.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		gsumadd.z	⊢ 0 = ( 0g ‘ 𝐺 )
3		gsumadd.p	⊢ + = ( +g ‘ 𝐺 )
4		gsumadd.g	⊢ ( 𝜑 → 𝐺 ∈ CMnd )
5		gsumadd.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
6		gsumadd.f	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
7		gsumadd.h	⊢ ( 𝜑 → 𝐻 : 𝐴 ⟶ 𝐵 )
8		gsumadd.fn	⊢ ( 𝜑 → 𝐹 finSupp 0 )
9		gsumadd.hn	⊢ ( 𝜑 → 𝐻 finSupp 0 )
10		eqid	⊢ ( Cntz ‘ 𝐺 ) = ( Cntz ‘ 𝐺 )
11		cmnmnd	⊢ ( 𝐺 ∈ CMnd → 𝐺 ∈ Mnd )
12	4 11	syl	⊢ ( 𝜑 → 𝐺 ∈ Mnd )
13	1	submid	⊢ ( 𝐺 ∈ Mnd → 𝐵 ∈ ( SubMnd ‘ 𝐺 ) )
14	12 13	syl	⊢ ( 𝜑 → 𝐵 ∈ ( SubMnd ‘ 𝐺 ) )
15		ssid	⊢ 𝐵 ⊆ 𝐵
16	1 10	cntzcmn	⊢ ( ( 𝐺 ∈ CMnd ∧ 𝐵 ⊆ 𝐵 ) → ( ( Cntz ‘ 𝐺 ) ‘ 𝐵 ) = 𝐵 )
17	4 15 16	sylancl	⊢ ( 𝜑 → ( ( Cntz ‘ 𝐺 ) ‘ 𝐵 ) = 𝐵 )
18	15 17	sseqtrrid	⊢ ( 𝜑 → 𝐵 ⊆ ( ( Cntz ‘ 𝐺 ) ‘ 𝐵 ) )
19	1 2 3 10 12 5 8 9 14 18 6 7	gsumzadd	⊢ ( 𝜑 → ( 𝐺 Σg ( 𝐹 ∘f + 𝐻 ) ) = ( ( 𝐺 Σg 𝐹 ) + ( 𝐺 Σg 𝐻 ) ) )