Metamath Proof Explorer

Theorem psmeasurelem

Description: M applied to a disjoint union of subsets of its domain is the sum of M applied to such subset. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypotheses psmeasurelem.x 
|- ( ph -> X e. V )
psmeasurelem.h 
|- ( ph -> H : X --> ( 0 [,] +oo ) )
psmeasurelem.m 
|- M = ( x e. ~P X |-> ( sum^ ` ( H |` x ) ) )
psmeasurelem.mf 
|- ( ph -> M : ~P X --> ( 0 [,] +oo ) )
psmeasurelem.y 
|- ( ph -> Y C_ ~P X )
psmeasurelem.dj 
|- ( ph -> Disj_ y e. Y y )
Assertion psmeasurelem 
|- ( ph -> ( M ` U. Y ) = ( sum^ ` ( M |` Y ) ) )

Proof

Step Hyp Ref Expression
1 psmeasurelem.x 
 |-  ( ph -> X e. V )
2 psmeasurelem.h 
 |-  ( ph -> H : X --> ( 0 [,] +oo ) )
3 psmeasurelem.m 
 |-  M = ( x e. ~P X |-> ( sum^ ` ( H |` x ) ) )
4 psmeasurelem.mf 
 |-  ( ph -> M : ~P X --> ( 0 [,] +oo ) )
5 psmeasurelem.y 
 |-  ( ph -> Y C_ ~P X )
6 psmeasurelem.dj 
 |-  ( ph -> Disj_ y e. Y y )
7 1 pwexd 
 |-  ( ph -> ~P X e. _V )
8 ssexg 
 |-  ( ( Y C_ ~P X /\ ~P X e. _V ) -> Y e. _V )
9 5 7 8 syl2anc 
 |-  ( ph -> Y e. _V )
10 simpr 
 |-  ( ( ph /\ y e. Y ) -> y e. Y )
11 uniiun 
 |-  U. Y = U_ y e. Y y
12 elpwg 
 |-  ( Y e. _V -> ( Y e. ~P ~P X <-> Y C_ ~P X ) )
13 9 12 syl 
 |-  ( ph -> ( Y e. ~P ~P X <-> Y C_ ~P X ) )
14 5 13 mpbird 
 |-  ( ph -> Y e. ~P ~P X )
15 pwpwuni 
 |-  ( Y e. _V -> ( Y e. ~P ~P X <-> U. Y e. ~P X ) )
16 9 15 syl 
 |-  ( ph -> ( Y e. ~P ~P X <-> U. Y e. ~P X ) )
17 14 16 mpbid 
 |-  ( ph -> U. Y e. ~P X )
18 17 elpwid 
 |-  ( ph -> U. Y C_ X )
19 2 18 fssresd 
 |-  ( ph -> ( H |` U. Y ) : U. Y --> ( 0 [,] +oo ) )
20 9 10 11 19 6 sge0iun 
 |-  ( ph -> ( sum^ ` ( H |` U. Y ) ) = ( sum^ ` ( y e. Y |-> ( sum^ ` ( ( H |` U. Y ) |` y ) ) ) ) )
21 reseq2 
 |-  ( x = U. Y -> ( H |` x ) = ( H |` U. Y ) )
22 21 fveq2d 
 |-  ( x = U. Y -> ( sum^ ` ( H |` x ) ) = ( sum^ ` ( H |` U. Y ) ) )
23 fvexd 
 |-  ( ph -> ( sum^ ` ( H |` U. Y ) ) e. _V )
24 3 22 17 23 fvmptd3 
 |-  ( ph -> ( M ` U. Y ) = ( sum^ ` ( H |` U. Y ) ) )
25 4 5 fssresd 
 |-  ( ph -> ( M |` Y ) : Y --> ( 0 [,] +oo ) )
26 25 feqmptd 
 |-  ( ph -> ( M |` Y ) = ( y e. Y |-> ( ( M |` Y ) ` y ) ) )
27 fvres 
 |-  ( y e. Y -> ( ( M |` Y ) ` y ) = ( M ` y ) )
28 10 27 syl 
 |-  ( ( ph /\ y e. Y ) -> ( ( M |` Y ) ` y ) = ( M ` y ) )
29 reseq2 
 |-  ( x = y -> ( H |` x ) = ( H |` y ) )
30 29 fveq2d 
 |-  ( x = y -> ( sum^ ` ( H |` x ) ) = ( sum^ ` ( H |` y ) ) )
31 5 sselda 
 |-  ( ( ph /\ y e. Y ) -> y e. ~P X )
32 fvexd 
 |-  ( ( ph /\ y e. Y ) -> ( sum^ ` ( H |` y ) ) e. _V )
33 3 30 31 32 fvmptd3 
 |-  ( ( ph /\ y e. Y ) -> ( M ` y ) = ( sum^ ` ( H |` y ) ) )
34 elssuni 
 |-  ( y e. Y -> y C_ U. Y )
35 resabs1 
 |-  ( y C_ U. Y -> ( ( H |` U. Y ) |` y ) = ( H |` y ) )
36 34 35 syl 
 |-  ( y e. Y -> ( ( H |` U. Y ) |` y ) = ( H |` y ) )
37 36 eqcomd 
 |-  ( y e. Y -> ( H |` y ) = ( ( H |` U. Y ) |` y ) )
38 37 adantl 
 |-  ( ( ph /\ y e. Y ) -> ( H |` y ) = ( ( H |` U. Y ) |` y ) )
39 38 fveq2d 
 |-  ( ( ph /\ y e. Y ) -> ( sum^ ` ( H |` y ) ) = ( sum^ ` ( ( H |` U. Y ) |` y ) ) )
40 28 33 39 3eqtrd 
 |-  ( ( ph /\ y e. Y ) -> ( ( M |` Y ) ` y ) = ( sum^ ` ( ( H |` U. Y ) |` y ) ) )
41 40 mpteq2dva 
 |-  ( ph -> ( y e. Y |-> ( ( M |` Y ) ` y ) ) = ( y e. Y |-> ( sum^ ` ( ( H |` U. Y ) |` y ) ) ) )
42 26 41 eqtrd 
 |-  ( ph -> ( M |` Y ) = ( y e. Y |-> ( sum^ ` ( ( H |` U. Y ) |` y ) ) ) )
43 42 fveq2d 
 |-  ( ph -> ( sum^ ` ( M |` Y ) ) = ( sum^ ` ( y e. Y |-> ( sum^ ` ( ( H |` U. Y ) |` y ) ) ) ) )
44 20 24 43 3eqtr4d 
 |-  ( ph -> ( M ` U. Y ) = ( sum^ ` ( M |` Y ) ) )