Metamath Proof Explorer

Theorem brfae

Description: 'almost everywhere' relation for two functions F and G with regard to the measure M . (Contributed by Thierry Arnoux, 22-Oct-2017)

Ref Expression
Hypotheses brfae.0 
|- dom R = D
brfae.1 
|- ( ph -> R e. _V )
brfae.2 
|- ( ph -> M e. U. ran measures )
brfae.3 
|- ( ph -> F e. ( D ^m U. dom M ) )
brfae.4 
|- ( ph -> G e. ( D ^m U. dom M ) )
Assertion brfae 
|- ( ph -> ( F ( R ~ae M ) G <-> { x e. U. dom M | ( F ` x ) R ( G ` x ) } ae M ) )

Proof

Step Hyp Ref Expression
1 brfae.0 
 |-  dom R = D
2 brfae.1 
 |-  ( ph -> R e. _V )
3 brfae.2 
 |-  ( ph -> M e. U. ran measures )
4 brfae.3 
 |-  ( ph -> F e. ( D ^m U. dom M ) )
5 brfae.4 
 |-  ( ph -> G e. ( D ^m U. dom M ) )
6 simpl 
 |-  ( ( f = F /\ g = G ) -> f = F )
7 6 eleq1d 
 |-  ( ( f = F /\ g = G ) -> ( f e. ( dom R ^m U. dom M ) <-> F e. ( dom R ^m U. dom M ) ) )
8 simpr 
 |-  ( ( f = F /\ g = G ) -> g = G )
9 8 eleq1d 
 |-  ( ( f = F /\ g = G ) -> ( g e. ( dom R ^m U. dom M ) <-> G e. ( dom R ^m U. dom M ) ) )
10 7 9 anbi12d 
 |-  ( ( f = F /\ g = G ) -> ( ( f e. ( dom R ^m U. dom M ) /\ g e. ( dom R ^m U. dom M ) ) <-> ( F e. ( dom R ^m U. dom M ) /\ G e. ( dom R ^m U. dom M ) ) ) )
11 6 fveq1d 
 |-  ( ( f = F /\ g = G ) -> ( f ` x ) = ( F ` x ) )
12 8 fveq1d 
 |-  ( ( f = F /\ g = G ) -> ( g ` x ) = ( G ` x ) )
13 11 12 breq12d 
 |-  ( ( f = F /\ g = G ) -> ( ( f ` x ) R ( g ` x ) <-> ( F ` x ) R ( G ` x ) ) )
14 13 rabbidv 
 |-  ( ( f = F /\ g = G ) -> { x e. U. dom M | ( f ` x ) R ( g ` x ) } = { x e. U. dom M | ( F ` x ) R ( G ` x ) } )
15 14 breq1d 
 |-  ( ( f = F /\ g = G ) -> ( { x e. U. dom M | ( f ` x ) R ( g ` x ) } ae M <-> { x e. U. dom M | ( F ` x ) R ( G ` x ) } ae M ) )
16 10 15 anbi12d 
 |-  ( ( f = F /\ g = G ) -> ( ( ( f e. ( dom R ^m U. dom M ) /\ g e. ( dom R ^m U. dom M ) ) /\ { x e. U. dom M | ( f ` x ) R ( g ` x ) } ae M ) <-> ( ( F e. ( dom R ^m U. dom M ) /\ G e. ( dom R ^m U. dom M ) ) /\ { x e. U. dom M | ( F ` x ) R ( G ` x ) } ae M ) ) )
17 eqid 
 |-  { <. f , g >. | ( ( f e. ( dom R ^m U. dom M ) /\ g e. ( dom R ^m U. dom M ) ) /\ { x e. U. dom M | ( f ` x ) R ( g ` x ) } ae M ) } = { <. f , g >. | ( ( f e. ( dom R ^m U. dom M ) /\ g e. ( dom R ^m U. dom M ) ) /\ { x e. U. dom M | ( f ` x ) R ( g ` x ) } ae M ) }
18 16 17 brabga 
 |-  ( ( F e. ( D ^m U. dom M ) /\ G e. ( D ^m U. dom M ) ) -> ( F { <. f , g >. | ( ( f e. ( dom R ^m U. dom M ) /\ g e. ( dom R ^m U. dom M ) ) /\ { x e. U. dom M | ( f ` x ) R ( g ` x ) } ae M ) } G <-> ( ( F e. ( dom R ^m U. dom M ) /\ G e. ( dom R ^m U. dom M ) ) /\ { x e. U. dom M | ( F ` x ) R ( G ` x ) } ae M ) ) )
19 4 5 18 syl2anc 
 |-  ( ph -> ( F { <. f , g >. | ( ( f e. ( dom R ^m U. dom M ) /\ g e. ( dom R ^m U. dom M ) ) /\ { x e. U. dom M | ( f ` x ) R ( g ` x ) } ae M ) } G <-> ( ( F e. ( dom R ^m U. dom M ) /\ G e. ( dom R ^m U. dom M ) ) /\ { x e. U. dom M | ( F ` x ) R ( G ` x ) } ae M ) ) )
20 faeval 
 |-  ( ( R e. _V /\ M e. U. ran measures ) -> ( R ~ae M ) = { <. f , g >. | ( ( f e. ( dom R ^m U. dom M ) /\ g e. ( dom R ^m U. dom M ) ) /\ { x e. U. dom M | ( f ` x ) R ( g ` x ) } ae M ) } )
21 2 3 20 syl2anc 
 |-  ( ph -> ( R ~ae M ) = { <. f , g >. | ( ( f e. ( dom R ^m U. dom M ) /\ g e. ( dom R ^m U. dom M ) ) /\ { x e. U. dom M | ( f ` x ) R ( g ` x ) } ae M ) } )
22 21 breqd 
 |-  ( ph -> ( F ( R ~ae M ) G <-> F { <. f , g >. | ( ( f e. ( dom R ^m U. dom M ) /\ g e. ( dom R ^m U. dom M ) ) /\ { x e. U. dom M | ( f ` x ) R ( g ` x ) } ae M ) } G ) )
23 1 oveq1i 
 |-  ( dom R ^m U. dom M ) = ( D ^m U. dom M )
24 4 23 eleqtrrdi 
 |-  ( ph -> F e. ( dom R ^m U. dom M ) )
25 5 23 eleqtrrdi 
 |-  ( ph -> G e. ( dom R ^m U. dom M ) )
26 24 25 jca 
 |-  ( ph -> ( F e. ( dom R ^m U. dom M ) /\ G e. ( dom R ^m U. dom M ) ) )
27 26 biantrurd 
 |-  ( ph -> ( { x e. U. dom M | ( F ` x ) R ( G ` x ) } ae M <-> ( ( F e. ( dom R ^m U. dom M ) /\ G e. ( dom R ^m U. dom M ) ) /\ { x e. U. dom M | ( F ` x ) R ( G ` x ) } ae M ) ) )
28 19 22 27 3bitr4d 
 |-  ( ph -> ( F ( R ~ae M ) G <-> { x e. U. dom M | ( F ` x ) R ( G ` x ) } ae M ) )