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	⊢ ( 𝜑 → 𝑀 ∈ Meas )
	meadjunre.x	⊢ 𝑆 = dom 𝑀
	meadjunre.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑆 )
	meadjunre.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑆 )
	meadjunre.d	⊢ ( 𝜑 → ( 𝐴 ∩ 𝐵 ) = ∅ )
	meadjunre.r	⊢ ( 𝜑 → ( 𝑀 ‘ 𝐴 ) ∈ ℝ )
	meadjunre.f	⊢ ( 𝜑 → ( 𝑀 ‘ 𝐵 ) ∈ ℝ )
Assertion	meadjunre	⊢ ( 𝜑 → ( 𝑀 ‘ ( 𝐴 ∪ 𝐵 ) ) = ( ( 𝑀 ‘ 𝐴 ) + ( 𝑀 ‘ 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		meadjunre.m	⊢ ( 𝜑 → 𝑀 ∈ Meas )
2		meadjunre.x	⊢ 𝑆 = dom 𝑀
3		meadjunre.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑆 )
4		meadjunre.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑆 )
5		meadjunre.d	⊢ ( 𝜑 → ( 𝐴 ∩ 𝐵 ) = ∅ )
6		meadjunre.r	⊢ ( 𝜑 → ( 𝑀 ‘ 𝐴 ) ∈ ℝ )
7		meadjunre.f	⊢ ( 𝜑 → ( 𝑀 ‘ 𝐵 ) ∈ ℝ )
8	1 2 3 4 5	meadjun	⊢ ( 𝜑 → ( 𝑀 ‘ ( 𝐴 ∪ 𝐵 ) ) = ( ( 𝑀 ‘ 𝐴 ) +𝑒 ( 𝑀 ‘ 𝐵 ) ) )
9	6 7	rexaddd	⊢ ( 𝜑 → ( ( 𝑀 ‘ 𝐴 ) +𝑒 ( 𝑀 ‘ 𝐵 ) ) = ( ( 𝑀 ‘ 𝐴 ) + ( 𝑀 ‘ 𝐵 ) ) )
10	8 9	eqtrd	⊢ ( 𝜑 → ( 𝑀 ‘ ( 𝐴 ∪ 𝐵 ) ) = ( ( 𝑀 ‘ 𝐴 ) + ( 𝑀 ‘ 𝐵 ) ) )