Theorem mgpsumunsn

Description: Extract a summand/factor from the group sum for the multiplicative group of a unital ring. (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$$
	mgpsumunsn.x	$$⊢\phi \to X\in {\mathrm{Base}}_R$$
	mgpsumunsn.e	$$⊢k=I\to A=X$$
Assertion	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{}}{·}X$$

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		mgpsumunsn.x	$$⊢\phi \to X\in {\mathrm{Base}}_R$$
8		mgpsumunsn.e	$$⊢k=I\to A=X$$
9		difsnid	$$⊢I\in N\to \left(N\setminus \left\{I\right\}\right)\cup \left\{I\right\}=N$$
10	5 9	syl	$$⊢\phi \to \left(N\setminus \left\{I\right\}\right)\cup \left\{I\right\}=N$$
11	10	eqcomd	$$⊢\phi \to N=\left(N\setminus \left\{I\right\}\right)\cup \left\{I\right\}$$
12	11	mpteq1d	$$⊢\phi \to \left(k\in N⟼A\right)=\left(k\in \left(\left(N\setminus \left\{I\right\}\right)\cup \left\{I\right\}\right)⟼A\right)$$
13	12	oveq2d	$$⊢\phi \to \underset{k\in N}{{\sum }_M}A=\underset{k\in \left(N\setminus \left\{I\right\}\right)\cup \left\{I\right\}}{{\sum }_M}A$$
14		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
15	1 14	mgpbas	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_M$$
16	1 2	mgpplusg	$$⊢\underset{\dot{}}{·}={+}_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		neldifsnd	$$⊢\phi \to \neg I\in \left(N\setminus \left\{I\right\}\right)$$
24	15 16 18 20 22 5 23 7 8	gsumunsn	$$⊢\phi \to \underset{k\in \left(N\setminus \left\{I\right\}\right)\cup \left\{I\right\}}{{\sum }_M}A=\left(\underset{k\in N\setminus \left\{I\right\}}{{\sum }_M},A\right)\underset{\dot{}}{·}X$$
25	13 24	eqtrd	$$⊢\phi \to \underset{k\in N}{{\sum }_M}A=\left(\underset{k\in N\setminus \left\{I\right\}}{{\sum }_M},A\right)\underset{\dot{}}{·}X$$