Theorem meadif

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

	Ref	Expression
Hypotheses	meadif.m	|- ( ph -> M e. Meas )
	meadif.a	|- ( ph -> A e. dom M )
	meadif.r	|- ( ph -> ( M ` A ) e. RR )
	meadif.b	|- ( ph -> B e. dom M )
	meadif.s	|- ( ph -> B C_ A )
Assertion	meadif	|- ( ph -> ( M ` ( A \ B ) ) = ( ( M ` A ) - ( M ` B ) ) )

Proof

Step	Hyp	Ref	Expression
1		meadif.m	|- ( ph -> M e. Meas )
2		meadif.a	|- ( ph -> A e. dom M )
3		meadif.r	|- ( ph -> ( M ` A ) e. RR )
4		meadif.b	|- ( ph -> B e. dom M )
5		meadif.s	|- ( ph -> B C_ A )
6		undif	|- ( B C_ A <-> ( B u. ( A \ B ) ) = A )
7	5 6	sylib	|- ( ph -> ( B u. ( A \ B ) ) = A )
8	7	eqcomd	|- ( ph -> A = ( B u. ( A \ B ) ) )
9	8	fveq2d	|- ( ph -> ( M ` A ) = ( M ` ( B u. ( A \ B ) ) ) )
10		eqid	|- dom M = dom M
11	1 10	dmmeasal	|- ( ph -> dom M e. SAlg )
12		saldifcl2	|- ( ( dom M e. SAlg /\ A e. dom M /\ B e. dom M ) -> ( A \ B ) e. dom M )
13	11 2 4 12	syl3anc	|- ( ph -> ( A \ B ) e. dom M )
14		disjdif	|- ( B i^i ( A \ B ) ) = (/)
15	14	a1i	|- ( ph -> ( B i^i ( A \ B ) ) = (/) )
16	1 2 3 5 4	meassre	|- ( ph -> ( M ` B ) e. RR )
17		difssd	|- ( ph -> ( A \ B ) C_ A )
18	1 2 3 17 13	meassre	|- ( ph -> ( M ` ( A \ B ) ) e. RR )
19	1 10 4 13 15 16 18	meadjunre	|- ( ph -> ( M ` ( B u. ( A \ B ) ) ) = ( ( M ` B ) + ( M ` ( A \ B ) ) ) )
20	9 19	eqtr2d	|- ( ph -> ( ( M ` B ) + ( M ` ( A \ B ) ) ) = ( M ` A ) )
21	16	recnd	|- ( ph -> ( M ` B ) e. CC )
22	18	recnd	|- ( ph -> ( M ` ( A \ B ) ) e. CC )
23	3	recnd	|- ( ph -> ( M ` A ) e. CC )
24	21 22 23	addrsub	|- ( ph -> ( ( ( M ` B ) + ( M ` ( A \ B ) ) ) = ( M ` A ) <-> ( M ` ( A \ B ) ) = ( ( M ` A ) - ( M ` B ) ) ) )
25	20 24	mpbid	|- ( ph -> ( M ` ( A \ B ) ) = ( ( M ` A ) - ( M ` B ) ) )