Theorem mgpsumz

Description: If the group sum for the multiplicative group of a unital ring contains a summand/factor that is the zero of the ring, the group sum itself is zero. (Contributed by AV, 29-Dec-2018)

	Ref	Expression
Hypotheses	mgpsumunsn.m	$$⊢M={\mathrm{mulGrp}}_R$$
	mgpsumunsn.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
	mgpsumunsn.r	$$⊢\phi \to R\in \mathrm{CRing}$$
	mgpsumunsn.n	$$⊢\phi \to N\in \mathrm{Fin}$$
	mgpsumunsn.i	$$⊢\phi \to I\in N$$
	mgpsumunsn.a	$$⊢\left(\phi \wedge k\in N\right)\to A\in {\mathrm{Base}}_R$$
	mgpsumz.z	$$⊢\underset{\dot{}}{0}=0_R$$
	mgpsumz.0	$$⊢k=I\to A=\underset{\dot{}}{0}$$
Assertion	mgpsumz	$$⊢\phi \to \underset{k\in N}{{\sum }_M}A=\underset{\dot{}}{0}$$

Proof

Step	Hyp	Ref	Expression
1		mgpsumunsn.m	$$⊢M={\mathrm{mulGrp}}_R$$
2		mgpsumunsn.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
3		mgpsumunsn.r	$$⊢\phi \to R\in \mathrm{CRing}$$
4		mgpsumunsn.n	$$⊢\phi \to N\in \mathrm{Fin}$$
5		mgpsumunsn.i	$$⊢\phi \to I\in N$$
6		mgpsumunsn.a	$$⊢\left(\phi \wedge k\in N\right)\to A\in {\mathrm{Base}}_R$$
7		mgpsumz.z	$$⊢\underset{\dot{}}{0}=0_R$$
8		mgpsumz.0	$$⊢k=I\to A=\underset{\dot{}}{0}$$
9		crngring	$$⊢R\in \mathrm{CRing}\to R\in \mathrm{Ring}$$
10		ringmnd	$$⊢R\in \mathrm{Ring}\to R\in \mathrm{Mnd}$$
11		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
12	11 7	mndidcl	$$⊢R\in \mathrm{Mnd}\to \underset{\dot{}}{0}\in {\mathrm{Base}}_R$$
13	3 9 10 12	4syl	$$⊢\phi \to \underset{\dot{}}{0}\in {\mathrm{Base}}_R$$
14	1 2 3 4 5 6 13 8	mgpsumunsn	$$⊢\phi \to \underset{k\in N}{{\sum }_M}A=\left(\underset{k\in N\setminus \left\{I\right\}}{{\sum }_M},A\right)\underset{\dot{}}{·}\underset{\dot{}}{0}$$
15	3 9	syl	$$⊢\phi \to R\in \mathrm{Ring}$$
16	1 11	mgpbas	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_M$$
17	1	crngmgp	$$⊢R\in \mathrm{CRing}\to M\in \mathrm{CMnd}$$
18	3 17	syl	$$⊢\phi \to M\in \mathrm{CMnd}$$
19		diffi	$$⊢N\in \mathrm{Fin}\to N\setminus \left\{I\right\}\in \mathrm{Fin}$$
20	4 19	syl	$$⊢\phi \to N\setminus \left\{I\right\}\in \mathrm{Fin}$$
21		eldifi	$$⊢k\in \left(N\setminus \left\{I\right\}\right)\to k\in N$$
22	21 6	sylan2	$$⊢\left(\phi \wedge k\in \left(N\setminus \left\{I\right\}\right)\right)\to A\in {\mathrm{Base}}_R$$
23	22	ralrimiva	$$⊢\phi \to \forall k\in \left(N\setminus \left\{I\right\}\right)A\in {\mathrm{Base}}_R$$
24	16 18 20 23	gsummptcl	$$⊢\phi \to \underset{k\in N\setminus \left\{I\right\}}{{\sum }_M}A\in {\mathrm{Base}}_R$$
25	11 2 7	ringrz	$$⊢\left(R\in \mathrm{Ring}\wedge \underset{k\in N\setminus \left\{I\right\}}{{\sum }_M}A\in {\mathrm{Base}}_R\right)\to \left(\underset{k\in N\setminus \left\{I\right\}}{{\sum }_M},A\right)\underset{\dot{}}{·}\underset{\dot{}}{0}=\underset{\dot{}}{0}$$
26	15 24 25	syl2anc	$$⊢\phi \to \left(\underset{k\in N\setminus \left\{I\right\}}{{\sum }_M},A\right)\underset{\dot{}}{·}\underset{\dot{}}{0}=\underset{\dot{}}{0}$$
27	14 26	eqtrd	$$⊢\phi \to \underset{k\in N}{{\sum }_M}A=\underset{\dot{}}{0}$$