Metamath Proof Explorer


Theorem gsumsnf

Description: Group sum of a singleton, using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Mario Carneiro, 19-Dec-2014) (Revised by Thierry Arnoux, 28-Mar-2018) (Proof shortened by AV, 11-Dec-2019)

Ref Expression
Hypotheses gsumsnf.c _kC
gsumsnf.b B=BaseG
gsumsnf.s k=MA=C
Assertion gsumsnf GMndMVCBGkMA=C

Proof

Step Hyp Ref Expression
1 gsumsnf.c _kC
2 gsumsnf.b B=BaseG
3 gsumsnf.s k=MA=C
4 simp1 GMndMVCBGMnd
5 simp2 GMndMVCBMV
6 simp3 GMndMVCBCB
7 3 adantl GMndMVCBk=MA=C
8 nfv kGMnd
9 nfv kMV
10 1 nfel1 kCB
11 8 9 10 nf3an kGMndMVCB
12 2 4 5 6 7 11 1 gsumsnfd GMndMVCBGkMA=C