Theorem meadjunre

Description: The measure of the union of two disjoint sets, with finite measure, is the sum of the measures, Property 112C (a) of Fremlin1 p. 15. (Contributed by Glauco Siliprandi, 8-Apr-2021)

	Ref	Expression
Hypotheses	meadjunre.m	$$⊢\phi \to M\in \mathrm{Meas}$$
	meadjunre.x	$$⊢S=\mathrm{dom}M$$
	meadjunre.a	$$⊢\phi \to A\in S$$
	meadjunre.b	$$⊢\phi \to B\in S$$
	meadjunre.d	$$⊢\phi \to A\cap B=\varnothing$$
	meadjunre.r	$$⊢\phi \to M\left(A\right)\in ℝ$$
	meadjunre.f	$$⊢\phi \to M\left(B\right)\in ℝ$$
Assertion	meadjunre	$$⊢\phi \to M\left(A\cup B\right)=M\left(A\right)+M\left(B\right)$$

Proof

Step	Hyp	Ref	Expression
1		meadjunre.m	$$⊢\phi \to M\in \mathrm{Meas}$$
2		meadjunre.x	$$⊢S=\mathrm{dom}M$$
3		meadjunre.a	$$⊢\phi \to A\in S$$
4		meadjunre.b	$$⊢\phi \to B\in S$$
5		meadjunre.d	$$⊢\phi \to A\cap B=\varnothing$$
6		meadjunre.r	$$⊢\phi \to M\left(A\right)\in ℝ$$
7		meadjunre.f	$$⊢\phi \to M\left(B\right)\in ℝ$$
8	1 2 3 4 5	meadjun	$$⊢\phi \to M\left(A\cup B\right)=M\left(A\right){+}_{𝑒}M\left(B\right)$$
9	6 7	rexaddd	$$⊢\phi \to M\left(A\right){+}_{𝑒}M\left(B\right)=M\left(A\right)+M\left(B\right)$$
10	8 9	eqtrd	$$⊢\phi \to M\left(A\cup B\right)=M\left(A\right)+M\left(B\right)$$