Theorem psrbagev1

Description: A bag of multipliers provides the conditions for a valid sum. (Contributed by Stefan O'Rear, 9-Mar-2015) (Revised by AV, 18-Jul-2019) (Revised by AV, 11-Apr-2024) Remove a sethood hypothesis. (Revised by SN, 7-Aug-2024)

	Ref	Expression
Hypotheses	psrbagev1.d	$$⊢D=\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
	psrbagev1.c	$$⊢C={\mathrm{Base}}_T$$
	psrbagev1.x	$$⊢\underset{\dot{}}{·}={\cdot }_T$$
	psrbagev1.z	$$⊢\underset{\dot{}}{0}=0_T$$
	psrbagev1.t	$$⊢\phi \to T\in \mathrm{CMnd}$$
	psrbagev1.b	$$⊢\phi \to B\in D$$
	psrbagev1.g	$$⊢\phi \to G:I⟶C$$
Assertion	psrbagev1	$$⊢\phi \to \left(\left(B{\underset{\dot{}}{·}}_{f}G\right):I⟶C\wedge {finSupp}_{\underset{\dot{}}{0}}\left(\left(B{\underset{\dot{}}{·}}_{f}G\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		psrbagev1.d	$$⊢D=\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
2		psrbagev1.c	$$⊢C={\mathrm{Base}}_T$$
3		psrbagev1.x	$$⊢\underset{\dot{}}{·}={\cdot }_T$$
4		psrbagev1.z	$$⊢\underset{\dot{}}{0}=0_T$$
5		psrbagev1.t	$$⊢\phi \to T\in \mathrm{CMnd}$$
6		psrbagev1.b	$$⊢\phi \to B\in D$$
7		psrbagev1.g	$$⊢\phi \to G:I⟶C$$
8	5	cmnmndd	$$⊢\phi \to T\in \mathrm{Mnd}$$
9	2 3	mulgnn0cl	$$⊢\left(T\in \mathrm{Mnd}\wedge y\in {\mathbb{N}}_0\wedge z\in C\right)\to y\underset{\dot{}}{·}z\in C$$
10	9	3expb	$$⊢\left(T\in \mathrm{Mnd}\wedge \left(y\in {\mathbb{N}}_0\wedge z\in C\right)\right)\to y\underset{\dot{}}{·}z\in C$$
11	8 10	sylan	$$⊢\left(\phi \wedge \left(y\in {\mathbb{N}}_0\wedge z\in C\right)\right)\to y\underset{\dot{}}{·}z\in C$$
12	1	psrbagf	$$⊢B\in D\to B:I⟶{\mathbb{N}}_0$$
13	6 12	syl	$$⊢\phi \to B:I⟶{\mathbb{N}}_0$$
14	13	ffnd	$$⊢\phi \to BFnI$$
15	6 14	fndmexd	$$⊢\phi \to I\in \mathrm{V}$$
16		inidm	$$⊢I\cap I=I$$
17	11 13 7 15 15 16	off	$$⊢\phi \to \left(B{\underset{\dot{}}{·}}_{f}G\right):I⟶C$$
18		ovexd	$$⊢\phi \to B{\underset{\dot{}}{·}}_{f}G\in \mathrm{V}$$
19	7	ffnd	$$⊢\phi \to GFnI$$
20	14 19 15 15	offun	$$⊢\phi \to \mathrm{Fun}\left(B{\underset{\dot{}}{·}}_{f}G\right)$$
21	4	fvexi	$$⊢\underset{\dot{}}{0}\in \mathrm{V}$$
22	21	a1i	$$⊢\phi \to \underset{\dot{}}{0}\in \mathrm{V}$$
23	1	psrbagfsupp	$$⊢B\in D\to {finSupp}_0\left(B\right)$$
24	6 23	syl	$$⊢\phi \to {finSupp}_0\left(B\right)$$
25	24	fsuppimpd	$$⊢\phi \to B\mathrm{supp}0\in \mathrm{Fin}$$
26		ssidd	$$⊢\phi \to B\mathrm{supp}0\subseteq B\mathrm{supp}0$$
27	2 4 3	mulg0	$$⊢z\in C\to 0\underset{\dot{}}{·}z=\underset{\dot{}}{0}$$
28	27	adantl	$$⊢\left(\phi \wedge z\in C\right)\to 0\underset{\dot{}}{·}z=\underset{\dot{}}{0}$$
29		c0ex	$$⊢0\in \mathrm{V}$$
30	29	a1i	$$⊢\phi \to 0\in \mathrm{V}$$
31	26 28 13 7 15 30	suppssof1	$$⊢\phi \to \left(B{\underset{\dot{}}{·}}_{f}G\right)\mathrm{supp}\underset{\dot{}}{0}\subseteq B\mathrm{supp}0$$
32		suppssfifsupp	$$⊢\left(\left(B{\underset{\dot{}}{·}}_{f}G\in \mathrm{V}\wedge \mathrm{Fun}\left(B{\underset{\dot{}}{·}}_{f}G\right)\wedge \underset{\dot{}}{0}\in \mathrm{V}\right)\wedge \left(B\mathrm{supp}0\in \mathrm{Fin}\wedge \left(B{\underset{\dot{}}{·}}_{f}G\right)\mathrm{supp}\underset{\dot{}}{0}\subseteq B\mathrm{supp}0\right)\right)\to {finSupp}_{\underset{\dot{}}{0}}\left(\left(B{\underset{\dot{}}{·}}_{f}G\right)\right)$$
33	18 20 22 25 31 32	syl32anc	$$⊢\phi \to {finSupp}_{\underset{\dot{}}{0}}\left(\left(B{\underset{\dot{}}{·}}_{f}G\right)\right)$$
34	17 33	jca	$$⊢\phi \to \left(\left(B{\underset{\dot{}}{·}}_{f}G\right):I⟶C\wedge {finSupp}_{\underset{\dot{}}{0}}\left(\left(B{\underset{\dot{}}{·}}_{f}G\right)\right)\right)$$