Metamath Proof Explorer


Theorem mbfposadd

Description: If the sum of two measurable functions is measurable, the sum of their nonnegative parts is measurable. (Contributed by Brendan Leahy, 2-Apr-2018)

Ref Expression
Hypotheses mbfposadd.1 φ x A B MblFn
mbfposadd.2 φ x A B
mbfposadd.3 φ x A C MblFn
mbfposadd.4 φ x A C
mbfposadd.5 φ x A B + C MblFn
Assertion mbfposadd φ x A if 0 B B 0 + if 0 C C 0 MblFn

Proof

Step Hyp Ref Expression
1 mbfposadd.1 φ x A B MblFn
2 mbfposadd.2 φ x A B
3 mbfposadd.3 φ x A C MblFn
4 mbfposadd.4 φ x A C
5 mbfposadd.5 φ x A B + C MblFn
6 0re 0
7 ifcl B 0 if 0 B B 0
8 2 6 7 sylancl φ x A if 0 B B 0
9 ifcl C 0 if 0 C C 0
10 4 6 9 sylancl φ x A if 0 C C 0
11 8 10 readdcld φ x A if 0 B B 0 + if 0 C C 0
12 11 fmpttd φ x A if 0 B B 0 + if 0 C C 0 : A
13 ssrab2 x A | 0 C A
14 fssres x A if 0 B B 0 + if 0 C C 0 : A x A | 0 C A x A if 0 B B 0 + if 0 C C 0 x A | 0 C : x A | 0 C
15 12 13 14 sylancl φ x A if 0 B B 0 + if 0 C C 0 x A | 0 C : x A | 0 C
16 inss2 x A | 0 B x A | 0 C x A | 0 C
17 resabs1 x A | 0 B x A | 0 C x A | 0 C x A if 0 B B 0 + if 0 C C 0 x A | 0 C x A | 0 B x A | 0 C = x A if 0 B B 0 + if 0 C C 0 x A | 0 B x A | 0 C
18 16 17 ax-mp x A if 0 B B 0 + if 0 C C 0 x A | 0 C x A | 0 B x A | 0 C = x A if 0 B B 0 + if 0 C C 0 x A | 0 B x A | 0 C
19 elin x x A | 0 B x A | 0 C x x A | 0 B x x A | 0 C
20 rabid x x A | 0 B x A 0 B
21 rabid x x A | 0 C x A 0 C
22 20 21 anbi12i x x A | 0 B x x A | 0 C x A 0 B x A 0 C
23 19 22 bitri x x A | 0 B x A | 0 C x A 0 B x A 0 C
24 iftrue 0 B if 0 B B 0 = B
25 iftrue 0 C if 0 C C 0 = C
26 24 25 oveqan12d 0 B 0 C if 0 B B 0 + if 0 C C 0 = B + C
27 26 ad2ant2l x A 0 B x A 0 C if 0 B B 0 + if 0 C C 0 = B + C
28 23 27 sylbi x x A | 0 B x A | 0 C if 0 B B 0 + if 0 C C 0 = B + C
29 28 mpteq2ia x x A | 0 B x A | 0 C if 0 B B 0 + if 0 C C 0 = x x A | 0 B x A | 0 C B + C
30 inss1 x A | 0 B x A | 0 C x A | 0 B
31 ssrab2 x A | 0 B A
32 30 31 sstri x A | 0 B x A | 0 C A
33 resmpt x A | 0 B x A | 0 C A y A y / x if 0 B B 0 + if 0 C C 0 x A | 0 B x A | 0 C = y x A | 0 B x A | 0 C y / x if 0 B B 0 + if 0 C C 0
34 nfcv _ y if 0 B B 0 + if 0 C C 0
35 nfcsb1v _ x y / x if 0 B B 0 + if 0 C C 0
36 csbeq1a x = y if 0 B B 0 + if 0 C C 0 = y / x if 0 B B 0 + if 0 C C 0
37 34 35 36 cbvmpt x A if 0 B B 0 + if 0 C C 0 = y A y / x if 0 B B 0 + if 0 C C 0
38 37 reseq1i x A if 0 B B 0 + if 0 C C 0 x A | 0 B x A | 0 C = y A y / x if 0 B B 0 + if 0 C C 0 x A | 0 B x A | 0 C
39 nfv y x x A | 0 B x A | 0 C z = if 0 B B 0 + if 0 C C 0
40 nfrab1 _ x x A | 0 B
41 nfrab1 _ x x A | 0 C
42 40 41 nfin _ x x A | 0 B x A | 0 C
43 42 nfcri x y x A | 0 B x A | 0 C
44 35 nfeq2 x z = y / x if 0 B B 0 + if 0 C C 0
45 43 44 nfan x y x A | 0 B x A | 0 C z = y / x if 0 B B 0 + if 0 C C 0
46 eleq1w x = y x x A | 0 B x A | 0 C y x A | 0 B x A | 0 C
47 36 eqeq2d x = y z = if 0 B B 0 + if 0 C C 0 z = y / x if 0 B B 0 + if 0 C C 0
48 46 47 anbi12d x = y x x A | 0 B x A | 0 C z = if 0 B B 0 + if 0 C C 0 y x A | 0 B x A | 0 C z = y / x if 0 B B 0 + if 0 C C 0
49 39 45 48 cbvopab1 x z | x x A | 0 B x A | 0 C z = if 0 B B 0 + if 0 C C 0 = y z | y x A | 0 B x A | 0 C z = y / x if 0 B B 0 + if 0 C C 0
50 df-mpt x x A | 0 B x A | 0 C if 0 B B 0 + if 0 C C 0 = x z | x x A | 0 B x A | 0 C z = if 0 B B 0 + if 0 C C 0
51 df-mpt y x A | 0 B x A | 0 C y / x if 0 B B 0 + if 0 C C 0 = y z | y x A | 0 B x A | 0 C z = y / x if 0 B B 0 + if 0 C C 0
52 49 50 51 3eqtr4i x x A | 0 B x A | 0 C if 0 B B 0 + if 0 C C 0 = y x A | 0 B x A | 0 C y / x if 0 B B 0 + if 0 C C 0
53 33 38 52 3eqtr4g x A | 0 B x A | 0 C A x A if 0 B B 0 + if 0 C C 0 x A | 0 B x A | 0 C = x x A | 0 B x A | 0 C if 0 B B 0 + if 0 C C 0
54 32 53 ax-mp x A if 0 B B 0 + if 0 C C 0 x A | 0 B x A | 0 C = x x A | 0 B x A | 0 C if 0 B B 0 + if 0 C C 0
55 resmpt x A | 0 B x A | 0 C A y A y / x B + C x A | 0 B x A | 0 C = y x A | 0 B x A | 0 C y / x B + C
56 nfcv _ y B + C
57 nfcsb1v _ x y / x B + C
58 csbeq1a x = y B + C = y / x B + C
59 56 57 58 cbvmpt x A B + C = y A y / x B + C
60 59 reseq1i x A B + C x A | 0 B x A | 0 C = y A y / x B + C x A | 0 B x A | 0 C
61 nfv y x x A | 0 B x A | 0 C z = B + C
62 57 nfeq2 x z = y / x B + C
63 43 62 nfan x y x A | 0 B x A | 0 C z = y / x B + C
64 58 eqeq2d x = y z = B + C z = y / x B + C
65 46 64 anbi12d x = y x x A | 0 B x A | 0 C z = B + C y x A | 0 B x A | 0 C z = y / x B + C
66 61 63 65 cbvopab1 x z | x x A | 0 B x A | 0 C z = B + C = y z | y x A | 0 B x A | 0 C z = y / x B + C
67 df-mpt x x A | 0 B x A | 0 C B + C = x z | x x A | 0 B x A | 0 C z = B + C
68 df-mpt y x A | 0 B x A | 0 C y / x B + C = y z | y x A | 0 B x A | 0 C z = y / x B + C
69 66 67 68 3eqtr4i x x A | 0 B x A | 0 C B + C = y x A | 0 B x A | 0 C y / x B + C
70 55 60 69 3eqtr4g x A | 0 B x A | 0 C A x A B + C x A | 0 B x A | 0 C = x x A | 0 B x A | 0 C B + C
71 32 70 ax-mp x A B + C x A | 0 B x A | 0 C = x x A | 0 B x A | 0 C B + C
72 29 54 71 3eqtr4i x A if 0 B B 0 + if 0 C C 0 x A | 0 B x A | 0 C = x A B + C x A | 0 B x A | 0 C
73 18 72 eqtri x A if 0 B B 0 + if 0 C C 0 x A | 0 C x A | 0 B x A | 0 C = x A B + C x A | 0 B x A | 0 C
74 2 biantrurd φ x A 0 B B 0 B
75 elrege0 B 0 +∞ B 0 B
76 74 75 bitr4di φ x A 0 B B 0 +∞
77 76 rabbidva φ x A | 0 B = x A | B 0 +∞
78 0xr 0 *
79 pnfxr +∞ *
80 0ltpnf 0 < +∞
81 snunioo 0 * +∞ * 0 < +∞ 0 0 +∞ = 0 +∞
82 78 79 80 81 mp3an 0 0 +∞ = 0 +∞
83 82 imaeq2i x A B -1 0 0 +∞ = x A B -1 0 +∞
84 imaundi x A B -1 0 0 +∞ = x A B -1 0 x A B -1 0 +∞
85 eqid x A B = x A B
86 85 mptpreima x A B -1 0 +∞ = x A | B 0 +∞
87 83 84 86 3eqtr3ri x A | B 0 +∞ = x A B -1 0 x A B -1 0 +∞
88 77 87 eqtrdi φ x A | 0 B = x A B -1 0 x A B -1 0 +∞
89 2 fmpttd φ x A B : A
90 mbfimasn x A B MblFn x A B : A 0 x A B -1 0 dom vol
91 6 90 mp3an3 x A B MblFn x A B : A x A B -1 0 dom vol
92 mbfima x A B MblFn x A B : A x A B -1 0 +∞ dom vol
93 unmbl x A B -1 0 dom vol x A B -1 0 +∞ dom vol x A B -1 0 x A B -1 0 +∞ dom vol
94 91 92 93 syl2anc x A B MblFn x A B : A x A B -1 0 x A B -1 0 +∞ dom vol
95 1 89 94 syl2anc φ x A B -1 0 x A B -1 0 +∞ dom vol
96 88 95 eqeltrd φ x A | 0 B dom vol
97 4 biantrurd φ x A 0 C C 0 C
98 elrege0 C 0 +∞ C 0 C
99 97 98 bitr4di φ x A 0 C C 0 +∞
100 99 rabbidva φ x A | 0 C = x A | C 0 +∞
101 82 imaeq2i x A C -1 0 0 +∞ = x A C -1 0 +∞
102 imaundi x A C -1 0 0 +∞ = x A C -1 0 x A C -1 0 +∞
103 eqid x A C = x A C
104 103 mptpreima x A C -1 0 +∞ = x A | C 0 +∞
105 101 102 104 3eqtr3ri x A | C 0 +∞ = x A C -1 0 x A C -1 0 +∞
106 100 105 eqtrdi φ x A | 0 C = x A C -1 0 x A C -1 0 +∞
107 4 fmpttd φ x A C : A
108 mbfimasn x A C MblFn x A C : A 0 x A C -1 0 dom vol
109 6 108 mp3an3 x A C MblFn x A C : A x A C -1 0 dom vol
110 mbfima x A C MblFn x A C : A x A C -1 0 +∞ dom vol
111 unmbl x A C -1 0 dom vol x A C -1 0 +∞ dom vol x A C -1 0 x A C -1 0 +∞ dom vol
112 109 110 111 syl2anc x A C MblFn x A C : A x A C -1 0 x A C -1 0 +∞ dom vol
113 3 107 112 syl2anc φ x A C -1 0 x A C -1 0 +∞ dom vol
114 106 113 eqeltrd φ x A | 0 C dom vol
115 inmbl x A | 0 B dom vol x A | 0 C dom vol x A | 0 B x A | 0 C dom vol
116 96 114 115 syl2anc φ x A | 0 B x A | 0 C dom vol
117 mbfres x A B + C MblFn x A | 0 B x A | 0 C dom vol x A B + C x A | 0 B x A | 0 C MblFn
118 5 116 117 syl2anc φ x A B + C x A | 0 B x A | 0 C MblFn
119 73 118 eqeltrid φ x A if 0 B B 0 + if 0 C C 0 x A | 0 C x A | 0 B x A | 0 C MblFn
120 inss2 x A | ¬ 0 B x A | 0 C x A | 0 C
121 resabs1 x A | ¬ 0 B x A | 0 C x A | 0 C x A if 0 B B 0 + if 0 C C 0 x A | 0 C x A | ¬ 0 B x A | 0 C = x A if 0 B B 0 + if 0 C C 0 x A | ¬ 0 B x A | 0 C
122 120 121 ax-mp x A if 0 B B 0 + if 0 C C 0 x A | 0 C x A | ¬ 0 B x A | 0 C = x A if 0 B B 0 + if 0 C C 0 x A | ¬ 0 B x A | 0 C
123 rabid x x A | ¬ 0 B x A ¬ 0 B
124 123 21 anbi12i x x A | ¬ 0 B x x A | 0 C x A ¬ 0 B x A 0 C
125 elin x x A | ¬ 0 B x A | 0 C x x A | ¬ 0 B x x A | 0 C
126 anandi x A ¬ 0 B 0 C x A ¬ 0 B x A 0 C
127 124 125 126 3bitr4i x x A | ¬ 0 B x A | 0 C x A ¬ 0 B 0 C
128 iffalse ¬ 0 B if 0 B B 0 = 0
129 128 25 oveqan12d ¬ 0 B 0 C if 0 B B 0 + if 0 C C 0 = 0 + C
130 129 ad2antll φ x A ¬ 0 B 0 C if 0 B B 0 + if 0 C C 0 = 0 + C
131 4 recnd φ x A C
132 131 addid2d φ x A 0 + C = C
133 132 adantrr φ x A ¬ 0 B 0 C 0 + C = C
134 130 133 eqtrd φ x A ¬ 0 B 0 C if 0 B B 0 + if 0 C C 0 = C
135 127 134 sylan2b φ x x A | ¬ 0 B x A | 0 C if 0 B B 0 + if 0 C C 0 = C
136 135 mpteq2dva φ x x A | ¬ 0 B x A | 0 C if 0 B B 0 + if 0 C C 0 = x x A | ¬ 0 B x A | 0 C C
137 inss1 x A | ¬ 0 B x A | 0 C x A | ¬ 0 B
138 ssrab2 x A | ¬ 0 B A
139 137 138 sstri x A | ¬ 0 B x A | 0 C A
140 resmpt x A | ¬ 0 B x A | 0 C A y A y / x if 0 B B 0 + if 0 C C 0 x A | ¬ 0 B x A | 0 C = y x A | ¬ 0 B x A | 0 C y / x if 0 B B 0 + if 0 C C 0
141 37 reseq1i x A if 0 B B 0 + if 0 C C 0 x A | ¬ 0 B x A | 0 C = y A y / x if 0 B B 0 + if 0 C C 0 x A | ¬ 0 B x A | 0 C
142 nfv y x x A | ¬ 0 B x A | 0 C z = if 0 B B 0 + if 0 C C 0
143 nfrab1 _ x x A | ¬ 0 B
144 143 41 nfin _ x x A | ¬ 0 B x A | 0 C
145 144 nfcri x y x A | ¬ 0 B x A | 0 C
146 145 44 nfan x y x A | ¬ 0 B x A | 0 C z = y / x if 0 B B 0 + if 0 C C 0
147 eleq1w x = y x x A | ¬ 0 B x A | 0 C y x A | ¬ 0 B x A | 0 C
148 147 47 anbi12d x = y x x A | ¬ 0 B x A | 0 C z = if 0 B B 0 + if 0 C C 0 y x A | ¬ 0 B x A | 0 C z = y / x if 0 B B 0 + if 0 C C 0
149 142 146 148 cbvopab1 x z | x x A | ¬ 0 B x A | 0 C z = if 0 B B 0 + if 0 C C 0 = y z | y x A | ¬ 0 B x A | 0 C z = y / x if 0 B B 0 + if 0 C C 0
150 df-mpt x x A | ¬ 0 B x A | 0 C if 0 B B 0 + if 0 C C 0 = x z | x x A | ¬ 0 B x A | 0 C z = if 0 B B 0 + if 0 C C 0
151 df-mpt y x A | ¬ 0 B x A | 0 C y / x if 0 B B 0 + if 0 C C 0 = y z | y x A | ¬ 0 B x A | 0 C z = y / x if 0 B B 0 + if 0 C C 0
152 149 150 151 3eqtr4i x x A | ¬ 0 B x A | 0 C if 0 B B 0 + if 0 C C 0 = y x A | ¬ 0 B x A | 0 C y / x if 0 B B 0 + if 0 C C 0
153 140 141 152 3eqtr4g x A | ¬ 0 B x A | 0 C A x A if 0 B B 0 + if 0 C C 0 x A | ¬ 0 B x A | 0 C = x x A | ¬ 0 B x A | 0 C if 0 B B 0 + if 0 C C 0
154 139 153 ax-mp x A if 0 B B 0 + if 0 C C 0 x A | ¬ 0 B x A | 0 C = x x A | ¬ 0 B x A | 0 C if 0 B B 0 + if 0 C C 0
155 resmpt x A | ¬ 0 B x A | 0 C A y A y / x C x A | ¬ 0 B x A | 0 C = y x A | ¬ 0 B x A | 0 C y / x C
156 nfcv _ y C
157 nfcsb1v _ x y / x C
158 csbeq1a x = y C = y / x C
159 156 157 158 cbvmpt x A C = y A y / x C
160 159 reseq1i x A C x A | ¬ 0 B x A | 0 C = y A y / x C x A | ¬ 0 B x A | 0 C
161 nfv y x x A | ¬ 0 B x A | 0 C z = C
162 157 nfeq2 x z = y / x C
163 145 162 nfan x y x A | ¬ 0 B x A | 0 C z = y / x C
164 158 eqeq2d x = y z = C z = y / x C
165 147 164 anbi12d x = y x x A | ¬ 0 B x A | 0 C z = C y x A | ¬ 0 B x A | 0 C z = y / x C
166 161 163 165 cbvopab1 x z | x x A | ¬ 0 B x A | 0 C z = C = y z | y x A | ¬ 0 B x A | 0 C z = y / x C
167 df-mpt x x A | ¬ 0 B x A | 0 C C = x z | x x A | ¬ 0 B x A | 0 C z = C
168 df-mpt y x A | ¬ 0 B x A | 0 C y / x C = y z | y x A | ¬ 0 B x A | 0 C z = y / x C
169 166 167 168 3eqtr4i x x A | ¬ 0 B x A | 0 C C = y x A | ¬ 0 B x A | 0 C y / x C
170 155 160 169 3eqtr4g x A | ¬ 0 B x A | 0 C A x A C x A | ¬ 0 B x A | 0 C = x x A | ¬ 0 B x A | 0 C C
171 139 170 ax-mp x A C x A | ¬ 0 B x A | 0 C = x x A | ¬ 0 B x A | 0 C C
172 136 154 171 3eqtr4g φ x A if 0 B B 0 + if 0 C C 0 x A | ¬ 0 B x A | 0 C = x A C x A | ¬ 0 B x A | 0 C
173 122 172 syl5eq φ x A if 0 B B 0 + if 0 C C 0 x A | 0 C x A | ¬ 0 B x A | 0 C = x A C x A | ¬ 0 B x A | 0 C
174 85 mptpreima x A B -1 −∞ 0 = x A | B −∞ 0
175 elioomnf 0 * B −∞ 0 B B < 0
176 78 175 ax-mp B −∞ 0 B B < 0
177 2 biantrurd φ x A B < 0 B B < 0
178 ltnle B 0 B < 0 ¬ 0 B
179 2 6 178 sylancl φ x A B < 0 ¬ 0 B
180 177 179 bitr3d φ x A B B < 0 ¬ 0 B
181 176 180 syl5bb φ x A B −∞ 0 ¬ 0 B
182 181 rabbidva φ x A | B −∞ 0 = x A | ¬ 0 B
183 174 182 syl5eq φ x A B -1 −∞ 0 = x A | ¬ 0 B
184 mbfima x A B MblFn x A B : A x A B -1 −∞ 0 dom vol
185 1 89 184 syl2anc φ x A B -1 −∞ 0 dom vol
186 183 185 eqeltrrd φ x A | ¬ 0 B dom vol
187 inmbl x A | ¬ 0 B dom vol x A | 0 C dom vol x A | ¬ 0 B x A | 0 C dom vol
188 186 114 187 syl2anc φ x A | ¬ 0 B x A | 0 C dom vol
189 mbfres x A C MblFn x A | ¬ 0 B x A | 0 C dom vol x A C x A | ¬ 0 B x A | 0 C MblFn
190 3 188 189 syl2anc φ x A C x A | ¬ 0 B x A | 0 C MblFn
191 173 190 eqeltrd φ x A if 0 B B 0 + if 0 C C 0 x A | 0 C x A | ¬ 0 B x A | 0 C MblFn
192 ssid A A
193 dfrab3ss A A x A | 0 C = A x A | 0 C
194 192 193 ax-mp x A | 0 C = A x A | 0 C
195 rabxm A = x A | 0 B x A | ¬ 0 B
196 195 ineq1i A x A | 0 C = x A | 0 B x A | ¬ 0 B x A | 0 C
197 indir x A | 0 B x A | ¬ 0 B x A | 0 C = x A | 0 B x A | 0 C x A | ¬ 0 B x A | 0 C
198 194 196 197 3eqtrri x A | 0 B x A | 0 C x A | ¬ 0 B x A | 0 C = x A | 0 C
199 198 a1i φ x A | 0 B x A | 0 C x A | ¬ 0 B x A | 0 C = x A | 0 C
200 15 119 191 199 mbfres2 φ x A if 0 B B 0 + if 0 C C 0 x A | 0 C MblFn
201 rabid x x A | ¬ 0 C x A ¬ 0 C
202 iffalse ¬ 0 C if 0 C C 0 = 0
203 202 oveq2d ¬ 0 C if 0 B B 0 + if 0 C C 0 = if 0 B B 0 + 0
204 8 recnd φ x A if 0 B B 0
205 204 addid1d φ x A if 0 B B 0 + 0 = if 0 B B 0
206 203 205 sylan9eqr φ x A ¬ 0 C if 0 B B 0 + if 0 C C 0 = if 0 B B 0
207 206 anasss φ x A ¬ 0 C if 0 B B 0 + if 0 C C 0 = if 0 B B 0
208 201 207 sylan2b φ x x A | ¬ 0 C if 0 B B 0 + if 0 C C 0 = if 0 B B 0
209 208 mpteq2dva φ x x A | ¬ 0 C if 0 B B 0 + if 0 C C 0 = x x A | ¬ 0 C if 0 B B 0
210 ssrab2 x A | ¬ 0 C A
211 resmpt x A | ¬ 0 C A y A y / x if 0 B B 0 + if 0 C C 0 x A | ¬ 0 C = y x A | ¬ 0 C y / x if 0 B B 0 + if 0 C C 0
212 37 reseq1i x A if 0 B B 0 + if 0 C C 0 x A | ¬ 0 C = y A y / x if 0 B B 0 + if 0 C C 0 x A | ¬ 0 C
213 nfv y x x A | ¬ 0 C z = if 0 B B 0 + if 0 C C 0
214 nfrab1 _ x x A | ¬ 0 C
215 214 nfcri x y x A | ¬ 0 C
216 215 44 nfan x y x A | ¬ 0 C z = y / x if 0 B B 0 + if 0 C C 0
217 eleq1w x = y x x A | ¬ 0 C y x A | ¬ 0 C
218 217 47 anbi12d x = y x x A | ¬ 0 C z = if 0 B B 0 + if 0 C C 0 y x A | ¬ 0 C z = y / x if 0 B B 0 + if 0 C C 0
219 213 216 218 cbvopab1 x z | x x A | ¬ 0 C z = if 0 B B 0 + if 0 C C 0 = y z | y x A | ¬ 0 C z = y / x if 0 B B 0 + if 0 C C 0
220 df-mpt x x A | ¬ 0 C if 0 B B 0 + if 0 C C 0 = x z | x x A | ¬ 0 C z = if 0 B B 0 + if 0 C C 0
221 df-mpt y x A | ¬ 0 C y / x if 0 B B 0 + if 0 C C 0 = y z | y x A | ¬ 0 C z = y / x if 0 B B 0 + if 0 C C 0
222 219 220 221 3eqtr4i x x A | ¬ 0 C if 0 B B 0 + if 0 C C 0 = y x A | ¬ 0 C y / x if 0 B B 0 + if 0 C C 0
223 211 212 222 3eqtr4g x A | ¬ 0 C A x A if 0 B B 0 + if 0 C C 0 x A | ¬ 0 C = x x A | ¬ 0 C if 0 B B 0 + if 0 C C 0
224 210 223 ax-mp x A if 0 B B 0 + if 0 C C 0 x A | ¬ 0 C = x x A | ¬ 0 C if 0 B B 0 + if 0 C C 0
225 resmpt x A | ¬ 0 C A y A y / x if 0 B B 0 x A | ¬ 0 C = y x A | ¬ 0 C y / x if 0 B B 0
226 nfcv _ y if 0 B B 0
227 nfcsb1v _ x y / x if 0 B B 0
228 csbeq1a x = y if 0 B B 0 = y / x if 0 B B 0
229 226 227 228 cbvmpt x A if 0 B B 0 = y A y / x if 0 B B 0
230 229 reseq1i x A if 0 B B 0 x A | ¬ 0 C = y A y / x if 0 B B 0 x A | ¬ 0 C
231 nfv y x x A | ¬ 0 C z = if 0 B B 0
232 227 nfeq2 x z = y / x if 0 B B 0
233 215 232 nfan x y x A | ¬ 0 C z = y / x if 0 B B 0
234 228 eqeq2d x = y z = if 0 B B 0 z = y / x if 0 B B 0
235 217 234 anbi12d x = y x x A | ¬ 0 C z = if 0 B B 0 y x A | ¬ 0 C z = y / x if 0 B B 0
236 231 233 235 cbvopab1 x z | x x A | ¬ 0 C z = if 0 B B 0 = y z | y x A | ¬ 0 C z = y / x if 0 B B 0
237 df-mpt x x A | ¬ 0 C if 0 B B 0 = x z | x x A | ¬ 0 C z = if 0 B B 0
238 df-mpt y x A | ¬ 0 C y / x if 0 B B 0 = y z | y x A | ¬ 0 C z = y / x if 0 B B 0
239 236 237 238 3eqtr4i x x A | ¬ 0 C if 0 B B 0 = y x A | ¬ 0 C y / x if 0 B B 0
240 225 230 239 3eqtr4g x A | ¬ 0 C A x A if 0 B B 0 x A | ¬ 0 C = x x A | ¬ 0 C if 0 B B 0
241 210 240 ax-mp x A if 0 B B 0 x A | ¬ 0 C = x x A | ¬ 0 C if 0 B B 0
242 209 224 241 3eqtr4g φ x A if 0 B B 0 + if 0 C C 0 x A | ¬ 0 C = x A if 0 B B 0 x A | ¬ 0 C
243 2 1 mbfpos φ x A if 0 B B 0 MblFn
244 103 mptpreima x A C -1 −∞ 0 = x A | C −∞ 0
245 elioomnf 0 * C −∞ 0 C C < 0
246 78 245 ax-mp C −∞ 0 C C < 0
247 4 biantrurd φ x A C < 0 C C < 0
248 ltnle C 0 C < 0 ¬ 0 C
249 4 6 248 sylancl φ x A C < 0 ¬ 0 C
250 247 249 bitr3d φ x A C C < 0 ¬ 0 C
251 246 250 syl5bb φ x A C −∞ 0 ¬ 0 C
252 251 rabbidva φ x A | C −∞ 0 = x A | ¬ 0 C
253 244 252 syl5eq φ x A C -1 −∞ 0 = x A | ¬ 0 C
254 mbfima x A C MblFn x A C : A x A C -1 −∞ 0 dom vol
255 3 107 254 syl2anc φ x A C -1 −∞ 0 dom vol
256 253 255 eqeltrrd φ x A | ¬ 0 C dom vol
257 mbfres x A if 0 B B 0 MblFn x A | ¬ 0 C dom vol x A if 0 B B 0 x A | ¬ 0 C MblFn
258 243 256 257 syl2anc φ x A if 0 B B 0 x A | ¬ 0 C MblFn
259 242 258 eqeltrd φ x A if 0 B B 0 + if 0 C C 0 x A | ¬ 0 C MblFn
260 rabxm A = x A | 0 C x A | ¬ 0 C
261 260 eqcomi x A | 0 C x A | ¬ 0 C = A
262 261 a1i φ x A | 0 C x A | ¬ 0 C = A
263 12 200 259 262 mbfres2 φ x A if 0 B B 0 + if 0 C C 0 MblFn