Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  brae Structured version   Visualization version   GIF version

Theorem brae 34220
Description: 'almost everywhere' relation for a measure and a measurable set 𝐴. (Contributed by Thierry Arnoux, 20-Oct-2017.)
Assertion
Ref Expression
brae ((𝑀 ran measures ∧ 𝐴 ∈ dom 𝑀) → (𝐴a.e.𝑀 ↔ (𝑀‘( dom 𝑀𝐴)) = 0))

Proof of Theorem brae
Dummy variables 𝑚 𝑎 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simpr 484 . . . . 5 ((𝑎 = 𝐴𝑚 = 𝑀) → 𝑚 = 𝑀)
21dmeqd 5914 . . . . . . 7 ((𝑎 = 𝐴𝑚 = 𝑀) → dom 𝑚 = dom 𝑀)
32unieqd 4918 . . . . . 6 ((𝑎 = 𝐴𝑚 = 𝑀) → dom 𝑚 = dom 𝑀)
4 simpl 482 . . . . . 6 ((𝑎 = 𝐴𝑚 = 𝑀) → 𝑎 = 𝐴)
53, 4difeq12d 4126 . . . . 5 ((𝑎 = 𝐴𝑚 = 𝑀) → ( dom 𝑚𝑎) = ( dom 𝑀𝐴))
61, 5fveq12d 6911 . . . 4 ((𝑎 = 𝐴𝑚 = 𝑀) → (𝑚‘( dom 𝑚𝑎)) = (𝑀‘( dom 𝑀𝐴)))
76eqeq1d 2738 . . 3 ((𝑎 = 𝐴𝑚 = 𝑀) → ((𝑚‘( dom 𝑚𝑎)) = 0 ↔ (𝑀‘( dom 𝑀𝐴)) = 0))
8 df-ae 34218 . . 3 a.e. = {⟨𝑎, 𝑚⟩ ∣ (𝑚‘( dom 𝑚𝑎)) = 0}
97, 8brabga 5537 . 2 ((𝐴 ∈ dom 𝑀𝑀 ran measures) → (𝐴a.e.𝑀 ↔ (𝑀‘( dom 𝑀𝐴)) = 0))
109ancoms 458 1 ((𝑀 ran measures ∧ 𝐴 ∈ dom 𝑀) → (𝐴a.e.𝑀 ↔ (𝑀‘( dom 𝑀𝐴)) = 0))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395   = wceq 1540  wcel 2108  cdif 3947   cuni 4905   class class class wbr 5141  dom cdm 5683  ran crn 5684  cfv 6559  0cc0 11151  measurescmeas 34174  a.e.cae 34216
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707  ax-sep 5294  ax-nul 5304  ax-pr 5430
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2728  df-clel 2815  df-rab 3436  df-v 3481  df-dif 3953  df-un 3955  df-ss 3967  df-nul 4333  df-if 4525  df-sn 4625  df-pr 4627  df-op 4631  df-uni 4906  df-br 5142  df-opab 5204  df-dm 5693  df-iota 6512  df-fv 6567  df-ae 34218
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator