meadjun

Description: The measure of the union of two disjoint sets is the sum of the measures, Property 112C (a) of Fremlin1 p. 15. (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Hypotheses	meadjun.m	$⊢ φ \to M \in Meas$
	meadjun.x	$⊢ S = dom M$
	meadjun.a	$⊢ φ \to A \in S$
	meadjun.b	$⊢ φ \to B \in S$
	meadjun.dj	$⊢ φ \to A \cap B = \emptyset$
Assertion	meadjun	$⊢ φ \to M (A \cup B) = M (A) +_{𝑒} M (B)$

Proof

Step	Hyp	Ref	Expression
1		meadjun.m	$⊢ φ \to M \in Meas$
2		meadjun.x	$⊢ S = dom M$
3		meadjun.a	$⊢ φ \to A \in S$
4		meadjun.b	$⊢ φ \to B \in S$
5		meadjun.dj	$⊢ φ \to A \cap B = \emptyset$
6		iccssxr	$⊢ [0, +∞] \subseteq ℝ^{*}$
7	1 2	meaf	$⊢ φ \to M : S ⟶ [0, +∞]$
8	7 4	ffvelrnd	$⊢ φ \to M (B) \in [0, +∞]$
9	6 8	sseldi	$⊢ φ \to M (B) \in ℝ^{*}$
10		xaddid2	$⊢ M (B) \in ℝ^{*} \to 0 +_{𝑒} M (B) = M (B)$
11	9 10	syl	$⊢ φ \to 0 +_{𝑒} M (B) = M (B)$
12	11	eqcomd	$⊢ φ \to M (B) = 0 +_{𝑒} M (B)$
13	12	adantr	$⊢ (φ \land A = \emptyset) \to M (B) = 0 +_{𝑒} M (B)$
14		uneq1	$⊢ A = \emptyset \to A \cup B = \emptyset \cup B$
15		0un	$⊢ \emptyset \cup B = B$
16	15	a1i	$⊢ A = \emptyset \to \emptyset \cup B = B$
17	14 16	eqtrd	$⊢ A = \emptyset \to A \cup B = B$
18	17	fveq2d	$⊢ A = \emptyset \to M (A \cup B) = M (B)$
19	18	adantl	$⊢ (φ \land A = \emptyset) \to M (A \cup B) = M (B)$
20		fveq2	$⊢ A = \emptyset \to M (A) = M (\emptyset)$
21	20	adantl	$⊢ (φ \land A = \emptyset) \to M (A) = M (\emptyset)$
22	1	mea0	$⊢ φ \to M (\emptyset) = 0$
23	22	adantr	$⊢ (φ \land A = \emptyset) \to M (\emptyset) = 0$
24	21 23	eqtrd	$⊢ (φ \land A = \emptyset) \to M (A) = 0$
25	24	oveq1d	$⊢ (φ \land A = \emptyset) \to M (A) +_{𝑒} M (B) = 0 +_{𝑒} M (B)$
26	13 19 25	3eqtr4d	$⊢ (φ \land A = \emptyset) \to M (A \cup B) = M (A) +_{𝑒} M (B)$
27		simpl	$⊢ (φ \land \neg A = \emptyset) \to φ$
28	5	ad2antrr	$⊢ ((φ \land \neg A = \emptyset) \land A = B) \to A \cap B = \emptyset$
29		inidm	$⊢ A \cap A = A$
30	29	eqcomi	$⊢ A = A \cap A$
31		ineq2	$⊢ A = B \to A \cap A = A \cap B$
32	30 31	syl5req	$⊢ A = B \to A \cap B = A$
33	32	adantl	$⊢ (\neg A = \emptyset \land A = B) \to A \cap B = A$
34		neqne	$⊢ \neg A = \emptyset \to A \neq \emptyset$
35	34	adantr	$⊢ (\neg A = \emptyset \land A = B) \to A \neq \emptyset$
36	33 35	eqnetrd	$⊢ (\neg A = \emptyset \land A = B) \to A \cap B \neq \emptyset$
37	36	neneqd	$⊢ (\neg A = \emptyset \land A = B) \to \neg A \cap B = \emptyset$
38	37	adantll	$⊢ ((φ \land \neg A = \emptyset) \land A = B) \to \neg A \cap B = \emptyset$
39	28 38	pm2.65da	$⊢ (φ \land \neg A = \emptyset) \to \neg A = B$
40	39	neqned	$⊢ (φ \land \neg A = \emptyset) \to A \neq B$
41		uniprg	$⊢ (A \in S \land B \in S) \to ⋃ \{A, B\} = A \cup B$
42	3 4 41	syl2anc	$⊢ φ \to ⋃ \{A, B\} = A \cup B$
43	42	eqcomd	$⊢ φ \to A \cup B = ⋃ \{A, B\}$
44	43	fveq2d	$⊢ φ \to M (A \cup B) = M (⋃ \{A, B\})$
45	44	adantr	$⊢ (φ \land A \neq B) \to M (A \cup B) = M (⋃ \{A, B\})$
46	3 4	prssd	$⊢ φ \to \{A, B\} \subseteq S$
47		prfi	$⊢ \{A, B\} \in Fin$
48		isfinite	$⊢ \{A, B\} \in Fin \leftrightarrow \{A, B\} ≺ ω$
49	48	biimpi	$⊢ \{A, B\} \in Fin \to \{A, B\} ≺ ω$
50		sdomdom	$⊢ \{A, B\} ≺ ω \to \{A, B\} ≼ ω$
51	49 50	syl	$⊢ \{A, B\} \in Fin \to \{A, B\} ≼ ω$
52	47 51	ax-mp	$⊢ \{A, B\} ≼ ω$
53	52	a1i	$⊢ φ \to \{A, B\} ≼ ω$
54		disjxsn	$⊢ \underset{x \in \{B\}}{Disj} x$
55	54	a1i	$⊢ A = B \to \underset{x \in \{B\}}{Disj} x$
56		preq1	$⊢ A = B \to \{A, B\} = \{B, B\}$
57		dfsn2	$⊢ \{B\} = \{B, B\}$
58	57	eqcomi	$⊢ \{B, B\} = \{B\}$
59	58	a1i	$⊢ A = B \to \{B, B\} = \{B\}$
60	56 59	eqtrd	$⊢ A = B \to \{A, B\} = \{B\}$
61	60	disjeq1d	$⊢ A = B \to (\underset{x \in \{A, B\}}{Disj} x \leftrightarrow \underset{x \in \{B\}}{Disj} x)$
62	55 61	mpbird	$⊢ A = B \to \underset{x \in \{A, B\}}{Disj} x$
63	62	adantl	$⊢ (φ \land A = B) \to \underset{x \in \{A, B\}}{Disj} x$
64		simpl	$⊢ (φ \land \neg A = B) \to φ$
65		neqne	$⊢ \neg A = B \to A \neq B$
66	65	adantl	$⊢ (φ \land \neg A = B) \to A \neq B$
67	5	adantr	$⊢ (φ \land A \neq B) \to A \cap B = \emptyset$
68	3	adantr	$⊢ (φ \land A \neq B) \to A \in S$
69	4	adantr	$⊢ (φ \land A \neq B) \to B \in S$
70		simpr	$⊢ (φ \land A \neq B) \to A \neq B$
71		id	$⊢ x = A \to x = A$
72		id	$⊢ x = B \to x = B$
73	71 72	disjprg	$⊢ (A \in S \land B \in S \land A \neq B) \to (\underset{x \in \{A, B\}}{Disj} x \leftrightarrow A \cap B = \emptyset)$
74	68 69 70 73	syl3anc	$⊢ (φ \land A \neq B) \to (\underset{x \in \{A, B\}}{Disj} x \leftrightarrow A \cap B = \emptyset)$
75	67 74	mpbird	$⊢ (φ \land A \neq B) \to \underset{x \in \{A, B\}}{Disj} x$
76	64 66 75	syl2anc	$⊢ (φ \land \neg A = B) \to \underset{x \in \{A, B\}}{Disj} x$
77	63 76	pm2.61dan	$⊢ φ \to \underset{x \in \{A, B\}}{Disj} x$
78	1 2 46 53 77	meadjuni	$⊢ φ \to M (⋃ \{A, B\}) = sum^({M ↾}_{\{A, B\}})$
79	78	adantr	$⊢ (φ \land A \neq B) \to M (⋃ \{A, B\}) = sum^({M ↾}_{\{A, B\}})$
80	7 3	ffvelrnd	$⊢ φ \to M (A) \in [0, +∞]$
81	80	adantr	$⊢ (φ \land A \neq B) \to M (A) \in [0, +∞]$
82	8	adantr	$⊢ (φ \land A \neq B) \to M (B) \in [0, +∞]$
83		fveq2	$⊢ x = A \to M (x) = M (A)$
84		fveq2	$⊢ x = B \to M (x) = M (B)$
85	68 69 81 82 83 84 70	sge0pr	$⊢ (φ \land A \neq B) \to sum^((x \in \{A, B\} ⟼ M (x))) = M (A) +_{𝑒} M (B)$
86	7 46	fssresd	$⊢ φ \to ({M ↾}_{\{A, B\}}) : \{A, B\} ⟶ [0, +∞]$
87	86	feqmptd	$⊢ φ \to {M ↾}_{\{A, B\}} = (x \in \{A, B\} ⟼ ({M ↾}_{\{A, B\}}) (x))$
88		fvres	$⊢ x \in \{A, B\} \to ({M ↾}_{\{A, B\}}) (x) = M (x)$
89	88	mpteq2ia	$⊢ (x \in \{A, B\} ⟼ ({M ↾}_{\{A, B\}}) (x)) = (x \in \{A, B\} ⟼ M (x))$
90	89	a1i	$⊢ φ \to (x \in \{A, B\} ⟼ ({M ↾}_{\{A, B\}}) (x)) = (x \in \{A, B\} ⟼ M (x))$
91	87 90	eqtrd	$⊢ φ \to {M ↾}_{\{A, B\}} = (x \in \{A, B\} ⟼ M (x))$
92	91	fveq2d	$⊢ φ \to sum^({M ↾}_{\{A, B\}}) = sum^((x \in \{A, B\} ⟼ M (x)))$
93	92	adantr	$⊢ (φ \land A \neq B) \to sum^({M ↾}_{\{A, B\}}) = sum^((x \in \{A, B\} ⟼ M (x)))$
94		eqidd	$⊢ (φ \land A \neq B) \to M (A) +_{𝑒} M (B) = M (A) +_{𝑒} M (B)$
95	85 93 94	3eqtr4d	$⊢ (φ \land A \neq B) \to sum^({M ↾}_{\{A, B\}}) = M (A) +_{𝑒} M (B)$
96	45 79 95	3eqtrd	$⊢ (φ \land A \neq B) \to M (A \cup B) = M (A) +_{𝑒} M (B)$
97	27 40 96	syl2anc	$⊢ (φ \land \neg A = \emptyset) \to M (A \cup B) = M (A) +_{𝑒} M (B)$
98	26 97	pm2.61dan	$⊢ φ \to M (A \cup B) = M (A) +_{𝑒} M (B)$

Metamath Proof Explorer

Theorem meadjun

Proof