Metamath Proof Explorer

Theorem mbfaddlem

Description: The sum of two measurable functions is measurable. (Contributed by Mario Carneiro, 15-Aug-2014)

Ref Expression
Hypotheses mbfadd.1 
|- ( ph -> F e. MblFn )
mbfadd.2 
|- ( ph -> G e. MblFn )
mbfadd.3 
|- ( ph -> F : A --> RR )
mbfadd.4 
|- ( ph -> G : A --> RR )
Assertion mbfaddlem 
|- ( ph -> ( F oF + G ) e. MblFn )

Proof

Step Hyp Ref Expression
1 mbfadd.1 
 |-  ( ph -> F e. MblFn )
2 mbfadd.2 
 |-  ( ph -> G e. MblFn )
3 mbfadd.3 
 |-  ( ph -> F : A --> RR )
4 mbfadd.4 
 |-  ( ph -> G : A --> RR )
5 readdcl 
 |-  ( ( x e. RR /\ y e. RR ) -> ( x + y ) e. RR )
6 5 adantl 
 |-  ( ( ph /\ ( x e. RR /\ y e. RR ) ) -> ( x + y ) e. RR )
7 3 fdmd 
 |-  ( ph -> dom F = A )
8 mbfdm 
 |-  ( F e. MblFn -> dom F e. dom vol )
9 1 8 syl 
 |-  ( ph -> dom F e. dom vol )
10 7 9 eqeltrrd 
 |-  ( ph -> A e. dom vol )
11 inidm 
 |-  ( A i^i A ) = A
12 6 3 4 10 10 11 off 
 |-  ( ph -> ( F oF + G ) : A --> RR )
13 eliun 
 |-  ( x e. U_ r e. QQ ( ( `' F " ( r (,) +oo ) ) i^i ( `' G " ( ( y - r ) (,) +oo ) ) ) <-> E. r e. QQ x e. ( ( `' F " ( r (,) +oo ) ) i^i ( `' G " ( ( y - r ) (,) +oo ) ) ) )
14 r19.42v 
 |-  ( E. r e. QQ ( x e. A /\ ( ( F ` x ) e. ( r (,) +oo ) /\ ( G ` x ) e. ( ( y - r ) (,) +oo ) ) ) <-> ( x e. A /\ E. r e. QQ ( ( F ` x ) e. ( r (,) +oo ) /\ ( G ` x ) e. ( ( y - r ) (,) +oo ) ) ) )
15 simplr 
 |-  ( ( ( ph /\ y e. RR ) /\ x e. A ) -> y e. RR )
16 4 adantr 
 |-  ( ( ph /\ y e. RR ) -> G : A --> RR )
17 16 ffvelcdmda 
 |-  ( ( ( ph /\ y e. RR ) /\ x e. A ) -> ( G ` x ) e. RR )
18 3 adantr 
 |-  ( ( ph /\ y e. RR ) -> F : A --> RR )
19 18 ffvelcdmda 
 |-  ( ( ( ph /\ y e. RR ) /\ x e. A ) -> ( F ` x ) e. RR )
20 15 17 19 ltsubaddd 
 |-  ( ( ( ph /\ y e. RR ) /\ x e. A ) -> ( ( y - ( G ` x ) ) < ( F ` x ) <-> y < ( ( F ` x ) + ( G ` x ) ) ) )
21 15 adantr 
 |-  ( ( ( ( ph /\ y e. RR ) /\ x e. A ) /\ r e. QQ ) -> y e. RR )
22 qre 
 |-  ( r e. QQ -> r e. RR )
23 22 adantl 
 |-  ( ( ( ( ph /\ y e. RR ) /\ x e. A ) /\ r e. QQ ) -> r e. RR )
24 17 adantr 
 |-  ( ( ( ( ph /\ y e. RR ) /\ x e. A ) /\ r e. QQ ) -> ( G ` x ) e. RR )
25 ltsub23 
 |-  ( ( y e. RR /\ r e. RR /\ ( G ` x ) e. RR ) -> ( ( y - r ) < ( G ` x ) <-> ( y - ( G ` x ) ) < r ) )
26 21 23 24 25 syl3anc 
 |-  ( ( ( ( ph /\ y e. RR ) /\ x e. A ) /\ r e. QQ ) -> ( ( y - r ) < ( G ` x ) <-> ( y - ( G ` x ) ) < r ) )
27 26 anbi1cd 
 |-  ( ( ( ( ph /\ y e. RR ) /\ x e. A ) /\ r e. QQ ) -> ( ( r < ( F ` x ) /\ ( y - r ) < ( G ` x ) ) <-> ( ( y - ( G ` x ) ) < r /\ r < ( F ` x ) ) ) )
28 27 rexbidva 
 |-  ( ( ( ph /\ y e. RR ) /\ x e. A ) -> ( E. r e. QQ ( r < ( F ` x ) /\ ( y - r ) < ( G ` x ) ) <-> E. r e. QQ ( ( y - ( G ` x ) ) < r /\ r < ( F ` x ) ) ) )
29 15 17 resubcld 
 |-  ( ( ( ph /\ y e. RR ) /\ x e. A ) -> ( y - ( G ` x ) ) e. RR )
30 29 adantr 
 |-  ( ( ( ( ph /\ y e. RR ) /\ x e. A ) /\ r e. QQ ) -> ( y - ( G ` x ) ) e. RR )
31 19 adantr 
 |-  ( ( ( ( ph /\ y e. RR ) /\ x e. A ) /\ r e. QQ ) -> ( F ` x ) e. RR )
32 lttr 
 |-  ( ( ( y - ( G ` x ) ) e. RR /\ r e. RR /\ ( F ` x ) e. RR ) -> ( ( ( y - ( G ` x ) ) < r /\ r < ( F ` x ) ) -> ( y - ( G ` x ) ) < ( F ` x ) ) )
33 30 23 31 32 syl3anc 
 |-  ( ( ( ( ph /\ y e. RR ) /\ x e. A ) /\ r e. QQ ) -> ( ( ( y - ( G ` x ) ) < r /\ r < ( F ` x ) ) -> ( y - ( G ` x ) ) < ( F ` x ) ) )
34 33 rexlimdva 
 |-  ( ( ( ph /\ y e. RR ) /\ x e. A ) -> ( E. r e. QQ ( ( y - ( G ` x ) ) < r /\ r < ( F ` x ) ) -> ( y - ( G ` x ) ) < ( F ` x ) ) )
35 qbtwnre 
 |-  ( ( ( y - ( G ` x ) ) e. RR /\ ( F ` x ) e. RR /\ ( y - ( G ` x ) ) < ( F ` x ) ) -> E. r e. QQ ( ( y - ( G ` x ) ) < r /\ r < ( F ` x ) ) )
36 35 3expia 
 |-  ( ( ( y - ( G ` x ) ) e. RR /\ ( F ` x ) e. RR ) -> ( ( y - ( G ` x ) ) < ( F ` x ) -> E. r e. QQ ( ( y - ( G ` x ) ) < r /\ r < ( F ` x ) ) ) )
37 29 19 36 syl2anc 
 |-  ( ( ( ph /\ y e. RR ) /\ x e. A ) -> ( ( y - ( G ` x ) ) < ( F ` x ) -> E. r e. QQ ( ( y - ( G ` x ) ) < r /\ r < ( F ` x ) ) ) )
38 34 37 impbid 
 |-  ( ( ( ph /\ y e. RR ) /\ x e. A ) -> ( E. r e. QQ ( ( y - ( G ` x ) ) < r /\ r < ( F ` x ) ) <-> ( y - ( G ` x ) ) < ( F ` x ) ) )
39 28 38 bitrd 
 |-  ( ( ( ph /\ y e. RR ) /\ x e. A ) -> ( E. r e. QQ ( r < ( F ` x ) /\ ( y - r ) < ( G ` x ) ) <-> ( y - ( G ` x ) ) < ( F ` x ) ) )
40 3 ffnd 
 |-  ( ph -> F Fn A )
41 40 adantr 
 |-  ( ( ph /\ y e. RR ) -> F Fn A )
42 4 ffnd 
 |-  ( ph -> G Fn A )
43 42 adantr 
 |-  ( ( ph /\ y e. RR ) -> G Fn A )
44 10 adantr 
 |-  ( ( ph /\ y e. RR ) -> A e. dom vol )
45 eqidd 
 |-  ( ( ( ph /\ y e. RR ) /\ x e. A ) -> ( F ` x ) = ( F ` x ) )
46 eqidd 
 |-  ( ( ( ph /\ y e. RR ) /\ x e. A ) -> ( G ` x ) = ( G ` x ) )
47 41 43 44 44 11 45 46 ofval 
 |-  ( ( ( ph /\ y e. RR ) /\ x e. A ) -> ( ( F oF + G ) ` x ) = ( ( F ` x ) + ( G ` x ) ) )
48 47 breq2d 
 |-  ( ( ( ph /\ y e. RR ) /\ x e. A ) -> ( y < ( ( F oF + G ) ` x ) <-> y < ( ( F ` x ) + ( G ` x ) ) ) )
49 20 39 48 3bitr4d 
 |-  ( ( ( ph /\ y e. RR ) /\ x e. A ) -> ( E. r e. QQ ( r < ( F ` x ) /\ ( y - r ) < ( G ` x ) ) <-> y < ( ( F oF + G ) ` x ) ) )
50 23 rexrd 
 |-  ( ( ( ( ph /\ y e. RR ) /\ x e. A ) /\ r e. QQ ) -> r e. RR* )
51 elioopnf 
 |-  ( r e. RR* -> ( ( F ` x ) e. ( r (,) +oo ) <-> ( ( F ` x ) e. RR /\ r < ( F ` x ) ) ) )
52 50 51 syl 
 |-  ( ( ( ( ph /\ y e. RR ) /\ x e. A ) /\ r e. QQ ) -> ( ( F ` x ) e. ( r (,) +oo ) <-> ( ( F ` x ) e. RR /\ r < ( F ` x ) ) ) )
53 31 52 mpbirand 
 |-  ( ( ( ( ph /\ y e. RR ) /\ x e. A ) /\ r e. QQ ) -> ( ( F ` x ) e. ( r (,) +oo ) <-> r < ( F ` x ) ) )
54 21 23 resubcld 
 |-  ( ( ( ( ph /\ y e. RR ) /\ x e. A ) /\ r e. QQ ) -> ( y - r ) e. RR )
55 54 rexrd 
 |-  ( ( ( ( ph /\ y e. RR ) /\ x e. A ) /\ r e. QQ ) -> ( y - r ) e. RR* )
56 elioopnf 
 |-  ( ( y - r ) e. RR* -> ( ( G ` x ) e. ( ( y - r ) (,) +oo ) <-> ( ( G ` x ) e. RR /\ ( y - r ) < ( G ` x ) ) ) )
57 55 56 syl 
 |-  ( ( ( ( ph /\ y e. RR ) /\ x e. A ) /\ r e. QQ ) -> ( ( G ` x ) e. ( ( y - r ) (,) +oo ) <-> ( ( G ` x ) e. RR /\ ( y - r ) < ( G ` x ) ) ) )
58 24 57 mpbirand 
 |-  ( ( ( ( ph /\ y e. RR ) /\ x e. A ) /\ r e. QQ ) -> ( ( G ` x ) e. ( ( y - r ) (,) +oo ) <-> ( y - r ) < ( G ` x ) ) )
59 53 58 anbi12d 
 |-  ( ( ( ( ph /\ y e. RR ) /\ x e. A ) /\ r e. QQ ) -> ( ( ( F ` x ) e. ( r (,) +oo ) /\ ( G ` x ) e. ( ( y - r ) (,) +oo ) ) <-> ( r < ( F ` x ) /\ ( y - r ) < ( G ` x ) ) ) )
60 59 rexbidva 
 |-  ( ( ( ph /\ y e. RR ) /\ x e. A ) -> ( E. r e. QQ ( ( F ` x ) e. ( r (,) +oo ) /\ ( G ` x ) e. ( ( y - r ) (,) +oo ) ) <-> E. r e. QQ ( r < ( F ` x ) /\ ( y - r ) < ( G ` x ) ) ) )
61 12 adantr 
 |-  ( ( ph /\ y e. RR ) -> ( F oF + G ) : A --> RR )
62 61 ffvelcdmda 
 |-  ( ( ( ph /\ y e. RR ) /\ x e. A ) -> ( ( F oF + G ) ` x ) e. RR )
63 15 rexrd 
 |-  ( ( ( ph /\ y e. RR ) /\ x e. A ) -> y e. RR* )
64 elioopnf 
 |-  ( y e. RR* -> ( ( ( F oF + G ) ` x ) e. ( y (,) +oo ) <-> ( ( ( F oF + G ) ` x ) e. RR /\ y < ( ( F oF + G ) ` x ) ) ) )
65 63 64 syl 
 |-  ( ( ( ph /\ y e. RR ) /\ x e. A ) -> ( ( ( F oF + G ) ` x ) e. ( y (,) +oo ) <-> ( ( ( F oF + G ) ` x ) e. RR /\ y < ( ( F oF + G ) ` x ) ) ) )
66 62 65 mpbirand 
 |-  ( ( ( ph /\ y e. RR ) /\ x e. A ) -> ( ( ( F oF + G ) ` x ) e. ( y (,) +oo ) <-> y < ( ( F oF + G ) ` x ) ) )
67 49 60 66 3bitr4d 
 |-  ( ( ( ph /\ y e. RR ) /\ x e. A ) -> ( E. r e. QQ ( ( F ` x ) e. ( r (,) +oo ) /\ ( G ` x ) e. ( ( y - r ) (,) +oo ) ) <-> ( ( F oF + G ) ` x ) e. ( y (,) +oo ) ) )
68 67 pm5.32da 
 |-  ( ( ph /\ y e. RR ) -> ( ( x e. A /\ E. r e. QQ ( ( F ` x ) e. ( r (,) +oo ) /\ ( G ` x ) e. ( ( y - r ) (,) +oo ) ) ) <-> ( x e. A /\ ( ( F oF + G ) ` x ) e. ( y (,) +oo ) ) ) )
69 14 68 bitrid 
 |-  ( ( ph /\ y e. RR ) -> ( E. r e. QQ ( x e. A /\ ( ( F ` x ) e. ( r (,) +oo ) /\ ( G ` x ) e. ( ( y - r ) (,) +oo ) ) ) <-> ( x e. A /\ ( ( F oF + G ) ` x ) e. ( y (,) +oo ) ) ) )
70 elpreima 
 |-  ( F Fn A -> ( x e. ( `' F " ( r (,) +oo ) ) <-> ( x e. A /\ ( F ` x ) e. ( r (,) +oo ) ) ) )
71 41 70 syl 
 |-  ( ( ph /\ y e. RR ) -> ( x e. ( `' F " ( r (,) +oo ) ) <-> ( x e. A /\ ( F ` x ) e. ( r (,) +oo ) ) ) )
72 elpreima 
 |-  ( G Fn A -> ( x e. ( `' G " ( ( y - r ) (,) +oo ) ) <-> ( x e. A /\ ( G ` x ) e. ( ( y - r ) (,) +oo ) ) ) )
73 43 72 syl 
 |-  ( ( ph /\ y e. RR ) -> ( x e. ( `' G " ( ( y - r ) (,) +oo ) ) <-> ( x e. A /\ ( G ` x ) e. ( ( y - r ) (,) +oo ) ) ) )
74 71 73 anbi12d 
 |-  ( ( ph /\ y e. RR ) -> ( ( x e. ( `' F " ( r (,) +oo ) ) /\ x e. ( `' G " ( ( y - r ) (,) +oo ) ) ) <-> ( ( x e. A /\ ( F ` x ) e. ( r (,) +oo ) ) /\ ( x e. A /\ ( G ` x ) e. ( ( y - r ) (,) +oo ) ) ) ) )
75 elin 
 |-  ( x e. ( ( `' F " ( r (,) +oo ) ) i^i ( `' G " ( ( y - r ) (,) +oo ) ) ) <-> ( x e. ( `' F " ( r (,) +oo ) ) /\ x e. ( `' G " ( ( y - r ) (,) +oo ) ) ) )
76 anandi 
 |-  ( ( x e. A /\ ( ( F ` x ) e. ( r (,) +oo ) /\ ( G ` x ) e. ( ( y - r ) (,) +oo ) ) ) <-> ( ( x e. A /\ ( F ` x ) e. ( r (,) +oo ) ) /\ ( x e. A /\ ( G ` x ) e. ( ( y - r ) (,) +oo ) ) ) )
77 74 75 76 3bitr4g 
 |-  ( ( ph /\ y e. RR ) -> ( x e. ( ( `' F " ( r (,) +oo ) ) i^i ( `' G " ( ( y - r ) (,) +oo ) ) ) <-> ( x e. A /\ ( ( F ` x ) e. ( r (,) +oo ) /\ ( G ` x ) e. ( ( y - r ) (,) +oo ) ) ) ) )
78 77 rexbidv 
 |-  ( ( ph /\ y e. RR ) -> ( E. r e. QQ x e. ( ( `' F " ( r (,) +oo ) ) i^i ( `' G " ( ( y - r ) (,) +oo ) ) ) <-> E. r e. QQ ( x e. A /\ ( ( F ` x ) e. ( r (,) +oo ) /\ ( G ` x ) e. ( ( y - r ) (,) +oo ) ) ) ) )
79 12 ffnd 
 |-  ( ph -> ( F oF + G ) Fn A )
80 79 adantr 
 |-  ( ( ph /\ y e. RR ) -> ( F oF + G ) Fn A )
81 elpreima 
 |-  ( ( F oF + G ) Fn A -> ( x e. ( `' ( F oF + G ) " ( y (,) +oo ) ) <-> ( x e. A /\ ( ( F oF + G ) ` x ) e. ( y (,) +oo ) ) ) )
82 80 81 syl 
 |-  ( ( ph /\ y e. RR ) -> ( x e. ( `' ( F oF + G ) " ( y (,) +oo ) ) <-> ( x e. A /\ ( ( F oF + G ) ` x ) e. ( y (,) +oo ) ) ) )
83 69 78 82 3bitr4d 
 |-  ( ( ph /\ y e. RR ) -> ( E. r e. QQ x e. ( ( `' F " ( r (,) +oo ) ) i^i ( `' G " ( ( y - r ) (,) +oo ) ) ) <-> x e. ( `' ( F oF + G ) " ( y (,) +oo ) ) ) )
84 13 83 bitrid 
 |-  ( ( ph /\ y e. RR ) -> ( x e. U_ r e. QQ ( ( `' F " ( r (,) +oo ) ) i^i ( `' G " ( ( y - r ) (,) +oo ) ) ) <-> x e. ( `' ( F oF + G ) " ( y (,) +oo ) ) ) )
85 84 eqrdv 
 |-  ( ( ph /\ y e. RR ) -> U_ r e. QQ ( ( `' F " ( r (,) +oo ) ) i^i ( `' G " ( ( y - r ) (,) +oo ) ) ) = ( `' ( F oF + G ) " ( y (,) +oo ) ) )
86 qnnen 
 |-  QQ ~~ NN
87 endom 
 |-  ( QQ ~~ NN -> QQ ~<_ NN )
88 86 87 ax-mp 
 |-  QQ ~<_ NN
89 mbfima 
 |-  ( ( F e. MblFn /\ F : A --> RR ) -> ( `' F " ( r (,) +oo ) ) e. dom vol )
90 1 3 89 syl2anc 
 |-  ( ph -> ( `' F " ( r (,) +oo ) ) e. dom vol )
91 mbfima 
 |-  ( ( G e. MblFn /\ G : A --> RR ) -> ( `' G " ( ( y - r ) (,) +oo ) ) e. dom vol )
92 2 4 91 syl2anc 
 |-  ( ph -> ( `' G " ( ( y - r ) (,) +oo ) ) e. dom vol )
93 inmbl 
 |-  ( ( ( `' F " ( r (,) +oo ) ) e. dom vol /\ ( `' G " ( ( y - r ) (,) +oo ) ) e. dom vol ) -> ( ( `' F " ( r (,) +oo ) ) i^i ( `' G " ( ( y - r ) (,) +oo ) ) ) e. dom vol )
94 90 92 93 syl2anc 
 |-  ( ph -> ( ( `' F " ( r (,) +oo ) ) i^i ( `' G " ( ( y - r ) (,) +oo ) ) ) e. dom vol )
95 94 ad2antrr 
 |-  ( ( ( ph /\ y e. RR ) /\ r e. QQ ) -> ( ( `' F " ( r (,) +oo ) ) i^i ( `' G " ( ( y - r ) (,) +oo ) ) ) e. dom vol )
96 95 ralrimiva 
 |-  ( ( ph /\ y e. RR ) -> A. r e. QQ ( ( `' F " ( r (,) +oo ) ) i^i ( `' G " ( ( y - r ) (,) +oo ) ) ) e. dom vol )
97 iunmbl2 
 |-  ( ( QQ ~<_ NN /\ A. r e. QQ ( ( `' F " ( r (,) +oo ) ) i^i ( `' G " ( ( y - r ) (,) +oo ) ) ) e. dom vol ) -> U_ r e. QQ ( ( `' F " ( r (,) +oo ) ) i^i ( `' G " ( ( y - r ) (,) +oo ) ) ) e. dom vol )
98 88 96 97 sylancr 
 |-  ( ( ph /\ y e. RR ) -> U_ r e. QQ ( ( `' F " ( r (,) +oo ) ) i^i ( `' G " ( ( y - r ) (,) +oo ) ) ) e. dom vol )
99 85 98 eqeltrrd 
 |-  ( ( ph /\ y e. RR ) -> ( `' ( F oF + G ) " ( y (,) +oo ) ) e. dom vol )
100 12 99 ismbf3d 
 |-  ( ph -> ( F oF + G ) e. MblFn )