Theorem gsumunsnfd

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 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$$
	gsumunsnfd.0	$$⊢\underset{\_}{Ⅎ}kY$$
Assertion	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$$

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		gsumunsnfd.0	$$⊢\underset{\_}{Ⅎ}kY$$
11		snfi	$$⊢\left\{M\right\}\in \mathrm{Fin}$$
12		unfi	$$⊢\left(A\in \mathrm{Fin}\wedge \left\{M\right\}\in \mathrm{Fin}\right)\to A\cup \left\{M\right\}\in \mathrm{Fin}$$
13	4 11 12	sylancl	$$⊢\phi \to A\cup \left\{M\right\}\in \mathrm{Fin}$$
14		elun	$$⊢k\in \left(A\cup \left\{M\right\}\right)\leftrightarrow \left(k\in A\vee k\in \left\{M\right\}\right)$$
15		elsni	$$⊢k\in \left\{M\right\}\to k=M$$
16	15 9	sylan2	$$⊢\left(\phi \wedge k\in \left\{M\right\}\right)\to X=Y$$
17	8	adantr	$$⊢\left(\phi \wedge k\in \left\{M\right\}\right)\to Y\in B$$
18	16 17	eqeltrd	$$⊢\left(\phi \wedge k\in \left\{M\right\}\right)\to X\in B$$
19	5 18	jaodan	$$⊢\left(\phi \wedge \left(k\in A\vee k\in \left\{M\right\}\right)\right)\to X\in B$$
20	14 19	sylan2b	$$⊢\left(\phi \wedge k\in \left(A\cup \left\{M\right\}\right)\right)\to X\in B$$
21		disjsn	$$⊢A\cap \left\{M\right\}=\varnothing \leftrightarrow \neg M\in A$$
22	7 21	sylibr	$$⊢\phi \to A\cap \left\{M\right\}=\varnothing$$
23		eqidd	$$⊢\phi \to A\cup \left\{M\right\}=A\cup \left\{M\right\}$$
24	1 2 3 13 20 22 23	gsummptfidmsplit	$$⊢\phi \to \underset{k\in A\cup \left\{M\right\}}{{\sum }_G}X=\left(\underset{k\in A}{{\sum }_G},X\right)\underset{\dot{}}{+}\left(\underset{k\in \left\{M\right\}}{{\sum }_G},X\right)$$
25		cmnmnd	$$⊢G\in \mathrm{CMnd}\to G\in \mathrm{Mnd}$$
26	3 25	syl	$$⊢\phi \to G\in \mathrm{Mnd}$$
27		nfv	$$⊢Ⅎk\phi$$
28	1 26 6 8 9 27 10	gsumsnfd	$$⊢\phi \to \underset{k\in \left\{M\right\}}{{\sum }_G}X=Y$$
29	28	oveq2d	$$⊢\phi \to \left(\underset{k\in A}{{\sum }_G},X\right)\underset{\dot{}}{+}\left(\underset{k\in \left\{M\right\}}{{\sum }_G},X\right)=\left(\underset{k\in A}{{\sum }_G},X\right)\underset{\dot{}}{+}Y$$
30	24 29	eqtrd	$$⊢\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$$