Theorem mgpsumn

Description: If the group sum for the multiplicative group of a unital ring contains a summand/factor that is the one of the ring, this summand/ factor can be removed from the group sum. (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$$
	mgpsumn.n	$$⊢\underset{\dot{}}{1}=1_R$$
	mgpsumn.1	$$⊢k=I\to A=\underset{\dot{}}{1}$$
Assertion	mgpsumn	$$⊢\phi \to \underset{k\in N}{{\sum }_M}A=\underset{k\in N\setminus \left\{I\right\}}{{\sum }_M}A$$

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