This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-vol

Description: Define the Lebesgue measure, which is just the outer measure with a peculiar domain of definition. The property of being Lebesgue-measurable can be expressed as A e. dom vol . (Contributed by Mario Carneiro, 17-Mar-2014)

Ref Expression
Assertion df-vol vol = ( vol* ↾ { 𝑥 ∣ ∀ 𝑦 ∈ ( ◡ vol* “ ℝ ) ( vol* ‘ 𝑦 ) = ( ( vol* ‘ ( 𝑦 ∩ 𝑥 ) ) + ( vol* ‘ ( 𝑦 ∖ 𝑥 ) ) ) } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cvol ⊢ vol
1 covol ⊢ vol*
2 vx ⊢ 𝑥
3 vy ⊢ 𝑦
4 1 ccnv ⊢ ◡ vol*
5 cr ⊢ ℝ
6 4 5 cima ⊢ ( ◡ vol* “ ℝ )
7 3 cv ⊢ 𝑦
8 7 1 cfv ⊢ ( vol* ‘ 𝑦 )
9 2 cv ⊢ 𝑥
10 7 9 cin ⊢ ( 𝑦 ∩ 𝑥 )
11 10 1 cfv ⊢ ( vol* ‘ ( 𝑦 ∩ 𝑥 ) )
12 caddc ⊢ +
13 7 9 cdif ⊢ ( 𝑦 ∖ 𝑥 )
14 13 1 cfv ⊢ ( vol* ‘ ( 𝑦 ∖ 𝑥 ) )
15 11 14 12 co ⊢ ( ( vol* ‘ ( 𝑦 ∩ 𝑥 ) ) + ( vol* ‘ ( 𝑦 ∖ 𝑥 ) ) )
16 8 15 wceq ⊢ ( vol* ‘ 𝑦 ) = ( ( vol* ‘ ( 𝑦 ∩ 𝑥 ) ) + ( vol* ‘ ( 𝑦 ∖ 𝑥 ) ) )
17 16 3 6 wral ⊢ ∀ 𝑦 ∈ ( ◡ vol* “ ℝ ) ( vol* ‘ 𝑦 ) = ( ( vol* ‘ ( 𝑦 ∩ 𝑥 ) ) + ( vol* ‘ ( 𝑦 ∖ 𝑥 ) ) )
18 17 2 cab ⊢ { 𝑥 ∣ ∀ 𝑦 ∈ ( ◡ vol* “ ℝ ) ( vol* ‘ 𝑦 ) = ( ( vol* ‘ ( 𝑦 ∩ 𝑥 ) ) + ( vol* ‘ ( 𝑦 ∖ 𝑥 ) ) ) }
19 1 18 cres ⊢ ( vol* ↾ { 𝑥 ∣ ∀ 𝑦 ∈ ( ◡ vol* “ ℝ ) ( vol* ‘ 𝑦 ) = ( ( vol* ‘ ( 𝑦 ∩ 𝑥 ) ) + ( vol* ‘ ( 𝑦 ∖ 𝑥 ) ) ) } )
20 0 19 wceq ⊢ vol = ( vol* ↾ { 𝑥 ∣ ∀ 𝑦 ∈ ( ◡ vol* “ ℝ ) ( vol* ‘ 𝑦 ) = ( ( vol* ‘ ( 𝑦 ∩ 𝑥 ) ) + ( vol* ‘ ( 𝑦 ∖ 𝑥 ) ) ) } )