Metamath Proof Explorer


Theorem gsumdifsndf

Description: Extract a summand from a finitely supported group sum. (Contributed by AV, 4-Sep-2019)

Ref Expression
Hypotheses gsumdifsndf.k _ k Y
gsumdifsndf.n k φ
gsumdifsndf.b B = Base G
gsumdifsndf.p + ˙ = + G
gsumdifsndf.g φ G CMnd
gsumdifsndf.a φ A W
gsumdifsndf.f φ finSupp 0 G k A X
gsumdifsndf.e φ k A X B
gsumdifsndf.m φ M A
gsumdifsndf.y φ Y B
gsumdifsndf.s φ k = M X = Y
Assertion gsumdifsndf φ G k A X = G k A M X + ˙ Y

Proof

Step Hyp Ref Expression
1 gsumdifsndf.k _ k Y
2 gsumdifsndf.n k φ
3 gsumdifsndf.b B = Base G
4 gsumdifsndf.p + ˙ = + G
5 gsumdifsndf.g φ G CMnd
6 gsumdifsndf.a φ A W
7 gsumdifsndf.f φ finSupp 0 G k A X
8 gsumdifsndf.e φ k A X B
9 gsumdifsndf.m φ M A
10 gsumdifsndf.y φ Y B
11 gsumdifsndf.s φ k = M X = Y
12 eqid 0 G = 0 G
13 9 snssd φ M A
14 difin2 M A M M = A M M
15 13 14 syl φ M M = A M M
16 difid M M =
17 15 16 eqtr3di φ A M M =
18 difsnid M A A M M = A
19 9 18 syl φ A M M = A
20 19 eqcomd φ A = A M M
21 2 3 12 4 5 6 8 7 17 20 gsumsplit2f φ G k A X = G k A M X + ˙ G k M X
22 cmnmnd G CMnd G Mnd
23 5 22 syl φ G Mnd
24 3 23 9 10 11 2 1 gsumsnfd φ G k M X = Y
25 24 oveq2d φ G k A M X + ˙ G k M X = G k A M X + ˙ Y
26 21 25 eqtrd φ G k A X = G k A M X + ˙ Y