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

Metamath Proof Explorer

Theorem gsumdifsnd

Description: Extract a summand from a finitely supported group sum. (Contributed by AV, 21-Apr-2019) (Revised by AV, 28-Jul-2019)

Ref Expression
Hypotheses gsumdifsnd.b ⊢ B = Base G
gsumdifsnd.p ⊢ + ˙ = + G
gsumdifsnd.g ⊢ φ → G ∈ CMnd
gsumdifsnd.a ⊢ φ → A ∈ W
gsumdifsnd.f ⊢ φ → finSupp 0 G⁡ k ∈ A ⟼ X
gsumdifsnd.e ⊢ φ ∧ k ∈ A → X ∈ B
gsumdifsnd.m ⊢ φ → M ∈ A
gsumdifsnd.y ⊢ φ → Y ∈ B
gsumdifsnd.s ⊢ φ ∧ k = M → X = Y
Assertion gsumdifsnd ⊢ φ → ∑ G k ∈ A X = ∑ G k ∈ A ∖ M X + ˙ Y

Proof

Step Hyp Ref Expression
1 gsumdifsnd.b ⊢ B = Base G
2 gsumdifsnd.p ⊢ + ˙ = + G
3 gsumdifsnd.g ⊢ φ → G ∈ CMnd
4 gsumdifsnd.a ⊢ φ → A ∈ W
5 gsumdifsnd.f ⊢ φ → finSupp 0 G⁡ k ∈ A ⟼ X
6 gsumdifsnd.e ⊢ φ ∧ k ∈ A → X ∈ B
7 gsumdifsnd.m ⊢ φ → M ∈ A
8 gsumdifsnd.y ⊢ φ → Y ∈ B
9 gsumdifsnd.s ⊢ φ ∧ k = M → X = Y
10 eqid ⊢ 0 G = 0 G
11 7 snssd ⊢ φ → M ⊆ A
12 difin2 ⊢ M ⊆ A → M ∖ M = A ∖ M ∩ M
13 11 12 syl ⊢ φ → M ∖ M = A ∖ M ∩ M
14 difid ⊢ M ∖ M = ∅
15 13 14 eqtr3di ⊢ φ → A ∖ M ∩ M = ∅
16 difsnid ⊢ M ∈ A → A ∖ M ∪ M = A
17 7 16 syl ⊢ φ → A ∖ M ∪ M = A
18 17 eqcomd ⊢ φ → A = A ∖ M ∪ M
19 1 10 2 3 4 6 5 15 18 gsumsplit2 ⊢ φ → ∑ G k ∈ A X = ∑ G k ∈ A ∖ M X + ˙ ∑ G k ∈ M X
20 cmnmnd ⊢ G ∈ CMnd → G ∈ Mnd
21 3 20 syl ⊢ φ → G ∈ Mnd
22 1 21 7 8 9 gsumsnd ⊢ φ → ∑ G k ∈ M X = Y
23 22 oveq2d ⊢ φ → ∑ G k ∈ A ∖ M X + ˙ ∑ G k ∈ M X = ∑ G k ∈ A ∖ M X + ˙ Y
24 19 23 eqtrd ⊢ φ → ∑ G k ∈ A X = ∑ G k ∈ A ∖ M X + ˙ Y