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 ⊢ Ⅎ _ k C
gsumsnf.b ⊢ B = Base G
gsumsnf.s ⊢ k = M → A = C
Assertion gsumsnf ⊢ G ∈ Mnd ∧ M ∈ V ∧ C ∈ B → ∑ G k ∈ M A = C

Proof

Step Hyp Ref Expression
1 gsumsnf.c ⊢ Ⅎ _ k C
2 gsumsnf.b ⊢ B = Base G
3 gsumsnf.s ⊢ k = M → A = C
4 simp1 ⊢ G ∈ Mnd ∧ M ∈ V ∧ C ∈ B → G ∈ Mnd
5 simp2 ⊢ G ∈ Mnd ∧ M ∈ V ∧ C ∈ B → M ∈ V
6 simp3 ⊢ G ∈ Mnd ∧ M ∈ V ∧ C ∈ B → C ∈ B
7 3 adantl ⊢ G ∈ Mnd ∧ M ∈ V ∧ C ∈ B ∧ k = M → A = C
8 nfv ⊢ Ⅎ k G ∈ Mnd
9 nfv ⊢ Ⅎ k M ∈ V
10 1 nfel1 ⊢ Ⅎ k C ∈ B
11 8 9 10 nf3an ⊢ Ⅎ k G ∈ Mnd ∧ M ∈ V ∧ C ∈ B
12 2 4 5 6 7 11 1 gsumsnfd ⊢ G ∈ Mnd ∧ M ∈ V ∧ C ∈ B → ∑ G k ∈ M A = C