Metamath Proof Explorer

Theorem ovn0val

Description: The Lebesgue outer measure (for the zero dimensional space of reals) of every subset is zero. (Contributed by Glauco Siliprandi, 11-Oct-2020)

Ref Expression
Hypothesis ovn0val.1 
|- ( ph -> A C_ ( RR ^m (/) ) )
Assertion ovn0val 
|- ( ph -> ( ( voln* ` (/) ) ` A ) = 0 )

Proof

Step Hyp Ref Expression
1 ovn0val.1 
 |-  ( ph -> A C_ ( RR ^m (/) ) )
2 0fin 
 |-  (/) e. Fin
3 2 a1i 
 |-  ( ph -> (/) e. Fin )
4 eqid 
 |-  { z e. RR* | E. i e. ( ( ( RR X. RR ) ^m (/) ) ^m NN ) ( A C_ U_ j e. NN X_ k e. (/) ( ( [,) o. ( i ` j ) ) ` k ) /\ z = ( sum^ ` ( j e. NN |-> prod_ k e. (/) ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) } = { z e. RR* | E. i e. ( ( ( RR X. RR ) ^m (/) ) ^m NN ) ( A C_ U_ j e. NN X_ k e. (/) ( ( [,) o. ( i ` j ) ) ` k ) /\ z = ( sum^ ` ( j e. NN |-> prod_ k e. (/) ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) }
5 3 1 4 ovnval2 
 |-  ( ph -> ( ( voln* ` (/) ) ` A ) = if ( (/) = (/) , 0 , inf ( { z e. RR* | E. i e. ( ( ( RR X. RR ) ^m (/) ) ^m NN ) ( A C_ U_ j e. NN X_ k e. (/) ( ( [,) o. ( i ` j ) ) ` k ) /\ z = ( sum^ ` ( j e. NN |-> prod_ k e. (/) ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) } , RR* , < ) ) )
6 eqid 
 |-  (/) = (/)
7 iftrue 
 |-  ( (/) = (/) -> if ( (/) = (/) , 0 , inf ( { z e. RR* | E. i e. ( ( ( RR X. RR ) ^m (/) ) ^m NN ) ( A C_ U_ j e. NN X_ k e. (/) ( ( [,) o. ( i ` j ) ) ` k ) /\ z = ( sum^ ` ( j e. NN |-> prod_ k e. (/) ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) } , RR* , < ) ) = 0 )
8 6 7 ax-mp 
 |-  if ( (/) = (/) , 0 , inf ( { z e. RR* | E. i e. ( ( ( RR X. RR ) ^m (/) ) ^m NN ) ( A C_ U_ j e. NN X_ k e. (/) ( ( [,) o. ( i ` j ) ) ` k ) /\ z = ( sum^ ` ( j e. NN |-> prod_ k e. (/) ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) } , RR* , < ) ) = 0
9 8 a1i 
 |-  ( ph -> if ( (/) = (/) , 0 , inf ( { z e. RR* | E. i e. ( ( ( RR X. RR ) ^m (/) ) ^m NN ) ( A C_ U_ j e. NN X_ k e. (/) ( ( [,) o. ( i ` j ) ) ` k ) /\ z = ( sum^ ` ( j e. NN |-> prod_ k e. (/) ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) } , RR* , < ) ) = 0 )
10 5 9 eqtrd 
 |-  ( ph -> ( ( voln* ` (/) ) ` A ) = 0 )