Theorem gsumzunsnd

Description: Append an element to a finite group sum, more general version of gsumunsnd . (Contributed by AV, 7-Oct-2019)

	Ref	Expression
Hypotheses	gsumzunsnd.b	$$⊢B={\mathrm{Base}}_G$$
	gsumzunsnd.p	$$⊢\underset{\dot{}}{+}={+}_G$$
	gsumzunsnd.z	$$⊢Z=\mathrm{Cntz}\left(G\right)$$
	gsumzunsnd.f	$$⊢F=\left(k\in \left(A\cup \left\{M\right\}\right)⟼X\right)$$
	gsumzunsnd.g	$$⊢\phi \to G\in \mathrm{Mnd}$$
	gsumzunsnd.a	$$⊢\phi \to A\in \mathrm{Fin}$$
	gsumzunsnd.c	$$⊢\phi \to \mathrm{ran}F\subseteq Z\left(\mathrm{ran}F\right)$$
	gsumzunsnd.x	$$⊢\left(\phi \wedge k\in A\right)\to X\in B$$
	gsumzunsnd.m	$$⊢\phi \to M\in V$$
	gsumzunsnd.d	$$⊢\phi \to \neg M\in A$$
	gsumzunsnd.y	$$⊢\phi \to Y\in B$$
	gsumzunsnd.s	$$⊢\left(\phi \wedge k=M\right)\to X=Y$$
Assertion	gsumzunsnd	$$⊢\phi \to {\sum }_{G}F=\left(\underset{k\in A}{{\sum }_G},X\right)\underset{\dot{}}{+}Y$$

Proof

Step	Hyp	Ref	Expression
1		gsumzunsnd.b	$$⊢B={\mathrm{Base}}_G$$
2		gsumzunsnd.p	$$⊢\underset{\dot{}}{+}={+}_G$$
3		gsumzunsnd.z	$$⊢Z=\mathrm{Cntz}\left(G\right)$$
4		gsumzunsnd.f	$$⊢F=\left(k\in \left(A\cup \left\{M\right\}\right)⟼X\right)$$
5		gsumzunsnd.g	$$⊢\phi \to G\in \mathrm{Mnd}$$
6		gsumzunsnd.a	$$⊢\phi \to A\in \mathrm{Fin}$$
7		gsumzunsnd.c	$$⊢\phi \to \mathrm{ran}F\subseteq Z\left(\mathrm{ran}F\right)$$
8		gsumzunsnd.x	$$⊢\left(\phi \wedge k\in A\right)\to X\in B$$
9		gsumzunsnd.m	$$⊢\phi \to M\in V$$
10		gsumzunsnd.d	$$⊢\phi \to \neg M\in A$$
11		gsumzunsnd.y	$$⊢\phi \to Y\in B$$
12		gsumzunsnd.s	$$⊢\left(\phi \wedge k=M\right)\to X=Y$$
13		eqid	$$⊢0_G=0_G$$
14		snfi	$$⊢\left\{M\right\}\in \mathrm{Fin}$$
15		unfi	$$⊢\left(A\in \mathrm{Fin}\wedge \left\{M\right\}\in \mathrm{Fin}\right)\to A\cup \left\{M\right\}\in \mathrm{Fin}$$
16	6 14 15	sylancl	$$⊢\phi \to A\cup \left\{M\right\}\in \mathrm{Fin}$$
17		elun	$$⊢k\in \left(A\cup \left\{M\right\}\right)\leftrightarrow \left(k\in A\vee k\in \left\{M\right\}\right)$$
18		elsni	$$⊢k\in \left\{M\right\}\to k=M$$
19	18 12	sylan2	$$⊢\left(\phi \wedge k\in \left\{M\right\}\right)\to X=Y$$
20	11	adantr	$$⊢\left(\phi \wedge k\in \left\{M\right\}\right)\to Y\in B$$
21	19 20	eqeltrd	$$⊢\left(\phi \wedge k\in \left\{M\right\}\right)\to X\in B$$
22	8 21	jaodan	$$⊢\left(\phi \wedge \left(k\in A\vee k\in \left\{M\right\}\right)\right)\to X\in B$$
23	17 22	sylan2b	$$⊢\left(\phi \wedge k\in \left(A\cup \left\{M\right\}\right)\right)\to X\in B$$
24	23 4	fmptd	$$⊢\phi \to F:A\cup \left\{M\right\}⟶B$$
25	8	expcom	$$⊢k\in A\to \left(\phi \to X\in B\right)$$
26	11	adantr	$$⊢\left(\phi \wedge k=M\right)\to Y\in B$$
27	12 26	eqeltrd	$$⊢\left(\phi \wedge k=M\right)\to X\in B$$
28	27	expcom	$$⊢k=M\to \left(\phi \to X\in B\right)$$
29	18 28	syl	$$⊢k\in \left\{M\right\}\to \left(\phi \to X\in B\right)$$
30	25 29	jaoi	$$⊢\left(k\in A\vee k\in \left\{M\right\}\right)\to \left(\phi \to X\in B\right)$$
31	17 30	sylbi	$$⊢k\in \left(A\cup \left\{M\right\}\right)\to \left(\phi \to X\in B\right)$$
32	31	impcom	$$⊢\left(\phi \wedge k\in \left(A\cup \left\{M\right\}\right)\right)\to X\in B$$
33		fvexd	$$⊢\phi \to 0_G\in \mathrm{V}$$
34	4 16 32 33	fsuppmptdm	$$⊢\phi \to {finSupp}_{0_G}\left(F\right)$$
35		disjsn	$$⊢A\cap \left\{M\right\}=\varnothing \leftrightarrow \neg M\in A$$
36	10 35	sylibr	$$⊢\phi \to A\cap \left\{M\right\}=\varnothing$$
37		eqidd	$$⊢\phi \to A\cup \left\{M\right\}=A\cup \left\{M\right\}$$
38	1 13 2 3 5 16 24 7 34 36 37	gsumzsplit	$$⊢\phi \to {\sum }_{G}F=\left({\sum }_G,\left({F\upharpoonright }_A\right)\right)\underset{\dot{}}{+}\left({\sum }_G,\left({F\upharpoonright }_{\left\{M\right\}}\right)\right)$$
39	4	reseq1i	$$⊢{F\upharpoonright }_A={\left(k\in \left(A\cup \left\{M\right\}\right)⟼X\right)\upharpoonright }_A$$
40		ssun1	$$⊢A\subseteq A\cup \left\{M\right\}$$
41		resmpt	$$⊢A\subseteq A\cup \left\{M\right\}\to {\left(k\in \left(A\cup \left\{M\right\}\right)⟼X\right)\upharpoonright }_A=\left(k\in A⟼X\right)$$
42	40 41	mp1i	$$⊢\phi \to {\left(k\in \left(A\cup \left\{M\right\}\right)⟼X\right)\upharpoonright }_A=\left(k\in A⟼X\right)$$
43	39 42	syl5eq	$$⊢\phi \to {F\upharpoonright }_A=\left(k\in A⟼X\right)$$
44	43	oveq2d	$$⊢\phi \to {\sum }_G\left({F\upharpoonright }_A\right)=\underset{k\in A}{{\sum }_G}X$$
45	4	reseq1i	$$⊢{F\upharpoonright }_{\left\{M\right\}}={\left(k\in \left(A\cup \left\{M\right\}\right)⟼X\right)\upharpoonright }_{\left\{M\right\}}$$
46		ssun2	$$⊢\left\{M\right\}\subseteq A\cup \left\{M\right\}$$
47		resmpt	$$⊢\left\{M\right\}\subseteq A\cup \left\{M\right\}\to {\left(k\in \left(A\cup \left\{M\right\}\right)⟼X\right)\upharpoonright }_{\left\{M\right\}}=\left(k\in \left\{M\right\}⟼X\right)$$
48	46 47	mp1i	$$⊢\phi \to {\left(k\in \left(A\cup \left\{M\right\}\right)⟼X\right)\upharpoonright }_{\left\{M\right\}}=\left(k\in \left\{M\right\}⟼X\right)$$
49	45 48	syl5eq	$$⊢\phi \to {F\upharpoonright }_{\left\{M\right\}}=\left(k\in \left\{M\right\}⟼X\right)$$
50	49	oveq2d	$$⊢\phi \to {\sum }_G\left({F\upharpoonright }_{\left\{M\right\}}\right)=\underset{k\in \left\{M\right\}}{{\sum }_G}X$$
51	44 50	oveq12d	$$⊢\phi \to \left({\sum }_G,\left({F\upharpoonright }_A\right)\right)\underset{\dot{}}{+}\left({\sum }_G,\left({F\upharpoonright }_{\left\{M\right\}}\right)\right)=\left(\underset{k\in A}{{\sum }_G},X\right)\underset{\dot{}}{+}\left(\underset{k\in \left\{M\right\}}{{\sum }_G},X\right)$$
52	1 5 9 11 12	gsumsnd	$$⊢\phi \to \underset{k\in \left\{M\right\}}{{\sum }_G}X=Y$$
53	52	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$$
54	38 51 53	3eqtrd	$$⊢\phi \to {\sum }_{G}F=\left(\underset{k\in A}{{\sum }_G},X\right)\underset{\dot{}}{+}Y$$