Theorem gsummptif1n0

Description: If only one summand in a finite group sum is not zero, the whole sum equals this summand. (Contributed by AV, 17-Feb-2019) (Proof shortened by AV, 11-Oct-2019)

	Ref	Expression
Hypotheses	gsummpt1n0.0	⊢ 0 = ( 0g ‘ 𝐺 )
	gsummpt1n0.g	⊢ ( 𝜑 → 𝐺 ∈ Mnd )
	gsummpt1n0.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
	gsummpt1n0.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐼 )
	gsummpt1n0.f	⊢ 𝐹 = ( 𝑛 ∈ 𝐼 ↦ if ( 𝑛 = 𝑋 , 𝐴 , 0 ) )
	gsummptif1n0.a	⊢ ( 𝜑 → 𝐴 ∈ ( Base ‘ 𝐺 ) )
Assertion	gsummptif1n0	⊢ ( 𝜑 → ( 𝐺 Σg 𝐹 ) = 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		gsummpt1n0.0	⊢ 0 = ( 0g ‘ 𝐺 )
2		gsummpt1n0.g	⊢ ( 𝜑 → 𝐺 ∈ Mnd )
3		gsummpt1n0.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
4		gsummpt1n0.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐼 )
5		gsummpt1n0.f	⊢ 𝐹 = ( 𝑛 ∈ 𝐼 ↦ if ( 𝑛 = 𝑋 , 𝐴 , 0 ) )
6		gsummptif1n0.a	⊢ ( 𝜑 → 𝐴 ∈ ( Base ‘ 𝐺 ) )
7	6	ralrimivw	⊢ ( 𝜑 → ∀ 𝑛 ∈ 𝐼 𝐴 ∈ ( Base ‘ 𝐺 ) )
8	1 2 3 4 5 7	gsummpt1n0	⊢ ( 𝜑 → ( 𝐺 Σg 𝐹 ) = ⦋ 𝑋 / 𝑛 ⦌ 𝐴 )
9		csbconstg	⊢ ( 𝑋 ∈ 𝐼 → ⦋ 𝑋 / 𝑛 ⦌ 𝐴 = 𝐴 )
10	4 9	syl	⊢ ( 𝜑 → ⦋ 𝑋 / 𝑛 ⦌ 𝐴 = 𝐴 )
11	8 10	eqtrd	⊢ ( 𝜑 → ( 𝐺 Σg 𝐹 ) = 𝐴 )