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 ( 𝑘 ∈ { 𝑀 } ↦ 𝐴 ) ) = 𝐶 )