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