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	⊢ ( ( 𝑀 ∈ ∪ ran measures ∧ 𝐴 ∈ dom 𝑀 ) → ( 𝐴 a.e. 𝑀 ↔ ( 𝑀 ‘ ( ∪ dom 𝑀 ∖ 𝐴 ) ) = 0 ) )

Proof

Step	Hyp	Ref	Expression
1		simpr	⊢ ( ( 𝑎 = 𝐴 ∧ 𝑚 = 𝑀 ) → 𝑚 = 𝑀 )
2	1	dmeqd	⊢ ( ( 𝑎 = 𝐴 ∧ 𝑚 = 𝑀 ) → dom 𝑚 = dom 𝑀 )
3	2	unieqd	⊢ ( ( 𝑎 = 𝐴 ∧ 𝑚 = 𝑀 ) → ∪ dom 𝑚 = ∪ dom 𝑀 )
4		simpl	⊢ ( ( 𝑎 = 𝐴 ∧ 𝑚 = 𝑀 ) → 𝑎 = 𝐴 )
5	3 4	difeq12d	⊢ ( ( 𝑎 = 𝐴 ∧ 𝑚 = 𝑀 ) → ( ∪ dom 𝑚 ∖ 𝑎 ) = ( ∪ dom 𝑀 ∖ 𝐴 ) )
6	1 5	fveq12d	⊢ ( ( 𝑎 = 𝐴 ∧ 𝑚 = 𝑀 ) → ( 𝑚 ‘ ( ∪ dom 𝑚 ∖ 𝑎 ) ) = ( 𝑀 ‘ ( ∪ dom 𝑀 ∖ 𝐴 ) ) )
7	6	eqeq1d	⊢ ( ( 𝑎 = 𝐴 ∧ 𝑚 = 𝑀 ) → ( ( 𝑚 ‘ ( ∪ dom 𝑚 ∖ 𝑎 ) ) = 0 ↔ ( 𝑀 ‘ ( ∪ dom 𝑀 ∖ 𝐴 ) ) = 0 ) )
8		df-ae	⊢ a.e. = { ⟨ 𝑎 , 𝑚 ⟩ ∣ ( 𝑚 ‘ ( ∪ dom 𝑚 ∖ 𝑎 ) ) = 0 }
9	7 8	brabga	⊢ ( ( 𝐴 ∈ dom 𝑀 ∧ 𝑀 ∈ ∪ ran measures ) → ( 𝐴 a.e. 𝑀 ↔ ( 𝑀 ‘ ( ∪ dom 𝑀 ∖ 𝐴 ) ) = 0 ) )
10	9	ancoms	⊢ ( ( 𝑀 ∈ ∪ ran measures ∧ 𝐴 ∈ dom 𝑀 ) → ( 𝐴 a.e. 𝑀 ↔ ( 𝑀 ‘ ( ∪ dom 𝑀 ∖ 𝐴 ) ) = 0 ) )