Metamath Proof Explorer

Theorem ismbl4

Description: The predicate " A is Lebesgue-measurable". Similar to ismbl , 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 ismbl4 ( 𝐴 ∈ dom vol ↔ ( 𝐴 ⊆ ℝ ∧ ∀ 𝑥 ∈ 𝒫 ℝ ( vol* ‘ 𝑥 ) = ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) +𝑒 ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 ismbl3 ⊢ ( 𝐴 ∈ dom vol ↔ ( 𝐴 ⊆ ℝ ∧ ∀ 𝑥 ∈ 𝒫 ℝ ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) +𝑒 ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) ≤ ( vol* ‘ 𝑥 ) ) )
2 elpwi ⊢ ( 𝑥 ∈ 𝒫 ℝ → 𝑥 ⊆ ℝ )
3 ovolcl ⊢ ( 𝑥 ⊆ ℝ → ( vol* ‘ 𝑥 ) ∈ ℝ* )
4 2 3 syl ⊢ ( 𝑥 ∈ 𝒫 ℝ → ( vol* ‘ 𝑥 ) ∈ ℝ* )
5 4 adantr ⊢ ( ( 𝑥 ∈ 𝒫 ℝ ∧ ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) +𝑒 ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) ≤ ( vol* ‘ 𝑥 ) ) → ( vol* ‘ 𝑥 ) ∈ ℝ* )
6 inss1 ⊢ ( 𝑥 ∩ 𝐴 ) ⊆ 𝑥
7 6 2 sstrid ⊢ ( 𝑥 ∈ 𝒫 ℝ → ( 𝑥 ∩ 𝐴 ) ⊆ ℝ )
8 ovolcl ⊢ ( ( 𝑥 ∩ 𝐴 ) ⊆ ℝ → ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) ∈ ℝ* )
9 7 8 syl ⊢ ( 𝑥 ∈ 𝒫 ℝ → ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) ∈ ℝ* )
10 2 ssdifssd ⊢ ( 𝑥 ∈ 𝒫 ℝ → ( 𝑥 ∖ 𝐴 ) ⊆ ℝ )
11 ovolcl ⊢ ( ( 𝑥 ∖ 𝐴 ) ⊆ ℝ → ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ∈ ℝ* )
12 10 11 syl ⊢ ( 𝑥 ∈ 𝒫 ℝ → ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ∈ ℝ* )
13 9 12 xaddcld ⊢ ( 𝑥 ∈ 𝒫 ℝ → ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) +𝑒 ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) ∈ ℝ* )
14 13 adantr ⊢ ( ( 𝑥 ∈ 𝒫 ℝ ∧ ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) +𝑒 ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) ≤ ( vol* ‘ 𝑥 ) ) → ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) +𝑒 ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) ∈ ℝ* )
15 2 ovolsplit ⊢ ( 𝑥 ∈ 𝒫 ℝ → ( vol* ‘ 𝑥 ) ≤ ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) +𝑒 ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) )
16 15 adantr ⊢ ( ( 𝑥 ∈ 𝒫 ℝ ∧ ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) +𝑒 ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) ≤ ( vol* ‘ 𝑥 ) ) → ( vol* ‘ 𝑥 ) ≤ ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) +𝑒 ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) )
17 simpr ⊢ ( ( 𝑥 ∈ 𝒫 ℝ ∧ ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) +𝑒 ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) ≤ ( vol* ‘ 𝑥 ) ) → ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) +𝑒 ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) ≤ ( vol* ‘ 𝑥 ) )
18 5 14 16 17 xrletrid ⊢ ( ( 𝑥 ∈ 𝒫 ℝ ∧ ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) +𝑒 ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) ≤ ( vol* ‘ 𝑥 ) ) → ( vol* ‘ 𝑥 ) = ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) +𝑒 ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) )
19 18 ex ⊢ ( 𝑥 ∈ 𝒫 ℝ → ( ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) +𝑒 ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) ≤ ( vol* ‘ 𝑥 ) → ( vol* ‘ 𝑥 ) = ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) +𝑒 ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) ) )
20 13 xrleidd ⊢ ( 𝑥 ∈ 𝒫 ℝ → ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) +𝑒 ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) ≤ ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) +𝑒 ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) )
21 20 adantr ⊢ ( ( 𝑥 ∈ 𝒫 ℝ ∧ ( vol* ‘ 𝑥 ) = ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) +𝑒 ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) ) → ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) +𝑒 ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) ≤ ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) +𝑒 ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) )
22 id ⊢ ( ( vol* ‘ 𝑥 ) = ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) +𝑒 ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) → ( vol* ‘ 𝑥 ) = ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) +𝑒 ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) )
23 22 eqcomd ⊢ ( ( vol* ‘ 𝑥 ) = ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) +𝑒 ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) → ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) +𝑒 ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) = ( vol* ‘ 𝑥 ) )
24 23 adantl ⊢ ( ( 𝑥 ∈ 𝒫 ℝ ∧ ( vol* ‘ 𝑥 ) = ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) +𝑒 ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) ) → ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) +𝑒 ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) = ( vol* ‘ 𝑥 ) )
25 21 24 breqtrd ⊢ ( ( 𝑥 ∈ 𝒫 ℝ ∧ ( vol* ‘ 𝑥 ) = ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) +𝑒 ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) ) → ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) +𝑒 ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) ≤ ( vol* ‘ 𝑥 ) )
26 25 ex ⊢ ( 𝑥 ∈ 𝒫 ℝ → ( ( vol* ‘ 𝑥 ) = ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) +𝑒 ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) → ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) +𝑒 ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) ≤ ( vol* ‘ 𝑥 ) ) )
27 19 26 impbid ⊢ ( 𝑥 ∈ 𝒫 ℝ → ( ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) +𝑒 ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) ≤ ( vol* ‘ 𝑥 ) ↔ ( vol* ‘ 𝑥 ) = ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) +𝑒 ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) ) )
28 27 ralbiia ⊢ ( ∀ 𝑥 ∈ 𝒫 ℝ ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) +𝑒 ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) ≤ ( vol* ‘ 𝑥 ) ↔ ∀ 𝑥 ∈ 𝒫 ℝ ( vol* ‘ 𝑥 ) = ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) +𝑒 ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) )
29 28 anbi2i ⊢ ( ( 𝐴 ⊆ ℝ ∧ ∀ 𝑥 ∈ 𝒫 ℝ ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) +𝑒 ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) ≤ ( vol* ‘ 𝑥 ) ) ↔ ( 𝐴 ⊆ ℝ ∧ ∀ 𝑥 ∈ 𝒫 ℝ ( vol* ‘ 𝑥 ) = ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) +𝑒 ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) ) )
30 1 29 bitri ⊢ ( 𝐴 ∈ dom vol ↔ ( 𝐴 ⊆ ℝ ∧ ∀ 𝑥 ∈ 𝒫 ℝ ( vol* ‘ 𝑥 ) = ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) +𝑒 ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) ) )