Metamath Proof Explorer

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

Proof

Step Hyp Ref Expression
1 psrbagev1.d 
 |-  D = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin }
2 psrbagev1.c 
 |-  C = ( Base ` T )
3 psrbagev1.x 
 |-  .x. = ( .g ` T )
4 psrbagev1.z 
 |-  .0. = ( 0g ` T )
5 psrbagev1.t 
 |-  ( ph -> T e. CMnd )
6 psrbagev1.b 
 |-  ( ph -> B e. D )
7 psrbagev1.g 
 |-  ( ph -> G : I --> C )
8 5 cmnmndd 
 |-  ( ph -> T e. Mnd )
9 2 3 mulgnn0cl 
 |-  ( ( T e. Mnd /\ y e. NN0 /\ z e. C ) -> ( y .x. z ) e. C )
10 9 3expb 
 |-  ( ( T e. Mnd /\ ( y e. NN0 /\ z e. C ) ) -> ( y .x. z ) e. C )
11 8 10 sylan 
 |-  ( ( ph /\ ( y e. NN0 /\ z e. C ) ) -> ( y .x. z ) e. C )
12 1 psrbagf 
 |-  ( B e. D -> B : I --> NN0 )
13 6 12 syl 
 |-  ( ph -> B : I --> NN0 )
14 13 ffnd 
 |-  ( ph -> B Fn I )
15 6 14 fndmexd 
 |-  ( ph -> I e. _V )
16 inidm 
 |-  ( I i^i I ) = I
17 11 13 7 15 15 16 off 
 |-  ( ph -> ( B oF .x. G ) : I --> C )
18 ovexd 
 |-  ( ph -> ( B oF .x. G ) e. _V )
19 7 ffnd 
 |-  ( ph -> G Fn I )
20 14 19 15 15 offun 
 |-  ( ph -> Fun ( B oF .x. G ) )
21 4 fvexi 
 |-  .0. e. _V
22 21 a1i 
 |-  ( ph -> .0. e. _V )
23 1 psrbagfsupp 
 |-  ( B e. D -> B finSupp 0 )
24 6 23 syl 
 |-  ( ph -> B finSupp 0 )
25 24 fsuppimpd 
 |-  ( ph -> ( B supp 0 ) e. Fin )
26 ssidd 
 |-  ( ph -> ( B supp 0 ) C_ ( B supp 0 ) )
27 2 4 3 mulg0 
 |-  ( z e. C -> ( 0 .x. z ) = .0. )
28 27 adantl 
 |-  ( ( ph /\ z e. C ) -> ( 0 .x. z ) = .0. )
29 c0ex 
 |-  0 e. _V
30 29 a1i 
 |-  ( ph -> 0 e. _V )
31 26 28 13 7 15 30 suppssof1 
 |-  ( ph -> ( ( B oF .x. G ) supp .0. ) C_ ( B supp 0 ) )
32 suppssfifsupp 
 |-  ( ( ( ( B oF .x. G ) e. _V /\ Fun ( B oF .x. G ) /\ .0. e. _V ) /\ ( ( B supp 0 ) e. Fin /\ ( ( B oF .x. G ) supp .0. ) C_ ( B supp 0 ) ) ) -> ( B oF .x. G ) finSupp .0. )
33 18 20 22 25 31 32 syl32anc 
 |-  ( ph -> ( B oF .x. G ) finSupp .0. )
34 17 33 jca 
 |-  ( ph -> ( ( B oF .x. G ) : I --> C /\ ( B oF .x. G ) finSupp .0. ) )