Metamath Proof Explorer

Theorem ovnval

Description: Value of the Lebesgue outer measure for a given finite dimension. (Contributed by Glauco Siliprandi, 11-Oct-2020)

Ref Expression
Hypothesis ovnval.1 
|- ( ph -> X e. Fin )
Assertion 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* , < ) ) ) )

Proof

Step Hyp Ref Expression
1 ovnval.1 
 |-  ( ph -> X e. Fin )
2 df-ovoln 
 |-  voln* = ( x e. Fin |-> ( 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* , < ) ) ) )
3 oveq2 
 |-  ( x = X -> ( RR ^m x ) = ( RR ^m X ) )
4 3 pweqd 
 |-  ( x = X -> ~P ( RR ^m x ) = ~P ( RR ^m X ) )
5 eqeq1 
 |-  ( x = X -> ( x = (/) <-> X = (/) ) )
6 oveq2 
 |-  ( x = X -> ( ( RR X. RR ) ^m x ) = ( ( RR X. RR ) ^m X ) )
7 6 oveq1d 
 |-  ( x = X -> ( ( ( RR X. RR ) ^m x ) ^m NN ) = ( ( ( RR X. RR ) ^m X ) ^m NN ) )
8 ixpeq1 
 |-  ( x = X -> X_ k e. x ( ( [,) o. ( i ` j ) ) ` k ) = X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) )
9 8 iuneq2d 
 |-  ( x = X -> U_ j e. NN X_ k e. x ( ( [,) o. ( i ` j ) ) ` k ) = U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) )
10 9 sseq2d 
 |-  ( x = X -> ( y C_ U_ j e. NN X_ k e. x ( ( [,) o. ( i ` j ) ) ` k ) <-> y C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) ) )
11 simpl 
 |-  ( ( x = X /\ j e. NN ) -> x = X )
12 11 prodeq1d 
 |-  ( ( x = X /\ j e. NN ) -> prod_ k e. x ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) = prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) )
13 12 mpteq2dva 
 |-  ( x = X -> ( j e. NN |-> prod_ k e. x ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) = ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) )
14 13 fveq2d 
 |-  ( x = X -> ( sum^ ` ( j e. NN |-> prod_ k e. x ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) )
15 14 eqeq2d 
 |-  ( x = X -> ( z = ( sum^ ` ( j e. NN |-> prod_ k e. x ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) <-> z = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) )
16 10 15 anbi12d 
 |-  ( x = X -> ( ( 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 ) ) ) ) ) <-> ( 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 ) ) ) ) ) ) )
17 7 16 rexeqbidv 
 |-  ( x = X -> ( 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 ) ( 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 ) ) ) ) ) ) )
18 17 rabbidv 
 |-  ( x = X -> { 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 ) ( 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 ) ) ) ) ) } )
19 18 infeq1d 
 |-  ( x = X -> 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 ( { 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* , < ) )
20 5 19 ifbieq2d 
 |-  ( x = 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* , < ) ) = 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* , < ) ) )
21 4 20 mpteq12dv 
 |-  ( x = 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* , < ) ) ) = ( 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* , < ) ) ) )
22 ovex 
 |-  ( RR ^m X ) e. _V
23 22 pwex 
 |-  ~P ( RR ^m X ) e. _V
24 23 mptex 
 |-  ( 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* , < ) ) ) e. _V
25 24 a1i 
 |-  ( ph -> ( 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* , < ) ) ) e. _V )
26 2 21 1 25 fvmptd3 
 |-  ( 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* , < ) ) ) )