Theorem 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	⊢ ( 𝜑 → 𝑀 ∈ Meas )
	meadjun.x	⊢ 𝑆 = dom 𝑀
	meadjun.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑆 )
	meadjun.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑆 )
	meadjun.dj	⊢ ( 𝜑 → ( 𝐴 ∩ 𝐵 ) = ∅ )
Assertion	meadjun	⊢ ( 𝜑 → ( 𝑀 ‘ ( 𝐴 ∪ 𝐵 ) ) = ( ( 𝑀 ‘ 𝐴 ) +𝑒 ( 𝑀 ‘ 𝐵 ) ) )

Proof

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