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 𝑅 = 𝐷
brfae.1 ( 𝜑𝑅 ∈ V )
brfae.2 ( 𝜑𝑀 ran measures )
brfae.3 ( 𝜑𝐹 ∈ ( 𝐷m dom 𝑀 ) )
brfae.4 ( 𝜑𝐺 ∈ ( 𝐷m dom 𝑀 ) )
Assertion brfae ( 𝜑 → ( 𝐹 ( 𝑅 ~ a.e. 𝑀 ) 𝐺 ↔ { 𝑥 dom 𝑀 ∣ ( 𝐹𝑥 ) 𝑅 ( 𝐺𝑥 ) } a.e. 𝑀 ) )

Proof

Step Hyp Ref Expression
1 brfae.0 dom 𝑅 = 𝐷
2 brfae.1 ( 𝜑𝑅 ∈ V )
3 brfae.2 ( 𝜑𝑀 ran measures )
4 brfae.3 ( 𝜑𝐹 ∈ ( 𝐷m dom 𝑀 ) )
5 brfae.4 ( 𝜑𝐺 ∈ ( 𝐷m dom 𝑀 ) )
6 simpl ( ( 𝑓 = 𝐹𝑔 = 𝐺 ) → 𝑓 = 𝐹 )
7 6 eleq1d ( ( 𝑓 = 𝐹𝑔 = 𝐺 ) → ( 𝑓 ∈ ( dom 𝑅m dom 𝑀 ) ↔ 𝐹 ∈ ( dom 𝑅m dom 𝑀 ) ) )
8 simpr ( ( 𝑓 = 𝐹𝑔 = 𝐺 ) → 𝑔 = 𝐺 )
9 8 eleq1d ( ( 𝑓 = 𝐹𝑔 = 𝐺 ) → ( 𝑔 ∈ ( dom 𝑅m dom 𝑀 ) ↔ 𝐺 ∈ ( dom 𝑅m dom 𝑀 ) ) )
10 7 9 anbi12d ( ( 𝑓 = 𝐹𝑔 = 𝐺 ) → ( ( 𝑓 ∈ ( dom 𝑅m dom 𝑀 ) ∧ 𝑔 ∈ ( dom 𝑅m dom 𝑀 ) ) ↔ ( 𝐹 ∈ ( dom 𝑅m dom 𝑀 ) ∧ 𝐺 ∈ ( dom 𝑅m dom 𝑀 ) ) ) )
11 6 fveq1d ( ( 𝑓 = 𝐹𝑔 = 𝐺 ) → ( 𝑓𝑥 ) = ( 𝐹𝑥 ) )
12 8 fveq1d ( ( 𝑓 = 𝐹𝑔 = 𝐺 ) → ( 𝑔𝑥 ) = ( 𝐺𝑥 ) )
13 11 12 breq12d ( ( 𝑓 = 𝐹𝑔 = 𝐺 ) → ( ( 𝑓𝑥 ) 𝑅 ( 𝑔𝑥 ) ↔ ( 𝐹𝑥 ) 𝑅 ( 𝐺𝑥 ) ) )
14 13 rabbidv ( ( 𝑓 = 𝐹𝑔 = 𝐺 ) → { 𝑥 dom 𝑀 ∣ ( 𝑓𝑥 ) 𝑅 ( 𝑔𝑥 ) } = { 𝑥 dom 𝑀 ∣ ( 𝐹𝑥 ) 𝑅 ( 𝐺𝑥 ) } )
15 14 breq1d ( ( 𝑓 = 𝐹𝑔 = 𝐺 ) → ( { 𝑥 dom 𝑀 ∣ ( 𝑓𝑥 ) 𝑅 ( 𝑔𝑥 ) } a.e. 𝑀 ↔ { 𝑥 dom 𝑀 ∣ ( 𝐹𝑥 ) 𝑅 ( 𝐺𝑥 ) } a.e. 𝑀 ) )
16 10 15 anbi12d ( ( 𝑓 = 𝐹𝑔 = 𝐺 ) → ( ( ( 𝑓 ∈ ( dom 𝑅m dom 𝑀 ) ∧ 𝑔 ∈ ( dom 𝑅m dom 𝑀 ) ) ∧ { 𝑥 dom 𝑀 ∣ ( 𝑓𝑥 ) 𝑅 ( 𝑔𝑥 ) } a.e. 𝑀 ) ↔ ( ( 𝐹 ∈ ( dom 𝑅m dom 𝑀 ) ∧ 𝐺 ∈ ( dom 𝑅m dom 𝑀 ) ) ∧ { 𝑥 dom 𝑀 ∣ ( 𝐹𝑥 ) 𝑅 ( 𝐺𝑥 ) } a.e. 𝑀 ) ) )
17 eqid { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( ( 𝑓 ∈ ( dom 𝑅m dom 𝑀 ) ∧ 𝑔 ∈ ( dom 𝑅m dom 𝑀 ) ) ∧ { 𝑥 dom 𝑀 ∣ ( 𝑓𝑥 ) 𝑅 ( 𝑔𝑥 ) } a.e. 𝑀 ) } = { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( ( 𝑓 ∈ ( dom 𝑅m dom 𝑀 ) ∧ 𝑔 ∈ ( dom 𝑅m dom 𝑀 ) ) ∧ { 𝑥 dom 𝑀 ∣ ( 𝑓𝑥 ) 𝑅 ( 𝑔𝑥 ) } a.e. 𝑀 ) }
18 16 17 brabga ( ( 𝐹 ∈ ( 𝐷m dom 𝑀 ) ∧ 𝐺 ∈ ( 𝐷m dom 𝑀 ) ) → ( 𝐹 { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( ( 𝑓 ∈ ( dom 𝑅m dom 𝑀 ) ∧ 𝑔 ∈ ( dom 𝑅m dom 𝑀 ) ) ∧ { 𝑥 dom 𝑀 ∣ ( 𝑓𝑥 ) 𝑅 ( 𝑔𝑥 ) } a.e. 𝑀 ) } 𝐺 ↔ ( ( 𝐹 ∈ ( dom 𝑅m dom 𝑀 ) ∧ 𝐺 ∈ ( dom 𝑅m dom 𝑀 ) ) ∧ { 𝑥 dom 𝑀 ∣ ( 𝐹𝑥 ) 𝑅 ( 𝐺𝑥 ) } a.e. 𝑀 ) ) )
19 4 5 18 syl2anc ( 𝜑 → ( 𝐹 { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( ( 𝑓 ∈ ( dom 𝑅m dom 𝑀 ) ∧ 𝑔 ∈ ( dom 𝑅m dom 𝑀 ) ) ∧ { 𝑥 dom 𝑀 ∣ ( 𝑓𝑥 ) 𝑅 ( 𝑔𝑥 ) } a.e. 𝑀 ) } 𝐺 ↔ ( ( 𝐹 ∈ ( dom 𝑅m dom 𝑀 ) ∧ 𝐺 ∈ ( dom 𝑅m dom 𝑀 ) ) ∧ { 𝑥 dom 𝑀 ∣ ( 𝐹𝑥 ) 𝑅 ( 𝐺𝑥 ) } a.e. 𝑀 ) ) )
20 faeval ( ( 𝑅 ∈ V ∧ 𝑀 ran measures ) → ( 𝑅 ~ a.e. 𝑀 ) = { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( ( 𝑓 ∈ ( dom 𝑅m dom 𝑀 ) ∧ 𝑔 ∈ ( dom 𝑅m dom 𝑀 ) ) ∧ { 𝑥 dom 𝑀 ∣ ( 𝑓𝑥 ) 𝑅 ( 𝑔𝑥 ) } a.e. 𝑀 ) } )
21 2 3 20 syl2anc ( 𝜑 → ( 𝑅 ~ a.e. 𝑀 ) = { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( ( 𝑓 ∈ ( dom 𝑅m dom 𝑀 ) ∧ 𝑔 ∈ ( dom 𝑅m dom 𝑀 ) ) ∧ { 𝑥 dom 𝑀 ∣ ( 𝑓𝑥 ) 𝑅 ( 𝑔𝑥 ) } a.e. 𝑀 ) } )
22 21 breqd ( 𝜑 → ( 𝐹 ( 𝑅 ~ a.e. 𝑀 ) 𝐺𝐹 { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( ( 𝑓 ∈ ( dom 𝑅m dom 𝑀 ) ∧ 𝑔 ∈ ( dom 𝑅m dom 𝑀 ) ) ∧ { 𝑥 dom 𝑀 ∣ ( 𝑓𝑥 ) 𝑅 ( 𝑔𝑥 ) } a.e. 𝑀 ) } 𝐺 ) )
23 1 oveq1i ( dom 𝑅m dom 𝑀 ) = ( 𝐷m dom 𝑀 )
24 4 23 eleqtrrdi ( 𝜑𝐹 ∈ ( dom 𝑅m dom 𝑀 ) )
25 5 23 eleqtrrdi ( 𝜑𝐺 ∈ ( dom 𝑅m dom 𝑀 ) )
26 24 25 jca ( 𝜑 → ( 𝐹 ∈ ( dom 𝑅m dom 𝑀 ) ∧ 𝐺 ∈ ( dom 𝑅m dom 𝑀 ) ) )
27 26 biantrurd ( 𝜑 → ( { 𝑥 dom 𝑀 ∣ ( 𝐹𝑥 ) 𝑅 ( 𝐺𝑥 ) } a.e. 𝑀 ↔ ( ( 𝐹 ∈ ( dom 𝑅m dom 𝑀 ) ∧ 𝐺 ∈ ( dom 𝑅m dom 𝑀 ) ) ∧ { 𝑥 dom 𝑀 ∣ ( 𝐹𝑥 ) 𝑅 ( 𝐺𝑥 ) } a.e. 𝑀 ) ) )
28 19 22 27 3bitr4d ( 𝜑 → ( 𝐹 ( 𝑅 ~ a.e. 𝑀 ) 𝐺 ↔ { 𝑥 dom 𝑀 ∣ ( 𝐹𝑥 ) 𝑅 ( 𝐺𝑥 ) } a.e. 𝑀 ) )