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