Metamath Proof Explorer

Theorem aean

Description: A conjunction holds almost everywhere if and only if both its terms do. (Contributed by Thierry Arnoux, 20-Oct-2017)

Ref Expression
Hypothesis aean.1 
|- U. dom M = O
Assertion aean 
|- ( ( M e. U. ran measures /\ { x e. O | -. ph } e. dom M /\ { x e. O | -. ps } e. dom M ) -> ( { x e. O | ( ph /\ ps ) } ae M <-> ( { x e. O | ph } ae M /\ { x e. O | ps } ae M ) ) )

Proof

Step Hyp Ref Expression
1 aean.1 
 |-  U. dom M = O
2 unrab 
 |-  ( { x e. O | -. ph } u. { x e. O | -. ps } ) = { x e. O | ( -. ph \/ -. ps ) }
3 ianor 
 |-  ( -. ( ph /\ ps ) <-> ( -. ph \/ -. ps ) )
4 3 rabbii 
 |-  { x e. O | -. ( ph /\ ps ) } = { x e. O | ( -. ph \/ -. ps ) }
5 2 4 eqtr4i 
 |-  ( { x e. O | -. ph } u. { x e. O | -. ps } ) = { x e. O | -. ( ph /\ ps ) }
6 5 fveq2i 
 |-  ( M ` ( { x e. O | -. ph } u. { x e. O | -. ps } ) ) = ( M ` { x e. O | -. ( ph /\ ps ) } )
7 6 eqeq1i 
 |-  ( ( M ` ( { x e. O | -. ph } u. { x e. O | -. ps } ) ) = 0 <-> ( M ` { x e. O | -. ( ph /\ ps ) } ) = 0 )
8 measbasedom 
 |-  ( M e. U. ran measures <-> M e. ( measures ` dom M ) )
9 8 biimpi 
 |-  ( M e. U. ran measures -> M e. ( measures ` dom M ) )
10 9 3ad2ant1 
 |-  ( ( M e. U. ran measures /\ { x e. O | -. ph } e. dom M /\ { x e. O | -. ps } e. dom M ) -> M e. ( measures ` dom M ) )
11 10 adantr 
 |-  ( ( ( M e. U. ran measures /\ { x e. O | -. ph } e. dom M /\ { x e. O | -. ps } e. dom M ) /\ ( M ` ( { x e. O | -. ph } u. { x e. O | -. ps } ) ) = 0 ) -> M e. ( measures ` dom M ) )
12 simp2 
 |-  ( ( M e. U. ran measures /\ { x e. O | -. ph } e. dom M /\ { x e. O | -. ps } e. dom M ) -> { x e. O | -. ph } e. dom M )
13 12 adantr 
 |-  ( ( ( M e. U. ran measures /\ { x e. O | -. ph } e. dom M /\ { x e. O | -. ps } e. dom M ) /\ ( M ` ( { x e. O | -. ph } u. { x e. O | -. ps } ) ) = 0 ) -> { x e. O | -. ph } e. dom M )
14 dmmeas 
 |-  ( M e. U. ran measures -> dom M e. U. ran sigAlgebra )
15 unelsiga 
 |-  ( ( dom M e. U. ran sigAlgebra /\ { x e. O | -. ph } e. dom M /\ { x e. O | -. ps } e. dom M ) -> ( { x e. O | -. ph } u. { x e. O | -. ps } ) e. dom M )
16 14 15 syl3an1 
 |-  ( ( M e. U. ran measures /\ { x e. O | -. ph } e. dom M /\ { x e. O | -. ps } e. dom M ) -> ( { x e. O | -. ph } u. { x e. O | -. ps } ) e. dom M )
17 ssun1 
 |-  { x e. O | -. ph } C_ ( { x e. O | -. ph } u. { x e. O | -. ps } )
18 17 a1i 
 |-  ( ( M e. U. ran measures /\ { x e. O | -. ph } e. dom M /\ { x e. O | -. ps } e. dom M ) -> { x e. O | -. ph } C_ ( { x e. O | -. ph } u. { x e. O | -. ps } ) )
19 10 12 16 18 measssd 
 |-  ( ( M e. U. ran measures /\ { x e. O | -. ph } e. dom M /\ { x e. O | -. ps } e. dom M ) -> ( M ` { x e. O | -. ph } ) <_ ( M ` ( { x e. O | -. ph } u. { x e. O | -. ps } ) ) )
20 19 adantr 
 |-  ( ( ( M e. U. ran measures /\ { x e. O | -. ph } e. dom M /\ { x e. O | -. ps } e. dom M ) /\ ( M ` ( { x e. O | -. ph } u. { x e. O | -. ps } ) ) = 0 ) -> ( M ` { x e. O | -. ph } ) <_ ( M ` ( { x e. O | -. ph } u. { x e. O | -. ps } ) ) )
21 simpr 
 |-  ( ( ( M e. U. ran measures /\ { x e. O | -. ph } e. dom M /\ { x e. O | -. ps } e. dom M ) /\ ( M ` ( { x e. O | -. ph } u. { x e. O | -. ps } ) ) = 0 ) -> ( M ` ( { x e. O | -. ph } u. { x e. O | -. ps } ) ) = 0 )
22 20 21 breqtrd 
 |-  ( ( ( M e. U. ran measures /\ { x e. O | -. ph } e. dom M /\ { x e. O | -. ps } e. dom M ) /\ ( M ` ( { x e. O | -. ph } u. { x e. O | -. ps } ) ) = 0 ) -> ( M ` { x e. O | -. ph } ) <_ 0 )
23 measle0 
 |-  ( ( M e. ( measures ` dom M ) /\ { x e. O | -. ph } e. dom M /\ ( M ` { x e. O | -. ph } ) <_ 0 ) -> ( M ` { x e. O | -. ph } ) = 0 )
24 11 13 22 23 syl3anc 
 |-  ( ( ( M e. U. ran measures /\ { x e. O | -. ph } e. dom M /\ { x e. O | -. ps } e. dom M ) /\ ( M ` ( { x e. O | -. ph } u. { x e. O | -. ps } ) ) = 0 ) -> ( M ` { x e. O | -. ph } ) = 0 )
25 simp3 
 |-  ( ( M e. U. ran measures /\ { x e. O | -. ph } e. dom M /\ { x e. O | -. ps } e. dom M ) -> { x e. O | -. ps } e. dom M )
26 25 adantr 
 |-  ( ( ( M e. U. ran measures /\ { x e. O | -. ph } e. dom M /\ { x e. O | -. ps } e. dom M ) /\ ( M ` ( { x e. O | -. ph } u. { x e. O | -. ps } ) ) = 0 ) -> { x e. O | -. ps } e. dom M )
27 ssun2 
 |-  { x e. O | -. ps } C_ ( { x e. O | -. ph } u. { x e. O | -. ps } )
28 27 a1i 
 |-  ( ( M e. U. ran measures /\ { x e. O | -. ph } e. dom M /\ { x e. O | -. ps } e. dom M ) -> { x e. O | -. ps } C_ ( { x e. O | -. ph } u. { x e. O | -. ps } ) )
29 10 25 16 28 measssd 
 |-  ( ( M e. U. ran measures /\ { x e. O | -. ph } e. dom M /\ { x e. O | -. ps } e. dom M ) -> ( M ` { x e. O | -. ps } ) <_ ( M ` ( { x e. O | -. ph } u. { x e. O | -. ps } ) ) )
30 29 adantr 
 |-  ( ( ( M e. U. ran measures /\ { x e. O | -. ph } e. dom M /\ { x e. O | -. ps } e. dom M ) /\ ( M ` ( { x e. O | -. ph } u. { x e. O | -. ps } ) ) = 0 ) -> ( M ` { x e. O | -. ps } ) <_ ( M ` ( { x e. O | -. ph } u. { x e. O | -. ps } ) ) )
31 30 21 breqtrd 
 |-  ( ( ( M e. U. ran measures /\ { x e. O | -. ph } e. dom M /\ { x e. O | -. ps } e. dom M ) /\ ( M ` ( { x e. O | -. ph } u. { x e. O | -. ps } ) ) = 0 ) -> ( M ` { x e. O | -. ps } ) <_ 0 )
32 measle0 
 |-  ( ( M e. ( measures ` dom M ) /\ { x e. O | -. ps } e. dom M /\ ( M ` { x e. O | -. ps } ) <_ 0 ) -> ( M ` { x e. O | -. ps } ) = 0 )
33 11 26 31 32 syl3anc 
 |-  ( ( ( M e. U. ran measures /\ { x e. O | -. ph } e. dom M /\ { x e. O | -. ps } e. dom M ) /\ ( M ` ( { x e. O | -. ph } u. { x e. O | -. ps } ) ) = 0 ) -> ( M ` { x e. O | -. ps } ) = 0 )
34 24 33 jca 
 |-  ( ( ( M e. U. ran measures /\ { x e. O | -. ph } e. dom M /\ { x e. O | -. ps } e. dom M ) /\ ( M ` ( { x e. O | -. ph } u. { x e. O | -. ps } ) ) = 0 ) -> ( ( M ` { x e. O | -. ph } ) = 0 /\ ( M ` { x e. O | -. ps } ) = 0 ) )
35 10 adantr 
 |-  ( ( ( M e. U. ran measures /\ { x e. O | -. ph } e. dom M /\ { x e. O | -. ps } e. dom M ) /\ ( ( M ` { x e. O | -. ph } ) = 0 /\ ( M ` { x e. O | -. ps } ) = 0 ) ) -> M e. ( measures ` dom M ) )
36 measbase 
 |-  ( M e. ( measures ` dom M ) -> dom M e. U. ran sigAlgebra )
37 35 36 syl 
 |-  ( ( ( M e. U. ran measures /\ { x e. O | -. ph } e. dom M /\ { x e. O | -. ps } e. dom M ) /\ ( ( M ` { x e. O | -. ph } ) = 0 /\ ( M ` { x e. O | -. ps } ) = 0 ) ) -> dom M e. U. ran sigAlgebra )
38 12 adantr 
 |-  ( ( ( M e. U. ran measures /\ { x e. O | -. ph } e. dom M /\ { x e. O | -. ps } e. dom M ) /\ ( ( M ` { x e. O | -. ph } ) = 0 /\ ( M ` { x e. O | -. ps } ) = 0 ) ) -> { x e. O | -. ph } e. dom M )
39 25 adantr 
 |-  ( ( ( M e. U. ran measures /\ { x e. O | -. ph } e. dom M /\ { x e. O | -. ps } e. dom M ) /\ ( ( M ` { x e. O | -. ph } ) = 0 /\ ( M ` { x e. O | -. ps } ) = 0 ) ) -> { x e. O | -. ps } e. dom M )
40 37 38 39 15 syl3anc 
 |-  ( ( ( M e. U. ran measures /\ { x e. O | -. ph } e. dom M /\ { x e. O | -. ps } e. dom M ) /\ ( ( M ` { x e. O | -. ph } ) = 0 /\ ( M ` { x e. O | -. ps } ) = 0 ) ) -> ( { x e. O | -. ph } u. { x e. O | -. ps } ) e. dom M )
41 35 38 39 measunl 
 |-  ( ( ( M e. U. ran measures /\ { x e. O | -. ph } e. dom M /\ { x e. O | -. ps } e. dom M ) /\ ( ( M ` { x e. O | -. ph } ) = 0 /\ ( M ` { x e. O | -. ps } ) = 0 ) ) -> ( M ` ( { x e. O | -. ph } u. { x e. O | -. ps } ) ) <_ ( ( M ` { x e. O | -. ph } ) +e ( M ` { x e. O | -. ps } ) ) )
42 simprl 
 |-  ( ( ( M e. U. ran measures /\ { x e. O | -. ph } e. dom M /\ { x e. O | -. ps } e. dom M ) /\ ( ( M ` { x e. O | -. ph } ) = 0 /\ ( M ` { x e. O | -. ps } ) = 0 ) ) -> ( M ` { x e. O | -. ph } ) = 0 )
43 simprr 
 |-  ( ( ( M e. U. ran measures /\ { x e. O | -. ph } e. dom M /\ { x e. O | -. ps } e. dom M ) /\ ( ( M ` { x e. O | -. ph } ) = 0 /\ ( M ` { x e. O | -. ps } ) = 0 ) ) -> ( M ` { x e. O | -. ps } ) = 0 )
44 42 43 oveq12d 
 |-  ( ( ( M e. U. ran measures /\ { x e. O | -. ph } e. dom M /\ { x e. O | -. ps } e. dom M ) /\ ( ( M ` { x e. O | -. ph } ) = 0 /\ ( M ` { x e. O | -. ps } ) = 0 ) ) -> ( ( M ` { x e. O | -. ph } ) +e ( M ` { x e. O | -. ps } ) ) = ( 0 +e 0 ) )
45 0xr 
 |-  0 e. RR*
46 xaddrid 
 |-  ( 0 e. RR* -> ( 0 +e 0 ) = 0 )
47 45 46 ax-mp 
 |-  ( 0 +e 0 ) = 0
48 44 47 eqtrdi 
 |-  ( ( ( M e. U. ran measures /\ { x e. O | -. ph } e. dom M /\ { x e. O | -. ps } e. dom M ) /\ ( ( M ` { x e. O | -. ph } ) = 0 /\ ( M ` { x e. O | -. ps } ) = 0 ) ) -> ( ( M ` { x e. O | -. ph } ) +e ( M ` { x e. O | -. ps } ) ) = 0 )
49 41 48 breqtrd 
 |-  ( ( ( M e. U. ran measures /\ { x e. O | -. ph } e. dom M /\ { x e. O | -. ps } e. dom M ) /\ ( ( M ` { x e. O | -. ph } ) = 0 /\ ( M ` { x e. O | -. ps } ) = 0 ) ) -> ( M ` ( { x e. O | -. ph } u. { x e. O | -. ps } ) ) <_ 0 )
50 measle0 
 |-  ( ( M e. ( measures ` dom M ) /\ ( { x e. O | -. ph } u. { x e. O | -. ps } ) e. dom M /\ ( M ` ( { x e. O | -. ph } u. { x e. O | -. ps } ) ) <_ 0 ) -> ( M ` ( { x e. O | -. ph } u. { x e. O | -. ps } ) ) = 0 )
51 35 40 49 50 syl3anc 
 |-  ( ( ( M e. U. ran measures /\ { x e. O | -. ph } e. dom M /\ { x e. O | -. ps } e. dom M ) /\ ( ( M ` { x e. O | -. ph } ) = 0 /\ ( M ` { x e. O | -. ps } ) = 0 ) ) -> ( M ` ( { x e. O | -. ph } u. { x e. O | -. ps } ) ) = 0 )
52 34 51 impbida 
 |-  ( ( M e. U. ran measures /\ { x e. O | -. ph } e. dom M /\ { x e. O | -. ps } e. dom M ) -> ( ( M ` ( { x e. O | -. ph } u. { x e. O | -. ps } ) ) = 0 <-> ( ( M ` { x e. O | -. ph } ) = 0 /\ ( M ` { x e. O | -. ps } ) = 0 ) ) )
53 7 52 bitr3id 
 |-  ( ( M e. U. ran measures /\ { x e. O | -. ph } e. dom M /\ { x e. O | -. ps } e. dom M ) -> ( ( M ` { x e. O | -. ( ph /\ ps ) } ) = 0 <-> ( ( M ` { x e. O | -. ph } ) = 0 /\ ( M ` { x e. O | -. ps } ) = 0 ) ) )
54 1 braew 
 |-  ( M e. U. ran measures -> ( { x e. O | ( ph /\ ps ) } ae M <-> ( M ` { x e. O | -. ( ph /\ ps ) } ) = 0 ) )
55 54 3ad2ant1 
 |-  ( ( M e. U. ran measures /\ { x e. O | -. ph } e. dom M /\ { x e. O | -. ps } e. dom M ) -> ( { x e. O | ( ph /\ ps ) } ae M <-> ( M ` { x e. O | -. ( ph /\ ps ) } ) = 0 ) )
56 1 braew 
 |-  ( M e. U. ran measures -> ( { x e. O | ph } ae M <-> ( M ` { x e. O | -. ph } ) = 0 ) )
57 1 braew 
 |-  ( M e. U. ran measures -> ( { x e. O | ps } ae M <-> ( M ` { x e. O | -. ps } ) = 0 ) )
58 56 57 anbi12d 
 |-  ( M e. U. ran measures -> ( ( { x e. O | ph } ae M /\ { x e. O | ps } ae M ) <-> ( ( M ` { x e. O | -. ph } ) = 0 /\ ( M ` { x e. O | -. ps } ) = 0 ) ) )
59 58 3ad2ant1 
 |-  ( ( M e. U. ran measures /\ { x e. O | -. ph } e. dom M /\ { x e. O | -. ps } e. dom M ) -> ( ( { x e. O | ph } ae M /\ { x e. O | ps } ae M ) <-> ( ( M ` { x e. O | -. ph } ) = 0 /\ ( M ` { x e. O | -. ps } ) = 0 ) ) )
60 53 55 59 3bitr4d 
 |-  ( ( M e. U. ran measures /\ { x e. O | -. ph } e. dom M /\ { x e. O | -. ps } e. dom M ) -> ( { x e. O | ( ph /\ ps ) } ae M <-> ( { x e. O | ph } ae M /\ { x e. O | ps } ae M ) ) )