Metamath Proof Explorer

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 
|- ( ph -> X e. Fin )
ovnsplit.a 
|- ( ph -> A C_ ( RR ^m X ) )
Assertion ovnsplit 
|- ( ph -> ( ( voln* ` X ) ` A ) <_ ( ( ( voln* ` X ) ` ( A i^i B ) ) +e ( ( voln* ` X ) ` ( A \ B ) ) ) )

Proof

Step Hyp Ref Expression
1 ovnsplit.x 
 |-  ( ph -> X e. Fin )
2 ovnsplit.a 
 |-  ( ph -> A C_ ( RR ^m X ) )
3 inundif 
 |-  ( ( A i^i B ) u. ( A \ B ) ) = A
4 3 eqcomi 
 |-  A = ( ( A i^i B ) u. ( A \ B ) )
5 4 fveq2i 
 |-  ( ( voln* ` X ) ` A ) = ( ( voln* ` X ) ` ( ( A i^i B ) u. ( A \ B ) ) )
6 5 a1i 
 |-  ( ph -> ( ( voln* ` X ) ` A ) = ( ( voln* ` X ) ` ( ( A i^i B ) u. ( A \ B ) ) ) )
7 2 ssinss1d 
 |-  ( ph -> ( A i^i B ) C_ ( RR ^m X ) )
8 2 ssdifssd 
 |-  ( ph -> ( A \ B ) C_ ( RR ^m X ) )
9 1 7 8 ovnsubadd2 
 |-  ( ph -> ( ( voln* ` X ) ` ( ( A i^i B ) u. ( A \ B ) ) ) <_ ( ( ( voln* ` X ) ` ( A i^i B ) ) +e ( ( voln* ` X ) ` ( A \ B ) ) ) )
10 6 9 eqbrtrd 
 |-  ( ph -> ( ( voln* ` X ) ` A ) <_ ( ( ( voln* ` X ) ` ( A i^i B ) ) +e ( ( voln* ` X ) ` ( A \ B ) ) ) )