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

Metamath Proof Explorer

Theorem volres

Description: A self-referencing abbreviated definition of the Lebesgue measure. (Contributed by Mario Carneiro, 19-Mar-2014)

Ref Expression
Assertion volres ⊢ vol = vol * ↾ dom ⁡ vol

Proof

Step Hyp Ref Expression
1 resdmres ⊢ vol * ↾ dom ⁡ vol * ↾ x | ∀ y ∈ vol * -1 ℝ vol * ⁡ y = vol * ⁡ y ∩ x + vol * ⁡ y ∖ x = vol * ↾ x | ∀ y ∈ vol * -1 ℝ vol * ⁡ y = vol * ⁡ y ∩ x + vol * ⁡ y ∖ x
2 df-vol ⊢ vol = vol * ↾ x | ∀ y ∈ vol * -1 ℝ vol * ⁡ y = vol * ⁡ y ∩ x + vol * ⁡ y ∖ x
3 2 dmeqi ⊢ dom ⁡ vol = dom ⁡ vol * ↾ x | ∀ y ∈ vol * -1 ℝ vol * ⁡ y = vol * ⁡ y ∩ x + vol * ⁡ y ∖ x
4 3 reseq2i ⊢ vol * ↾ dom ⁡ vol = vol * ↾ dom ⁡ vol * ↾ x | ∀ y ∈ vol * -1 ℝ vol * ⁡ y = vol * ⁡ y ∩ x + vol * ⁡ y ∖ x
5 1 4 2 3eqtr4ri ⊢ vol = vol * ↾ dom ⁡ vol