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	$$⊢\underset{\dot{}}{0}=0_G$$
	gsummpt1n0.g	$$⊢\phi \to G\in \mathrm{Mnd}$$
	gsummpt1n0.i	$$⊢\phi \to I\in W$$
	gsummpt1n0.x	$$⊢\phi \to X\in I$$
	gsummpt1n0.f	$$⊢F=\left(n\in I⟼if\left(n=X,A,\underset{\dot{}}{0}\right)\right)$$
	gsummptif1n0.a	$$⊢\phi \to A\in {\mathrm{Base}}_G$$
Assertion	gsummptif1n0	$$⊢\phi \to {\sum }_{G}F=A$$

Proof

Step	Hyp	Ref	Expression
1		gsummpt1n0.0	$$⊢\underset{\dot{}}{0}=0_G$$
2		gsummpt1n0.g	$$⊢\phi \to G\in \mathrm{Mnd}$$
3		gsummpt1n0.i	$$⊢\phi \to I\in W$$
4		gsummpt1n0.x	$$⊢\phi \to X\in I$$
5		gsummpt1n0.f	$$⊢F=\left(n\in I⟼if\left(n=X,A,\underset{\dot{}}{0}\right)\right)$$
6		gsummptif1n0.a	$$⊢\phi \to A\in {\mathrm{Base}}_G$$
7	6	ralrimivw	$$⊢\phi \to \forall n\in IA\in {\mathrm{Base}}_G$$
8	1 2 3 4 5 7	gsummpt1n0	$$⊢\phi \to {\sum }_{G}F=⦋X/n⦌A$$
9		csbconstg	$$⊢X\in I\to ⦋X/n⦌A=A$$
10	4 9	syl	$$⊢\phi \to ⦋X/n⦌A=A$$
11	8 10	eqtrd	$$⊢\phi \to {\sum }_{G}F=A$$