Theorem gsumunsnf

Description: Append an element to a finite group sum, using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Mario Carneiro, 19-Dec-2014) (Revised by Thierry Arnoux, 28-Mar-2018) (Proof shortened by AV, 11-Dec-2019)

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