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	|- ( ph -> M e. Meas )
	meale0eq0.a	|- ( ph -> A e. dom M )
	meale0eq0.l	|- ( ph -> ( M ` A ) <_ 0 )
Assertion	meale0eq0	|- ( ph -> ( M ` A ) = 0 )

Proof

Step	Hyp	Ref	Expression
1		meale0eq0.m	|- ( ph -> M e. Meas )
2		meale0eq0.a	|- ( ph -> A e. dom M )
3		meale0eq0.l	|- ( ph -> ( M ` A ) <_ 0 )
4		eqid	|- dom M = dom M
5	1 4 2	meaxrcl	|- ( ph -> ( M ` A ) e. RR* )
6		0xr	|- 0 e. RR*
7	6	a1i	|- ( ph -> 0 e. RR* )
8	1 2	meage0	|- ( ph -> 0 <_ ( M ` A ) )
9	5 7 3 8	xrletrid	|- ( ph -> ( M ` A ) = 0 )