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 dom M = O
Assertion aean M ran measures x O | ¬ φ dom M x O | ¬ ψ dom M x O | φ ψ M-ae. x O | φ M-ae. x O | ψ M-ae.

Proof

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