Metamath Proof Explorer

Theorem ovnssle

Description: The (multidimensional) Lebesgue outer measure of a subset is less than the L.o.m. of the whole set. This is step (iii) of the proof of Proposition 115D (a) of Fremlin1 p. 30. (Contributed by Glauco Siliprandi, 11-Oct-2020)

Ref Expression
Hypotheses ovnssle.1 
|- ( ph -> X e. Fin )
ovnssle.2 
|- ( ph -> A C_ B )
ovnssle.3 
|- ( ph -> B C_ ( RR ^m X ) )
Assertion ovnssle 
|- ( ph -> ( ( voln* ` X ) ` A ) <_ ( ( voln* ` X ) ` B ) )

Proof

Step Hyp Ref Expression
1 ovnssle.1 
 |-  ( ph -> X e. Fin )
2 ovnssle.2 
 |-  ( ph -> A C_ B )
3 ovnssle.3 
 |-  ( ph -> B C_ ( RR ^m X ) )
4 0le0 
 |-  0 <_ 0
5 4 a1i 
 |-  ( ( ph /\ X = (/) ) -> 0 <_ 0 )
6 fveq2 
 |-  ( X = (/) -> ( voln* ` X ) = ( voln* ` (/) ) )
7 6 fveq1d 
 |-  ( X = (/) -> ( ( voln* ` X ) ` A ) = ( ( voln* ` (/) ) ` A ) )
8 7 adantl 
 |-  ( ( ph /\ X = (/) ) -> ( ( voln* ` X ) ` A ) = ( ( voln* ` (/) ) ` A ) )
9 2 adantr 
 |-  ( ( ph /\ X = (/) ) -> A C_ B )
10 3 adantr 
 |-  ( ( ph /\ X = (/) ) -> B C_ ( RR ^m X ) )
11 simpr 
 |-  ( ( ph /\ X = (/) ) -> X = (/) )
12 11 oveq2d 
 |-  ( ( ph /\ X = (/) ) -> ( RR ^m X ) = ( RR ^m (/) ) )
13 10 12 sseqtrd 
 |-  ( ( ph /\ X = (/) ) -> B C_ ( RR ^m (/) ) )
14 9 13 sstrd 
 |-  ( ( ph /\ X = (/) ) -> A C_ ( RR ^m (/) ) )
15 14 ovn0val 
 |-  ( ( ph /\ X = (/) ) -> ( ( voln* ` (/) ) ` A ) = 0 )
16 8 15 eqtrd 
 |-  ( ( ph /\ X = (/) ) -> ( ( voln* ` X ) ` A ) = 0 )
17 6 fveq1d 
 |-  ( X = (/) -> ( ( voln* ` X ) ` B ) = ( ( voln* ` (/) ) ` B ) )
18 17 adantl 
 |-  ( ( ph /\ X = (/) ) -> ( ( voln* ` X ) ` B ) = ( ( voln* ` (/) ) ` B ) )
19 13 ovn0val 
 |-  ( ( ph /\ X = (/) ) -> ( ( voln* ` (/) ) ` B ) = 0 )
20 18 19 eqtrd 
 |-  ( ( ph /\ X = (/) ) -> ( ( voln* ` X ) ` B ) = 0 )
21 16 20 breq12d 
 |-  ( ( ph /\ X = (/) ) -> ( ( ( voln* ` X ) ` A ) <_ ( ( voln* ` X ) ` B ) <-> 0 <_ 0 ) )
22 5 21 mpbird 
 |-  ( ( ph /\ X = (/) ) -> ( ( voln* ` X ) ` A ) <_ ( ( voln* ` X ) ` B ) )
23 1 adantr 
 |-  ( ( ph /\ -. X = (/) ) -> X e. Fin )
24 neqne 
 |-  ( -. X = (/) -> X =/= (/) )
25 24 adantl 
 |-  ( ( ph /\ -. X = (/) ) -> X =/= (/) )
26 2 adantr 
 |-  ( ( ph /\ -. X = (/) ) -> A C_ B )
27 3 adantr 
 |-  ( ( ph /\ -. X = (/) ) -> B C_ ( RR ^m X ) )
28 eqid 
 |-  { z e. RR* | E. i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ( A C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) /\ z = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) } = { z e. RR* | E. i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ( A C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) /\ z = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) }
29 eqid 
 |-  { z e. RR* | E. i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ( B C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) /\ z = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) } = { z e. RR* | E. i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ( B C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) /\ z = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) }
30 23 25 26 27 28 29 ovnsslelem 
 |-  ( ( ph /\ -. X = (/) ) -> ( ( voln* ` X ) ` A ) <_ ( ( voln* ` X ) ` B ) )
31 22 30 pm2.61dan 
 |-  ( ph -> ( ( voln* ` X ) ` A ) <_ ( ( voln* ` X ) ` B ) )