Theorem fsuppmptif

Description: A function mapping an argument to either a value of a finitely supported function or zero is finitely supported. (Contributed by AV, 6-Jun-2019)

	Ref	Expression
Hypotheses	fsuppmptif.f	$$⊢\phi \to F:A⟶B$$
	fsuppmptif.a	$$⊢\phi \to A\in V$$
	fsuppmptif.z	$$⊢\phi \to Z\in W$$
	fsuppmptif.s	$$⊢\phi \to {finSupp}_Z\left(F\right)$$
Assertion	fsuppmptif	$$⊢\phi \to {finSupp}_Z\left(\left(k\in A⟼if\left(k\in D,F\left(k\right),Z\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		fsuppmptif.f	$$⊢\phi \to F:A⟶B$$
2		fsuppmptif.a	$$⊢\phi \to A\in V$$
3		fsuppmptif.z	$$⊢\phi \to Z\in W$$
4		fsuppmptif.s	$$⊢\phi \to {finSupp}_Z\left(F\right)$$
5		fvex	$$⊢F\left(k\right)\in \mathrm{V}$$
6	3	adantr	$$⊢\left(\phi \wedge k\in A\right)\to Z\in W$$
7		ifexg	$$⊢\left(F\left(k\right)\in \mathrm{V}\wedge Z\in W\right)\to if\left(k\in D,F\left(k\right),Z\right)\in \mathrm{V}$$
8	5 6 7	sylancr	$$⊢\left(\phi \wedge k\in A\right)\to if\left(k\in D,F\left(k\right),Z\right)\in \mathrm{V}$$
9	8	fmpttd	$$⊢\phi \to \left(k\in A⟼if\left(k\in D,F\left(k\right),Z\right)\right):A⟶\mathrm{V}$$
10	9	ffund	$$⊢\phi \to \mathrm{Fun}\left(k\in A⟼if\left(k\in D,F\left(k\right),Z\right)\right)$$
11	4	fsuppimpd	$$⊢\phi \to F\mathrm{supp}Z\in \mathrm{Fin}$$
12		ssidd	$$⊢\phi \to F\mathrm{supp}Z\subseteq F\mathrm{supp}Z$$
13	1 12 2 3	suppssr	$$⊢\left(\phi \wedge k\in \left(A\setminus {supp}_Z\left(F\right)\right)\right)\to F\left(k\right)=Z$$
14	13	ifeq1d	$$⊢\left(\phi \wedge k\in \left(A\setminus {supp}_Z\left(F\right)\right)\right)\to if\left(k\in D,F\left(k\right),Z\right)=if\left(k\in D,Z,Z\right)$$
15		ifid	$$⊢if\left(k\in D,Z,Z\right)=Z$$
16	14 15	syl6eq	$$⊢\left(\phi \wedge k\in \left(A\setminus {supp}_Z\left(F\right)\right)\right)\to if\left(k\in D,F\left(k\right),Z\right)=Z$$
17	16 2	suppss2	$$⊢\phi \to \left(k\in A⟼if\left(k\in D,F\left(k\right),Z\right)\right)\mathrm{supp}Z\subseteq F\mathrm{supp}Z$$
18	11 17	ssfid	$$⊢\phi \to \left(k\in A⟼if\left(k\in D,F\left(k\right),Z\right)\right)\mathrm{supp}Z\in \mathrm{Fin}$$
19	2	mptexd	$$⊢\phi \to \left(k\in A⟼if\left(k\in D,F\left(k\right),Z\right)\right)\in \mathrm{V}$$
20		isfsupp	$$⊢\left(\left(k\in A⟼if\left(k\in D,F\left(k\right),Z\right)\right)\in \mathrm{V}\wedge Z\in W\right)\to \left({finSupp}_Z\left(\left(k\in A⟼if\left(k\in D,F\left(k\right),Z\right)\right)\right)\leftrightarrow \left(\mathrm{Fun}\left(k\in A⟼if\left(k\in D,F\left(k\right),Z\right)\right)\wedge \left(k\in A⟼if\left(k\in D,F\left(k\right),Z\right)\right)\mathrm{supp}Z\in \mathrm{Fin}\right)\right)$$
21	19 3 20	syl2anc	$$⊢\phi \to \left({finSupp}_Z\left(\left(k\in A⟼if\left(k\in D,F\left(k\right),Z\right)\right)\right)\leftrightarrow \left(\mathrm{Fun}\left(k\in A⟼if\left(k\in D,F\left(k\right),Z\right)\right)\wedge \left(k\in A⟼if\left(k\in D,F\left(k\right),Z\right)\right)\mathrm{supp}Z\in \mathrm{Fin}\right)\right)$$
22	10 18 21	mpbir2and	$$⊢\phi \to {finSupp}_Z\left(\left(k\in A⟼if\left(k\in D,F\left(k\right),Z\right)\right)\right)$$