Theorem gsummptfidmadd2

Description: The sum of two group sums expressed as mappings with finite domain, using a function operation. (Contributed by AV, 23-Jul-2019)

	Ref	Expression
Hypotheses	gsummptfidmadd.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
	gsummptfidmadd.p	⊢ + = ( +g ‘ 𝐺 )
	gsummptfidmadd.g	⊢ ( 𝜑 → 𝐺 ∈ CMnd )
	gsummptfidmadd.a	⊢ ( 𝜑 → 𝐴 ∈ Fin )
	gsummptfidmadd.c	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ 𝐵 )
	gsummptfidmadd.d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐷 ∈ 𝐵 )
	gsummptfidmadd.f	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐶 )
	gsummptfidmadd.h	⊢ 𝐻 = ( 𝑥 ∈ 𝐴 ↦ 𝐷 )
Assertion	gsummptfidmadd2	⊢ ( 𝜑 → ( 𝐺 Σg ( 𝐹 ∘f + 𝐻 ) ) = ( ( 𝐺 Σg 𝐹 ) + ( 𝐺 Σg 𝐻 ) ) )

Proof

Step	Hyp	Ref	Expression
1		gsummptfidmadd.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		gsummptfidmadd.p	⊢ + = ( +g ‘ 𝐺 )
3		gsummptfidmadd.g	⊢ ( 𝜑 → 𝐺 ∈ CMnd )
4		gsummptfidmadd.a	⊢ ( 𝜑 → 𝐴 ∈ Fin )
5		gsummptfidmadd.c	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ 𝐵 )
6		gsummptfidmadd.d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐷 ∈ 𝐵 )
7		gsummptfidmadd.f	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐶 )
8		gsummptfidmadd.h	⊢ 𝐻 = ( 𝑥 ∈ 𝐴 ↦ 𝐷 )
9	7	a1i	⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) )
10	8	a1i	⊢ ( 𝜑 → 𝐻 = ( 𝑥 ∈ 𝐴 ↦ 𝐷 ) )
11	4 5 6 9 10	offval2	⊢ ( 𝜑 → ( 𝐹 ∘f + 𝐻 ) = ( 𝑥 ∈ 𝐴 ↦ ( 𝐶 + 𝐷 ) ) )
12	11	oveq2d	⊢ ( 𝜑 → ( 𝐺 Σg ( 𝐹 ∘f + 𝐻 ) ) = ( 𝐺 Σg ( 𝑥 ∈ 𝐴 ↦ ( 𝐶 + 𝐷 ) ) ) )
13	1 2 3 4 5 6 7 8	gsummptfidmadd	⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑥 ∈ 𝐴 ↦ ( 𝐶 + 𝐷 ) ) ) = ( ( 𝐺 Σg 𝐹 ) + ( 𝐺 Σg 𝐻 ) ) )
14	12 13	eqtrd	⊢ ( 𝜑 → ( 𝐺 Σg ( 𝐹 ∘f + 𝐻 ) ) = ( ( 𝐺 Σg 𝐹 ) + ( 𝐺 Σg 𝐻 ) ) )