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	⊢ ( ( 𝜑 ∧ 𝑒 : ℕ ⟶ dom vol ∧ Disj 𝑛 ∈ ℕ ( 𝑒 ‘ 𝑛 ) ) → 𝜑 )
8		simp2	⊢ ( ( 𝜑 ∧ 𝑒 : ℕ ⟶ dom vol ∧ Disj 𝑛 ∈ ℕ ( 𝑒 ‘ 𝑛 ) ) → 𝑒 : ℕ ⟶ dom vol )
9		fveq2	⊢ ( 𝑚 = 𝑛 → ( 𝑒 ‘ 𝑚 ) = ( 𝑒 ‘ 𝑛 ) )
10	9	cbvdisjv	⊢ ( Disj 𝑚 ∈ ℕ ( 𝑒 ‘ 𝑚 ) ↔ Disj 𝑛 ∈ ℕ ( 𝑒 ‘ 𝑛 ) )
11	10	biimpri	⊢ ( Disj 𝑛 ∈ ℕ ( 𝑒 ‘ 𝑛 ) → Disj 𝑚 ∈ ℕ ( 𝑒 ‘ 𝑚 ) )
12	11	3ad2ant3	⊢ ( ( 𝜑 ∧ 𝑒 : ℕ ⟶ dom vol ∧ Disj 𝑛 ∈ ℕ ( 𝑒 ‘ 𝑛 ) ) → Disj 𝑚 ∈ ℕ ( 𝑒 ‘ 𝑚 ) )
13		simp2	⊢ ( ( 𝜑 ∧ 𝑒 : ℕ ⟶ dom vol ∧ Disj 𝑚 ∈ ℕ ( 𝑒 ‘ 𝑚 ) ) → 𝑒 : ℕ ⟶ dom vol )
14	10	biimpi	⊢ ( Disj 𝑚 ∈ ℕ ( 𝑒 ‘ 𝑚 ) → Disj 𝑛 ∈ ℕ ( 𝑒 ‘ 𝑛 ) )
15	14	3ad2ant3	⊢ ( ( 𝜑 ∧ 𝑒 : ℕ ⟶ dom vol ∧ Disj 𝑚 ∈ ℕ ( 𝑒 ‘ 𝑚 ) ) → Disj 𝑛 ∈ ℕ ( 𝑒 ‘ 𝑛 ) )
16	13 15	voliunsge0	⊢ ( ( 𝜑 ∧ 𝑒 : ℕ ⟶ dom vol ∧ Disj 𝑚 ∈ ℕ ( 𝑒 ‘ 𝑚 ) ) → ( vol ‘ ∪ 𝑛 ∈ ℕ ( 𝑒 ‘ 𝑛 ) ) = ( Σ^ ‘ ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( 𝑒 ‘ 𝑛 ) ) ) ) )
17	7 8 12 16	syl3anc	⊢ ( ( 𝜑 ∧ 𝑒 : ℕ ⟶ dom vol ∧ Disj 𝑛 ∈ ℕ ( 𝑒 ‘ 𝑛 ) ) → ( vol ‘ ∪ 𝑛 ∈ ℕ ( 𝑒 ‘ 𝑛 ) ) = ( Σ^ ‘ ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( 𝑒 ‘ 𝑛 ) ) ) ) )
18	2 4 6 17	ismeannd	⊢ ( 𝜑 → vol ∈ Meas )