Theorem gsummpt1n0

Description: If only one summand in a finite group sum is not zero, the whole sum equals this summand. More general version of gsummptif1n0 . (Contributed 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)$$
	gsummpt1n0.a	$$⊢\phi \to \forall n\in IA\in {\mathrm{Base}}_G$$
Assertion	gsummpt1n0	$$⊢\phi \to {\sum }_{G}F=⦋X/n⦌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		gsummpt1n0.a	$$⊢\phi \to \forall n\in IA\in {\mathrm{Base}}_G$$
7		eqid	$$⊢{\mathrm{Base}}_G={\mathrm{Base}}_G$$
8	6	r19.21bi	$$⊢\left(\phi \wedge n\in I\right)\to A\in {\mathrm{Base}}_G$$
9	7 1	mndidcl	$$⊢G\in \mathrm{Mnd}\to \underset{\dot{}}{0}\in {\mathrm{Base}}_G$$
10	2 9	syl	$$⊢\phi \to \underset{\dot{}}{0}\in {\mathrm{Base}}_G$$
11	10	adantr	$$⊢\left(\phi \wedge n\in I\right)\to \underset{\dot{}}{0}\in {\mathrm{Base}}_G$$
12	8 11	ifcld	$$⊢\left(\phi \wedge n\in I\right)\to if\left(n=X,A,\underset{\dot{}}{0}\right)\in {\mathrm{Base}}_G$$
13	12 5	fmptd	$$⊢\phi \to F:I⟶{\mathrm{Base}}_G$$
14	5	oveq1i	$$⊢F\mathrm{supp}\underset{\dot{}}{0}=\left(n\in I⟼if\left(n=X,A,\underset{\dot{}}{0}\right)\right)\mathrm{supp}\underset{\dot{}}{0}$$
15		eldifsni	$$⊢n\in \left(I\setminus \left\{X\right\}\right)\to n\ne X$$
16	15	adantl	$$⊢\left(\phi \wedge n\in \left(I\setminus \left\{X\right\}\right)\right)\to n\ne X$$
17		ifnefalse	$$⊢n\ne X\to if\left(n=X,A,\underset{\dot{}}{0}\right)=\underset{\dot{}}{0}$$
18	16 17	syl	$$⊢\left(\phi \wedge n\in \left(I\setminus \left\{X\right\}\right)\right)\to if\left(n=X,A,\underset{\dot{}}{0}\right)=\underset{\dot{}}{0}$$
19	18 3	suppss2	$$⊢\phi \to \left(n\in I⟼if\left(n=X,A,\underset{\dot{}}{0}\right)\right)\mathrm{supp}\underset{\dot{}}{0}\subseteq \left\{X\right\}$$
20	14 19	eqsstrid	$$⊢\phi \to F\mathrm{supp}\underset{\dot{}}{0}\subseteq \left\{X\right\}$$
21	7 1 2 3 4 13 20	gsumpt	$$⊢\phi \to {\sum }_{G}F=F\left(X\right)$$
22		nfcv	$$⊢\underset{\_}{Ⅎ}yif\left(n=X,A,\underset{\dot{}}{0}\right)$$
23		nfv	$$⊢Ⅎny=X$$
24		nfcsb1v	$$⊢\underset{\_}{Ⅎ}n⦋y/n⦌A$$
25		nfcv	$$⊢\underset{\_}{Ⅎ}n\underset{\dot{}}{0}$$
26	23 24 25	nfif	$$⊢\underset{\_}{Ⅎ}nif\left(y=X,⦋y/n⦌A,\underset{\dot{}}{0}\right)$$
27		eqeq1	$$⊢n=y\to \left(n=X\leftrightarrow y=X\right)$$
28		csbeq1a	$$⊢n=y\to A=⦋y/n⦌A$$
29	27 28	ifbieq1d	$$⊢n=y\to if\left(n=X,A,\underset{\dot{}}{0}\right)=if\left(y=X,⦋y/n⦌A,\underset{\dot{}}{0}\right)$$
30	22 26 29	cbvmpt	$$⊢\left(n\in I⟼if\left(n=X,A,\underset{\dot{}}{0}\right)\right)=\left(y\in I⟼if\left(y=X,⦋y/n⦌A,\underset{\dot{}}{0}\right)\right)$$
31	5 30	eqtri	$$⊢F=\left(y\in I⟼if\left(y=X,⦋y/n⦌A,\underset{\dot{}}{0}\right)\right)$$
32		iftrue	$$⊢y=X\to if\left(y=X,⦋y/n⦌A,\underset{\dot{}}{0}\right)=⦋y/n⦌A$$
33		csbeq1	$$⊢y=X\to ⦋y/n⦌A=⦋X/n⦌A$$
34	32 33	eqtrd	$$⊢y=X\to if\left(y=X,⦋y/n⦌A,\underset{\dot{}}{0}\right)=⦋X/n⦌A$$
35		rspcsbela	$$⊢\left(X\in I\wedge \forall n\in IA\in {\mathrm{Base}}_G\right)\to ⦋X/n⦌A\in {\mathrm{Base}}_G$$
36	4 6 35	syl2anc	$$⊢\phi \to ⦋X/n⦌A\in {\mathrm{Base}}_G$$
37	31 34 4 36	fvmptd3	$$⊢\phi \to F\left(X\right)=⦋X/n⦌A$$
38	21 37	eqtrd	$$⊢\phi \to {\sum }_{G}F=⦋X/n⦌A$$