brae

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

		Ref	Expression
	Assertion	brae	$⊢ (M \in ⋃ ran measures \land A \in dom M) \to (A M -ae. \leftrightarrow M (⋃ dom M ∖ A) = 0)$

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

Metamath Proof Explorer