Theorem fsuppco2

Description: The composition of a function which maps the zero to zero with a finitely supported function is finitely supported. This is not only a special case of fsuppcor because it does not require that the "zero" is an element of the range of the finitely supported function. (Contributed by AV, 6-Jun-2019)

	Ref	Expression
Hypotheses	fsuppco2.z	$$⊢\phi \to Z\in W$$
	fsuppco2.f	$$⊢\phi \to F:A⟶B$$
	fsuppco2.g	$$⊢\phi \to G:B⟶B$$
	fsuppco2.a	$$⊢\phi \to A\in U$$
	fsuppco2.b	$$⊢\phi \to B\in V$$
	fsuppco2.n	$$⊢\phi \to {finSupp}_Z\left(F\right)$$
	fsuppco2.i	$$⊢\phi \to G\left(Z\right)=Z$$
Assertion	fsuppco2	$$⊢\phi \to {finSupp}_Z\left(\left(G\circ F\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		fsuppco2.z	$$⊢\phi \to Z\in W$$
2		fsuppco2.f	$$⊢\phi \to F:A⟶B$$
3		fsuppco2.g	$$⊢\phi \to G:B⟶B$$
4		fsuppco2.a	$$⊢\phi \to A\in U$$
5		fsuppco2.b	$$⊢\phi \to B\in V$$
6		fsuppco2.n	$$⊢\phi \to {finSupp}_Z\left(F\right)$$
7		fsuppco2.i	$$⊢\phi \to G\left(Z\right)=Z$$
8	3	ffund	$$⊢\phi \to \mathrm{Fun}G$$
9	2	ffund	$$⊢\phi \to \mathrm{Fun}F$$
10		funco	$$⊢\left(\mathrm{Fun}G\wedge \mathrm{Fun}F\right)\to \mathrm{Fun}\left(G\circ F\right)$$
11	8 9 10	syl2anc	$$⊢\phi \to \mathrm{Fun}\left(G\circ F\right)$$
12	6	fsuppimpd	$$⊢\phi \to F\mathrm{supp}Z\in \mathrm{Fin}$$
13		fco	$$⊢\left(G:B⟶B\wedge F:A⟶B\right)\to \left(G\circ F\right):A⟶B$$
14	3 2 13	syl2anc	$$⊢\phi \to \left(G\circ F\right):A⟶B$$
15		eldifi	$$⊢x\in \left(A\setminus {supp}_Z\left(F\right)\right)\to x\in A$$
16		fvco3	$$⊢\left(F:A⟶B\wedge x\in A\right)\to \left(G\circ F\right)\left(x\right)=G\left(F\left(x\right)\right)$$
17	2 15 16	syl2an	$$⊢\left(\phi \wedge x\in \left(A\setminus {supp}_Z\left(F\right)\right)\right)\to \left(G\circ F\right)\left(x\right)=G\left(F\left(x\right)\right)$$
18		ssidd	$$⊢\phi \to F\mathrm{supp}Z\subseteq F\mathrm{supp}Z$$
19	2 18 4 1	suppssr	$$⊢\left(\phi \wedge x\in \left(A\setminus {supp}_Z\left(F\right)\right)\right)\to F\left(x\right)=Z$$
20	19	fveq2d	$$⊢\left(\phi \wedge x\in \left(A\setminus {supp}_Z\left(F\right)\right)\right)\to G\left(F\left(x\right)\right)=G\left(Z\right)$$
21	7	adantr	$$⊢\left(\phi \wedge x\in \left(A\setminus {supp}_Z\left(F\right)\right)\right)\to G\left(Z\right)=Z$$
22	17 20 21	3eqtrd	$$⊢\left(\phi \wedge x\in \left(A\setminus {supp}_Z\left(F\right)\right)\right)\to \left(G\circ F\right)\left(x\right)=Z$$
23	14 22	suppss	$$⊢\phi \to \left(G\circ F\right)\mathrm{supp}Z\subseteq F\mathrm{supp}Z$$
24	12 23	ssfid	$$⊢\phi \to \left(G\circ F\right)\mathrm{supp}Z\in \mathrm{Fin}$$
25	3 5	fexd	$$⊢\phi \to G\in \mathrm{V}$$
26	2 4	fexd	$$⊢\phi \to F\in \mathrm{V}$$
27		coexg	$$⊢\left(G\in \mathrm{V}\wedge F\in \mathrm{V}\right)\to G\circ F\in \mathrm{V}$$
28	25 26 27	syl2anc	$$⊢\phi \to G\circ F\in \mathrm{V}$$
29		isfsupp	$$⊢\left(G\circ F\in \mathrm{V}\wedge Z\in W\right)\to \left({finSupp}_Z\left(\left(G\circ F\right)\right)\leftrightarrow \left(\mathrm{Fun}\left(G\circ F\right)\wedge \left(G\circ F\right)\mathrm{supp}Z\in \mathrm{Fin}\right)\right)$$
30	28 1 29	syl2anc	$$⊢\phi \to \left({finSupp}_Z\left(\left(G\circ F\right)\right)\leftrightarrow \left(\mathrm{Fun}\left(G\circ F\right)\wedge \left(G\circ F\right)\mathrm{supp}Z\in \mathrm{Fin}\right)\right)$$
31	11 24 30	mpbir2and	$$⊢\phi \to {finSupp}_Z\left(\left(G\circ F\right)\right)$$