Theorem gsumunsnd

Description: Append an element to a finite group sum. (Contributed by Mario Carneiro, 19-Dec-2014) (Revised by AV, 2-Jan-2019) (Proof shortened by AV, 11-Dec-2019)

	Ref	Expression
Hypotheses	gsumunsnd.b	$$⊢B={\mathrm{Base}}_G$$
	gsumunsnd.p	$$⊢\underset{\dot{}}{+}={+}_G$$
	gsumunsnd.g	$$⊢\phi \to G\in \mathrm{CMnd}$$
	gsumunsnd.a	$$⊢\phi \to A\in \mathrm{Fin}$$
	gsumunsnd.f	$$⊢\left(\phi \wedge k\in A\right)\to X\in B$$
	gsumunsnd.m	$$⊢\phi \to M\in V$$
	gsumunsnd.d	$$⊢\phi \to \neg M\in A$$
	gsumunsnd.y	$$⊢\phi \to Y\in B$$
	gsumunsnd.s	$$⊢\left(\phi \wedge k=M\right)\to X=Y$$
Assertion	gsumunsnd	$$⊢\phi \to \underset{k\in A\cup \left\{M\right\}}{{\sum }_G}X=\left(\underset{k\in A}{{\sum }_G},X\right)\underset{\dot{}}{+}Y$$

Proof

Step	Hyp	Ref	Expression
1		gsumunsnd.b	$$⊢B={\mathrm{Base}}_G$$
2		gsumunsnd.p	$$⊢\underset{\dot{}}{+}={+}_G$$
3		gsumunsnd.g	$$⊢\phi \to G\in \mathrm{CMnd}$$
4		gsumunsnd.a	$$⊢\phi \to A\in \mathrm{Fin}$$
5		gsumunsnd.f	$$⊢\left(\phi \wedge k\in A\right)\to X\in B$$
6		gsumunsnd.m	$$⊢\phi \to M\in V$$
7		gsumunsnd.d	$$⊢\phi \to \neg M\in A$$
8		gsumunsnd.y	$$⊢\phi \to Y\in B$$
9		gsumunsnd.s	$$⊢\left(\phi \wedge k=M\right)\to X=Y$$
10		nfcv	$$⊢\underset{\_}{Ⅎ}kY$$
11	1 2 3 4 5 6 7 8 9 10	gsumunsnfd	$$⊢\phi \to \underset{k\in A\cup \left\{M\right\}}{{\sum }_G}X=\left(\underset{k\in A}{{\sum }_G},X\right)\underset{\dot{}}{+}Y$$