meadif

Description: The measure of the difference of two sets. (Contributed by Glauco Siliprandi, 8-Apr-2021)

Step	Hyp	Ref	Expression
1		meadif.m	$⊢ φ \to M \in Meas$
2		meadif.a	$⊢ φ \to A \in dom M$
3		meadif.r	$⊢ φ \to M (A) \in ℝ$
4		meadif.b	$⊢ φ \to B \in dom M$
5		meadif.s	$⊢ φ \to B \subseteq A$
6		undif	$⊢ B \subseteq A \leftrightarrow B \cup (A ∖ B) = A$
7	5 6	sylib	$⊢ φ \to B \cup (A ∖ B) = A$
8	7	eqcomd	$⊢ φ \to A = B \cup (A ∖ B)$
9	8	fveq2d	$⊢ φ \to M (A) = M (B \cup (A ∖ B))$
10		eqid	$⊢ dom M = dom M$
11	1 10	dmmeasal	$⊢ φ \to dom M \in SAlg$
12		saldifcl2	$⊢ (dom M \in SAlg \land A \in dom M \land B \in dom M) \to A ∖ B \in dom M$
13	11 2 4 12	syl3anc	$⊢ φ \to A ∖ B \in dom M$
14		disjdif	$⊢ B \cap (A ∖ B) = \emptyset$
15	14	a1i	$⊢ φ \to B \cap (A ∖ B) = \emptyset$
16	1 2 3 5 4	meassre	$⊢ φ \to M (B) \in ℝ$
17		difssd	$⊢ φ \to A ∖ B \subseteq A$
18	1 2 3 17 13	meassre	$⊢ φ \to M (A ∖ B) \in ℝ$
19	1 10 4 13 15 16 18	meadjunre	$⊢ φ \to M (B \cup (A ∖ B)) = M (B) + M (A ∖ B)$
20	9 19	eqtr2d	$⊢ φ \to M (B) + M (A ∖ B) = M (A)$
21	16	recnd	$⊢ φ \to M (B) \in ℂ$
22	18	recnd	$⊢ φ \to M (A ∖ B) \in ℂ$
23	3	recnd	$⊢ φ \to M (A) \in ℂ$
24	21 22 23	addrsub	$⊢ φ \to (M (B) + M (A ∖ B) = M (A) \leftrightarrow M (A ∖ B) = M (A) - M (B))$
25	20 24	mpbid	$⊢ φ \to M (A ∖ B) = M (A) - M (B)$

Metamath Proof Explorer