Theorem psrbagev2

Description: Closure of a sum using a bag of multipliers. (Contributed by Stefan O'Rear, 9-Mar-2015) (Proof shortened by AV, 18-Jul-2019) (Revised by AV, 11-Apr-2024) Remove a sethood hypothesis. (Revised by SN, 7-Aug-2024)

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

Proof

Step	Hyp	Ref	Expression
1		psrbagev2.d	$$⊢D=\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
2		psrbagev2.c	$$⊢C={\mathrm{Base}}_T$$
3		psrbagev2.x	$$⊢\underset{\dot{}}{·}={\cdot }_T$$
4		psrbagev2.t	$$⊢\phi \to T\in \mathrm{CMnd}$$
5		psrbagev2.b	$$⊢\phi \to B\in D$$
6		psrbagev2.g	$$⊢\phi \to G:I⟶C$$
7		eqid	$$⊢0_T=0_T$$
8		ovexd	$$⊢\phi \to B{\underset{\dot{}}{·}}_{f}G\in \mathrm{V}$$
9	1 2 3 7 4 5 6	psrbagev1	$$⊢\phi \to \left(\left(B{\underset{\dot{}}{·}}_{f}G\right):I⟶C\wedge {finSupp}_{0_T}\left(\left(B{\underset{\dot{}}{·}}_{f}G\right)\right)\right)$$
10	9	simpld	$$⊢\phi \to \left(B{\underset{\dot{}}{·}}_{f}G\right):I⟶C$$
11	10	ffnd	$$⊢\phi \to \left(B{\underset{\dot{}}{·}}_{f}G\right)FnI$$
12	8 11	fndmexd	$$⊢\phi \to I\in \mathrm{V}$$
13	9	simprd	$$⊢\phi \to {finSupp}_{0_T}\left(\left(B{\underset{\dot{}}{·}}_{f}G\right)\right)$$
14	2 7 4 12 10 13	gsumcl	$$⊢\phi \to {\sum }_T\left(B{\underset{\dot{}}{·}}_{f}G\right)\in C$$