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

Metamath Proof Explorer

Theorem gsummptfidmsub

Description: The difference of two group sums expressed as mappings with finite domain. (Contributed by AV, 7-Nov-2019)

Ref Expression
Hypotheses gsummptfidmsub.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
gsummptfidmsub.s ⊢ − = ( -g ‘ 𝐺 )
gsummptfidmsub.g ⊢ ( 𝜑 → 𝐺 ∈ Abel )
gsummptfidmsub.a ⊢ ( 𝜑 → 𝐴 ∈ Fin )
gsummptfidmsub.c ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ 𝐵 )
gsummptfidmsub.d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐷 ∈ 𝐵 )
gsummptfidmsub.f ⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐶 )
gsummptfidmsub.h ⊢ 𝐻 = ( 𝑥 ∈ 𝐴 ↦ 𝐷 )
Assertion gsummptfidmsub ( 𝜑 → ( 𝐺 Σg ( 𝑥 ∈ 𝐴 ↦ ( 𝐶 − 𝐷 ) ) ) = ( ( 𝐺 Σg 𝐹 ) − ( 𝐺 Σg 𝐻 ) ) )

Proof

Step Hyp Ref Expression
1 gsummptfidmsub.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 gsummptfidmsub.s ⊢ − = ( -g ‘ 𝐺 )
3 gsummptfidmsub.g ⊢ ( 𝜑 → 𝐺 ∈ Abel )
4 gsummptfidmsub.a ⊢ ( 𝜑 → 𝐴 ∈ Fin )
5 gsummptfidmsub.c ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ 𝐵 )
6 gsummptfidmsub.d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐷 ∈ 𝐵 )
7 gsummptfidmsub.f ⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐶 )
8 gsummptfidmsub.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 gsummptfssub ⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑥 ∈ 𝐴 ↦ ( 𝐶 − 𝐷 ) ) ) = ( ( 𝐺 Σg 𝐹 ) − ( 𝐺 Σg 𝐻 ) ) )