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

Metamath Proof Explorer

Theorem gsumsnd

Description: Group sum of a singleton, deduction form. (Contributed by Thierry Arnoux, 30-Jan-2017) (Proof shortened by AV, 11-Dec-2019)

Ref Expression
Hypotheses gsumsnd.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
gsumsnd.g ⊢ ( 𝜑 → 𝐺 ∈ Mnd )
gsumsnd.m ⊢ ( 𝜑 → 𝑀 ∈ 𝑉 )
gsumsnd.c ⊢ ( 𝜑 → 𝐶 ∈ 𝐵 )
gsumsnd.s ⊢ ( ( 𝜑 ∧ 𝑘 = 𝑀 ) → 𝐴 = 𝐶 )
Assertion gsumsnd ( 𝜑 → ( 𝐺 Σg ( 𝑘 ∈ { 𝑀 } ↦ 𝐴 ) ) = 𝐶 )

Proof

Step Hyp Ref Expression
1 gsumsnd.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 gsumsnd.g ⊢ ( 𝜑 → 𝐺 ∈ Mnd )
3 gsumsnd.m ⊢ ( 𝜑 → 𝑀 ∈ 𝑉 )
4 gsumsnd.c ⊢ ( 𝜑 → 𝐶 ∈ 𝐵 )
5 gsumsnd.s ⊢ ( ( 𝜑 ∧ 𝑘 = 𝑀 ) → 𝐴 = 𝐶 )
6 nfv ⊢ Ⅎ 𝑘 𝜑
7 nfcv ⊢ Ⅎ 𝑘 𝐶
8 1 2 3 4 5 6 7 gsumsnfd ⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑘 ∈ { 𝑀 } ↦ 𝐴 ) ) = 𝐶 )