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

Metamath Proof Explorer

Theorem gsumsnfd

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

Ref Expression
Hypotheses gsumsnd.b ⊢ B = Base G
gsumsnd.g ⊢ φ → G ∈ Mnd
gsumsnd.m ⊢ φ → M ∈ V
gsumsnd.c ⊢ φ → C ∈ B
gsumsnd.s ⊢ φ ∧ k = M → A = C
gsumsnfd.p ⊢ Ⅎ k φ
gsumsnfd.c ⊢ Ⅎ _ k C
Assertion gsumsnfd ⊢ φ → ∑ G k ∈ M A = C

Proof

Step Hyp Ref Expression
1 gsumsnd.b ⊢ B = Base G
2 gsumsnd.g ⊢ φ → G ∈ Mnd
3 gsumsnd.m ⊢ φ → M ∈ V
4 gsumsnd.c ⊢ φ → C ∈ B
5 gsumsnd.s ⊢ φ ∧ k = M → A = C
6 gsumsnfd.p ⊢ Ⅎ k φ
7 gsumsnfd.c ⊢ Ⅎ _ k C
8 elsni ⊢ k ∈ M → k = M
9 8 5 sylan2 ⊢ φ ∧ k ∈ M → A = C
10 6 9 mpteq2da ⊢ φ → k ∈ M ⟼ A = k ∈ M ⟼ C
11 10 oveq2d ⊢ φ → ∑ G k ∈ M A = ∑ G k ∈ M C
12 snfi ⊢ M ∈ Fin
13 12 a1i ⊢ φ → M ∈ Fin
14 eqid ⊢ ⋅ G = ⋅ G
15 7 1 14 gsumconstf ⊢ G ∈ Mnd ∧ M ∈ Fin ∧ C ∈ B → ∑ G k ∈ M C = M ⋅ G C
16 2 13 4 15 syl3anc ⊢ φ → ∑ G k ∈ M C = M ⋅ G C
17 11 16 eqtrd ⊢ φ → ∑ G k ∈ M A = M ⋅ G C
18 hashsng ⊢ M ∈ V → M = 1
19 3 18 syl ⊢ φ → M = 1
20 19 oveq1d ⊢ φ → M ⋅ G C = 1 ⋅ G C
21 1 14 mulg1 ⊢ C ∈ B → 1 ⋅ G C = C
22 4 21 syl ⊢ φ → 1 ⋅ G C = C
23 17 20 22 3eqtrd ⊢ φ → ∑ G k ∈ M A = C