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

Metamath Proof Explorer

Theorem gsumsn

Description: Group sum of a singleton. (Contributed by Mario Carneiro, 19-Dec-2014) (Revised by Mario Carneiro, 24-Apr-2016) (Proof shortened by AV, 11-Dec-2019)

Ref Expression
Hypotheses gsumsn.b ⊢ B = Base G
gsumsn.s ⊢ k = M → A = C
Assertion gsumsn ⊢ G ∈ Mnd ∧ M ∈ V ∧ C ∈ B → ∑ G k ∈ M A = C

Proof

Step Hyp Ref Expression
1 gsumsn.b ⊢ B = Base G
2 gsumsn.s ⊢ k = M → A = C
3 nfcv ⊢ Ⅎ _ k C
4 3 1 2 gsumsnf ⊢ G ∈ Mnd ∧ M ∈ V ∧ C ∈ B → ∑ G k ∈ M A = C