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 = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin }
	psrbagev2.c	|- C = ( Base ` T )
	psrbagev2.x	|- .x. = ( .g ` T )
	psrbagev2.t	|- ( ph -> T e. CMnd )
	psrbagev2.b	|- ( ph -> B e. D )
	psrbagev2.g	|- ( ph -> G : I --> C )
Assertion	psrbagev2	|- ( ph -> ( T gsum ( B oF .x. G ) ) e. C )

Proof

Step	Hyp	Ref	Expression
1		psrbagev2.d	|- D = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin }
2		psrbagev2.c	|- C = ( Base ` T )
3		psrbagev2.x	|- .x. = ( .g ` T )
4		psrbagev2.t	|- ( ph -> T e. CMnd )
5		psrbagev2.b	|- ( ph -> B e. D )
6		psrbagev2.g	|- ( ph -> G : I --> C )
7		eqid	|- ( 0g ` T ) = ( 0g ` T )
8		ovexd	|- ( ph -> ( B oF .x. G ) e. _V )
9	1 2 3 7 4 5 6	psrbagev1	|- ( ph -> ( ( B oF .x. G ) : I --> C /\ ( B oF .x. G ) finSupp ( 0g ` T ) ) )
10	9	simpld	|- ( ph -> ( B oF .x. G ) : I --> C )
11	10	ffnd	|- ( ph -> ( B oF .x. G ) Fn I )
12	8 11	fndmexd	|- ( ph -> I e. _V )
13	9	simprd	|- ( ph -> ( B oF .x. G ) finSupp ( 0g ` T ) )
14	2 7 4 12 10 13	gsumcl	|- ( ph -> ( T gsum ( B oF .x. G ) ) e. C )