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

Metamath Proof Explorer

Theorem gsummptfidmadd

Description: The sum of two group sums expressed as mappings with finite domain. (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 gsummptfidmadd ( 𝜑 → ( 𝐺 Σg ( 𝑥 ∈ 𝐴 ↦ ( 𝐶 + 𝐷 ) ) ) = ( ( 𝐺 Σ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 eqid ⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
10 7 a1i ⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) )
11 8 a1i ⊢ ( 𝜑 → 𝐻 = ( 𝑥 ∈ 𝐴 ↦ 𝐷 ) )
12 fvexd ⊢ ( 𝜑 → ( 0g ‘ 𝐺 ) ∈ V )
13 7 4 5 12 fsuppmptdm ⊢ ( 𝜑 → 𝐹 finSupp ( 0g ‘ 𝐺 ) )
14 8 4 6 12 fsuppmptdm ⊢ ( 𝜑 → 𝐻 finSupp ( 0g ‘ 𝐺 ) )
15 1 9 2 3 4 5 6 10 11 13 14 gsummptfsadd ⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑥 ∈ 𝐴 ↦ ( 𝐶 + 𝐷 ) ) ) = ( ( 𝐺 Σg 𝐹 ) + ( 𝐺 Σg 𝐻 ) ) )