Metamath Proof Explorer


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