Metamath Proof Explorer

Theorem volmea

Description: The Lebesgue measure on the Reals is actually a measure. (Contributed by Glauco Siliprandi, 3-Mar-2021)

Ref Expression
Assertion volmea ⊢ φ → vol ∈ Meas

Proof

Step Hyp Ref Expression
1 dmvolsal ⊢ dom ⁡ vol ∈ SAlg
2 1 a1i ⊢ φ → dom ⁡ vol ∈ SAlg
3 volf ⊢ vol : dom ⁡ vol ⟶ 0 +∞
4 3 a1i ⊢ φ → vol : dom ⁡ vol ⟶ 0 +∞
5 vol0 ⊢ vol ⁡ ∅ = 0
6 5 a1i ⊢ φ → vol ⁡ ∅ = 0
7 simp1 ⊢ φ ∧ e : ℕ ⟶ dom ⁡ vol ∧ Disj n ∈ ℕ e ⁡ n → φ
8 simp2 ⊢ φ ∧ e : ℕ ⟶ dom ⁡ vol ∧ Disj n ∈ ℕ e ⁡ n → e : ℕ ⟶ dom ⁡ vol
9 fveq2 ⊢ m = n → e ⁡ m = e ⁡ n
10 9 cbvdisjv ⊢ Disj m ∈ ℕ e ⁡ m ↔ Disj n ∈ ℕ e ⁡ n
11 10 biimpri ⊢ Disj n ∈ ℕ e ⁡ n → Disj m ∈ ℕ e ⁡ m
12 11 3ad2ant3 ⊢ φ ∧ e : ℕ ⟶ dom ⁡ vol ∧ Disj n ∈ ℕ e ⁡ n → Disj m ∈ ℕ e ⁡ m
13 simp2 ⊢ φ ∧ e : ℕ ⟶ dom ⁡ vol ∧ Disj m ∈ ℕ e ⁡ m → e : ℕ ⟶ dom ⁡ vol
14 10 biimpi ⊢ Disj m ∈ ℕ e ⁡ m → Disj n ∈ ℕ e ⁡ n
15 14 3ad2ant3 ⊢ φ ∧ e : ℕ ⟶ dom ⁡ vol ∧ Disj m ∈ ℕ e ⁡ m → Disj n ∈ ℕ e ⁡ n
16 13 15 voliunsge0 ⊢ φ ∧ e : ℕ ⟶ dom ⁡ vol ∧ Disj m ∈ ℕ e ⁡ m → vol ⁡ ⋃ n ∈ ℕ e ⁡ n = sum^ ⁡ n ∈ ℕ ⟼ vol ⁡ e ⁡ n
17 7 8 12 16 syl3anc ⊢ φ ∧ e : ℕ ⟶ dom ⁡ vol ∧ Disj n ∈ ℕ e ⁡ n → vol ⁡ ⋃ n ∈ ℕ e ⁡ n = sum^ ⁡ n ∈ ℕ ⟼ vol ⁡ e ⁡ n
18 2 4 6 17 ismeannd ⊢ φ → vol ∈ Meas