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

Metamath Proof Explorer

Theorem gsumsplit2

Description: Split a group sum into two parts. (Contributed by Mario Carneiro, 19-Dec-2014) (Revised by AV, 5-Jun-2019)

Ref Expression
Hypotheses gsumsplit2.b ⊢ B = Base G
gsumsplit2.z ⊢ 0 ˙ = 0 G
gsumsplit2.p ⊢ + ˙ = + G
gsumsplit2.g ⊢ φ → G ∈ CMnd
gsumsplit2.a ⊢ φ → A ∈ V
gsumsplit2.f ⊢ φ ∧ k ∈ A → X ∈ B
gsumsplit2.w ⊢ φ → finSupp 0 ˙⁡ k ∈ A ⟼ X
gsumsplit2.i ⊢ φ → C ∩ D = ∅
gsumsplit2.u ⊢ φ → A = C ∪ D
Assertion gsumsplit2 ⊢ φ → ∑ G k ∈ A X = ∑ G k ∈ C X + ˙ ∑ G k ∈ D X

Proof

Step Hyp Ref Expression
1 gsumsplit2.b ⊢ B = Base G
2 gsumsplit2.z ⊢ 0 ˙ = 0 G
3 gsumsplit2.p ⊢ + ˙ = + G
4 gsumsplit2.g ⊢ φ → G ∈ CMnd
5 gsumsplit2.a ⊢ φ → A ∈ V
6 gsumsplit2.f ⊢ φ ∧ k ∈ A → X ∈ B
7 gsumsplit2.w ⊢ φ → finSupp 0 ˙⁡ k ∈ A ⟼ X
8 gsumsplit2.i ⊢ φ → C ∩ D = ∅
9 gsumsplit2.u ⊢ φ → A = C ∪ D
10 6 fmpttd ⊢ φ → k ∈ A ⟼ X : A ⟶ B
11 1 2 3 4 5 10 7 8 9 gsumsplit ⊢ φ → ∑ G k ∈ A X = ∑ G k ∈ A ⟼ X ↾ C + ˙ ∑ G k ∈ A ⟼ X ↾ D
12 ssun1 ⊢ C ⊆ C ∪ D
13 12 9 sseqtrrid ⊢ φ → C ⊆ A
14 13 resmptd ⊢ φ → k ∈ A ⟼ X ↾ C = k ∈ C ⟼ X
15 14 oveq2d ⊢ φ → ∑ G k ∈ A ⟼ X ↾ C = ∑ G k ∈ C X
16 ssun2 ⊢ D ⊆ C ∪ D
17 16 9 sseqtrrid ⊢ φ → D ⊆ A
18 17 resmptd ⊢ φ → k ∈ A ⟼ X ↾ D = k ∈ D ⟼ X
19 18 oveq2d ⊢ φ → ∑ G k ∈ A ⟼ X ↾ D = ∑ G k ∈ D X
20 15 19 oveq12d ⊢ φ → ∑ G k ∈ A ⟼ X ↾ C + ˙ ∑ G k ∈ A ⟼ X ↾ D = ∑ G k ∈ C X + ˙ ∑ G k ∈ D X
21 11 20 eqtrd ⊢ φ → ∑ G k ∈ A X = ∑ G k ∈ C X + ˙ ∑ G k ∈ D X