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 ffvelrnd
 |-  ( ( 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 ffvelrnda
 |-  ( ( 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 ffvelrnd
 |-  ( ( ph /\ j e. Y ) -> ( G ` j ) e. S )
54 50 53 ffvelrnd
 |-  ( ( 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 ffvelrnd
 |-  ( ( 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 ) ) )