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	⊢ Ⅎ 𝑘 𝐶
	gsumsnf.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
	gsumsnf.s	⊢ ( 𝑘 = 𝑀 → 𝐴 = 𝐶 )
Assertion	gsumsnf	⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑀 ∈ 𝑉 ∧ 𝐶 ∈ 𝐵 ) → ( 𝐺 Σg ( 𝑘 ∈ { 𝑀 } ↦ 𝐴 ) ) = 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		gsumsnf.c	⊢ Ⅎ 𝑘 𝐶
2		gsumsnf.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
3		gsumsnf.s	⊢ ( 𝑘 = 𝑀 → 𝐴 = 𝐶 )
4		simp1	⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑀 ∈ 𝑉 ∧ 𝐶 ∈ 𝐵 ) → 𝐺 ∈ Mnd )
5		simp2	⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑀 ∈ 𝑉 ∧ 𝐶 ∈ 𝐵 ) → 𝑀 ∈ 𝑉 )
6		simp3	⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑀 ∈ 𝑉 ∧ 𝐶 ∈ 𝐵 ) → 𝐶 ∈ 𝐵 )
7	3	adantl	⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝑀 ∈ 𝑉 ∧ 𝐶 ∈ 𝐵 ) ∧ 𝑘 = 𝑀 ) → 𝐴 = 𝐶 )
8		nfv	⊢ Ⅎ 𝑘 𝐺 ∈ Mnd
9		nfv	⊢ Ⅎ 𝑘 𝑀 ∈ 𝑉
10	1	nfel1	⊢ Ⅎ 𝑘 𝐶 ∈ 𝐵
11	8 9 10	nf3an	⊢ Ⅎ 𝑘 ( 𝐺 ∈ Mnd ∧ 𝑀 ∈ 𝑉 ∧ 𝐶 ∈ 𝐵 )
12	2 4 5 6 7 11 1	gsumsnfd	⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑀 ∈ 𝑉 ∧ 𝐶 ∈ 𝐵 ) → ( 𝐺 Σg ( 𝑘 ∈ { 𝑀 } ↦ 𝐴 ) ) = 𝐶 )