Theorem ovnsplit

Description: The n-dimensional Lebesgue outer measure function is finitely sub-additive: application to a set split in two parts. (Contributed by Glauco Siliprandi, 3-Mar-2021)

	Ref	Expression
Hypotheses	ovnsplit.x	⊢ ( 𝜑 → 𝑋 ∈ Fin )
	ovnsplit.a	⊢ ( 𝜑 → 𝐴 ⊆ ( ℝ ↑m 𝑋 ) )
Assertion	ovnsplit	⊢ ( 𝜑 → ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ∩ 𝐵 ) ) +e ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ∖ 𝐵 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		ovnsplit.x	⊢ ( 𝜑 → 𝑋 ∈ Fin )
2		ovnsplit.a	⊢ ( 𝜑 → 𝐴 ⊆ ( ℝ ↑m 𝑋 ) )
3		inundif	⊢ ( ( 𝐴 ∩ 𝐵 ) ∪ ( 𝐴 ∖ 𝐵 ) ) = 𝐴
4	3	eqcomi	⊢ 𝐴 = ( ( 𝐴 ∩ 𝐵 ) ∪ ( 𝐴 ∖ 𝐵 ) )
5	4	fveq2i	⊢ ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) = ( ( voln* ‘ 𝑋 ) ‘ ( ( 𝐴 ∩ 𝐵 ) ∪ ( 𝐴 ∖ 𝐵 ) ) )
6	5	a1i	⊢ ( 𝜑 → ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) = ( ( voln* ‘ 𝑋 ) ‘ ( ( 𝐴 ∩ 𝐵 ) ∪ ( 𝐴 ∖ 𝐵 ) ) ) )
7	2	ssinss1d	⊢ ( 𝜑 → ( 𝐴 ∩ 𝐵 ) ⊆ ( ℝ ↑m 𝑋 ) )
8	2	ssdifssd	⊢ ( 𝜑 → ( 𝐴 ∖ 𝐵 ) ⊆ ( ℝ ↑m 𝑋 ) )
9	1 7 8	ovnsubadd2	⊢ ( 𝜑 → ( ( voln* ‘ 𝑋 ) ‘ ( ( 𝐴 ∩ 𝐵 ) ∪ ( 𝐴 ∖ 𝐵 ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ∩ 𝐵 ) ) +e ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ∖ 𝐵 ) ) ) )
10	6 9	eqbrtrd	⊢ ( 𝜑 → ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ∩ 𝐵 ) ) +e ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ∖ 𝐵 ) ) ) )