Metamath Proof Explorer

Theorem meadjiunlem

Description: The sum of nonnegative extended reals, restricted to the range of another function. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypotheses meadjiunlem.f 
|- ( ph -> M e. Meas )
meadjiunlem.3 
|- S = dom M
meadjiunlem.x 
|- ( ph -> X e. V )
meadjiunlem.g 
|- ( ph -> G : X --> S )
meadjiunlem.y 
|- Y = { i e. X | ( G ` i ) =/= (/) }
meadjiunlem.dj 
|- ( ph -> Disj_ i e. X ( G ` i ) )
Assertion meadjiunlem 
|- ( ph -> ( sum^ ` ( M |` ran G ) ) = ( sum^ ` ( M o. G ) ) )

Proof

Step Hyp Ref Expression
1 meadjiunlem.f 
 |-  ( ph -> M e. Meas )
2 meadjiunlem.3 
 |-  S = dom M
3 meadjiunlem.x 
 |-  ( ph -> X e. V )
4 meadjiunlem.g 
 |-  ( ph -> G : X --> S )
5 meadjiunlem.y 
 |-  Y = { i e. X | ( G ` i ) =/= (/) }
6 meadjiunlem.dj 
 |-  ( ph -> Disj_ i e. X ( G ` i ) )
7 nfv 
 |-  F/ k ph
8 4 3 jca 
 |-  ( ph -> ( G : X --> S /\ X e. V ) )
9 fex 
 |-  ( ( G : X --> S /\ X e. V ) -> G e. _V )
10 rnexg 
 |-  ( G e. _V -> ran G e. _V )
11 8 9 10 3syl 
 |-  ( ph -> ran G e. _V )
12 difssd 
 |-  ( ph -> ( ran G \ { (/) } ) C_ ran G )
13 1 2 meaf 
 |-  ( ph -> M : S --> ( 0 [,] +oo ) )
14 13 adantr 
 |-  ( ( ph /\ k e. ( ran G \ { (/) } ) ) -> M : S --> ( 0 [,] +oo ) )
15 4 frnd 
 |-  ( ph -> ran G C_ S )
16 15 adantr 
 |-  ( ( ph /\ k e. ( ran G \ { (/) } ) ) -> ran G C_ S )
17 12 sselda 
 |-  ( ( ph /\ k e. ( ran G \ { (/) } ) ) -> k e. ran G )
18 16 17 sseldd 
 |-  ( ( ph /\ k e. ( ran G \ { (/) } ) ) -> k e. S )
19 14 18 ffvelcdmd 
 |-  ( ( ph /\ k e. ( ran G \ { (/) } ) ) -> ( M ` k ) e. ( 0 [,] +oo ) )
20 simpl 
 |-  ( ( ph /\ k e. ( ran G \ ( ran G \ { (/) } ) ) ) -> ph )
21 id 
 |-  ( k e. ( ran G \ ( ran G \ { (/) } ) ) -> k e. ( ran G \ ( ran G \ { (/) } ) ) )
22 dfin4 
 |-  ( ran G i^i { (/) } ) = ( ran G \ ( ran G \ { (/) } ) )
23 22 eqcomi 
 |-  ( ran G \ ( ran G \ { (/) } ) ) = ( ran G i^i { (/) } )
24 21 23 eleqtrdi 
 |-  ( k e. ( ran G \ ( ran G \ { (/) } ) ) -> k e. ( ran G i^i { (/) } ) )
25 elinel2 
 |-  ( k e. ( ran G i^i { (/) } ) -> k e. { (/) } )
26 elsni 
 |-  ( k e. { (/) } -> k = (/) )
27 25 26 syl 
 |-  ( k e. ( ran G i^i { (/) } ) -> k = (/) )
28 24 27 syl 
 |-  ( k e. ( ran G \ ( ran G \ { (/) } ) ) -> k = (/) )
29 28 adantl 
 |-  ( ( ph /\ k e. ( ran G \ ( ran G \ { (/) } ) ) ) -> k = (/) )
30 simpr 
 |-  ( ( ph /\ k = (/) ) -> k = (/) )
31 30 fveq2d 
 |-  ( ( ph /\ k = (/) ) -> ( M ` k ) = ( M ` (/) ) )
32 1 mea0 
 |-  ( ph -> ( M ` (/) ) = 0 )
33 32 adantr 
 |-  ( ( ph /\ k = (/) ) -> ( M ` (/) ) = 0 )
34 31 33 eqtrd 
 |-  ( ( ph /\ k = (/) ) -> ( M ` k ) = 0 )
35 20 29 34 syl2anc 
 |-  ( ( ph /\ k e. ( ran G \ ( ran G \ { (/) } ) ) ) -> ( M ` k ) = 0 )
36 7 11 12 19 35 sge0ss 
 |-  ( ph -> ( sum^ ` ( k e. ( ran G \ { (/) } ) |-> ( M ` k ) ) ) = ( sum^ ` ( k e. ran G |-> ( M ` k ) ) ) )
37 36 eqcomd 
 |-  ( ph -> ( sum^ ` ( k e. ran G |-> ( M ` k ) ) ) = ( sum^ ` ( k e. ( ran G \ { (/) } ) |-> ( M ` k ) ) ) )
38 13 15 feqresmpt 
 |-  ( ph -> ( M |` ran G ) = ( k e. ran G |-> ( M ` k ) ) )
39 38 fveq2d 
 |-  ( ph -> ( sum^ ` ( M |` ran G ) ) = ( sum^ ` ( k e. ran G |-> ( M ` k ) ) ) )
40 4 ffvelcdmda 
 |-  ( ( ph /\ j e. X ) -> ( G ` j ) e. S )
41 4 feqmptd 
 |-  ( ph -> G = ( j e. X |-> ( G ` j ) ) )
42 13 feqmptd 
 |-  ( ph -> M = ( k e. S |-> ( M ` k ) ) )
43 fveq2 
 |-  ( k = ( G ` j ) -> ( M ` k ) = ( M ` ( G ` j ) ) )
44 40 41 42 43 fmptco 
 |-  ( ph -> ( M o. G ) = ( j e. X |-> ( M ` ( G ` j ) ) ) )
45 44 fveq2d 
 |-  ( ph -> ( sum^ ` ( M o. G ) ) = ( sum^ ` ( j e. X |-> ( M ` ( G ` j ) ) ) ) )
46 nfv 
 |-  F/ j ph
47 ssrab2 
 |-  { i e. X | ( G ` i ) =/= (/) } C_ X
48 47 a1i 
 |-  ( ph -> { i e. X | ( G ` i ) =/= (/) } C_ X )
49 5 48 eqsstrid 
 |-  ( ph -> Y C_ X )
50 13 adantr 
 |-  ( ( ph /\ j e. Y ) -> M : S --> ( 0 [,] +oo ) )
51 4 adantr 
 |-  ( ( ph /\ j e. Y ) -> G : X --> S )
52 49 sselda 
 |-  ( ( ph /\ j e. Y ) -> j e. X )
53 51 52 ffvelcdmd 
 |-  ( ( ph /\ j e. Y ) -> ( G ` j ) e. S )
54 50 53 ffvelcdmd 
 |-  ( ( ph /\ j e. Y ) -> ( M ` ( G ` j ) ) e. ( 0 [,] +oo ) )
55 eldifi 
 |-  ( j e. ( X \ Y ) -> j e. X )
56 55 ad2antlr 
 |-  ( ( ( ph /\ j e. ( X \ Y ) ) /\ ( M ` ( G ` j ) ) =/= 0 ) -> j e. X )
57 fveq2 
 |-  ( ( G ` j ) = (/) -> ( M ` ( G ` j ) ) = ( M ` (/) ) )
58 57 adantl 
 |-  ( ( ph /\ ( G ` j ) = (/) ) -> ( M ` ( G ` j ) ) = ( M ` (/) ) )
59 1 adantr 
 |-  ( ( ph /\ ( G ` j ) = (/) ) -> M e. Meas )
60 59 mea0 
 |-  ( ( ph /\ ( G ` j ) = (/) ) -> ( M ` (/) ) = 0 )
61 58 60 eqtrd 
 |-  ( ( ph /\ ( G ` j ) = (/) ) -> ( M ` ( G ` j ) ) = 0 )
62 61 ad4ant14 
 |-  ( ( ( ( ph /\ j e. ( X \ Y ) ) /\ ( M ` ( G ` j ) ) =/= 0 ) /\ ( G ` j ) = (/) ) -> ( M ` ( G ` j ) ) = 0 )
63 neneq 
 |-  ( ( M ` ( G ` j ) ) =/= 0 -> -. ( M ` ( G ` j ) ) = 0 )
64 63 ad2antlr 
 |-  ( ( ( ( ph /\ j e. ( X \ Y ) ) /\ ( M ` ( G ` j ) ) =/= 0 ) /\ ( G ` j ) = (/) ) -> -. ( M ` ( G ` j ) ) = 0 )
65 62 64 pm2.65da 
 |-  ( ( ( ph /\ j e. ( X \ Y ) ) /\ ( M ` ( G ` j ) ) =/= 0 ) -> -. ( G ` j ) = (/) )
66 65 neqned 
 |-  ( ( ( ph /\ j e. ( X \ Y ) ) /\ ( M ` ( G ` j ) ) =/= 0 ) -> ( G ` j ) =/= (/) )
67 56 66 jca 
 |-  ( ( ( ph /\ j e. ( X \ Y ) ) /\ ( M ` ( G ` j ) ) =/= 0 ) -> ( j e. X /\ ( G ` j ) =/= (/) ) )
68 fveq2 
 |-  ( i = j -> ( G ` i ) = ( G ` j ) )
69 68 neeq1d 
 |-  ( i = j -> ( ( G ` i ) =/= (/) <-> ( G ` j ) =/= (/) ) )
70 69 elrab 
 |-  ( j e. { i e. X | ( G ` i ) =/= (/) } <-> ( j e. X /\ ( G ` j ) =/= (/) ) )
71 67 70 sylibr 
 |-  ( ( ( ph /\ j e. ( X \ Y ) ) /\ ( M ` ( G ` j ) ) =/= 0 ) -> j e. { i e. X | ( G ` i ) =/= (/) } )
72 71 5 eleqtrrdi 
 |-  ( ( ( ph /\ j e. ( X \ Y ) ) /\ ( M ` ( G ` j ) ) =/= 0 ) -> j e. Y )
73 eldifn 
 |-  ( j e. ( X \ Y ) -> -. j e. Y )
74 73 ad2antlr 
 |-  ( ( ( ph /\ j e. ( X \ Y ) ) /\ ( M ` ( G ` j ) ) =/= 0 ) -> -. j e. Y )
75 72 74 pm2.65da 
 |-  ( ( ph /\ j e. ( X \ Y ) ) -> -. ( M ` ( G ` j ) ) =/= 0 )
76 nne 
 |-  ( -. ( M ` ( G ` j ) ) =/= 0 <-> ( M ` ( G ` j ) ) = 0 )
77 75 76 sylib 
 |-  ( ( ph /\ j e. ( X \ Y ) ) -> ( M ` ( G ` j ) ) = 0 )
78 46 3 49 54 77 sge0ss 
 |-  ( ph -> ( sum^ ` ( j e. Y |-> ( M ` ( G ` j ) ) ) ) = ( sum^ ` ( j e. X |-> ( M ` ( G ` j ) ) ) ) )
79 78 eqcomd 
 |-  ( ph -> ( sum^ ` ( j e. X |-> ( M ` ( G ` j ) ) ) ) = ( sum^ ` ( j e. Y |-> ( M ` ( G ` j ) ) ) ) )
80 3 49 ssexd 
 |-  ( ph -> Y e. _V )
81 nfv 
 |-  F/ i ph
82 eqid 
 |-  ( i e. Y |-> ( G ` i ) ) = ( i e. Y |-> ( G ` i ) )
83 4 ffnd 
 |-  ( ph -> G Fn X )
84 dffn3 
 |-  ( G Fn X <-> G : X --> ran G )
85 83 84 sylib 
 |-  ( ph -> G : X --> ran G )
86 85 adantr 
 |-  ( ( ph /\ i e. Y ) -> G : X --> ran G )
87 49 sselda 
 |-  ( ( ph /\ i e. Y ) -> i e. X )
88 86 87 ffvelcdmd 
 |-  ( ( ph /\ i e. Y ) -> ( G ` i ) e. ran G )
89 5 eleq2i 
 |-  ( i e. Y <-> i e. { i e. X | ( G ` i ) =/= (/) } )
90 rabid 
 |-  ( i e. { i e. X | ( G ` i ) =/= (/) } <-> ( i e. X /\ ( G ` i ) =/= (/) ) )
91 89 90 bitri 
 |-  ( i e. Y <-> ( i e. X /\ ( G ` i ) =/= (/) ) )
92 91 biimpi 
 |-  ( i e. Y -> ( i e. X /\ ( G ` i ) =/= (/) ) )
93 92 simprd 
 |-  ( i e. Y -> ( G ` i ) =/= (/) )
94 93 adantl 
 |-  ( ( ph /\ i e. Y ) -> ( G ` i ) =/= (/) )
95 nelsn 
 |-  ( ( G ` i ) =/= (/) -> -. ( G ` i ) e. { (/) } )
96 94 95 syl 
 |-  ( ( ph /\ i e. Y ) -> -. ( G ` i ) e. { (/) } )
97 88 96 eldifd 
 |-  ( ( ph /\ i e. Y ) -> ( G ` i ) e. ( ran G \ { (/) } ) )
98 disjss1 
 |-  ( Y C_ X -> ( Disj_ i e. X ( G ` i ) -> Disj_ i e. Y ( G ` i ) ) )
99 49 6 98 sylc 
 |-  ( ph -> Disj_ i e. Y ( G ` i ) )
100 81 82 97 94 99 disjf1 
 |-  ( ph -> ( i e. Y |-> ( G ` i ) ) : Y -1-1-> ( ran G \ { (/) } ) )
101 4 49 feqresmpt 
 |-  ( ph -> ( G |` Y ) = ( i e. Y |-> ( G ` i ) ) )
102 f1eq1 
 |-  ( ( G |` Y ) = ( i e. Y |-> ( G ` i ) ) -> ( ( G |` Y ) : Y -1-1-> ( ran G \ { (/) } ) <-> ( i e. Y |-> ( G ` i ) ) : Y -1-1-> ( ran G \ { (/) } ) ) )
103 101 102 syl 
 |-  ( ph -> ( ( G |` Y ) : Y -1-1-> ( ran G \ { (/) } ) <-> ( i e. Y |-> ( G ` i ) ) : Y -1-1-> ( ran G \ { (/) } ) ) )
104 100 103 mpbird 
 |-  ( ph -> ( G |` Y ) : Y -1-1-> ( ran G \ { (/) } ) )
105 101 rneqd 
 |-  ( ph -> ran ( G |` Y ) = ran ( i e. Y |-> ( G ` i ) ) )
106 97 ralrimiva 
 |-  ( ph -> A. i e. Y ( G ` i ) e. ( ran G \ { (/) } ) )
107 82 rnmptss 
 |-  ( A. i e. Y ( G ` i ) e. ( ran G \ { (/) } ) -> ran ( i e. Y |-> ( G ` i ) ) C_ ( ran G \ { (/) } ) )
108 106 107 syl 
 |-  ( ph -> ran ( i e. Y |-> ( G ` i ) ) C_ ( ran G \ { (/) } ) )
109 105 108 eqsstrd 
 |-  ( ph -> ran ( G |` Y ) C_ ( ran G \ { (/) } ) )
110 simpl 
 |-  ( ( ph /\ x e. ( ran G \ { (/) } ) ) -> ph )
111 eldifi 
 |-  ( x e. ( ran G \ { (/) } ) -> x e. ran G )
112 111 adantl 
 |-  ( ( ph /\ x e. ( ran G \ { (/) } ) ) -> x e. ran G )
113 eldifsni 
 |-  ( x e. ( ran G \ { (/) } ) -> x =/= (/) )
114 113 adantl 
 |-  ( ( ph /\ x e. ( ran G \ { (/) } ) ) -> x =/= (/) )
115 simpr 
 |-  ( ( ph /\ x e. ran G ) -> x e. ran G )
116 fvelrnb 
 |-  ( G Fn X -> ( x e. ran G <-> E. i e. X ( G ` i ) = x ) )
117 83 116 syl 
 |-  ( ph -> ( x e. ran G <-> E. i e. X ( G ` i ) = x ) )
118 117 adantr 
 |-  ( ( ph /\ x e. ran G ) -> ( x e. ran G <-> E. i e. X ( G ` i ) = x ) )
119 115 118 mpbid 
 |-  ( ( ph /\ x e. ran G ) -> E. i e. X ( G ` i ) = x )
120 119 3adant3 
 |-  ( ( ph /\ x e. ran G /\ x =/= (/) ) -> E. i e. X ( G ` i ) = x )
121 id 
 |-  ( ( G ` i ) = x -> ( G ` i ) = x )
122 121 eqcomd 
 |-  ( ( G ` i ) = x -> x = ( G ` i ) )
123 122 3ad2ant3 
 |-  ( ( ( ph /\ x =/= (/) ) /\ i e. X /\ ( G ` i ) = x ) -> x = ( G ` i ) )
124 simp1l 
 |-  ( ( ( ph /\ x =/= (/) ) /\ i e. X /\ ( G ` i ) = x ) -> ph )
125 simp2 
 |-  ( ( ( ph /\ x =/= (/) ) /\ i e. X /\ ( G ` i ) = x ) -> i e. X )
126 simpr 
 |-  ( ( x =/= (/) /\ ( G ` i ) = x ) -> ( G ` i ) = x )
127 simpl 
 |-  ( ( x =/= (/) /\ ( G ` i ) = x ) -> x =/= (/) )
128 126 127 eqnetrd 
 |-  ( ( x =/= (/) /\ ( G ` i ) = x ) -> ( G ` i ) =/= (/) )
129 128 adantll 
 |-  ( ( ( ph /\ x =/= (/) ) /\ ( G ` i ) = x ) -> ( G ` i ) =/= (/) )
130 129 3adant2 
 |-  ( ( ( ph /\ x =/= (/) ) /\ i e. X /\ ( G ` i ) = x ) -> ( G ` i ) =/= (/) )
131 91 biimpri 
 |-  ( ( i e. X /\ ( G ` i ) =/= (/) ) -> i e. Y )
132 fvexd 
 |-  ( ( i e. X /\ ( G ` i ) =/= (/) ) -> ( G ` i ) e. _V )
133 82 elrnmpt1 
 |-  ( ( i e. Y /\ ( G ` i ) e. _V ) -> ( G ` i ) e. ran ( i e. Y |-> ( G ` i ) ) )
134 131 132 133 syl2anc 
 |-  ( ( i e. X /\ ( G ` i ) =/= (/) ) -> ( G ` i ) e. ran ( i e. Y |-> ( G ` i ) ) )
135 134 3adant1 
 |-  ( ( ph /\ i e. X /\ ( G ` i ) =/= (/) ) -> ( G ` i ) e. ran ( i e. Y |-> ( G ` i ) ) )
136 105 eqcomd 
 |-  ( ph -> ran ( i e. Y |-> ( G ` i ) ) = ran ( G |` Y ) )
137 136 3ad2ant1 
 |-  ( ( ph /\ i e. X /\ ( G ` i ) =/= (/) ) -> ran ( i e. Y |-> ( G ` i ) ) = ran ( G |` Y ) )
138 135 137 eleqtrd 
 |-  ( ( ph /\ i e. X /\ ( G ` i ) =/= (/) ) -> ( G ` i ) e. ran ( G |` Y ) )
139 124 125 130 138 syl3anc 
 |-  ( ( ( ph /\ x =/= (/) ) /\ i e. X /\ ( G ` i ) = x ) -> ( G ` i ) e. ran ( G |` Y ) )
140 123 139 eqeltrd 
 |-  ( ( ( ph /\ x =/= (/) ) /\ i e. X /\ ( G ` i ) = x ) -> x e. ran ( G |` Y ) )
141 140 3exp 
 |-  ( ( ph /\ x =/= (/) ) -> ( i e. X -> ( ( G ` i ) = x -> x e. ran ( G |` Y ) ) ) )
142 141 rexlimdv 
 |-  ( ( ph /\ x =/= (/) ) -> ( E. i e. X ( G ` i ) = x -> x e. ran ( G |` Y ) ) )
143 142 3adant2 
 |-  ( ( ph /\ x e. ran G /\ x =/= (/) ) -> ( E. i e. X ( G ` i ) = x -> x e. ran ( G |` Y ) ) )
144 120 143 mpd 
 |-  ( ( ph /\ x e. ran G /\ x =/= (/) ) -> x e. ran ( G |` Y ) )
145 110 112 114 144 syl3anc 
 |-  ( ( ph /\ x e. ( ran G \ { (/) } ) ) -> x e. ran ( G |` Y ) )
146 109 145 eqelssd 
 |-  ( ph -> ran ( G |` Y ) = ( ran G \ { (/) } ) )
147 104 146 jca 
 |-  ( ph -> ( ( G |` Y ) : Y -1-1-> ( ran G \ { (/) } ) /\ ran ( G |` Y ) = ( ran G \ { (/) } ) ) )
148 dff1o5 
 |-  ( ( G |` Y ) : Y -1-1-onto-> ( ran G \ { (/) } ) <-> ( ( G |` Y ) : Y -1-1-> ( ran G \ { (/) } ) /\ ran ( G |` Y ) = ( ran G \ { (/) } ) ) )
149 147 148 sylibr 
 |-  ( ph -> ( G |` Y ) : Y -1-1-onto-> ( ran G \ { (/) } ) )
150 fvres 
 |-  ( j e. Y -> ( ( G |` Y ) ` j ) = ( G ` j ) )
151 150 adantl 
 |-  ( ( ph /\ j e. Y ) -> ( ( G |` Y ) ` j ) = ( G ` j ) )
152 7 46 43 80 149 151 19 sge0f1o 
 |-  ( ph -> ( sum^ ` ( k e. ( ran G \ { (/) } ) |-> ( M ` k ) ) ) = ( sum^ ` ( j e. Y |-> ( M ` ( G ` j ) ) ) ) )
153 152 eqcomd 
 |-  ( ph -> ( sum^ ` ( j e. Y |-> ( M ` ( G ` j ) ) ) ) = ( sum^ ` ( k e. ( ran G \ { (/) } ) |-> ( M ` k ) ) ) )
154 45 79 153 3eqtrd 
 |-  ( ph -> ( sum^ ` ( M o. G ) ) = ( sum^ ` ( k e. ( ran G \ { (/) } ) |-> ( M ` k ) ) ) )
155 37 39 154 3eqtr4d 
 |-  ( ph -> ( sum^ ` ( M |` ran G ) ) = ( sum^ ` ( M o. G ) ) )