Metamath Proof Explorer

Theorem ismbl2

Description: From ovolun , it suffices to show that the measure of x is at least the sum of the measures of x i^i A and x \ A . (Contributed by Mario Carneiro, 15-Jun-2014)

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

Proof

Step Hyp Ref Expression
1 ismbl ⊢ ( 𝐴 ∈ dom vol ↔ ( 𝐴 ⊆ ℝ ∧ ∀ 𝑥 ∈ 𝒫 ℝ ( ( vol* ‘ 𝑥 ) ∈ ℝ → ( vol* ‘ 𝑥 ) = ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) + ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) ) ) )
2 elpwi ⊢ ( 𝑥 ∈ 𝒫 ℝ → 𝑥 ⊆ ℝ )
3 inundif ⊢ ( ( 𝑥 ∩ 𝐴 ) ∪ ( 𝑥 ∖ 𝐴 ) ) = 𝑥
4 3 fveq2i ⊢ ( vol* ‘ ( ( 𝑥 ∩ 𝐴 ) ∪ ( 𝑥 ∖ 𝐴 ) ) ) = ( vol* ‘ 𝑥 )
5 inss1 ⊢ ( 𝑥 ∩ 𝐴 ) ⊆ 𝑥
6 simprl ⊢ ( ( 𝐴 ⊆ ℝ ∧ ( 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) ) → 𝑥 ⊆ ℝ )
7 5 6 sstrid ⊢ ( ( 𝐴 ⊆ ℝ ∧ ( 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) ) → ( 𝑥 ∩ 𝐴 ) ⊆ ℝ )
8 ovolsscl ⊢ ( ( ( 𝑥 ∩ 𝐴 ) ⊆ 𝑥 ∧ 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) → ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) ∈ ℝ )
9 5 8 mp3an1 ⊢ ( ( 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) → ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) ∈ ℝ )
10 9 adantl ⊢ ( ( 𝐴 ⊆ ℝ ∧ ( 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) ) → ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) ∈ ℝ )
11 difss ⊢ ( 𝑥 ∖ 𝐴 ) ⊆ 𝑥
12 11 6 sstrid ⊢ ( ( 𝐴 ⊆ ℝ ∧ ( 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) ) → ( 𝑥 ∖ 𝐴 ) ⊆ ℝ )
13 ovolsscl ⊢ ( ( ( 𝑥 ∖ 𝐴 ) ⊆ 𝑥 ∧ 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) → ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ∈ ℝ )
14 11 13 mp3an1 ⊢ ( ( 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) → ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ∈ ℝ )
15 14 adantl ⊢ ( ( 𝐴 ⊆ ℝ ∧ ( 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) ) → ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ∈ ℝ )
16 ovolun ⊢ ( ( ( ( 𝑥 ∩ 𝐴 ) ⊆ ℝ ∧ ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) ∈ ℝ ) ∧ ( ( 𝑥 ∖ 𝐴 ) ⊆ ℝ ∧ ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ∈ ℝ ) ) → ( vol* ‘ ( ( 𝑥 ∩ 𝐴 ) ∪ ( 𝑥 ∖ 𝐴 ) ) ) ≤ ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) + ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) )
17 7 10 12 15 16 syl22anc ⊢ ( ( 𝐴 ⊆ ℝ ∧ ( 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) ) → ( vol* ‘ ( ( 𝑥 ∩ 𝐴 ) ∪ ( 𝑥 ∖ 𝐴 ) ) ) ≤ ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) + ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) )
18 4 17 eqbrtrrid ⊢ ( ( 𝐴 ⊆ ℝ ∧ ( 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) ) → ( vol* ‘ 𝑥 ) ≤ ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) + ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) )
19 simprr ⊢ ( ( 𝐴 ⊆ ℝ ∧ ( 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) ) → ( vol* ‘ 𝑥 ) ∈ ℝ )
20 10 15 readdcld ⊢ ( ( 𝐴 ⊆ ℝ ∧ ( 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) ) → ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) + ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) ∈ ℝ )
21 19 20 letri3d ⊢ ( ( 𝐴 ⊆ ℝ ∧ ( 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) ) → ( ( vol* ‘ 𝑥 ) = ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) + ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) ↔ ( ( vol* ‘ 𝑥 ) ≤ ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) + ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) ∧ ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) + ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) ≤ ( vol* ‘ 𝑥 ) ) ) )
22 18 21 mpbirand ⊢ ( ( 𝐴 ⊆ ℝ ∧ ( 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) ) → ( ( vol* ‘ 𝑥 ) = ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) + ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) ↔ ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) + ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) ≤ ( vol* ‘ 𝑥 ) ) )
23 22 expr ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝑥 ⊆ ℝ ) → ( ( vol* ‘ 𝑥 ) ∈ ℝ → ( ( vol* ‘ 𝑥 ) = ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) + ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) ↔ ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) + ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) ≤ ( vol* ‘ 𝑥 ) ) ) )
24 23 pm5.74d ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝑥 ⊆ ℝ ) → ( ( ( vol* ‘ 𝑥 ) ∈ ℝ → ( vol* ‘ 𝑥 ) = ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) + ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) ) ↔ ( ( vol* ‘ 𝑥 ) ∈ ℝ → ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) + ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) ≤ ( vol* ‘ 𝑥 ) ) ) )
25 2 24 sylan2 ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝑥 ∈ 𝒫 ℝ ) → ( ( ( vol* ‘ 𝑥 ) ∈ ℝ → ( vol* ‘ 𝑥 ) = ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) + ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) ) ↔ ( ( vol* ‘ 𝑥 ) ∈ ℝ → ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) + ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) ≤ ( vol* ‘ 𝑥 ) ) ) )
26 25 ralbidva ⊢ ( 𝐴 ⊆ ℝ → ( ∀ 𝑥 ∈ 𝒫 ℝ ( ( vol* ‘ 𝑥 ) ∈ ℝ → ( vol* ‘ 𝑥 ) = ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) + ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) ) ↔ ∀ 𝑥 ∈ 𝒫 ℝ ( ( vol* ‘ 𝑥 ) ∈ ℝ → ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) + ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) ≤ ( vol* ‘ 𝑥 ) ) ) )
27 26 pm5.32i ⊢ ( ( 𝐴 ⊆ ℝ ∧ ∀ 𝑥 ∈ 𝒫 ℝ ( ( vol* ‘ 𝑥 ) ∈ ℝ → ( vol* ‘ 𝑥 ) = ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) + ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) ) ) ↔ ( 𝐴 ⊆ ℝ ∧ ∀ 𝑥 ∈ 𝒫 ℝ ( ( vol* ‘ 𝑥 ) ∈ ℝ → ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) + ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) ≤ ( vol* ‘ 𝑥 ) ) ) )
28 1 27 bitri ⊢ ( 𝐴 ∈ dom vol ↔ ( 𝐴 ⊆ ℝ ∧ ∀ 𝑥 ∈ 𝒫 ℝ ( ( vol* ‘ 𝑥 ) ∈ ℝ → ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) + ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) ≤ ( vol* ‘ 𝑥 ) ) ) )