Metamath Proof Explorer

Theorem ismbl3

Description: The predicate " A is Lebesgue-measurable". Similar to ismbl2 , but here +e is used, and the precondition ( vol*x ) e. RR can be dropped. (Contributed by Glauco Siliprandi, 3-Mar-2021)

Ref Expression
Assertion ismbl3 ( 𝐴 ∈ dom vol ↔ ( 𝐴 ⊆ ℝ ∧ ∀ 𝑥 ∈ 𝒫 ℝ ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) +𝑒 ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) ≤ ( vol* ‘ 𝑥 ) ) )

Proof

Step Hyp Ref Expression
1 ismbl2 ⊢ ( 𝐴 ∈ dom vol ↔ ( 𝐴 ⊆ ℝ ∧ ∀ 𝑥 ∈ 𝒫 ℝ ( ( vol* ‘ 𝑥 ) ∈ ℝ → ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) + ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) ≤ ( vol* ‘ 𝑥 ) ) ) )
2 inss1 ⊢ ( 𝑥 ∩ 𝐴 ) ⊆ 𝑥
3 2 a1i ⊢ ( ( 𝑥 ∈ 𝒫 ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) → ( 𝑥 ∩ 𝐴 ) ⊆ 𝑥 )
4 elpwi ⊢ ( 𝑥 ∈ 𝒫 ℝ → 𝑥 ⊆ ℝ )
5 4 adantr ⊢ ( ( 𝑥 ∈ 𝒫 ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) → 𝑥 ⊆ ℝ )
6 simpr ⊢ ( ( 𝑥 ∈ 𝒫 ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) → ( vol* ‘ 𝑥 ) ∈ ℝ )
7 ovolsscl ⊢ ( ( ( 𝑥 ∩ 𝐴 ) ⊆ 𝑥 ∧ 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) → ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) ∈ ℝ )
8 3 5 6 7 syl3anc ⊢ ( ( 𝑥 ∈ 𝒫 ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) → ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) ∈ ℝ )
9 difssd ⊢ ( ( 𝑥 ∈ 𝒫 ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) → ( 𝑥 ∖ 𝐴 ) ⊆ 𝑥 )
10 ovolsscl ⊢ ( ( ( 𝑥 ∖ 𝐴 ) ⊆ 𝑥 ∧ 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) → ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ∈ ℝ )
11 9 5 6 10 syl3anc ⊢ ( ( 𝑥 ∈ 𝒫 ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) → ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ∈ ℝ )
12 8 11 rexaddd ⊢ ( ( 𝑥 ∈ 𝒫 ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) → ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) +𝑒 ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) = ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) + ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) )
13 12 adantlr ⊢ ( ( ( 𝑥 ∈ 𝒫 ℝ ∧ ( ( vol* ‘ 𝑥 ) ∈ ℝ → ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) + ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) ≤ ( vol* ‘ 𝑥 ) ) ) ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) → ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) +𝑒 ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) = ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) + ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) )
14 id ⊢ ( ( ( vol* ‘ 𝑥 ) ∈ ℝ → ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) + ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) ≤ ( vol* ‘ 𝑥 ) ) → ( ( vol* ‘ 𝑥 ) ∈ ℝ → ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) + ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) ≤ ( vol* ‘ 𝑥 ) ) )
15 14 imp ⊢ ( ( ( ( vol* ‘ 𝑥 ) ∈ ℝ → ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) + ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) ≤ ( vol* ‘ 𝑥 ) ) ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) → ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) + ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) ≤ ( vol* ‘ 𝑥 ) )
16 15 adantll ⊢ ( ( ( 𝑥 ∈ 𝒫 ℝ ∧ ( ( vol* ‘ 𝑥 ) ∈ ℝ → ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) + ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) ≤ ( vol* ‘ 𝑥 ) ) ) ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) → ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) + ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) ≤ ( vol* ‘ 𝑥 ) )
17 13 16 eqbrtrd ⊢ ( ( ( 𝑥 ∈ 𝒫 ℝ ∧ ( ( vol* ‘ 𝑥 ) ∈ ℝ → ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) + ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) ≤ ( vol* ‘ 𝑥 ) ) ) ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) → ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) +𝑒 ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) ≤ ( vol* ‘ 𝑥 ) )
18 2 4 sstrid ⊢ ( 𝑥 ∈ 𝒫 ℝ → ( 𝑥 ∩ 𝐴 ) ⊆ ℝ )
19 ovolcl ⊢ ( ( 𝑥 ∩ 𝐴 ) ⊆ ℝ → ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) ∈ ℝ* )
20 18 19 syl ⊢ ( 𝑥 ∈ 𝒫 ℝ → ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) ∈ ℝ* )
21 4 ssdifssd ⊢ ( 𝑥 ∈ 𝒫 ℝ → ( 𝑥 ∖ 𝐴 ) ⊆ ℝ )
22 ovolcl ⊢ ( ( 𝑥 ∖ 𝐴 ) ⊆ ℝ → ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ∈ ℝ* )
23 21 22 syl ⊢ ( 𝑥 ∈ 𝒫 ℝ → ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ∈ ℝ* )
24 20 23 xaddcld ⊢ ( 𝑥 ∈ 𝒫 ℝ → ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) +𝑒 ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) ∈ ℝ* )
25 pnfge ⊢ ( ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) +𝑒 ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) ∈ ℝ* → ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) +𝑒 ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) ≤ +∞ )
26 24 25 syl ⊢ ( 𝑥 ∈ 𝒫 ℝ → ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) +𝑒 ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) ≤ +∞ )
27 26 adantr ⊢ ( ( 𝑥 ∈ 𝒫 ℝ ∧ ¬ ( vol* ‘ 𝑥 ) ∈ ℝ ) → ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) +𝑒 ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) ≤ +∞ )
28 ovolf ⊢ vol* : 𝒫 ℝ ⟶ ( 0 [,] +∞ )
29 28 ffvelrni ⊢ ( 𝑥 ∈ 𝒫 ℝ → ( vol* ‘ 𝑥 ) ∈ ( 0 [,] +∞ ) )
30 29 adantr ⊢ ( ( 𝑥 ∈ 𝒫 ℝ ∧ ¬ ( vol* ‘ 𝑥 ) ∈ ℝ ) → ( vol* ‘ 𝑥 ) ∈ ( 0 [,] +∞ ) )
31 simpr ⊢ ( ( 𝑥 ∈ 𝒫 ℝ ∧ ¬ ( vol* ‘ 𝑥 ) ∈ ℝ ) → ¬ ( vol* ‘ 𝑥 ) ∈ ℝ )
32 xrge0nre ⊢ ( ( ( vol* ‘ 𝑥 ) ∈ ( 0 [,] +∞ ) ∧ ¬ ( vol* ‘ 𝑥 ) ∈ ℝ ) → ( vol* ‘ 𝑥 ) = +∞ )
33 30 31 32 syl2anc ⊢ ( ( 𝑥 ∈ 𝒫 ℝ ∧ ¬ ( vol* ‘ 𝑥 ) ∈ ℝ ) → ( vol* ‘ 𝑥 ) = +∞ )
34 33 eqcomd ⊢ ( ( 𝑥 ∈ 𝒫 ℝ ∧ ¬ ( vol* ‘ 𝑥 ) ∈ ℝ ) → +∞ = ( vol* ‘ 𝑥 ) )
35 27 34 breqtrd ⊢ ( ( 𝑥 ∈ 𝒫 ℝ ∧ ¬ ( vol* ‘ 𝑥 ) ∈ ℝ ) → ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) +𝑒 ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) ≤ ( vol* ‘ 𝑥 ) )
36 35 adantlr ⊢ ( ( ( 𝑥 ∈ 𝒫 ℝ ∧ ( ( vol* ‘ 𝑥 ) ∈ ℝ → ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) + ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) ≤ ( vol* ‘ 𝑥 ) ) ) ∧ ¬ ( vol* ‘ 𝑥 ) ∈ ℝ ) → ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) +𝑒 ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) ≤ ( vol* ‘ 𝑥 ) )
37 17 36 pm2.61dan ⊢ ( ( 𝑥 ∈ 𝒫 ℝ ∧ ( ( vol* ‘ 𝑥 ) ∈ ℝ → ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) + ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) ≤ ( vol* ‘ 𝑥 ) ) ) → ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) +𝑒 ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) ≤ ( vol* ‘ 𝑥 ) )
38 37 ex ⊢ ( 𝑥 ∈ 𝒫 ℝ → ( ( ( vol* ‘ 𝑥 ) ∈ ℝ → ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) + ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) ≤ ( vol* ‘ 𝑥 ) ) → ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) +𝑒 ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) ≤ ( vol* ‘ 𝑥 ) ) )
39 12 eqcomd ⊢ ( ( 𝑥 ∈ 𝒫 ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) → ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) + ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) = ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) +𝑒 ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) )
40 39 3adant2 ⊢ ( ( 𝑥 ∈ 𝒫 ℝ ∧ ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) +𝑒 ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) ≤ ( vol* ‘ 𝑥 ) ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) → ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) + ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) = ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) +𝑒 ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) )
41 simp2 ⊢ ( ( 𝑥 ∈ 𝒫 ℝ ∧ ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) +𝑒 ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) ≤ ( vol* ‘ 𝑥 ) ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) → ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) +𝑒 ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) ≤ ( vol* ‘ 𝑥 ) )
42 40 41 eqbrtrd ⊢ ( ( 𝑥 ∈ 𝒫 ℝ ∧ ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) +𝑒 ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) ≤ ( vol* ‘ 𝑥 ) ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) → ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) + ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) ≤ ( vol* ‘ 𝑥 ) )
43 42 3exp ⊢ ( 𝑥 ∈ 𝒫 ℝ → ( ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) +𝑒 ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) ≤ ( vol* ‘ 𝑥 ) → ( ( vol* ‘ 𝑥 ) ∈ ℝ → ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) + ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) ≤ ( vol* ‘ 𝑥 ) ) ) )
44 38 43 impbid ⊢ ( 𝑥 ∈ 𝒫 ℝ → ( ( ( vol* ‘ 𝑥 ) ∈ ℝ → ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) + ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) ≤ ( vol* ‘ 𝑥 ) ) ↔ ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) +𝑒 ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) ≤ ( vol* ‘ 𝑥 ) ) )
45 44 ralbiia ⊢ ( ∀ 𝑥 ∈ 𝒫 ℝ ( ( vol* ‘ 𝑥 ) ∈ ℝ → ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) + ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) ≤ ( vol* ‘ 𝑥 ) ) ↔ ∀ 𝑥 ∈ 𝒫 ℝ ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) +𝑒 ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) ≤ ( vol* ‘ 𝑥 ) )
46 45 anbi2i ⊢ ( ( 𝐴 ⊆ ℝ ∧ ∀ 𝑥 ∈ 𝒫 ℝ ( ( vol* ‘ 𝑥 ) ∈ ℝ → ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) + ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) ≤ ( vol* ‘ 𝑥 ) ) ) ↔ ( 𝐴 ⊆ ℝ ∧ ∀ 𝑥 ∈ 𝒫 ℝ ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) +𝑒 ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) ≤ ( vol* ‘ 𝑥 ) ) )
47 1 46 bitri ⊢ ( 𝐴 ∈ dom vol ↔ ( 𝐴 ⊆ ℝ ∧ ∀ 𝑥 ∈ 𝒫 ℝ ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) +𝑒 ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) ≤ ( vol* ‘ 𝑥 ) ) )