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	9 10	syl	$$⊢R\in \mathrm{CRing}\to R\in \mathrm{Mnd}$$
12	3 11	syl	$$⊢\phi \to R\in \mathrm{Mnd}$$
13		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
14	13 7	mndidcl	$$⊢R\in \mathrm{Mnd}\to \underset{\dot{}}{0}\in {\mathrm{Base}}_R$$
15	12 14	syl	$$⊢\phi \to \underset{\dot{}}{0}\in {\mathrm{Base}}_R$$
16	1 2 3 4 5 6 15 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}$$
17	3 9	syl	$$⊢\phi \to R\in \mathrm{Ring}$$
18	1 13	mgpbas	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_M$$
19	1	crngmgp	$$⊢R\in \mathrm{CRing}\to M\in \mathrm{CMnd}$$
20	3 19	syl	$$⊢\phi \to M\in \mathrm{CMnd}$$
21		diffi	$$⊢N\in \mathrm{Fin}\to N\setminus \left\{I\right\}\in \mathrm{Fin}$$
22	4 21	syl	$$⊢\phi \to N\setminus \left\{I\right\}\in \mathrm{Fin}$$
23		eldifi	$$⊢k\in \left(N\setminus \left\{I\right\}\right)\to k\in N$$
24	23 6	sylan2	$$⊢\left(\phi \wedge k\in \left(N\setminus \left\{I\right\}\right)\right)\to A\in {\mathrm{Base}}_R$$
25	24	ralrimiva	$$⊢\phi \to \forall k\in \left(N\setminus \left\{I\right\}\right)A\in {\mathrm{Base}}_R$$
26	18 20 22 25	gsummptcl	$$⊢\phi \to \underset{k\in N\setminus \left\{I\right\}}{{\sum }_M}A\in {\mathrm{Base}}_R$$
27	13 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}$$
28	17 26 27	syl2anc	$$⊢\phi \to \left(\underset{k\in N\setminus \left\{I\right\}}{{\sum }_M},A\right)\underset{\dot{}}{·}\underset{\dot{}}{0}=\underset{\dot{}}{0}$$
29	16 28	eqtrd	$$⊢\phi \to \underset{k\in N}{{\sum }_M}A=\underset{\dot{}}{0}$$