Theorem meale0eq0

Description: A measure that is less than or equal to 0 is 0 . (Contributed by Glauco Siliprandi, 8-Apr-2021)

	Ref	Expression
Hypotheses	meale0eq0.m	$$⊢\phi \to M\in \mathrm{Meas}$$
	meale0eq0.a	$$⊢\phi \to A\in \mathrm{dom}M$$
	meale0eq0.l	$$⊢\phi \to M\left(A\right)\le 0$$
Assertion	meale0eq0	$$⊢\phi \to M\left(A\right)=0$$

Proof

Step	Hyp	Ref	Expression
1		meale0eq0.m	$$⊢\phi \to M\in \mathrm{Meas}$$
2		meale0eq0.a	$$⊢\phi \to A\in \mathrm{dom}M$$
3		meale0eq0.l	$$⊢\phi \to M\left(A\right)\le 0$$
4		eqid	$$⊢\mathrm{dom}M=\mathrm{dom}M$$
5	1 4 2	meaxrcl	$$⊢\phi \to M\left(A\right)\in {ℝ}^{*}$$
6		0xr	$$⊢0\in {ℝ}^{*}$$
7	6	a1i	$$⊢\phi \to 0\in {ℝ}^{*}$$
8	1 2	meage0	$$⊢\phi \to 0\le M\left(A\right)$$
9	5 7 3 8	xrletrid	$$⊢\phi \to M\left(A\right)=0$$