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	$⊢ φ \to R \in V$
	brfae.2	$⊢ φ \to M \in ⋃ ran measures$
	brfae.3	$⊢ φ \to F \in (D^{⋃ dom M})$
	brfae.4	$⊢ φ \to G \in (D^{⋃ dom M})$
Assertion	brfae	$⊢ φ \to (F R G M -ae. \leftrightarrow \{x \in ⋃ dom M \| F (x) R G (x)\} M -ae.)$

Proof

Step	Hyp	Ref	Expression
1		brfae.0	$⊢ dom R = D$
2		brfae.1	$⊢ φ \to R \in V$
3		brfae.2	$⊢ φ \to M \in ⋃ ran measures$
4		brfae.3	$⊢ φ \to F \in (D^{⋃ dom M})$
5		brfae.4	$⊢ φ \to G \in (D^{⋃ dom M})$
6		simpl	$⊢ (f = F \land g = G) \to f = F$
7	6	eleq1d	$⊢ (f = F \land g = G) \to (f \in ({dom R}^{⋃ dom M}) \leftrightarrow F \in ({dom R}^{⋃ dom M}))$
8		simpr	$⊢ (f = F \land g = G) \to g = G$
9	8	eleq1d	$⊢ (f = F \land g = G) \to (g \in ({dom R}^{⋃ dom M}) \leftrightarrow G \in ({dom R}^{⋃ dom M}))$
10	7 9	anbi12d	$⊢ (f = F \land g = G) \to ((f \in ({dom R}^{⋃ dom M}) \land g \in ({dom R}^{⋃ dom M})) \leftrightarrow (F \in ({dom R}^{⋃ dom M}) \land G \in ({dom R}^{⋃ dom M})))$
11	6	fveq1d	$⊢ (f = F \land g = G) \to f (x) = F (x)$
12	8	fveq1d	$⊢ (f = F \land g = G) \to g (x) = G (x)$
13	11 12	breq12d	$⊢ (f = F \land g = G) \to (f (x) R g (x) \leftrightarrow F (x) R G (x))$
14	13	rabbidv	$⊢ (f = F \land g = G) \to \{x \in ⋃ dom M \| f (x) R g (x)\} = \{x \in ⋃ dom M \| F (x) R G (x)\}$
15	14	breq1d	$⊢ (f = F \land g = G) \to (\{x \in ⋃ dom M \| f (x) R g (x)\} M -ae. \leftrightarrow \{x \in ⋃ dom M \| F (x) R G (x)\} M -ae.)$
16	10 15	anbi12d	$⊢ (f = F \land g = G) \to (((f \in ({dom R}^{⋃ dom M}) \land g \in ({dom R}^{⋃ dom M})) \land \{x \in ⋃ dom M \| f (x) R g (x)\} M -ae.) \leftrightarrow ((F \in ({dom R}^{⋃ dom M}) \land G \in ({dom R}^{⋃ dom M})) \land \{x \in ⋃ dom M \| F (x) R G (x)\} M -ae.))$
17		eqid	$⊢ \{⟨f, g⟩ \| ((f \in ({dom R}^{⋃ dom M}) \land g \in ({dom R}^{⋃ dom M})) \land \{x \in ⋃ dom M \| f (x) R g (x)\} M -ae.)\} = \{⟨f, g⟩ \| ((f \in ({dom R}^{⋃ dom M}) \land g \in ({dom R}^{⋃ dom M})) \land \{x \in ⋃ dom M \| f (x) R g (x)\} M -ae.)\}$
18	16 17	brabga	$⊢ (F \in (D^{⋃ dom M}) \land G \in (D^{⋃ dom M})) \to (F \{⟨f, g⟩ \| ((f \in ({dom R}^{⋃ dom M}) \land g \in ({dom R}^{⋃ dom M})) \land \{x \in ⋃ dom M \| f (x) R g (x)\} M -ae.)\} G \leftrightarrow ((F \in ({dom R}^{⋃ dom M}) \land G \in ({dom R}^{⋃ dom M})) \land \{x \in ⋃ dom M \| F (x) R G (x)\} M -ae.))$
19	4 5 18	syl2anc	$⊢ φ \to (F \{⟨f, g⟩ \| ((f \in ({dom R}^{⋃ dom M}) \land g \in ({dom R}^{⋃ dom M})) \land \{x \in ⋃ dom M \| f (x) R g (x)\} M -ae.)\} G \leftrightarrow ((F \in ({dom R}^{⋃ dom M}) \land G \in ({dom R}^{⋃ dom M})) \land \{x \in ⋃ dom M \| F (x) R G (x)\} M -ae.))$
20		faeval	$⊢ (R \in V \land M \in ⋃ ran measures) \to R ~_{ae} M = \{⟨f, g⟩ \| ((f \in ({dom R}^{⋃ dom M}) \land g \in ({dom R}^{⋃ dom M})) \land \{x \in ⋃ dom M \| f (x) R g (x)\} M -ae.)\}$
21	2 3 20	syl2anc	$⊢ φ \to R ~_{ae} M = \{⟨f, g⟩ \| ((f \in ({dom R}^{⋃ dom M}) \land g \in ({dom R}^{⋃ dom M})) \land \{x \in ⋃ dom M \| f (x) R g (x)\} M -ae.)\}$
22	21	breqd	$⊢ φ \to (F R G M -ae. \leftrightarrow F \{⟨f, g⟩ \| ((f \in ({dom R}^{⋃ dom M}) \land g \in ({dom R}^{⋃ dom M})) \land \{x \in ⋃ dom M \| f (x) R g (x)\} M -ae.)\} G)$
23	1	oveq1i	$⊢ {dom R}^{⋃ dom M} = D^{⋃ dom M}$
24	4 23	eleqtrrdi	$⊢ φ \to F \in ({dom R}^{⋃ dom M})$
25	5 23	eleqtrrdi	$⊢ φ \to G \in ({dom R}^{⋃ dom M})$
26	24 25	jca	$⊢ φ \to (F \in ({dom R}^{⋃ dom M}) \land G \in ({dom R}^{⋃ dom M}))$
27	26	biantrurd	$⊢ φ \to (\{x \in ⋃ dom M \| F (x) R G (x)\} M -ae. \leftrightarrow ((F \in ({dom R}^{⋃ dom M}) \land G \in ({dom R}^{⋃ dom M})) \land \{x \in ⋃ dom M \| F (x) R G (x)\} M -ae.))$
28	19 22 27	3bitr4d	$⊢ φ \to (F R G M -ae. \leftrightarrow \{x \in ⋃ dom M \| F (x) R G (x)\} M -ae.)$

Metamath Proof Explorer

Theorem brfae

Proof