Metamath Proof Explorer

Theorem ftc1anclem1

Description: Lemma for ftc1anc - the absolute value of a real-valued measurable function is measurable. Would be trivial with cncombf , but this proof avoids ax-cc . (Contributed by Brendan Leahy, 18-Jun-2018)

Ref Expression
Assertion ftc1anclem1 
|- ( ( F : A --> RR /\ F e. MblFn ) -> ( abs o. F ) e. MblFn )

Proof

Step Hyp Ref Expression
1 ffvelcdm 
 |-  ( ( F : A --> RR /\ t e. A ) -> ( F ` t ) e. RR )
2 1 recnd 
 |-  ( ( F : A --> RR /\ t e. A ) -> ( F ` t ) e. CC )
3 id 
 |-  ( F : A --> RR -> F : A --> RR )
4 3 feqmptd 
 |-  ( F : A --> RR -> F = ( t e. A |-> ( F ` t ) ) )
5 absf 
 |-  abs : CC --> RR
6 5 a1i 
 |-  ( F : A --> RR -> abs : CC --> RR )
7 6 feqmptd 
 |-  ( F : A --> RR -> abs = ( x e. CC |-> ( abs ` x ) ) )
8 fveq2 
 |-  ( x = ( F ` t ) -> ( abs ` x ) = ( abs ` ( F ` t ) ) )
9 2 4 7 8 fmptco 
 |-  ( F : A --> RR -> ( abs o. F ) = ( t e. A |-> ( abs ` ( F ` t ) ) ) )
10 9 adantr 
 |-  ( ( F : A --> RR /\ F e. MblFn ) -> ( abs o. F ) = ( t e. A |-> ( abs ` ( F ` t ) ) ) )
11 2 abscld 
 |-  ( ( F : A --> RR /\ t e. A ) -> ( abs ` ( F ` t ) ) e. RR )
12 11 fmpttd 
 |-  ( F : A --> RR -> ( t e. A |-> ( abs ` ( F ` t ) ) ) : A --> RR )
13 12 adantr 
 |-  ( ( F : A --> RR /\ F e. MblFn ) -> ( t e. A |-> ( abs ` ( F ` t ) ) ) : A --> RR )
14 fdm 
 |-  ( F : A --> RR -> dom F = A )
15 14 adantr 
 |-  ( ( F : A --> RR /\ F e. MblFn ) -> dom F = A )
16 mbfdm 
 |-  ( F e. MblFn -> dom F e. dom vol )
17 16 adantl 
 |-  ( ( F : A --> RR /\ F e. MblFn ) -> dom F e. dom vol )
18 15 17 eqeltrrd 
 |-  ( ( F : A --> RR /\ F e. MblFn ) -> A e. dom vol )
19 rexr 
 |-  ( x e. RR -> x e. RR* )
20 elioopnf 
 |-  ( x e. RR* -> ( ( abs ` ( F ` t ) ) e. ( x (,) +oo ) <-> ( ( abs ` ( F ` t ) ) e. RR /\ x < ( abs ` ( F ` t ) ) ) ) )
21 19 20 syl 
 |-  ( x e. RR -> ( ( abs ` ( F ` t ) ) e. ( x (,) +oo ) <-> ( ( abs ` ( F ` t ) ) e. RR /\ x < ( abs ` ( F ` t ) ) ) ) )
22 11 biantrurd 
 |-  ( ( F : A --> RR /\ t e. A ) -> ( x < ( abs ` ( F ` t ) ) <-> ( ( abs ` ( F ` t ) ) e. RR /\ x < ( abs ` ( F ` t ) ) ) ) )
23 22 bicomd 
 |-  ( ( F : A --> RR /\ t e. A ) -> ( ( ( abs ` ( F ` t ) ) e. RR /\ x < ( abs ` ( F ` t ) ) ) <-> x < ( abs ` ( F ` t ) ) ) )
24 21 23 sylan9bbr 
 |-  ( ( ( F : A --> RR /\ t e. A ) /\ x e. RR ) -> ( ( abs ` ( F ` t ) ) e. ( x (,) +oo ) <-> x < ( abs ` ( F ` t ) ) ) )
25 ltnle 
 |-  ( ( x e. RR /\ ( abs ` ( F ` t ) ) e. RR ) -> ( x < ( abs ` ( F ` t ) ) <-> -. ( abs ` ( F ` t ) ) <_ x ) )
26 25 ancoms 
 |-  ( ( ( abs ` ( F ` t ) ) e. RR /\ x e. RR ) -> ( x < ( abs ` ( F ` t ) ) <-> -. ( abs ` ( F ` t ) ) <_ x ) )
27 11 26 sylan 
 |-  ( ( ( F : A --> RR /\ t e. A ) /\ x e. RR ) -> ( x < ( abs ` ( F ` t ) ) <-> -. ( abs ` ( F ` t ) ) <_ x ) )
28 absle 
 |-  ( ( ( F ` t ) e. RR /\ x e. RR ) -> ( ( abs ` ( F ` t ) ) <_ x <-> ( -u x <_ ( F ` t ) /\ ( F ` t ) <_ x ) ) )
29 1 28 sylan 
 |-  ( ( ( F : A --> RR /\ t e. A ) /\ x e. RR ) -> ( ( abs ` ( F ` t ) ) <_ x <-> ( -u x <_ ( F ` t ) /\ ( F ` t ) <_ x ) ) )
30 renegcl 
 |-  ( x e. RR -> -u x e. RR )
31 lenlt 
 |-  ( ( -u x e. RR /\ ( F ` t ) e. RR ) -> ( -u x <_ ( F ` t ) <-> -. ( F ` t ) < -u x ) )
32 30 1 31 syl2anr 
 |-  ( ( ( F : A --> RR /\ t e. A ) /\ x e. RR ) -> ( -u x <_ ( F ` t ) <-> -. ( F ` t ) < -u x ) )
33 1 biantrurd 
 |-  ( ( F : A --> RR /\ t e. A ) -> ( ( F ` t ) < -u x <-> ( ( F ` t ) e. RR /\ ( F ` t ) < -u x ) ) )
34 30 rexrd 
 |-  ( x e. RR -> -u x e. RR* )
35 elioomnf 
 |-  ( -u x e. RR* -> ( ( F ` t ) e. ( -oo (,) -u x ) <-> ( ( F ` t ) e. RR /\ ( F ` t ) < -u x ) ) )
36 34 35 syl 
 |-  ( x e. RR -> ( ( F ` t ) e. ( -oo (,) -u x ) <-> ( ( F ` t ) e. RR /\ ( F ` t ) < -u x ) ) )
37 36 bicomd 
 |-  ( x e. RR -> ( ( ( F ` t ) e. RR /\ ( F ` t ) < -u x ) <-> ( F ` t ) e. ( -oo (,) -u x ) ) )
38 33 37 sylan9bb 
 |-  ( ( ( F : A --> RR /\ t e. A ) /\ x e. RR ) -> ( ( F ` t ) < -u x <-> ( F ` t ) e. ( -oo (,) -u x ) ) )
39 38 notbid 
 |-  ( ( ( F : A --> RR /\ t e. A ) /\ x e. RR ) -> ( -. ( F ` t ) < -u x <-> -. ( F ` t ) e. ( -oo (,) -u x ) ) )
40 32 39 bitrd 
 |-  ( ( ( F : A --> RR /\ t e. A ) /\ x e. RR ) -> ( -u x <_ ( F ` t ) <-> -. ( F ` t ) e. ( -oo (,) -u x ) ) )
41 lenlt 
 |-  ( ( ( F ` t ) e. RR /\ x e. RR ) -> ( ( F ` t ) <_ x <-> -. x < ( F ` t ) ) )
42 1 41 sylan 
 |-  ( ( ( F : A --> RR /\ t e. A ) /\ x e. RR ) -> ( ( F ` t ) <_ x <-> -. x < ( F ` t ) ) )
43 1 biantrurd 
 |-  ( ( F : A --> RR /\ t e. A ) -> ( x < ( F ` t ) <-> ( ( F ` t ) e. RR /\ x < ( F ` t ) ) ) )
44 elioopnf 
 |-  ( x e. RR* -> ( ( F ` t ) e. ( x (,) +oo ) <-> ( ( F ` t ) e. RR /\ x < ( F ` t ) ) ) )
45 19 44 syl 
 |-  ( x e. RR -> ( ( F ` t ) e. ( x (,) +oo ) <-> ( ( F ` t ) e. RR /\ x < ( F ` t ) ) ) )
46 45 bicomd 
 |-  ( x e. RR -> ( ( ( F ` t ) e. RR /\ x < ( F ` t ) ) <-> ( F ` t ) e. ( x (,) +oo ) ) )
47 43 46 sylan9bb 
 |-  ( ( ( F : A --> RR /\ t e. A ) /\ x e. RR ) -> ( x < ( F ` t ) <-> ( F ` t ) e. ( x (,) +oo ) ) )
48 47 notbid 
 |-  ( ( ( F : A --> RR /\ t e. A ) /\ x e. RR ) -> ( -. x < ( F ` t ) <-> -. ( F ` t ) e. ( x (,) +oo ) ) )
49 42 48 bitrd 
 |-  ( ( ( F : A --> RR /\ t e. A ) /\ x e. RR ) -> ( ( F ` t ) <_ x <-> -. ( F ` t ) e. ( x (,) +oo ) ) )
50 40 49 anbi12d 
 |-  ( ( ( F : A --> RR /\ t e. A ) /\ x e. RR ) -> ( ( -u x <_ ( F ` t ) /\ ( F ` t ) <_ x ) <-> ( -. ( F ` t ) e. ( -oo (,) -u x ) /\ -. ( F ` t ) e. ( x (,) +oo ) ) ) )
51 29 50 bitrd 
 |-  ( ( ( F : A --> RR /\ t e. A ) /\ x e. RR ) -> ( ( abs ` ( F ` t ) ) <_ x <-> ( -. ( F ` t ) e. ( -oo (,) -u x ) /\ -. ( F ` t ) e. ( x (,) +oo ) ) ) )
52 51 notbid 
 |-  ( ( ( F : A --> RR /\ t e. A ) /\ x e. RR ) -> ( -. ( abs ` ( F ` t ) ) <_ x <-> -. ( -. ( F ` t ) e. ( -oo (,) -u x ) /\ -. ( F ` t ) e. ( x (,) +oo ) ) ) )
53 elun 
 |-  ( ( F ` t ) e. ( ( -oo (,) -u x ) u. ( x (,) +oo ) ) <-> ( ( F ` t ) e. ( -oo (,) -u x ) \/ ( F ` t ) e. ( x (,) +oo ) ) )
54 oran 
 |-  ( ( ( F ` t ) e. ( -oo (,) -u x ) \/ ( F ` t ) e. ( x (,) +oo ) ) <-> -. ( -. ( F ` t ) e. ( -oo (,) -u x ) /\ -. ( F ` t ) e. ( x (,) +oo ) ) )
55 53 54 bitri 
 |-  ( ( F ` t ) e. ( ( -oo (,) -u x ) u. ( x (,) +oo ) ) <-> -. ( -. ( F ` t ) e. ( -oo (,) -u x ) /\ -. ( F ` t ) e. ( x (,) +oo ) ) )
56 52 55 bitr4di 
 |-  ( ( ( F : A --> RR /\ t e. A ) /\ x e. RR ) -> ( -. ( abs ` ( F ` t ) ) <_ x <-> ( F ` t ) e. ( ( -oo (,) -u x ) u. ( x (,) +oo ) ) ) )
57 24 27 56 3bitrd 
 |-  ( ( ( F : A --> RR /\ t e. A ) /\ x e. RR ) -> ( ( abs ` ( F ` t ) ) e. ( x (,) +oo ) <-> ( F ` t ) e. ( ( -oo (,) -u x ) u. ( x (,) +oo ) ) ) )
58 57 an32s 
 |-  ( ( ( F : A --> RR /\ x e. RR ) /\ t e. A ) -> ( ( abs ` ( F ` t ) ) e. ( x (,) +oo ) <-> ( F ` t ) e. ( ( -oo (,) -u x ) u. ( x (,) +oo ) ) ) )
59 58 rabbidva 
 |-  ( ( F : A --> RR /\ x e. RR ) -> { t e. A | ( abs ` ( F ` t ) ) e. ( x (,) +oo ) } = { t e. A | ( F ` t ) e. ( ( -oo (,) -u x ) u. ( x (,) +oo ) ) } )
60 eqid 
 |-  ( t e. A |-> ( abs ` ( F ` t ) ) ) = ( t e. A |-> ( abs ` ( F ` t ) ) )
61 60 mptpreima 
 |-  ( `' ( t e. A |-> ( abs ` ( F ` t ) ) ) " ( x (,) +oo ) ) = { t e. A | ( abs ` ( F ` t ) ) e. ( x (,) +oo ) }
62 eqid 
 |-  ( t e. A |-> ( F ` t ) ) = ( t e. A |-> ( F ` t ) )
63 62 mptpreima 
 |-  ( `' ( t e. A |-> ( F ` t ) ) " ( ( -oo (,) -u x ) u. ( x (,) +oo ) ) ) = { t e. A | ( F ` t ) e. ( ( -oo (,) -u x ) u. ( x (,) +oo ) ) }
64 59 61 63 3eqtr4g 
 |-  ( ( F : A --> RR /\ x e. RR ) -> ( `' ( t e. A |-> ( abs ` ( F ` t ) ) ) " ( x (,) +oo ) ) = ( `' ( t e. A |-> ( F ` t ) ) " ( ( -oo (,) -u x ) u. ( x (,) +oo ) ) ) )
65 simpl 
 |-  ( ( F : A --> RR /\ x e. RR ) -> F : A --> RR )
66 65 feqmptd 
 |-  ( ( F : A --> RR /\ x e. RR ) -> F = ( t e. A |-> ( F ` t ) ) )
67 66 cnveqd 
 |-  ( ( F : A --> RR /\ x e. RR ) -> `' F = `' ( t e. A |-> ( F ` t ) ) )
68 67 imaeq1d 
 |-  ( ( F : A --> RR /\ x e. RR ) -> ( `' F " ( ( -oo (,) -u x ) u. ( x (,) +oo ) ) ) = ( `' ( t e. A |-> ( F ` t ) ) " ( ( -oo (,) -u x ) u. ( x (,) +oo ) ) ) )
69 64 68 eqtr4d 
 |-  ( ( F : A --> RR /\ x e. RR ) -> ( `' ( t e. A |-> ( abs ` ( F ` t ) ) ) " ( x (,) +oo ) ) = ( `' F " ( ( -oo (,) -u x ) u. ( x (,) +oo ) ) ) )
70 imaundi 
 |-  ( `' F " ( ( -oo (,) -u x ) u. ( x (,) +oo ) ) ) = ( ( `' F " ( -oo (,) -u x ) ) u. ( `' F " ( x (,) +oo ) ) )
71 69 70 eqtrdi 
 |-  ( ( F : A --> RR /\ x e. RR ) -> ( `' ( t e. A |-> ( abs ` ( F ` t ) ) ) " ( x (,) +oo ) ) = ( ( `' F " ( -oo (,) -u x ) ) u. ( `' F " ( x (,) +oo ) ) ) )
72 71 adantlr 
 |-  ( ( ( F : A --> RR /\ F e. MblFn ) /\ x e. RR ) -> ( `' ( t e. A |-> ( abs ` ( F ` t ) ) ) " ( x (,) +oo ) ) = ( ( `' F " ( -oo (,) -u x ) ) u. ( `' F " ( x (,) +oo ) ) ) )
73 mbfima 
 |-  ( ( F e. MblFn /\ F : A --> RR ) -> ( `' F " ( -oo (,) -u x ) ) e. dom vol )
74 mbfima 
 |-  ( ( F e. MblFn /\ F : A --> RR ) -> ( `' F " ( x (,) +oo ) ) e. dom vol )
75 unmbl 
 |-  ( ( ( `' F " ( -oo (,) -u x ) ) e. dom vol /\ ( `' F " ( x (,) +oo ) ) e. dom vol ) -> ( ( `' F " ( -oo (,) -u x ) ) u. ( `' F " ( x (,) +oo ) ) ) e. dom vol )
76 73 74 75 syl2anc 
 |-  ( ( F e. MblFn /\ F : A --> RR ) -> ( ( `' F " ( -oo (,) -u x ) ) u. ( `' F " ( x (,) +oo ) ) ) e. dom vol )
77 76 ancoms 
 |-  ( ( F : A --> RR /\ F e. MblFn ) -> ( ( `' F " ( -oo (,) -u x ) ) u. ( `' F " ( x (,) +oo ) ) ) e. dom vol )
78 77 adantr 
 |-  ( ( ( F : A --> RR /\ F e. MblFn ) /\ x e. RR ) -> ( ( `' F " ( -oo (,) -u x ) ) u. ( `' F " ( x (,) +oo ) ) ) e. dom vol )
79 72 78 eqeltrd 
 |-  ( ( ( F : A --> RR /\ F e. MblFn ) /\ x e. RR ) -> ( `' ( t e. A |-> ( abs ` ( F ` t ) ) ) " ( x (,) +oo ) ) e. dom vol )
80 abslt 
 |-  ( ( ( F ` t ) e. RR /\ x e. RR ) -> ( ( abs ` ( F ` t ) ) < x <-> ( -u x < ( F ` t ) /\ ( F ` t ) < x ) ) )
81 1 80 sylan 
 |-  ( ( ( F : A --> RR /\ t e. A ) /\ x e. RR ) -> ( ( abs ` ( F ` t ) ) < x <-> ( -u x < ( F ` t ) /\ ( F ` t ) < x ) ) )
82 elioomnf 
 |-  ( x e. RR* -> ( ( abs ` ( F ` t ) ) e. ( -oo (,) x ) <-> ( ( abs ` ( F ` t ) ) e. RR /\ ( abs ` ( F ` t ) ) < x ) ) )
83 19 82 syl 
 |-  ( x e. RR -> ( ( abs ` ( F ` t ) ) e. ( -oo (,) x ) <-> ( ( abs ` ( F ` t ) ) e. RR /\ ( abs ` ( F ` t ) ) < x ) ) )
84 11 biantrurd 
 |-  ( ( F : A --> RR /\ t e. A ) -> ( ( abs ` ( F ` t ) ) < x <-> ( ( abs ` ( F ` t ) ) e. RR /\ ( abs ` ( F ` t ) ) < x ) ) )
85 84 bicomd 
 |-  ( ( F : A --> RR /\ t e. A ) -> ( ( ( abs ` ( F ` t ) ) e. RR /\ ( abs ` ( F ` t ) ) < x ) <-> ( abs ` ( F ` t ) ) < x ) )
86 83 85 sylan9bbr 
 |-  ( ( ( F : A --> RR /\ t e. A ) /\ x e. RR ) -> ( ( abs ` ( F ` t ) ) e. ( -oo (,) x ) <-> ( abs ` ( F ` t ) ) < x ) )
87 34 19 jca 
 |-  ( x e. RR -> ( -u x e. RR* /\ x e. RR* ) )
88 1 rexrd 
 |-  ( ( F : A --> RR /\ t e. A ) -> ( F ` t ) e. RR* )
89 elioo5 
 |-  ( ( -u x e. RR* /\ x e. RR* /\ ( F ` t ) e. RR* ) -> ( ( F ` t ) e. ( -u x (,) x ) <-> ( -u x < ( F ` t ) /\ ( F ` t ) < x ) ) )
90 89 3expa 
 |-  ( ( ( -u x e. RR* /\ x e. RR* ) /\ ( F ` t ) e. RR* ) -> ( ( F ` t ) e. ( -u x (,) x ) <-> ( -u x < ( F ` t ) /\ ( F ` t ) < x ) ) )
91 87 88 90 syl2anr 
 |-  ( ( ( F : A --> RR /\ t e. A ) /\ x e. RR ) -> ( ( F ` t ) e. ( -u x (,) x ) <-> ( -u x < ( F ` t ) /\ ( F ` t ) < x ) ) )
92 81 86 91 3bitr4d 
 |-  ( ( ( F : A --> RR /\ t e. A ) /\ x e. RR ) -> ( ( abs ` ( F ` t ) ) e. ( -oo (,) x ) <-> ( F ` t ) e. ( -u x (,) x ) ) )
93 92 an32s 
 |-  ( ( ( F : A --> RR /\ x e. RR ) /\ t e. A ) -> ( ( abs ` ( F ` t ) ) e. ( -oo (,) x ) <-> ( F ` t ) e. ( -u x (,) x ) ) )
94 93 rabbidva 
 |-  ( ( F : A --> RR /\ x e. RR ) -> { t e. A | ( abs ` ( F ` t ) ) e. ( -oo (,) x ) } = { t e. A | ( F ` t ) e. ( -u x (,) x ) } )
95 60 mptpreima 
 |-  ( `' ( t e. A |-> ( abs ` ( F ` t ) ) ) " ( -oo (,) x ) ) = { t e. A | ( abs ` ( F ` t ) ) e. ( -oo (,) x ) }
96 62 mptpreima 
 |-  ( `' ( t e. A |-> ( F ` t ) ) " ( -u x (,) x ) ) = { t e. A | ( F ` t ) e. ( -u x (,) x ) }
97 94 95 96 3eqtr4g 
 |-  ( ( F : A --> RR /\ x e. RR ) -> ( `' ( t e. A |-> ( abs ` ( F ` t ) ) ) " ( -oo (,) x ) ) = ( `' ( t e. A |-> ( F ` t ) ) " ( -u x (,) x ) ) )
98 67 imaeq1d 
 |-  ( ( F : A --> RR /\ x e. RR ) -> ( `' F " ( -u x (,) x ) ) = ( `' ( t e. A |-> ( F ` t ) ) " ( -u x (,) x ) ) )
99 97 98 eqtr4d 
 |-  ( ( F : A --> RR /\ x e. RR ) -> ( `' ( t e. A |-> ( abs ` ( F ` t ) ) ) " ( -oo (,) x ) ) = ( `' F " ( -u x (,) x ) ) )
100 99 adantlr 
 |-  ( ( ( F : A --> RR /\ F e. MblFn ) /\ x e. RR ) -> ( `' ( t e. A |-> ( abs ` ( F ` t ) ) ) " ( -oo (,) x ) ) = ( `' F " ( -u x (,) x ) ) )
101 mbfima 
 |-  ( ( F e. MblFn /\ F : A --> RR ) -> ( `' F " ( -u x (,) x ) ) e. dom vol )
102 101 ancoms 
 |-  ( ( F : A --> RR /\ F e. MblFn ) -> ( `' F " ( -u x (,) x ) ) e. dom vol )
103 102 adantr 
 |-  ( ( ( F : A --> RR /\ F e. MblFn ) /\ x e. RR ) -> ( `' F " ( -u x (,) x ) ) e. dom vol )
104 100 103 eqeltrd 
 |-  ( ( ( F : A --> RR /\ F e. MblFn ) /\ x e. RR ) -> ( `' ( t e. A |-> ( abs ` ( F ` t ) ) ) " ( -oo (,) x ) ) e. dom vol )
105 13 18 79 104 ismbf2d 
 |-  ( ( F : A --> RR /\ F e. MblFn ) -> ( t e. A |-> ( abs ` ( F ` t ) ) ) e. MblFn )
106 10 105 eqeltrd 
 |-  ( ( F : A --> RR /\ F e. MblFn ) -> ( abs o. F ) e. MblFn )