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 φ M Meas
meadjiunlem.3 S = dom M
meadjiunlem.x φ X V
meadjiunlem.g φ G : X S
meadjiunlem.y Y = i X | G i
meadjiunlem.dj φ Disj i X G i
Assertion meadjiunlem φ sum^ M ran G = sum^ M G

Proof

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