Theorem gsum2dlem1

Description: Lemma 1 for gsum2d . (Contributed by Mario Carneiro, 28-Dec-2014) (Revised by AV, 8-Jun-2019)

	Ref	Expression
Hypotheses	gsum2d.b	$$⊢B={\mathrm{Base}}_G$$
	gsum2d.z	$$⊢\underset{\dot{}}{0}=0_G$$
	gsum2d.g	$$⊢\phi \to G\in \mathrm{CMnd}$$
	gsum2d.a	$$⊢\phi \to A\in V$$
	gsum2d.r	$$⊢\phi \to \mathrm{Rel}A$$
	gsum2d.d	$$⊢\phi \to D\in W$$
	gsum2d.s	$$⊢\phi \to \mathrm{dom}A\subseteq D$$
	gsum2d.f	$$⊢\phi \to F:A⟶B$$
	gsum2d.w	$$⊢\phi \to {finSupp}_{\underset{\dot{}}{0}}\left(F\right)$$
Assertion	gsum2dlem1	$$⊢\phi \to \underset{k\in A\left[\left\{j\right\}\right]}{{\sum }_G}\left(jFk\right)\in B$$

Proof

Step	Hyp	Ref	Expression
1		gsum2d.b	$$⊢B={\mathrm{Base}}_G$$
2		gsum2d.z	$$⊢\underset{\dot{}}{0}=0_G$$
3		gsum2d.g	$$⊢\phi \to G\in \mathrm{CMnd}$$
4		gsum2d.a	$$⊢\phi \to A\in V$$
5		gsum2d.r	$$⊢\phi \to \mathrm{Rel}A$$
6		gsum2d.d	$$⊢\phi \to D\in W$$
7		gsum2d.s	$$⊢\phi \to \mathrm{dom}A\subseteq D$$
8		gsum2d.f	$$⊢\phi \to F:A⟶B$$
9		gsum2d.w	$$⊢\phi \to {finSupp}_{\underset{\dot{}}{0}}\left(F\right)$$
10		imaexg	$$⊢A\in V\to A\left[\left\{j\right\}\right]\in \mathrm{V}$$
11	4 10	syl	$$⊢\phi \to A\left[\left\{j\right\}\right]\in \mathrm{V}$$
12		vex	$$⊢j\in \mathrm{V}$$
13		vex	$$⊢k\in \mathrm{V}$$
14	12 13	elimasn	$$⊢k\in A\left[\left\{j\right\}\right]\leftrightarrow ⟨j,k⟩\in A$$
15		df-ov	$$⊢jFk=F\left(⟨j,k⟩\right)$$
16	8	ffvelrnda	$$⊢\left(\phi \wedge ⟨j,k⟩\in A\right)\to F\left(⟨j,k⟩\right)\in B$$
17	15 16	eqeltrid	$$⊢\left(\phi \wedge ⟨j,k⟩\in A\right)\to jFk\in B$$
18	14 17	sylan2b	$$⊢\left(\phi \wedge k\in A\left[\left\{j\right\}\right]\right)\to jFk\in B$$
19	18	fmpttd	$$⊢\phi \to \left(k\in A\left[\left\{j\right\}\right]⟼jFk\right):A\left[\left\{j\right\}\right]⟶B$$
20	9	fsuppimpd	$$⊢\phi \to F\mathrm{supp}\underset{\dot{}}{0}\in \mathrm{Fin}$$
21		rnfi	$$⊢F\mathrm{supp}\underset{\dot{}}{0}\in \mathrm{Fin}\to \mathrm{ran}{supp}_{\underset{\dot{}}{0}}\left(F\right)\in \mathrm{Fin}$$
22	20 21	syl	$$⊢\phi \to \mathrm{ran}{supp}_{\underset{\dot{}}{0}}\left(F\right)\in \mathrm{Fin}$$
23	14	biimpi	$$⊢k\in A\left[\left\{j\right\}\right]\to ⟨j,k⟩\in A$$
24	12 13	opelrn	$$⊢⟨j,k⟩\in {supp}_{\underset{\dot{}}{0}}\left(F\right)\to k\in \mathrm{ran}{supp}_{\underset{\dot{}}{0}}\left(F\right)$$
25	24	con3i	$$⊢\neg k\in \mathrm{ran}{supp}_{\underset{\dot{}}{0}}\left(F\right)\to \neg ⟨j,k⟩\in {supp}_{\underset{\dot{}}{0}}\left(F\right)$$
26	23 25	anim12i	$$⊢\left(k\in A\left[\left\{j\right\}\right]\wedge \neg k\in \mathrm{ran}{supp}_{\underset{\dot{}}{0}}\left(F\right)\right)\to \left(⟨j,k⟩\in A\wedge \neg ⟨j,k⟩\in {supp}_{\underset{\dot{}}{0}}\left(F\right)\right)$$
27		eldif	$$⊢k\in \left(A\left[\left\{j\right\}\right]\setminus \mathrm{ran}{supp}_{\underset{\dot{}}{0}}\left(F\right)\right)\leftrightarrow \left(k\in A\left[\left\{j\right\}\right]\wedge \neg k\in \mathrm{ran}{supp}_{\underset{\dot{}}{0}}\left(F\right)\right)$$
28		eldif	$$⊢⟨j,k⟩\in \left(A\setminus {supp}_{\underset{\dot{}}{0}}\left(F\right)\right)\leftrightarrow \left(⟨j,k⟩\in A\wedge \neg ⟨j,k⟩\in {supp}_{\underset{\dot{}}{0}}\left(F\right)\right)$$
29	26 27 28	3imtr4i	$$⊢k\in \left(A\left[\left\{j\right\}\right]\setminus \mathrm{ran}{supp}_{\underset{\dot{}}{0}}\left(F\right)\right)\to ⟨j,k⟩\in \left(A\setminus {supp}_{\underset{\dot{}}{0}}\left(F\right)\right)$$
30		ssidd	$$⊢\phi \to F\mathrm{supp}\underset{\dot{}}{0}\subseteq F\mathrm{supp}\underset{\dot{}}{0}$$
31	2	fvexi	$$⊢\underset{\dot{}}{0}\in \mathrm{V}$$
32	31	a1i	$$⊢\phi \to \underset{\dot{}}{0}\in \mathrm{V}$$
33	8 30 4 32	suppssr	$$⊢\left(\phi \wedge ⟨j,k⟩\in \left(A\setminus {supp}_{\underset{\dot{}}{0}}\left(F\right)\right)\right)\to F\left(⟨j,k⟩\right)=\underset{\dot{}}{0}$$
34	15 33	syl5eq	$$⊢\left(\phi \wedge ⟨j,k⟩\in \left(A\setminus {supp}_{\underset{\dot{}}{0}}\left(F\right)\right)\right)\to jFk=\underset{\dot{}}{0}$$
35	29 34	sylan2	$$⊢\left(\phi \wedge k\in \left(A\left[\left\{j\right\}\right]\setminus \mathrm{ran}{supp}_{\underset{\dot{}}{0}}\left(F\right)\right)\right)\to jFk=\underset{\dot{}}{0}$$
36	35 11	suppss2	$$⊢\phi \to \left(k\in A\left[\left\{j\right\}\right]⟼jFk\right)\mathrm{supp}\underset{\dot{}}{0}\subseteq \mathrm{ran}{supp}_{\underset{\dot{}}{0}}\left(F\right)$$
37	22 36	ssfid	$$⊢\phi \to \left(k\in A\left[\left\{j\right\}\right]⟼jFk\right)\mathrm{supp}\underset{\dot{}}{0}\in \mathrm{Fin}$$
38	1 2 3 11 19 37	gsumcl2	$$⊢\phi \to \underset{k\in A\left[\left\{j\right\}\right]}{{\sum }_G}\left(jFk\right)\in B$$