Theorem mea0

Description: The measure of the empty set is always 0 . (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Hypothesis	mea0.1	⊢ ( 𝜑 → 𝑀 ∈ Meas )
Assertion	mea0	⊢ ( 𝜑 → ( 𝑀 ‘ ∅ ) = 0 )

Proof

Step	Hyp	Ref	Expression
1		mea0.1	⊢ ( 𝜑 → 𝑀 ∈ Meas )
2		ismea	⊢ ( 𝑀 ∈ Meas ↔ ( ( ( 𝑀 : dom 𝑀 ⟶ ( 0 [,] +∞ ) ∧ dom 𝑀 ∈ SAlg ) ∧ ( 𝑀 ‘ ∅ ) = 0 ) ∧ ∀ 𝑥 ∈ 𝒫 dom 𝑀 ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ( 𝑀 ‘ ∪ 𝑥 ) = ( Σ^ ‘ ( 𝑀 ↾ 𝑥 ) ) ) ) )
3	1 2	sylib	⊢ ( 𝜑 → ( ( ( 𝑀 : dom 𝑀 ⟶ ( 0 [,] +∞ ) ∧ dom 𝑀 ∈ SAlg ) ∧ ( 𝑀 ‘ ∅ ) = 0 ) ∧ ∀ 𝑥 ∈ 𝒫 dom 𝑀 ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ( 𝑀 ‘ ∪ 𝑥 ) = ( Σ^ ‘ ( 𝑀 ↾ 𝑥 ) ) ) ) )
4	3	simplrd	⊢ ( 𝜑 → ( 𝑀 ‘ ∅ ) = 0 )