Theorem fsuppcor

Description: The composition of a function which maps the zero of the range of a finitely supported function to the zero of its range with this finitely supported function is finitely supported. (Contributed by AV, 6-Jun-2019)

	Ref	Expression
Hypotheses	fsuppcor.0	$$⊢\phi \to \underset{\dot{}}{0}\in W$$
	fsuppcor.z	$$⊢\phi \to Z\in B$$
	fsuppcor.f	$$⊢\phi \to F:A⟶C$$
	fsuppcor.g	$$⊢\phi \to G:B⟶D$$
	fsuppcor.s	$$⊢\phi \to C\subseteq B$$
	fsuppcor.a	$$⊢\phi \to A\in U$$
	fsuppcor.b	$$⊢\phi \to B\in V$$
	fsuppcor.n	$$⊢\phi \to {finSupp}_Z\left(F\right)$$
	fsuppcor.i	$$⊢\phi \to G\left(Z\right)=\underset{\dot{}}{0}$$
Assertion	fsuppcor	$$⊢\phi \to {finSupp}_{\underset{\dot{}}{0}}\left(\left(G\circ F\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		fsuppcor.0	$$⊢\phi \to \underset{\dot{}}{0}\in W$$
2		fsuppcor.z	$$⊢\phi \to Z\in B$$
3		fsuppcor.f	$$⊢\phi \to F:A⟶C$$
4		fsuppcor.g	$$⊢\phi \to G:B⟶D$$
5		fsuppcor.s	$$⊢\phi \to C\subseteq B$$
6		fsuppcor.a	$$⊢\phi \to A\in U$$
7		fsuppcor.b	$$⊢\phi \to B\in V$$
8		fsuppcor.n	$$⊢\phi \to {finSupp}_Z\left(F\right)$$
9		fsuppcor.i	$$⊢\phi \to G\left(Z\right)=\underset{\dot{}}{0}$$
10	4	ffund	$$⊢\phi \to \mathrm{Fun}G$$
11	3	ffund	$$⊢\phi \to \mathrm{Fun}F$$
12		funco	$$⊢\left(\mathrm{Fun}G\wedge \mathrm{Fun}F\right)\to \mathrm{Fun}\left(G\circ F\right)$$
13	10 11 12	syl2anc	$$⊢\phi \to \mathrm{Fun}\left(G\circ F\right)$$
14	8	fsuppimpd	$$⊢\phi \to F\mathrm{supp}Z\in \mathrm{Fin}$$
15	4 5	fssresd	$$⊢\phi \to \left({G\upharpoonright }_C\right):C⟶D$$
16		fco2	$$⊢\left(\left({G\upharpoonright }_C\right):C⟶D\wedge F:A⟶C\right)\to \left(G\circ F\right):A⟶D$$
17	15 3 16	syl2anc	$$⊢\phi \to \left(G\circ F\right):A⟶D$$
18		eldifi	$$⊢x\in \left(A\setminus {supp}_Z\left(F\right)\right)\to x\in A$$
19		fvco3	$$⊢\left(F:A⟶C\wedge x\in A\right)\to \left(G\circ F\right)\left(x\right)=G\left(F\left(x\right)\right)$$
20	3 18 19	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)$$
21		ssidd	$$⊢\phi \to F\mathrm{supp}Z\subseteq F\mathrm{supp}Z$$
22	3 21 6 2	suppssr	$$⊢\left(\phi \wedge x\in \left(A\setminus {supp}_Z\left(F\right)\right)\right)\to F\left(x\right)=Z$$
23	22	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)$$
24	9	adantr	$$⊢\left(\phi \wedge x\in \left(A\setminus {supp}_Z\left(F\right)\right)\right)\to G\left(Z\right)=\underset{\dot{}}{0}$$
25	20 23 24	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)=\underset{\dot{}}{0}$$
26	17 25	suppss	$$⊢\phi \to \left(G\circ F\right)\mathrm{supp}\underset{\dot{}}{0}\subseteq F\mathrm{supp}Z$$
27	14 26	ssfid	$$⊢\phi \to \left(G\circ F\right)\mathrm{supp}\underset{\dot{}}{0}\in \mathrm{Fin}$$
28		fex	$$⊢\left(G:B⟶D\wedge B\in V\right)\to G\in \mathrm{V}$$
29	4 7 28	syl2anc	$$⊢\phi \to G\in \mathrm{V}$$
30		fex	$$⊢\left(F:A⟶C\wedge A\in U\right)\to F\in \mathrm{V}$$
31	3 6 30	syl2anc	$$⊢\phi \to F\in \mathrm{V}$$
32		coexg	$$⊢\left(G\in \mathrm{V}\wedge F\in \mathrm{V}\right)\to G\circ F\in \mathrm{V}$$
33	29 31 32	syl2anc	$$⊢\phi \to G\circ F\in \mathrm{V}$$
34		isfsupp	$$⊢\left(G\circ F\in \mathrm{V}\wedge \underset{\dot{}}{0}\in W\right)\to \left({finSupp}_{\underset{\dot{}}{0}}\left(\left(G\circ F\right)\right)\leftrightarrow \left(\mathrm{Fun}\left(G\circ F\right)\wedge \left(G\circ F\right)\mathrm{supp}\underset{\dot{}}{0}\in \mathrm{Fin}\right)\right)$$
35	33 1 34	syl2anc	$$⊢\phi \to \left({finSupp}_{\underset{\dot{}}{0}}\left(\left(G\circ F\right)\right)\leftrightarrow \left(\mathrm{Fun}\left(G\circ F\right)\wedge \left(G\circ F\right)\mathrm{supp}\underset{\dot{}}{0}\in \mathrm{Fin}\right)\right)$$
36	13 27 35	mpbir2and	$$⊢\phi \to {finSupp}_{\underset{\dot{}}{0}}\left(\left(G\circ F\right)\right)$$