Theorem meadif

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

	Ref	Expression
Hypotheses	meadif.m	⊢ ( 𝜑 → 𝑀 ∈ Meas )
	meadif.a	⊢ ( 𝜑 → 𝐴 ∈ dom 𝑀 )
	meadif.r	⊢ ( 𝜑 → ( 𝑀 ‘ 𝐴 ) ∈ ℝ )
	meadif.b	⊢ ( 𝜑 → 𝐵 ∈ dom 𝑀 )
	meadif.s	⊢ ( 𝜑 → 𝐵 ⊆ 𝐴 )
Assertion	meadif	⊢ ( 𝜑 → ( 𝑀 ‘ ( 𝐴 ∖ 𝐵 ) ) = ( ( 𝑀 ‘ 𝐴 ) − ( 𝑀 ‘ 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		meadif.m	⊢ ( 𝜑 → 𝑀 ∈ Meas )
2		meadif.a	⊢ ( 𝜑 → 𝐴 ∈ dom 𝑀 )
3		meadif.r	⊢ ( 𝜑 → ( 𝑀 ‘ 𝐴 ) ∈ ℝ )
4		meadif.b	⊢ ( 𝜑 → 𝐵 ∈ dom 𝑀 )
5		meadif.s	⊢ ( 𝜑 → 𝐵 ⊆ 𝐴 )
6		undif	⊢ ( 𝐵 ⊆ 𝐴 ↔ ( 𝐵 ∪ ( 𝐴 ∖ 𝐵 ) ) = 𝐴 )
7	5 6	sylib	⊢ ( 𝜑 → ( 𝐵 ∪ ( 𝐴 ∖ 𝐵 ) ) = 𝐴 )
8	7	eqcomd	⊢ ( 𝜑 → 𝐴 = ( 𝐵 ∪ ( 𝐴 ∖ 𝐵 ) ) )
9	8	fveq2d	⊢ ( 𝜑 → ( 𝑀 ‘ 𝐴 ) = ( 𝑀 ‘ ( 𝐵 ∪ ( 𝐴 ∖ 𝐵 ) ) ) )
10		eqid	⊢ dom 𝑀 = dom 𝑀
11	1 10	dmmeasal	⊢ ( 𝜑 → dom 𝑀 ∈ SAlg )
12		saldifcl2	⊢ ( ( dom 𝑀 ∈ SAlg ∧ 𝐴 ∈ dom 𝑀 ∧ 𝐵 ∈ dom 𝑀 ) → ( 𝐴 ∖ 𝐵 ) ∈ dom 𝑀 )
13	11 2 4 12	syl3anc	⊢ ( 𝜑 → ( 𝐴 ∖ 𝐵 ) ∈ dom 𝑀 )
14		disjdif	⊢ ( 𝐵 ∩ ( 𝐴 ∖ 𝐵 ) ) = ∅
15	14	a1i	⊢ ( 𝜑 → ( 𝐵 ∩ ( 𝐴 ∖ 𝐵 ) ) = ∅ )
16	1 2 3 5 4	meassre	⊢ ( 𝜑 → ( 𝑀 ‘ 𝐵 ) ∈ ℝ )
17		difssd	⊢ ( 𝜑 → ( 𝐴 ∖ 𝐵 ) ⊆ 𝐴 )
18	1 2 3 17 13	meassre	⊢ ( 𝜑 → ( 𝑀 ‘ ( 𝐴 ∖ 𝐵 ) ) ∈ ℝ )
19	1 10 4 13 15 16 18	meadjunre	⊢ ( 𝜑 → ( 𝑀 ‘ ( 𝐵 ∪ ( 𝐴 ∖ 𝐵 ) ) ) = ( ( 𝑀 ‘ 𝐵 ) + ( 𝑀 ‘ ( 𝐴 ∖ 𝐵 ) ) ) )
20	9 19	eqtr2d	⊢ ( 𝜑 → ( ( 𝑀 ‘ 𝐵 ) + ( 𝑀 ‘ ( 𝐴 ∖ 𝐵 ) ) ) = ( 𝑀 ‘ 𝐴 ) )
21	16	recnd	⊢ ( 𝜑 → ( 𝑀 ‘ 𝐵 ) ∈ ℂ )
22	18	recnd	⊢ ( 𝜑 → ( 𝑀 ‘ ( 𝐴 ∖ 𝐵 ) ) ∈ ℂ )
23	3	recnd	⊢ ( 𝜑 → ( 𝑀 ‘ 𝐴 ) ∈ ℂ )
24	21 22 23	addrsub	⊢ ( 𝜑 → ( ( ( 𝑀 ‘ 𝐵 ) + ( 𝑀 ‘ ( 𝐴 ∖ 𝐵 ) ) ) = ( 𝑀 ‘ 𝐴 ) ↔ ( 𝑀 ‘ ( 𝐴 ∖ 𝐵 ) ) = ( ( 𝑀 ‘ 𝐴 ) − ( 𝑀 ‘ 𝐵 ) ) ) )
25	20 24	mpbid	⊢ ( 𝜑 → ( 𝑀 ‘ ( 𝐴 ∖ 𝐵 ) ) = ( ( 𝑀 ‘ 𝐴 ) − ( 𝑀 ‘ 𝐵 ) ) )