Metamath Proof Explorer

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 
|- ( ( M e. U. ran measures /\ A e. dom M ) -> ( A ae M <-> ( M ` ( U. dom M \ A ) ) = 0 ) )

Proof

Step Hyp Ref Expression
1 simpr 
 |-  ( ( a = A /\ m = M ) -> m = M )
2 1 dmeqd 
 |-  ( ( a = A /\ m = M ) -> dom m = dom M )
3 2 unieqd 
 |-  ( ( a = A /\ m = M ) -> U. dom m = U. dom M )
4 simpl 
 |-  ( ( a = A /\ m = M ) -> a = A )
5 3 4 difeq12d 
 |-  ( ( a = A /\ m = M ) -> ( U. dom m \ a ) = ( U. dom M \ A ) )
6 1 5 fveq12d 
 |-  ( ( a = A /\ m = M ) -> ( m ` ( U. dom m \ a ) ) = ( M ` ( U. dom M \ A ) ) )
7 6 eqeq1d 
 |-  ( ( a = A /\ m = M ) -> ( ( m ` ( U. dom m \ a ) ) = 0 <-> ( M ` ( U. dom M \ A ) ) = 0 ) )
8 df-ae 
 |-  ae = { <. a , m >. | ( m ` ( U. dom m \ a ) ) = 0 }
9 7 8 brabga 
 |-  ( ( A e. dom M /\ M e. U. ran measures ) -> ( A ae M <-> ( M ` ( U. dom M \ A ) ) = 0 ) )
10 9 ancoms 
 |-  ( ( M e. U. ran measures /\ A e. dom M ) -> ( A ae M <-> ( M ` ( U. dom M \ A ) ) = 0 ) )