Theorem gsummptres

Description: Extend a finite group sum by padding outside with zeroes. Proof generated using OpenAI's proof assistant. (Contributed by Thierry Arnoux, 11-Jul-2020)

	Ref	Expression
Hypotheses	gsummptres.0	$$⊢B={\mathrm{Base}}_G$$
	gsummptres.1	$$⊢\underset{\dot{}}{0}=0_G$$
	gsummptres.2	$$⊢\phi \to G\in \mathrm{CMnd}$$
	gsummptres.3	$$⊢\phi \to A\in \mathrm{Fin}$$
	gsummptres.4	$$⊢\left(\phi \wedge x\in A\right)\to C\in B$$
	gsummptres.5	$$⊢\left(\phi \wedge x\in \left(A\setminus D\right)\right)\to C=\underset{\dot{}}{0}$$
Assertion	gsummptres	$$⊢\phi \to \underset{x\in A}{{\sum }_G}C=\underset{x\in A\cap D}{{\sum }_G}C$$

Proof

Step	Hyp	Ref	Expression
1		gsummptres.0	$$⊢B={\mathrm{Base}}_G$$
2		gsummptres.1	$$⊢\underset{\dot{}}{0}=0_G$$
3		gsummptres.2	$$⊢\phi \to G\in \mathrm{CMnd}$$
4		gsummptres.3	$$⊢\phi \to A\in \mathrm{Fin}$$
5		gsummptres.4	$$⊢\left(\phi \wedge x\in A\right)\to C\in B$$
6		gsummptres.5	$$⊢\left(\phi \wedge x\in \left(A\setminus D\right)\right)\to C=\underset{\dot{}}{0}$$
7		eqid	$$⊢{+}_G={+}_G$$
8		eqid	$$⊢\left(x\in A⟼C\right)=\left(x\in A⟼C\right)$$
9	2	fvexi	$$⊢\underset{\dot{}}{0}\in \mathrm{V}$$
10	9	a1i	$$⊢\phi \to \underset{\dot{}}{0}\in \mathrm{V}$$
11	8 4 5 10	fsuppmptdm	$$⊢\phi \to {finSupp}_{\underset{\dot{}}{0}}\left(\left(x\in A⟼C\right)\right)$$
12		inindif	$$⊢\left(A\cap D\right)\cap \left(A\setminus D\right)=\varnothing$$
13	12	a1i	$$⊢\phi \to \left(A\cap D\right)\cap \left(A\setminus D\right)=\varnothing$$
14		inundif	$$⊢\left(A\cap D\right)\cup \left(A\setminus D\right)=A$$
15	14	eqcomi	$$⊢A=\left(A\cap D\right)\cup \left(A\setminus D\right)$$
16	15	a1i	$$⊢\phi \to A=\left(A\cap D\right)\cup \left(A\setminus D\right)$$
17	1 2 7 3 4 5 11 13 16	gsumsplit2	$$⊢\phi \to \underset{x\in A}{{\sum }_G}C=\left(\underset{x\in A\cap D}{{\sum }_G},C\right){+}_G\left(\underset{x\in A\setminus D}{{\sum }_G},C\right)$$
18	6	mpteq2dva	$$⊢\phi \to \left(x\in \left(A\setminus D\right)⟼C\right)=\left(x\in \left(A\setminus D\right)⟼\underset{\dot{}}{0}\right)$$
19	18	oveq2d	$$⊢\phi \to \underset{x\in A\setminus D}{{\sum }_G}C=\underset{x\in A\setminus D}{{\sum }_G}\underset{\dot{}}{0}$$
20		cmnmnd	$$⊢G\in \mathrm{CMnd}\to G\in \mathrm{Mnd}$$
21	3 20	syl	$$⊢\phi \to G\in \mathrm{Mnd}$$
22		diffi	$$⊢A\in \mathrm{Fin}\to A\setminus D\in \mathrm{Fin}$$
23	4 22	syl	$$⊢\phi \to A\setminus D\in \mathrm{Fin}$$
24	2	gsumz	$$⊢\left(G\in \mathrm{Mnd}\wedge A\setminus D\in \mathrm{Fin}\right)\to \underset{x\in A\setminus D}{{\sum }_G}\underset{\dot{}}{0}=\underset{\dot{}}{0}$$
25	21 23 24	syl2anc	$$⊢\phi \to \underset{x\in A\setminus D}{{\sum }_G}\underset{\dot{}}{0}=\underset{\dot{}}{0}$$
26	19 25	eqtrd	$$⊢\phi \to \underset{x\in A\setminus D}{{\sum }_G}C=\underset{\dot{}}{0}$$
27	26	oveq2d	$$⊢\phi \to \left(\underset{x\in A\cap D}{{\sum }_G},C\right){+}_G\left(\underset{x\in A\setminus D}{{\sum }_G},C\right)=\left(\underset{x\in A\cap D}{{\sum }_G},C\right){+}_G\underset{\dot{}}{0}$$
28		infi	$$⊢A\in \mathrm{Fin}\to A\cap D\in \mathrm{Fin}$$
29	4 28	syl	$$⊢\phi \to A\cap D\in \mathrm{Fin}$$
30		inss1	$$⊢A\cap D\subseteq A$$
31	30	sseli	$$⊢x\in \left(A\cap D\right)\to x\in A$$
32	31 5	sylan2	$$⊢\left(\phi \wedge x\in \left(A\cap D\right)\right)\to C\in B$$
33	32	ralrimiva	$$⊢\phi \to \forall x\in \left(A\cap D\right)C\in B$$
34	1 3 29 33	gsummptcl	$$⊢\phi \to \underset{x\in A\cap D}{{\sum }_G}C\in B$$
35	1 7 2	mndrid	$$⊢\left(G\in \mathrm{Mnd}\wedge \underset{x\in A\cap D}{{\sum }_G}C\in B\right)\to \left(\underset{x\in A\cap D}{{\sum }_G},C\right){+}_G\underset{\dot{}}{0}=\underset{x\in A\cap D}{{\sum }_G}C$$
36	21 34 35	syl2anc	$$⊢\phi \to \left(\underset{x\in A\cap D}{{\sum }_G},C\right){+}_G\underset{\dot{}}{0}=\underset{x\in A\cap D}{{\sum }_G}C$$
37	27 36	eqtrd	$$⊢\phi \to \left(\underset{x\in A\cap D}{{\sum }_G},C\right){+}_G\left(\underset{x\in A\setminus D}{{\sum }_G},C\right)=\underset{x\in A\cap D}{{\sum }_G}C$$
38	17 37	eqtrd	$$⊢\phi \to \underset{x\in A}{{\sum }_G}C=\underset{x\in A\cap D}{{\sum }_G}C$$