Metamath Proof Explorer

Theorem isvonmbl

Description: The predicate " A is measurable w.r.t. the n-dimensional Lebesgue measure". A set is measurable if it splits every other set x in a "nice" way, that is, if the measure of the pieces x i^i A and x \ A sum up to the measure of x . Definition 114E of Fremlin1 p. 25. (Contributed by Glauco Siliprandi, 3-Mar-2021)

Ref Expression
Hypothesis isvonmbl.1 ⊢ ( 𝜑 → 𝑋 ∈ Fin )
Assertion isvonmbl ( 𝜑 → ( 𝐸 ∈ dom ( voln ‘ 𝑋 ) ↔ ( 𝐸 ⊆ ( ℝ ↑m 𝑋 ) ∧ ∀ 𝑎 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ( ( ( voln* ‘ 𝑋 ) ‘ ( 𝑎 ∩ 𝐸 ) ) +e ( ( voln* ‘ 𝑋 ) ‘ ( 𝑎 ∖ 𝐸 ) ) ) = ( ( voln* ‘ 𝑋 ) ‘ 𝑎 ) ) ) )

Proof

Step Hyp Ref Expression
1 isvonmbl.1 ⊢ ( 𝜑 → 𝑋 ∈ Fin )
2 1 dmvon ⊢ ( 𝜑 → dom ( voln ‘ 𝑋 ) = ( CaraGen ‘ ( voln* ‘ 𝑋 ) ) )
3 2 eleq2d ⊢ ( 𝜑 → ( 𝐸 ∈ dom ( voln ‘ 𝑋 ) ↔ 𝐸 ∈ ( CaraGen ‘ ( voln* ‘ 𝑋 ) ) ) )
4 1 ovnome ⊢ ( 𝜑 → ( voln* ‘ 𝑋 ) ∈ OutMeas )
5 eqid ⊢ ( CaraGen ‘ ( voln* ‘ 𝑋 ) ) = ( CaraGen ‘ ( voln* ‘ 𝑋 ) )
6 4 5 caragenel ⊢ ( 𝜑 → ( 𝐸 ∈ ( CaraGen ‘ ( voln* ‘ 𝑋 ) ) ↔ ( 𝐸 ∈ 𝒫 ∪ dom ( voln* ‘ 𝑋 ) ∧ ∀ 𝑎 ∈ 𝒫 ∪ dom ( voln* ‘ 𝑋 ) ( ( ( voln* ‘ 𝑋 ) ‘ ( 𝑎 ∩ 𝐸 ) ) +e ( ( voln* ‘ 𝑋 ) ‘ ( 𝑎 ∖ 𝐸 ) ) ) = ( ( voln* ‘ 𝑋 ) ‘ 𝑎 ) ) ) )
7 elpwi ⊢ ( 𝐸 ∈ 𝒫 ∪ dom ( voln* ‘ 𝑋 ) → 𝐸 ⊆ ∪ dom ( voln* ‘ 𝑋 ) )
8 7 adantl ⊢ ( ( 𝜑 ∧ 𝐸 ∈ 𝒫 ∪ dom ( voln* ‘ 𝑋 ) ) → 𝐸 ⊆ ∪ dom ( voln* ‘ 𝑋 ) )
9 1 unidmovn ⊢ ( 𝜑 → ∪ dom ( voln* ‘ 𝑋 ) = ( ℝ ↑m 𝑋 ) )
10 9 adantr ⊢ ( ( 𝜑 ∧ 𝐸 ∈ 𝒫 ∪ dom ( voln* ‘ 𝑋 ) ) → ∪ dom ( voln* ‘ 𝑋 ) = ( ℝ ↑m 𝑋 ) )
11 8 10 sseqtrd ⊢ ( ( 𝜑 ∧ 𝐸 ∈ 𝒫 ∪ dom ( voln* ‘ 𝑋 ) ) → 𝐸 ⊆ ( ℝ ↑m 𝑋 ) )
12 11 ex ⊢ ( 𝜑 → ( 𝐸 ∈ 𝒫 ∪ dom ( voln* ‘ 𝑋 ) → 𝐸 ⊆ ( ℝ ↑m 𝑋 ) ) )
13 simpr ⊢ ( ( 𝜑 ∧ 𝐸 ⊆ ( ℝ ↑m 𝑋 ) ) → 𝐸 ⊆ ( ℝ ↑m 𝑋 ) )
14 9 eqcomd ⊢ ( 𝜑 → ( ℝ ↑m 𝑋 ) = ∪ dom ( voln* ‘ 𝑋 ) )
15 14 adantr ⊢ ( ( 𝜑 ∧ 𝐸 ⊆ ( ℝ ↑m 𝑋 ) ) → ( ℝ ↑m 𝑋 ) = ∪ dom ( voln* ‘ 𝑋 ) )
16 13 15 sseqtrd ⊢ ( ( 𝜑 ∧ 𝐸 ⊆ ( ℝ ↑m 𝑋 ) ) → 𝐸 ⊆ ∪ dom ( voln* ‘ 𝑋 ) )
17 ovex ⊢ ( ℝ ↑m 𝑋 ) ∈ V
18 17 ssex ⊢ ( 𝐸 ⊆ ( ℝ ↑m 𝑋 ) → 𝐸 ∈ V )
19 elpwg ⊢ ( 𝐸 ∈ V → ( 𝐸 ∈ 𝒫 ∪ dom ( voln* ‘ 𝑋 ) ↔ 𝐸 ⊆ ∪ dom ( voln* ‘ 𝑋 ) ) )
20 18 19 syl ⊢ ( 𝐸 ⊆ ( ℝ ↑m 𝑋 ) → ( 𝐸 ∈ 𝒫 ∪ dom ( voln* ‘ 𝑋 ) ↔ 𝐸 ⊆ ∪ dom ( voln* ‘ 𝑋 ) ) )
21 20 adantl ⊢ ( ( 𝜑 ∧ 𝐸 ⊆ ( ℝ ↑m 𝑋 ) ) → ( 𝐸 ∈ 𝒫 ∪ dom ( voln* ‘ 𝑋 ) ↔ 𝐸 ⊆ ∪ dom ( voln* ‘ 𝑋 ) ) )
22 16 21 mpbird ⊢ ( ( 𝜑 ∧ 𝐸 ⊆ ( ℝ ↑m 𝑋 ) ) → 𝐸 ∈ 𝒫 ∪ dom ( voln* ‘ 𝑋 ) )
23 22 ex ⊢ ( 𝜑 → ( 𝐸 ⊆ ( ℝ ↑m 𝑋 ) → 𝐸 ∈ 𝒫 ∪ dom ( voln* ‘ 𝑋 ) ) )
24 12 23 impbid ⊢ ( 𝜑 → ( 𝐸 ∈ 𝒫 ∪ dom ( voln* ‘ 𝑋 ) ↔ 𝐸 ⊆ ( ℝ ↑m 𝑋 ) ) )
25 9 pweqd ⊢ ( 𝜑 → 𝒫 ∪ dom ( voln* ‘ 𝑋 ) = 𝒫 ( ℝ ↑m 𝑋 ) )
26 raleq ⊢ ( 𝒫 ∪ dom ( voln* ‘ 𝑋 ) = 𝒫 ( ℝ ↑m 𝑋 ) → ( ∀ 𝑎 ∈ 𝒫 ∪ dom ( voln* ‘ 𝑋 ) ( ( ( voln* ‘ 𝑋 ) ‘ ( 𝑎 ∩ 𝐸 ) ) +e ( ( voln* ‘ 𝑋 ) ‘ ( 𝑎 ∖ 𝐸 ) ) ) = ( ( voln* ‘ 𝑋 ) ‘ 𝑎 ) ↔ ∀ 𝑎 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ( ( ( voln* ‘ 𝑋 ) ‘ ( 𝑎 ∩ 𝐸 ) ) +e ( ( voln* ‘ 𝑋 ) ‘ ( 𝑎 ∖ 𝐸 ) ) ) = ( ( voln* ‘ 𝑋 ) ‘ 𝑎 ) ) )
27 25 26 syl ⊢ ( 𝜑 → ( ∀ 𝑎 ∈ 𝒫 ∪ dom ( voln* ‘ 𝑋 ) ( ( ( voln* ‘ 𝑋 ) ‘ ( 𝑎 ∩ 𝐸 ) ) +e ( ( voln* ‘ 𝑋 ) ‘ ( 𝑎 ∖ 𝐸 ) ) ) = ( ( voln* ‘ 𝑋 ) ‘ 𝑎 ) ↔ ∀ 𝑎 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ( ( ( voln* ‘ 𝑋 ) ‘ ( 𝑎 ∩ 𝐸 ) ) +e ( ( voln* ‘ 𝑋 ) ‘ ( 𝑎 ∖ 𝐸 ) ) ) = ( ( voln* ‘ 𝑋 ) ‘ 𝑎 ) ) )
28 24 27 anbi12d ⊢ ( 𝜑 → ( ( 𝐸 ∈ 𝒫 ∪ dom ( voln* ‘ 𝑋 ) ∧ ∀ 𝑎 ∈ 𝒫 ∪ dom ( voln* ‘ 𝑋 ) ( ( ( voln* ‘ 𝑋 ) ‘ ( 𝑎 ∩ 𝐸 ) ) +e ( ( voln* ‘ 𝑋 ) ‘ ( 𝑎 ∖ 𝐸 ) ) ) = ( ( voln* ‘ 𝑋 ) ‘ 𝑎 ) ) ↔ ( 𝐸 ⊆ ( ℝ ↑m 𝑋 ) ∧ ∀ 𝑎 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ( ( ( voln* ‘ 𝑋 ) ‘ ( 𝑎 ∩ 𝐸 ) ) +e ( ( voln* ‘ 𝑋 ) ‘ ( 𝑎 ∖ 𝐸 ) ) ) = ( ( voln* ‘ 𝑋 ) ‘ 𝑎 ) ) ) )
29 3 6 28 3bitrd ⊢ ( 𝜑 → ( 𝐸 ∈ dom ( voln ‘ 𝑋 ) ↔ ( 𝐸 ⊆ ( ℝ ↑m 𝑋 ) ∧ ∀ 𝑎 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ( ( ( voln* ‘ 𝑋 ) ‘ ( 𝑎 ∩ 𝐸 ) ) +e ( ( voln* ‘ 𝑋 ) ‘ ( 𝑎 ∖ 𝐸 ) ) ) = ( ( voln* ‘ 𝑋 ) ‘ 𝑎 ) ) ) )