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 ) |
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 ) |