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

Metamath Proof Explorer

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 𝐻 ) ) )