Theorem omelesplit

Description: The outer measure of a set A is less than or equal to the extended addition of the outer measures of the decomposition induced on A by any E . Step (a) in the proof of Caratheodory's Method, Theorem 113C of Fremlin1 p. 19. (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Hypotheses	omelesplit.1	⊢ ( 𝜑 → 𝑂 ∈ OutMeas )
	omelesplit.2	⊢ 𝑋 = ∪ dom 𝑂
	omelesplit.3	⊢ ( 𝜑 → 𝐴 ⊆ 𝑋 )
Assertion	omelesplit	⊢ ( 𝜑 → ( 𝑂 ‘ 𝐴 ) ≤ ( ( 𝑂 ‘ ( 𝐴 ∩ 𝐸 ) ) +𝑒 ( 𝑂 ‘ ( 𝐴 ∖ 𝐸 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		omelesplit.1	⊢ ( 𝜑 → 𝑂 ∈ OutMeas )
2		omelesplit.2	⊢ 𝑋 = ∪ dom 𝑂
3		omelesplit.3	⊢ ( 𝜑 → 𝐴 ⊆ 𝑋 )
4		inundif	⊢ ( ( 𝐴 ∩ 𝐸 ) ∪ ( 𝐴 ∖ 𝐸 ) ) = 𝐴
5	4	eqcomi	⊢ 𝐴 = ( ( 𝐴 ∩ 𝐸 ) ∪ ( 𝐴 ∖ 𝐸 ) )
6	5	a1i	⊢ ( 𝜑 → 𝐴 = ( ( 𝐴 ∩ 𝐸 ) ∪ ( 𝐴 ∖ 𝐸 ) ) )
7	6	fveq2d	⊢ ( 𝜑 → ( 𝑂 ‘ 𝐴 ) = ( 𝑂 ‘ ( ( 𝐴 ∩ 𝐸 ) ∪ ( 𝐴 ∖ 𝐸 ) ) ) )
8		ssinss1	⊢ ( 𝐴 ⊆ 𝑋 → ( 𝐴 ∩ 𝐸 ) ⊆ 𝑋 )
9	3 8	syl	⊢ ( 𝜑 → ( 𝐴 ∩ 𝐸 ) ⊆ 𝑋 )
10	3	ssdifssd	⊢ ( 𝜑 → ( 𝐴 ∖ 𝐸 ) ⊆ 𝑋 )
11	1 2 9 10	omeunle	⊢ ( 𝜑 → ( 𝑂 ‘ ( ( 𝐴 ∩ 𝐸 ) ∪ ( 𝐴 ∖ 𝐸 ) ) ) ≤ ( ( 𝑂 ‘ ( 𝐴 ∩ 𝐸 ) ) +𝑒 ( 𝑂 ‘ ( 𝐴 ∖ 𝐸 ) ) ) )
12	7 11	eqbrtrd	⊢ ( 𝜑 → ( 𝑂 ‘ 𝐴 ) ≤ ( ( 𝑂 ‘ ( 𝐴 ∩ 𝐸 ) ) +𝑒 ( 𝑂 ‘ ( 𝐴 ∖ 𝐸 ) ) ) )