Theorem fsuppco

Description: The composition of a 1-1 function with a finitely supported function is finitely supported. (Contributed by AV, 28-May-2019)

	Ref	Expression
Hypotheses	fsuppco.f	$$⊢\phi \to {finSupp}_Z\left(F\right)$$
	fsuppco.g	$$⊢\phi \to G:X\underset{1-1}{⟶}Y$$
	fsuppco.z	$$⊢\phi \to Z\in W$$
	fsuppco.v	$$⊢\phi \to F\in V$$
Assertion	fsuppco	$$⊢\phi \to {finSupp}_Z\left(\left(F\circ G\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		fsuppco.f	$$⊢\phi \to {finSupp}_Z\left(F\right)$$
2		fsuppco.g	$$⊢\phi \to G:X\underset{1-1}{⟶}Y$$
3		fsuppco.z	$$⊢\phi \to Z\in W$$
4		fsuppco.v	$$⊢\phi \to F\in V$$
5		df-f1	$$⊢G:X\underset{1-1}{⟶}Y\leftrightarrow \left(G:X⟶Y\wedge \mathrm{Fun}{G}^{-1}\right)$$
6	5	simprbi	$$⊢G:X\underset{1-1}{⟶}Y\to \mathrm{Fun}{G}^{-1}$$
7	2 6	syl	$$⊢\phi \to \mathrm{Fun}{G}^{-1}$$
8		cofunex2g	$$⊢\left(F\in V\wedge \mathrm{Fun}{G}^{-1}\right)\to F\circ G\in \mathrm{V}$$
9	4 7 8	syl2anc	$$⊢\phi \to F\circ G\in \mathrm{V}$$
10		suppimacnv	$$⊢\left(F\circ G\in \mathrm{V}\wedge Z\in W\right)\to \left(F\circ G\right)\mathrm{supp}Z={\left(F\circ G\right)}^{-1}\left[\mathrm{V}\setminus \left\{Z\right\}\right]$$
11	9 3 10	syl2anc	$$⊢\phi \to \left(F\circ G\right)\mathrm{supp}Z={\left(F\circ G\right)}^{-1}\left[\mathrm{V}\setminus \left\{Z\right\}\right]$$
12		suppimacnv	$$⊢\left(F\in V\wedge Z\in W\right)\to F\mathrm{supp}Z=F^{-1}\left[\mathrm{V}\setminus \left\{Z\right\}\right]$$
13	4 3 12	syl2anc	$$⊢\phi \to F\mathrm{supp}Z=F^{-1}\left[\mathrm{V}\setminus \left\{Z\right\}\right]$$
14	1	fsuppimpd	$$⊢\phi \to F\mathrm{supp}Z\in \mathrm{Fin}$$
15	13 14	eqeltrrd	$$⊢\phi \to F^{-1}\left[\mathrm{V}\setminus \left\{Z\right\}\right]\in \mathrm{Fin}$$
16	15 2	fsuppcolem	$$⊢\phi \to {\left(F\circ G\right)}^{-1}\left[\mathrm{V}\setminus \left\{Z\right\}\right]\in \mathrm{Fin}$$
17	11 16	eqeltrd	$$⊢\phi \to \left(F\circ G\right)\mathrm{supp}Z\in \mathrm{Fin}$$
18		fsuppimp	$$⊢{finSupp}_Z\left(F\right)\to \left(\mathrm{Fun}F\wedge F\mathrm{supp}Z\in \mathrm{Fin}\right)$$
19	18	simpld	$$⊢{finSupp}_Z\left(F\right)\to \mathrm{Fun}F$$
20	1 19	syl	$$⊢\phi \to \mathrm{Fun}F$$
21		f1fun	$$⊢G:X\underset{1-1}{⟶}Y\to \mathrm{Fun}G$$
22	2 21	syl	$$⊢\phi \to \mathrm{Fun}G$$
23		funco	$$⊢\left(\mathrm{Fun}F\wedge \mathrm{Fun}G\right)\to \mathrm{Fun}\left(F\circ G\right)$$
24	20 22 23	syl2anc	$$⊢\phi \to \mathrm{Fun}\left(F\circ G\right)$$
25		funisfsupp	$$⊢\left(\mathrm{Fun}\left(F\circ G\right)\wedge F\circ G\in \mathrm{V}\wedge Z\in W\right)\to \left({finSupp}_Z\left(\left(F\circ G\right)\right)\leftrightarrow \left(F\circ G\right)\mathrm{supp}Z\in \mathrm{Fin}\right)$$
26	24 9 3 25	syl3anc	$$⊢\phi \to \left({finSupp}_Z\left(\left(F\circ G\right)\right)\leftrightarrow \left(F\circ G\right)\mathrm{supp}Z\in \mathrm{Fin}\right)$$
27	17 26	mpbird	$$⊢\phi \to {finSupp}_Z\left(\left(F\circ G\right)\right)$$