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 \in ⋃ ran measures \land \{x \in O \| \neg φ\} \in dom M \land \{x \in O \| \neg ψ\} \in dom M) \to (\{x \in O \| (φ \land ψ)\} M -ae. \leftrightarrow (\{x \in O \| φ\} M -ae. \land \{x \in O \| ψ\} M -ae.))$

Proof

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

Metamath Proof Explorer

Theorem aean

Proof