This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )