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

Metamath Proof Explorer

Theorem gsummptfidmsplit

Description: Split a group sum expressed as mapping with a finite domain into two parts. (Contributed by AV, 23-Jul-2019)

Ref Expression
Hypotheses gsummptfidmsplit.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
gsummptfidmsplit.p ⊢ + = ( +g ‘ 𝐺 )
gsummptfidmsplit.g ⊢ ( 𝜑 → 𝐺 ∈ CMnd )
gsummptfidmsplit.a ⊢ ( 𝜑 → 𝐴 ∈ Fin )
gsummptfidmsplit.y ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝑌 ∈ 𝐵 )
gsummptfidmsplit.i ⊢ ( 𝜑 → ( 𝐶 ∩ 𝐷 ) = ∅ )
gsummptfidmsplit.u ⊢ ( 𝜑 → 𝐴 = ( 𝐶 ∪ 𝐷 ) )
Assertion gsummptfidmsplit ( 𝜑 → ( 𝐺 Σg ( 𝑘 ∈ 𝐴 ↦ 𝑌 ) ) = ( ( 𝐺 Σg ( 𝑘 ∈ 𝐶 ↦ 𝑌 ) ) + ( 𝐺 Σg ( 𝑘 ∈ 𝐷 ↦ 𝑌 ) ) ) )

Proof

Step Hyp Ref Expression
1 gsummptfidmsplit.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 gsummptfidmsplit.p ⊢ + = ( +g ‘ 𝐺 )
3 gsummptfidmsplit.g ⊢ ( 𝜑 → 𝐺 ∈ CMnd )
4 gsummptfidmsplit.a ⊢ ( 𝜑 → 𝐴 ∈ Fin )
5 gsummptfidmsplit.y ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝑌 ∈ 𝐵 )
6 gsummptfidmsplit.i ⊢ ( 𝜑 → ( 𝐶 ∩ 𝐷 ) = ∅ )
7 gsummptfidmsplit.u ⊢ ( 𝜑 → 𝐴 = ( 𝐶 ∪ 𝐷 ) )
8 eqid ⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
9 eqid ⊢ ( 𝑘 ∈ 𝐴 ↦ 𝑌 ) = ( 𝑘 ∈ 𝐴 ↦ 𝑌 )
10 fvexd ⊢ ( 𝜑 → ( 0g ‘ 𝐺 ) ∈ V )
11 9 4 5 10 fsuppmptdm ⊢ ( 𝜑 → ( 𝑘 ∈ 𝐴 ↦ 𝑌 ) finSupp ( 0g ‘ 𝐺 ) )
12 1 8 2 3 4 5 11 6 7 gsumsplit2 ⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑘 ∈ 𝐴 ↦ 𝑌 ) ) = ( ( 𝐺 Σg ( 𝑘 ∈ 𝐶 ↦ 𝑌 ) ) + ( 𝐺 Σg ( 𝑘 ∈ 𝐷 ↦ 𝑌 ) ) ) )