Metamath Proof Explorer

Theorem ovnval2

Description: Value of the Lebesgue outer measure of a subset A of the space of multidimensional real numbers. (Contributed by Glauco Siliprandi, 11-Oct-2020)

Ref Expression
Hypotheses ovnval2.1 
|- ( ph -> X e. Fin )
ovnval2.2 
|- ( ph -> A C_ ( RR ^m X ) )
ovnval2.3 
|- M = { 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 ) ) ) ) ) }
Assertion ovnval2 
|- ( ph -> ( ( voln* ` X ) ` A ) = if ( X = (/) , 0 , inf ( M , RR* , < ) ) )

Proof

Step Hyp Ref Expression
1 ovnval2.1 
 |-  ( ph -> X e. Fin )
2 ovnval2.2 
 |-  ( ph -> A C_ ( RR ^m X ) )
3 ovnval2.3 
 |-  M = { 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 ) ) ) ) ) }
4 1 ovnval 
 |-  ( ph -> ( voln* ` X ) = ( y e. ~P ( RR ^m X ) |-> if ( X = (/) , 0 , inf ( { z e. RR* | E. i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ( y 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 ) ) ) ) ) } , RR* , < ) ) ) )
5 biidd 
 |-  ( y = A -> ( X = (/) <-> X = (/) ) )
6 sseq1 
 |-  ( y = A -> ( y C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) <-> A C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) ) )
7 6 anbi1d 
 |-  ( y = A -> ( ( y 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 ) ) ) ) ) <-> ( 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 ) ) ) ) ) ) )
8 7 rexbidv 
 |-  ( y = A -> ( E. i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ( y 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 ) ) ) ) ) <-> 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 ) ) ) ) ) ) )
9 8 rabbidv 
 |-  ( y = A -> { z e. RR* | E. i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ( y 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 ) ) ) ) ) } )
10 9 3 eqtr4di 
 |-  ( y = A -> { z e. RR* | E. i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ( y 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 ) ) ) ) ) } = M )
11 10 infeq1d 
 |-  ( y = A -> inf ( { z e. RR* | E. i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ( y 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 ) ) ) ) ) } , RR* , < ) = inf ( M , RR* , < ) )
12 5 11 ifbieq2d 
 |-  ( y = A -> if ( X = (/) , 0 , inf ( { z e. RR* | E. i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ( y 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 ) ) ) ) ) } , RR* , < ) ) = if ( X = (/) , 0 , inf ( M , RR* , < ) ) )
13 12 adantl 
 |-  ( ( ph /\ y = A ) -> if ( X = (/) , 0 , inf ( { z e. RR* | E. i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ( y 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 ) ) ) ) ) } , RR* , < ) ) = if ( X = (/) , 0 , inf ( M , RR* , < ) ) )
14 ovexd 
 |-  ( ph -> ( RR ^m X ) e. _V )
15 14 2 ssexd 
 |-  ( ph -> A e. _V )
16 elpwg 
 |-  ( A e. _V -> ( A e. ~P ( RR ^m X ) <-> A C_ ( RR ^m X ) ) )
17 15 16 syl 
 |-  ( ph -> ( A e. ~P ( RR ^m X ) <-> A C_ ( RR ^m X ) ) )
18 2 17 mpbird 
 |-  ( ph -> A e. ~P ( RR ^m X ) )
19 c0ex 
 |-  0 e. _V
20 19 a1i 
 |-  ( ph -> 0 e. _V )
21 3 infeq1i 
 |-  inf ( M , RR* , < ) = inf ( { 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 ) ) ) ) ) } , RR* , < )
22 xrltso 
 |-  < Or RR*
23 22 infex 
 |-  inf ( { 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 ) ) ) ) ) } , RR* , < ) e. _V
24 23 a1i 
 |-  ( ph -> inf ( { 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 ) ) ) ) ) } , RR* , < ) e. _V )
25 21 24 eqeltrid 
 |-  ( ph -> inf ( M , RR* , < ) e. _V )
26 20 25 ifcld 
 |-  ( ph -> if ( X = (/) , 0 , inf ( M , RR* , < ) ) e. _V )
27 4 13 18 26 fvmptd 
 |-  ( ph -> ( ( voln* ` X ) ` A ) = if ( X = (/) , 0 , inf ( M , RR* , < ) ) )