Metamath Proof Explorer

Theorem itgcn

Description: Transfer itg2cn to the full Lebesgue integral. (Contributed by Mario Carneiro, 1-Sep-2014)

Ref Expression
Hypotheses itgcn.1 ⊢ φ ∧ x ∈ A → B ∈ V
itgcn.2 ⊢ φ → x ∈ A ⟼ B ∈ 𝐿 1
itgcn.3 ⊢ φ → C ∈ ℝ +
Assertion itgcn ⊢ φ → ∃ d ∈ ℝ + ∀ u ∈ dom ⁡ vol u ⊆ A ∧ vol ⁡ u < d → ∫ u B dx < C

Proof

Step Hyp Ref Expression
1 itgcn.1 ⊢ φ ∧ x ∈ A → B ∈ V
2 itgcn.2 ⊢ φ → x ∈ A ⟼ B ∈ 𝐿 1
3 itgcn.3 ⊢ φ → C ∈ ℝ +
4 iblmbf ⊢ x ∈ A ⟼ B ∈ 𝐿 1 → x ∈ A ⟼ B ∈ MblFn
5 2 4 syl ⊢ φ → x ∈ A ⟼ B ∈ MblFn
6 5 1 mbfmptcl ⊢ φ ∧ x ∈ A → B ∈ ℂ
7 6 abscld ⊢ φ ∧ x ∈ A → B ∈ ℝ
8 6 absge0d ⊢ φ ∧ x ∈ A → 0 ≤ B
9 elrege0 ⊢ B ∈ 0 +∞ ↔ B ∈ ℝ ∧ 0 ≤ B
10 7 8 9 sylanbrc ⊢ φ ∧ x ∈ A → B ∈ 0 +∞
11 0e0icopnf ⊢ 0 ∈ 0 +∞
12 11 a1i ⊢ φ ∧ ¬ x ∈ A → 0 ∈ 0 +∞
13 10 12 ifclda ⊢ φ → if x ∈ A B 0 ∈ 0 +∞
14 13 adantr ⊢ φ ∧ x ∈ ℝ → if x ∈ A B 0 ∈ 0 +∞
15 14 fmpttd ⊢ φ → x ∈ ℝ ⟼ if x ∈ A B 0 : ℝ ⟶ 0 +∞
16 5 1 mbfdm2 ⊢ φ → A ∈ dom ⁡ vol
17 mblss ⊢ A ∈ dom ⁡ vol → A ⊆ ℝ
18 16 17 syl ⊢ φ → A ⊆ ℝ
19 rembl ⊢ ℝ ∈ dom ⁡ vol
20 19 a1i ⊢ φ → ℝ ∈ dom ⁡ vol
21 13 adantr ⊢ φ ∧ x ∈ A → if x ∈ A B 0 ∈ 0 +∞
22 eldifn ⊢ x ∈ ℝ ∖ A → ¬ x ∈ A
23 22 adantl ⊢ φ ∧ x ∈ ℝ ∖ A → ¬ x ∈ A
24 23 iffalsed ⊢ φ ∧ x ∈ ℝ ∖ A → if x ∈ A B 0 = 0
25 iftrue ⊢ x ∈ A → if x ∈ A B 0 = B
26 25 mpteq2ia ⊢ x ∈ A ⟼ if x ∈ A B 0 = x ∈ A ⟼ B
27 1 2 iblabs ⊢ φ → x ∈ A ⟼ B ∈ 𝐿 1
28 7 8 iblpos ⊢ φ → x ∈ A ⟼ B ∈ 𝐿 1 ↔ x ∈ A ⟼ B ∈ MblFn ∧ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A B 0 ∈ ℝ
29 27 28 mpbid ⊢ φ → x ∈ A ⟼ B ∈ MblFn ∧ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A B 0 ∈ ℝ
30 29 simpld ⊢ φ → x ∈ A ⟼ B ∈ MblFn
31 26 30 eqeltrid ⊢ φ → x ∈ A ⟼ if x ∈ A B 0 ∈ MblFn
32 18 20 21 24 31 mbfss ⊢ φ → x ∈ ℝ ⟼ if x ∈ A B 0 ∈ MblFn
33 29 simprd ⊢ φ → ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A B 0 ∈ ℝ
34 15 32 33 3 itg2cn ⊢ φ → ∃ d ∈ ℝ + ∀ u ∈ dom ⁡ vol vol ⁡ u < d → ∫ 2 ⁡ y ∈ ℝ ⟼ if y ∈ u x ∈ ℝ ⟼ if x ∈ A B 0 ⁡ y 0 < C
35 simprr ⊢ φ ∧ u ∈ dom ⁡ vol ∧ u ⊆ A → u ⊆ A
36 35 sselda ⊢ φ ∧ u ∈ dom ⁡ vol ∧ u ⊆ A ∧ x ∈ u → x ∈ A
37 6 adantlr ⊢ φ ∧ u ∈ dom ⁡ vol ∧ u ⊆ A ∧ x ∈ A → B ∈ ℂ
38 36 37 syldan ⊢ φ ∧ u ∈ dom ⁡ vol ∧ u ⊆ A ∧ x ∈ u → B ∈ ℂ
39 38 abscld ⊢ φ ∧ u ∈ dom ⁡ vol ∧ u ⊆ A ∧ x ∈ u → B ∈ ℝ
40 simprl ⊢ φ ∧ u ∈ dom ⁡ vol ∧ u ⊆ A → u ∈ dom ⁡ vol
41 37 abscld ⊢ φ ∧ u ∈ dom ⁡ vol ∧ u ⊆ A ∧ x ∈ A → B ∈ ℝ
42 27 adantr ⊢ φ ∧ u ∈ dom ⁡ vol ∧ u ⊆ A → x ∈ A ⟼ B ∈ 𝐿 1
43 35 40 41 42 iblss ⊢ φ ∧ u ∈ dom ⁡ vol ∧ u ⊆ A → x ∈ u ⟼ B ∈ 𝐿 1
44 38 absge0d ⊢ φ ∧ u ∈ dom ⁡ vol ∧ u ⊆ A ∧ x ∈ u → 0 ≤ B
45 39 43 44 itgposval ⊢ φ ∧ u ∈ dom ⁡ vol ∧ u ⊆ A → ∫ u B dx = ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ u B 0
46 35 sseld ⊢ φ ∧ u ∈ dom ⁡ vol ∧ u ⊆ A → x ∈ u → x ∈ A
47 46 pm4.71d ⊢ φ ∧ u ∈ dom ⁡ vol ∧ u ⊆ A → x ∈ u ↔ x ∈ u ∧ x ∈ A
48 47 ifbid ⊢ φ ∧ u ∈ dom ⁡ vol ∧ u ⊆ A → if x ∈ u B 0 = if x ∈ u ∧ x ∈ A B 0
49 ifan ⊢ if x ∈ u ∧ x ∈ A B 0 = if x ∈ u if x ∈ A B 0 0
50 48 49 eqtrdi ⊢ φ ∧ u ∈ dom ⁡ vol ∧ u ⊆ A → if x ∈ u B 0 = if x ∈ u if x ∈ A B 0 0
51 50 mpteq2dv ⊢ φ ∧ u ∈ dom ⁡ vol ∧ u ⊆ A → x ∈ ℝ ⟼ if x ∈ u B 0 = x ∈ ℝ ⟼ if x ∈ u if x ∈ A B 0 0
52 51 fveq2d ⊢ φ ∧ u ∈ dom ⁡ vol ∧ u ⊆ A → ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ u B 0 = ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ u if x ∈ A B 0 0
53 45 52 eqtrd ⊢ φ ∧ u ∈ dom ⁡ vol ∧ u ⊆ A → ∫ u B dx = ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ u if x ∈ A B 0 0
54 nfv ⊢ Ⅎ x y ∈ u
55 nffvmpt1 ⊢ Ⅎ _ x x ∈ ℝ ⟼ if x ∈ A B 0 ⁡ y
56 nfcv ⊢ Ⅎ _ x 0
57 54 55 56 nfif ⊢ Ⅎ _ x if y ∈ u x ∈ ℝ ⟼ if x ∈ A B 0 ⁡ y 0
58 nfcv ⊢ Ⅎ _ y if x ∈ u x ∈ ℝ ⟼ if x ∈ A B 0 ⁡ x 0
59 elequ1 ⊢ y = x → y ∈ u ↔ x ∈ u
60 fveq2 ⊢ y = x → x ∈ ℝ ⟼ if x ∈ A B 0 ⁡ y = x ∈ ℝ ⟼ if x ∈ A B 0 ⁡ x
61 59 60 ifbieq1d ⊢ y = x → if y ∈ u x ∈ ℝ ⟼ if x ∈ A B 0 ⁡ y 0 = if x ∈ u x ∈ ℝ ⟼ if x ∈ A B 0 ⁡ x 0
62 57 58 61 cbvmpt ⊢ y ∈ ℝ ⟼ if y ∈ u x ∈ ℝ ⟼ if x ∈ A B 0 ⁡ y 0 = x ∈ ℝ ⟼ if x ∈ u x ∈ ℝ ⟼ if x ∈ A B 0 ⁡ x 0
63 fvex ⊢ B ∈ V
64 c0ex ⊢ 0 ∈ V
65 63 64 ifex ⊢ if x ∈ A B 0 ∈ V
66 eqid ⊢ x ∈ ℝ ⟼ if x ∈ A B 0 = x ∈ ℝ ⟼ if x ∈ A B 0
67 66 fvmpt2 ⊢ x ∈ ℝ ∧ if x ∈ A B 0 ∈ V → x ∈ ℝ ⟼ if x ∈ A B 0 ⁡ x = if x ∈ A B 0
68 65 67 mpan2 ⊢ x ∈ ℝ → x ∈ ℝ ⟼ if x ∈ A B 0 ⁡ x = if x ∈ A B 0
69 68 ifeq1d ⊢ x ∈ ℝ → if x ∈ u x ∈ ℝ ⟼ if x ∈ A B 0 ⁡ x 0 = if x ∈ u if x ∈ A B 0 0
70 69 mpteq2ia ⊢ x ∈ ℝ ⟼ if x ∈ u x ∈ ℝ ⟼ if x ∈ A B 0 ⁡ x 0 = x ∈ ℝ ⟼ if x ∈ u if x ∈ A B 0 0
71 62 70 eqtri ⊢ y ∈ ℝ ⟼ if y ∈ u x ∈ ℝ ⟼ if x ∈ A B 0 ⁡ y 0 = x ∈ ℝ ⟼ if x ∈ u if x ∈ A B 0 0
72 71 fveq2i ⊢ ∫ 2 ⁡ y ∈ ℝ ⟼ if y ∈ u x ∈ ℝ ⟼ if x ∈ A B 0 ⁡ y 0 = ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ u if x ∈ A B 0 0
73 53 72 eqtr4di ⊢ φ ∧ u ∈ dom ⁡ vol ∧ u ⊆ A → ∫ u B dx = ∫ 2 ⁡ y ∈ ℝ ⟼ if y ∈ u x ∈ ℝ ⟼ if x ∈ A B 0 ⁡ y 0
74 73 breq1d ⊢ φ ∧ u ∈ dom ⁡ vol ∧ u ⊆ A → ∫ u B dx < C ↔ ∫ 2 ⁡ y ∈ ℝ ⟼ if y ∈ u x ∈ ℝ ⟼ if x ∈ A B 0 ⁡ y 0 < C
75 74 biimprd ⊢ φ ∧ u ∈ dom ⁡ vol ∧ u ⊆ A → ∫ 2 ⁡ y ∈ ℝ ⟼ if y ∈ u x ∈ ℝ ⟼ if x ∈ A B 0 ⁡ y 0 < C → ∫ u B dx < C
76 75 imim2d ⊢ φ ∧ u ∈ dom ⁡ vol ∧ u ⊆ A → vol ⁡ u < d → ∫ 2 ⁡ y ∈ ℝ ⟼ if y ∈ u x ∈ ℝ ⟼ if x ∈ A B 0 ⁡ y 0 < C → vol ⁡ u < d → ∫ u B dx < C
77 76 expr ⊢ φ ∧ u ∈ dom ⁡ vol → u ⊆ A → vol ⁡ u < d → ∫ 2 ⁡ y ∈ ℝ ⟼ if y ∈ u x ∈ ℝ ⟼ if x ∈ A B 0 ⁡ y 0 < C → vol ⁡ u < d → ∫ u B dx < C
78 77 com23 ⊢ φ ∧ u ∈ dom ⁡ vol → vol ⁡ u < d → ∫ 2 ⁡ y ∈ ℝ ⟼ if y ∈ u x ∈ ℝ ⟼ if x ∈ A B 0 ⁡ y 0 < C → u ⊆ A → vol ⁡ u < d → ∫ u B dx < C
79 78 imp4a ⊢ φ ∧ u ∈ dom ⁡ vol → vol ⁡ u < d → ∫ 2 ⁡ y ∈ ℝ ⟼ if y ∈ u x ∈ ℝ ⟼ if x ∈ A B 0 ⁡ y 0 < C → u ⊆ A ∧ vol ⁡ u < d → ∫ u B dx < C
80 79 ralimdva ⊢ φ → ∀ u ∈ dom ⁡ vol vol ⁡ u < d → ∫ 2 ⁡ y ∈ ℝ ⟼ if y ∈ u x ∈ ℝ ⟼ if x ∈ A B 0 ⁡ y 0 < C → ∀ u ∈ dom ⁡ vol u ⊆ A ∧ vol ⁡ u < d → ∫ u B dx < C
81 80 reximdv ⊢ φ → ∃ d ∈ ℝ + ∀ u ∈ dom ⁡ vol vol ⁡ u < d → ∫ 2 ⁡ y ∈ ℝ ⟼ if y ∈ u x ∈ ℝ ⟼ if x ∈ A B 0 ⁡ y 0 < C → ∃ d ∈ ℝ + ∀ u ∈ dom ⁡ vol u ⊆ A ∧ vol ⁡ u < d → ∫ u B dx < C
82 34 81 mpd ⊢ φ → ∃ d ∈ ℝ + ∀ u ∈ dom ⁡ vol u ⊆ A ∧ vol ⁡ u < d → ∫ u B dx < C