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 F MblFn abs F MblFn

Proof

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