Theorem gsumunsn

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

	Ref	Expression
Hypotheses	gsumunsn.b	$$⊢B={\mathrm{Base}}_G$$
	gsumunsn.p	$$⊢\underset{\dot{}}{+}={+}_G$$
	gsumunsn.g	$$⊢\phi \to G\in \mathrm{CMnd}$$
	gsumunsn.a	$$⊢\phi \to A\in \mathrm{Fin}$$
	gsumunsn.f	$$⊢\left(\phi \wedge k\in A\right)\to X\in B$$
	gsumunsn.m	$$⊢\phi \to M\in V$$
	gsumunsn.d	$$⊢\phi \to \neg M\in A$$
	gsumunsn.y	$$⊢\phi \to Y\in B$$
	gsumunsn.s	$$⊢k=M\to X=Y$$
Assertion	gsumunsn	$$⊢\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		gsumunsn.b	$$⊢B={\mathrm{Base}}_G$$
2		gsumunsn.p	$$⊢\underset{\dot{}}{+}={+}_G$$
3		gsumunsn.g	$$⊢\phi \to G\in \mathrm{CMnd}$$
4		gsumunsn.a	$$⊢\phi \to A\in \mathrm{Fin}$$
5		gsumunsn.f	$$⊢\left(\phi \wedge k\in A\right)\to X\in B$$
6		gsumunsn.m	$$⊢\phi \to M\in V$$
7		gsumunsn.d	$$⊢\phi \to \neg M\in A$$
8		gsumunsn.y	$$⊢\phi \to Y\in B$$
9		gsumunsn.s	$$⊢k=M\to X=Y$$
10	9	adantl	$$⊢\left(\phi \wedge k=M\right)\to X=Y$$
11	1 2 3 4 5 6 7 8 10	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$$