Theorem psrbagaddcl

Description: The sum of two finite bags is a finite bag. (Contributed by Mario Carneiro, 9-Jan-2015) Shorten proof and remove a sethood antecedent. (Revised by SN, 7-Aug-2024)

	Ref	Expression
Hypothesis	psrbag.d	$$⊢D=\left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
Assertion	psrbagaddcl	$$⊢\left(F\in D\wedge G\in D\right)\to F{+}_{f}G\in D$$

Proof

Step	Hyp	Ref	Expression
1		psrbag.d	$$⊢D=\left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
2		nn0addcl	$$⊢\left(x\in {\mathbb{N}}_0\wedge y\in {\mathbb{N}}_0\right)\to x+y\in {\mathbb{N}}_0$$
3	2	adantl	$$⊢\left(\left(F\in D\wedge G\in D\right)\wedge \left(x\in {\mathbb{N}}_0\wedge y\in {\mathbb{N}}_0\right)\right)\to x+y\in {\mathbb{N}}_0$$
4	1	psrbagf	$$⊢F\in D\to F:I⟶{\mathbb{N}}_0$$
5	4	adantr	$$⊢\left(F\in D\wedge G\in D\right)\to F:I⟶{\mathbb{N}}_0$$
6	1	psrbagf	$$⊢G\in D\to G:I⟶{\mathbb{N}}_0$$
7	6	adantl	$$⊢\left(F\in D\wedge G\in D\right)\to G:I⟶{\mathbb{N}}_0$$
8		simpl	$$⊢\left(F\in D\wedge G\in D\right)\to F\in D$$
9	5	ffnd	$$⊢\left(F\in D\wedge G\in D\right)\to FFnI$$
10	8 9	fndmexd	$$⊢\left(F\in D\wedge G\in D\right)\to I\in \mathrm{V}$$
11		inidm	$$⊢I\cap I=I$$
12	3 5 7 10 10 11	off	$$⊢\left(F\in D\wedge G\in D\right)\to \left(F{+}_{f}G\right):I⟶{\mathbb{N}}_0$$
13		ovex	$$⊢F{+}_{f}G\in \mathrm{V}$$
14		frnnn0suppg	$$⊢\left(F{+}_{f}G\in \mathrm{V}\wedge \left(F{+}_{f}G\right):I⟶{\mathbb{N}}_0\right)\to \left(F{+}_{f}G\right)\mathrm{supp}0={\left(F{+}_{f}G\right)}^{-1}\left[\mathbb{N}\right]$$
15	13 12 14	sylancr	$$⊢\left(F\in D\wedge G\in D\right)\to \left(F{+}_{f}G\right)\mathrm{supp}0={\left(F{+}_{f}G\right)}^{-1}\left[\mathbb{N}\right]$$
16	1	psrbagfsupp	$$⊢F\in D\to {finSupp}_0\left(F\right)$$
17	16	adantr	$$⊢\left(F\in D\wedge G\in D\right)\to {finSupp}_0\left(F\right)$$
18	1	psrbagfsupp	$$⊢G\in D\to {finSupp}_0\left(G\right)$$
19	18	adantl	$$⊢\left(F\in D\wedge G\in D\right)\to {finSupp}_0\left(G\right)$$
20	17 19	fsuppunfi	$$⊢\left(F\in D\wedge G\in D\right)\to {supp}_0\left(F\right)\cup {supp}_0\left(G\right)\in \mathrm{Fin}$$
21		0nn0	$$⊢0\in {\mathbb{N}}_0$$
22	21	a1i	$$⊢\left(F\in D\wedge G\in D\right)\to 0\in {\mathbb{N}}_0$$
23		00id	$$⊢0+0=0$$
24	23	a1i	$$⊢\left(F\in D\wedge G\in D\right)\to 0+0=0$$
25	10 22 5 7 24	suppofssd	$$⊢\left(F\in D\wedge G\in D\right)\to \left(F{+}_{f}G\right)\mathrm{supp}0\subseteq {supp}_0\left(F\right)\cup {supp}_0\left(G\right)$$
26	20 25	ssfid	$$⊢\left(F\in D\wedge G\in D\right)\to \left(F{+}_{f}G\right)\mathrm{supp}0\in \mathrm{Fin}$$
27	15 26	eqeltrrd	$$⊢\left(F\in D\wedge G\in D\right)\to {\left(F{+}_{f}G\right)}^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}$$
28	1	psrbag	$$⊢I\in \mathrm{V}\to \left(F{+}_{f}G\in D\leftrightarrow \left(\left(F{+}_{f}G\right):I⟶{\mathbb{N}}_0\wedge {\left(F{+}_{f}G\right)}^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right)\right)$$
29	10 28	syl	$$⊢\left(F\in D\wedge G\in D\right)\to \left(F{+}_{f}G\in D\leftrightarrow \left(\left(F{+}_{f}G\right):I⟶{\mathbb{N}}_0\wedge {\left(F{+}_{f}G\right)}^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right)\right)$$
30	12 27 29	mpbir2and	$$⊢\left(F\in D\wedge G\in D\right)\to F{+}_{f}G\in D$$