Theorem brae

Description: 'almost everywhere' relation for a measure and a measurable set A . (Contributed by Thierry Arnoux, 20-Oct-2017)

	Ref	Expression
Assertion	brae	$$⊢\left(M\in \bigcup \mathrm{ran}\mathrm{measures}\wedge A\in \mathrm{dom}M\right)\to \left(AM\mathrm{-ae.}\leftrightarrow M\left(\bigcup \mathrm{dom}M\setminus A\right)=0\right)$$

Proof

Step	Hyp	Ref	Expression
1		simpr	$$⊢\left(a=A\wedge m=M\right)\to m=M$$
2	1	dmeqd	$$⊢\left(a=A\wedge m=M\right)\to \mathrm{dom}m=\mathrm{dom}M$$
3	2	unieqd	$$⊢\left(a=A\wedge m=M\right)\to \bigcup \mathrm{dom}m=\bigcup \mathrm{dom}M$$
4		simpl	$$⊢\left(a=A\wedge m=M\right)\to a=A$$
5	3 4	difeq12d	$$⊢\left(a=A\wedge m=M\right)\to \bigcup \mathrm{dom}m\setminus a=\bigcup \mathrm{dom}M\setminus A$$
6	1 5	fveq12d	$$⊢\left(a=A\wedge m=M\right)\to m\left(\bigcup \mathrm{dom}m\setminus a\right)=M\left(\bigcup \mathrm{dom}M\setminus A\right)$$
7	6	eqeq1d	$$⊢\left(a=A\wedge m=M\right)\to \left(m\left(\bigcup \mathrm{dom}m\setminus a\right)=0\leftrightarrow M\left(\bigcup \mathrm{dom}M\setminus A\right)=0\right)$$
8		df-ae	$$⊢\mathrm{ae}=\left\{⟨a,m⟩|m\left(\bigcup \mathrm{dom}m\setminus a\right)=0\right\}$$
9	7 8	brabga	$$⊢\left(A\in \mathrm{dom}M\wedge M\in \bigcup \mathrm{ran}\mathrm{measures}\right)\to \left(AM\mathrm{-ae.}\leftrightarrow M\left(\bigcup \mathrm{dom}M\setminus A\right)=0\right)$$
10	9	ancoms	$$⊢\left(M\in \bigcup \mathrm{ran}\mathrm{measures}\wedge A\in \mathrm{dom}M\right)\to \left(AM\mathrm{-ae.}\leftrightarrow M\left(\bigcup \mathrm{dom}M\setminus A\right)=0\right)$$