Metamath Proof Explorer


Theorem iblabsnclem

Description: Lemma for iblabsnc ; cf. iblabslem . (Contributed by Brendan Leahy, 7-Nov-2017)

Ref Expression
Hypotheses iblabsnc.1 φ x A B V
iblabsnc.2 φ x A B 𝐿 1
iblabsnclem.1 G = x if x A F B 0
iblabsnclem.2 φ x A F B 𝐿 1
iblabsnclem.3 φ x A F B
Assertion iblabsnclem φ G MblFn 2 G

Proof

Step Hyp Ref Expression
1 iblabsnc.1 φ x A B V
2 iblabsnc.2 φ x A B 𝐿 1
3 iblabsnclem.1 G = x if x A F B 0
4 iblabsnclem.2 φ x A F B 𝐿 1
5 iblabsnclem.3 φ x A F B
6 5 iblrelem φ x A F B 𝐿 1 x A F B MblFn 2 x if x A 0 F B F B 0 2 x if x A 0 F B F B 0
7 4 6 mpbid φ x A F B MblFn 2 x if x A 0 F B F B 0 2 x if x A 0 F B F B 0
8 7 simp1d φ x A F B MblFn
9 8 5 mbfdm2 φ A dom vol
10 mblss A dom vol A
11 9 10 syl φ A
12 rembl dom vol
13 12 a1i φ dom vol
14 5 recnd φ x A F B
15 14 abscld φ x A F B
16 0re 0
17 ifcl F B 0 if x A F B 0
18 15 16 17 sylancl φ x A if x A F B 0
19 eldifn x A ¬ x A
20 19 adantl φ x A ¬ x A
21 iffalse ¬ x A if x A F B 0 = 0
22 20 21 syl φ x A if x A F B 0 = 0
23 iftrue x A if x A F B 0 = F B
24 23 mpteq2ia x A if x A F B 0 = x A F B
25 15 fmpttd φ x A F B : A
26 15 adantlr φ y x A F B
27 26 biantrurd φ y x A y < F B F B y < F B
28 5 adantlr φ y x A F B
29 simplr φ y x A y
30 28 29 absled φ y x A F B y y F B F B y
31 30 notbid φ y x A ¬ F B y ¬ y F B F B y
32 29 26 ltnled φ y x A y < F B ¬ F B y
33 renegcl y y
34 33 rexrd y y *
35 34 ad2antlr φ y x A y *
36 elioomnf y * F B −∞ y F B F B < y
37 35 36 syl φ y x A F B −∞ y F B F B < y
38 28 biantrurd φ y x A F B < y F B F B < y
39 29 renegcld φ y x A y
40 28 39 ltnled φ y x A F B < y ¬ y F B
41 37 38 40 3bitr2d φ y x A F B −∞ y ¬ y F B
42 rexr y y *
43 42 ad2antlr φ y x A y *
44 elioopnf y * F B y +∞ F B y < F B
45 43 44 syl φ y x A F B y +∞ F B y < F B
46 28 biantrurd φ y x A y < F B F B y < F B
47 29 28 ltnled φ y x A y < F B ¬ F B y
48 45 46 47 3bitr2d φ y x A F B y +∞ ¬ F B y
49 41 48 orbi12d φ y x A F B −∞ y F B y +∞ ¬ y F B ¬ F B y
50 ianor ¬ y F B F B y ¬ y F B ¬ F B y
51 49 50 bitr4di φ y x A F B −∞ y F B y +∞ ¬ y F B F B y
52 31 32 51 3bitr4rd φ y x A F B −∞ y F B y +∞ y < F B
53 elioopnf y * F B y +∞ F B y < F B
54 43 53 syl φ y x A F B y +∞ F B y < F B
55 27 52 54 3bitr4rd φ y x A F B y +∞ F B −∞ y F B y +∞
56 55 rabbidva φ y x A | F B y +∞ = x A | F B −∞ y F B y +∞
57 eqid x A F B = x A F B
58 57 mptpreima x A F B -1 y +∞ = x A | F B y +∞
59 eqid x A F B = x A F B
60 59 mptpreima x A F B -1 −∞ y = x A | F B −∞ y
61 59 mptpreima x A F B -1 y +∞ = x A | F B y +∞
62 60 61 uneq12i x A F B -1 −∞ y x A F B -1 y +∞ = x A | F B −∞ y x A | F B y +∞
63 unrab x A | F B −∞ y x A | F B y +∞ = x A | F B −∞ y F B y +∞
64 62 63 eqtri x A F B -1 −∞ y x A F B -1 y +∞ = x A | F B −∞ y F B y +∞
65 56 58 64 3eqtr4g φ y x A F B -1 y +∞ = x A F B -1 −∞ y x A F B -1 y +∞
66 iblmbf x A F B 𝐿 1 x A F B MblFn
67 4 66 syl φ x A F B MblFn
68 5 fmpttd φ x A F B : A
69 mbfima x A F B MblFn x A F B : A x A F B -1 −∞ y dom vol
70 mbfima x A F B MblFn x A F B : A x A F B -1 y +∞ dom vol
71 unmbl x A F B -1 −∞ y dom vol x A F B -1 y +∞ dom vol x A F B -1 −∞ y x A F B -1 y +∞ dom vol
72 69 70 71 syl2anc x A F B MblFn x A F B : A x A F B -1 −∞ y x A F B -1 y +∞ dom vol
73 67 68 72 syl2anc φ x A F B -1 −∞ y x A F B -1 y +∞ dom vol
74 73 adantr φ y x A F B -1 −∞ y x A F B -1 y +∞ dom vol
75 65 74 eqeltrd φ y x A F B -1 y +∞ dom vol
76 elioomnf y * F B −∞ y F B F B < y
77 43 76 syl φ y x A F B −∞ y F B F B < y
78 26 biantrurd φ y x A F B < y F B F B < y
79 28 29 absltd φ y x A F B < y y < F B F B < y
80 77 78 79 3bitr2d φ y x A F B −∞ y y < F B F B < y
81 28 biantrurd φ y x A y < F B F B < y F B y < F B F B < y
82 80 81 bitrd φ y x A F B −∞ y F B y < F B F B < y
83 3anass F B y < F B F B < y F B y < F B F B < y
84 82 83 bitr4di φ y x A F B −∞ y F B y < F B F B < y
85 elioo2 y * y * F B y y F B y < F B F B < y
86 34 42 85 syl2anc y F B y y F B y < F B F B < y
87 86 ad2antlr φ y x A F B y y F B y < F B F B < y
88 84 87 bitr4d φ y x A F B −∞ y F B y y
89 88 rabbidva φ y x A | F B −∞ y = x A | F B y y
90 57 mptpreima x A F B -1 −∞ y = x A | F B −∞ y
91 59 mptpreima x A F B -1 y y = x A | F B y y
92 89 90 91 3eqtr4g φ y x A F B -1 −∞ y = x A F B -1 y y
93 mbfima x A F B MblFn x A F B : A x A F B -1 y y dom vol
94 67 68 93 syl2anc φ x A F B -1 y y dom vol
95 94 adantr φ y x A F B -1 y y dom vol
96 92 95 eqeltrd φ y x A F B -1 −∞ y dom vol
97 25 9 75 96 ismbf2d φ x A F B MblFn
98 24 97 eqeltrid φ x A if x A F B 0 MblFn
99 11 13 18 22 98 mbfss φ x if x A F B 0 MblFn
100 3 99 eqeltrid φ G MblFn
101 reex V
102 101 a1i φ V
103 ifan if x A 0 F B F B 0 = if x A if 0 F B F B 0 0
104 ifcl F B 0 if 0 F B F B 0
105 5 16 104 sylancl φ x A if 0 F B F B 0
106 max1 0 F B 0 if 0 F B F B 0
107 16 5 106 sylancr φ x A 0 if 0 F B F B 0
108 elrege0 if 0 F B F B 0 0 +∞ if 0 F B F B 0 0 if 0 F B F B 0
109 105 107 108 sylanbrc φ x A if 0 F B F B 0 0 +∞
110 0e0icopnf 0 0 +∞
111 110 a1i φ ¬ x A 0 0 +∞
112 109 111 ifclda φ if x A if 0 F B F B 0 0 0 +∞
113 103 112 eqeltrid φ if x A 0 F B F B 0 0 +∞
114 113 adantr φ x if x A 0 F B F B 0 0 +∞
115 ifan if x A 0 F B F B 0 = if x A if 0 F B F B 0 0
116 5 renegcld φ x A F B
117 ifcl F B 0 if 0 F B F B 0
118 116 16 117 sylancl φ x A if 0 F B F B 0
119 max1 0 F B 0 if 0 F B F B 0
120 16 116 119 sylancr φ x A 0 if 0 F B F B 0
121 elrege0 if 0 F B F B 0 0 +∞ if 0 F B F B 0 0 if 0 F B F B 0
122 118 120 121 sylanbrc φ x A if 0 F B F B 0 0 +∞
123 122 111 ifclda φ if x A if 0 F B F B 0 0 0 +∞
124 115 123 eqeltrid φ if x A 0 F B F B 0 0 +∞
125 124 adantr φ x if x A 0 F B F B 0 0 +∞
126 eqidd φ x if x A 0 F B F B 0 = x if x A 0 F B F B 0
127 eqidd φ x if x A 0 F B F B 0 = x if x A 0 F B F B 0
128 102 114 125 126 127 offval2 φ x if x A 0 F B F B 0 + f x if x A 0 F B F B 0 = x if x A 0 F B F B 0 + if x A 0 F B F B 0
129 103 115 oveq12i if x A 0 F B F B 0 + if x A 0 F B F B 0 = if x A if 0 F B F B 0 0 + if x A if 0 F B F B 0 0
130 max0add F B if 0 F B F B 0 + if 0 F B F B 0 = F B
131 5 130 syl φ x A if 0 F B F B 0 + if 0 F B F B 0 = F B
132 iftrue x A if x A if 0 F B F B 0 0 = if 0 F B F B 0
133 132 adantl φ x A if x A if 0 F B F B 0 0 = if 0 F B F B 0
134 iftrue x A if x A if 0 F B F B 0 0 = if 0 F B F B 0
135 134 adantl φ x A if x A if 0 F B F B 0 0 = if 0 F B F B 0
136 133 135 oveq12d φ x A if x A if 0 F B F B 0 0 + if x A if 0 F B F B 0 0 = if 0 F B F B 0 + if 0 F B F B 0
137 23 adantl φ x A if x A F B 0 = F B
138 131 136 137 3eqtr4d φ x A if x A if 0 F B F B 0 0 + if x A if 0 F B F B 0 0 = if x A F B 0
139 138 ex φ x A if x A if 0 F B F B 0 0 + if x A if 0 F B F B 0 0 = if x A F B 0
140 00id 0 + 0 = 0
141 iffalse ¬ x A if x A if 0 F B F B 0 0 = 0
142 iffalse ¬ x A if x A if 0 F B F B 0 0 = 0
143 141 142 oveq12d ¬ x A if x A if 0 F B F B 0 0 + if x A if 0 F B F B 0 0 = 0 + 0
144 140 143 21 3eqtr4a ¬ x A if x A if 0 F B F B 0 0 + if x A if 0 F B F B 0 0 = if x A F B 0
145 139 144 pm2.61d1 φ if x A if 0 F B F B 0 0 + if x A if 0 F B F B 0 0 = if x A F B 0
146 129 145 syl5eq φ if x A 0 F B F B 0 + if x A 0 F B F B 0 = if x A F B 0
147 146 mpteq2dv φ x if x A 0 F B F B 0 + if x A 0 F B F B 0 = x if x A F B 0
148 128 147 eqtrd φ x if x A 0 F B F B 0 + f x if x A 0 F B F B 0 = x if x A F B 0
149 3 148 eqtr4id φ G = x if x A 0 F B F B 0 + f x if x A 0 F B F B 0
150 149 fveq2d φ 2 G = 2 x if x A 0 F B F B 0 + f x if x A 0 F B F B 0
151 113 adantr φ x A if x A 0 F B F B 0 0 +∞
152 103 141 syl5eq ¬ x A if x A 0 F B F B 0 = 0
153 20 152 syl φ x A if x A 0 F B F B 0 = 0
154 ibar x A 0 F B x A 0 F B
155 154 ifbid x A if 0 F B F B 0 = if x A 0 F B F B 0
156 155 mpteq2ia x A if 0 F B F B 0 = x A if x A 0 F B F B 0
157 5 8 mbfpos φ x A if 0 F B F B 0 MblFn
158 156 157 eqeltrrid φ x A if x A 0 F B F B 0 MblFn
159 11 13 151 153 158 mbfss φ x if x A 0 F B F B 0 MblFn
160 114 fmpttd φ x if x A 0 F B F B 0 : 0 +∞
161 7 simp2d φ 2 x if x A 0 F B F B 0
162 125 fmpttd φ x if x A 0 F B F B 0 : 0 +∞
163 7 simp3d φ 2 x if x A 0 F B F B 0
164 159 160 161 162 163 itg2addnc φ 2 x if x A 0 F B F B 0 + f x if x A 0 F B F B 0 = 2 x if x A 0 F B F B 0 + 2 x if x A 0 F B F B 0
165 150 164 eqtrd φ 2 G = 2 x if x A 0 F B F B 0 + 2 x if x A 0 F B F B 0
166 161 163 readdcld φ 2 x if x A 0 F B F B 0 + 2 x if x A 0 F B F B 0
167 165 166 eqeltrd φ 2 G
168 100 167 jca φ G MblFn 2 G