Theorem gsummptfsadd

Description: The sum of two group sums expressed as mappings. (Contributed by AV, 4-Apr-2019) (Revised by AV, 9-Jul-2019)

	Ref	Expression
Hypotheses	gsummptfsadd.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
	gsummptfsadd.z	⊢ 0 = ( 0g ‘ 𝐺 )
	gsummptfsadd.p	⊢ + = ( +g ‘ 𝐺 )
	gsummptfsadd.g	⊢ ( 𝜑 → 𝐺 ∈ CMnd )
	gsummptfsadd.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	gsummptfsadd.c	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ 𝐵 )
	gsummptfsadd.d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐷 ∈ 𝐵 )
	gsummptfsadd.f	⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) )
	gsummptfsadd.h	⊢ ( 𝜑 → 𝐻 = ( 𝑥 ∈ 𝐴 ↦ 𝐷 ) )
	gsummptfsadd.w	⊢ ( 𝜑 → 𝐹 finSupp 0 )
	gsummptfsadd.v	⊢ ( 𝜑 → 𝐻 finSupp 0 )
Assertion	gsummptfsadd	⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑥 ∈ 𝐴 ↦ ( 𝐶 + 𝐷 ) ) ) = ( ( 𝐺 Σg 𝐹 ) + ( 𝐺 Σg 𝐻 ) ) )

Proof

Step	Hyp	Ref	Expression
1		gsummptfsadd.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		gsummptfsadd.z	⊢ 0 = ( 0g ‘ 𝐺 )
3		gsummptfsadd.p	⊢ + = ( +g ‘ 𝐺 )
4		gsummptfsadd.g	⊢ ( 𝜑 → 𝐺 ∈ CMnd )
5		gsummptfsadd.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
6		gsummptfsadd.c	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ 𝐵 )
7		gsummptfsadd.d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐷 ∈ 𝐵 )
8		gsummptfsadd.f	⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) )
9		gsummptfsadd.h	⊢ ( 𝜑 → 𝐻 = ( 𝑥 ∈ 𝐴 ↦ 𝐷 ) )
10		gsummptfsadd.w	⊢ ( 𝜑 → 𝐹 finSupp 0 )
11		gsummptfsadd.v	⊢ ( 𝜑 → 𝐻 finSupp 0 )
12	5 6 7 8 9	offval2	⊢ ( 𝜑 → ( 𝐹 ∘f + 𝐻 ) = ( 𝑥 ∈ 𝐴 ↦ ( 𝐶 + 𝐷 ) ) )
13	12	eqcomd	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( 𝐶 + 𝐷 ) ) = ( 𝐹 ∘f + 𝐻 ) )
14	13	oveq2d	⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑥 ∈ 𝐴 ↦ ( 𝐶 + 𝐷 ) ) ) = ( 𝐺 Σg ( 𝐹 ∘f + 𝐻 ) ) )
15	8 6	fmpt3d	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
16	9 7	fmpt3d	⊢ ( 𝜑 → 𝐻 : 𝐴 ⟶ 𝐵 )
17	1 2 3 4 5 15 16 10 11	gsumadd	⊢ ( 𝜑 → ( 𝐺 Σg ( 𝐹 ∘f + 𝐻 ) ) = ( ( 𝐺 Σg 𝐹 ) + ( 𝐺 Σg 𝐻 ) ) )
18	14 17	eqtrd	⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑥 ∈ 𝐴 ↦ ( 𝐶 + 𝐷 ) ) ) = ( ( 𝐺 Σg 𝐹 ) + ( 𝐺 Σg 𝐻 ) ) )