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

Proof

Step	Hyp	Ref	Expression
1		gsumsnd.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		gsumsnd.g	⊢ ( 𝜑 → 𝐺 ∈ Mnd )
3		gsumsnd.m	⊢ ( 𝜑 → 𝑀 ∈ 𝑉 )
4		gsumsnd.c	⊢ ( 𝜑 → 𝐶 ∈ 𝐵 )
5		gsumsnd.s	⊢ ( ( 𝜑 ∧ 𝑘 = 𝑀 ) → 𝐴 = 𝐶 )
6		gsumsnfd.p	⊢ Ⅎ 𝑘 𝜑
7		gsumsnfd.c	⊢ Ⅎ 𝑘 𝐶
8		elsni	⊢ ( 𝑘 ∈ { 𝑀 } → 𝑘 = 𝑀 )
9	8 5	sylan2	⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑀 } ) → 𝐴 = 𝐶 )
10	6 9	mpteq2da	⊢ ( 𝜑 → ( 𝑘 ∈ { 𝑀 } ↦ 𝐴 ) = ( 𝑘 ∈ { 𝑀 } ↦ 𝐶 ) )
11	10	oveq2d	⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑘 ∈ { 𝑀 } ↦ 𝐴 ) ) = ( 𝐺 Σg ( 𝑘 ∈ { 𝑀 } ↦ 𝐶 ) ) )
12		snfi	⊢ { 𝑀 } ∈ Fin
13	12	a1i	⊢ ( 𝜑 → { 𝑀 } ∈ Fin )
14		eqid	⊢ ( .g ‘ 𝐺 ) = ( .g ‘ 𝐺 )
15	7 1 14	gsumconstf	⊢ ( ( 𝐺 ∈ Mnd ∧ { 𝑀 } ∈ Fin ∧ 𝐶 ∈ 𝐵 ) → ( 𝐺 Σg ( 𝑘 ∈ { 𝑀 } ↦ 𝐶 ) ) = ( ( ♯ ‘ { 𝑀 } ) ( .g ‘ 𝐺 ) 𝐶 ) )
16	2 13 4 15	syl3anc	⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑘 ∈ { 𝑀 } ↦ 𝐶 ) ) = ( ( ♯ ‘ { 𝑀 } ) ( .g ‘ 𝐺 ) 𝐶 ) )
17	11 16	eqtrd	⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑘 ∈ { 𝑀 } ↦ 𝐴 ) ) = ( ( ♯ ‘ { 𝑀 } ) ( .g ‘ 𝐺 ) 𝐶 ) )
18		hashsng	⊢ ( 𝑀 ∈ 𝑉 → ( ♯ ‘ { 𝑀 } ) = 1 )
19	3 18	syl	⊢ ( 𝜑 → ( ♯ ‘ { 𝑀 } ) = 1 )
20	19	oveq1d	⊢ ( 𝜑 → ( ( ♯ ‘ { 𝑀 } ) ( .g ‘ 𝐺 ) 𝐶 ) = ( 1 ( .g ‘ 𝐺 ) 𝐶 ) )
21	1 14	mulg1	⊢ ( 𝐶 ∈ 𝐵 → ( 1 ( .g ‘ 𝐺 ) 𝐶 ) = 𝐶 )
22	4 21	syl	⊢ ( 𝜑 → ( 1 ( .g ‘ 𝐺 ) 𝐶 ) = 𝐶 )
23	17 20 22	3eqtrd	⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑘 ∈ { 𝑀 } ↦ 𝐴 ) ) = 𝐶 )