Metamath Proof Explorer

Definition df-ovoln

Description: Define the outer measure for the space of multidimensional real numbers. The cardinality of x is the dimension of the space modeled. Definition 115C of Fremlin1 p. 30. (Contributed by Glauco Siliprandi, 11-Oct-2020)

Ref Expression
Assertion 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* , < ) ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 covoln 
 |-  voln*
1 vx 
 |-  x
2 cfn 
 |-  Fin
3 vy 
 |-  y
4 cr 
 |-  RR
5 cmap 
 |-  ^m
6 1 cv 
 |-  x
7 4 6 5 co 
 |-  ( RR ^m x )
8 7 cpw 
 |-  ~P ( RR ^m x )
9 c0 
 |-  (/)
10 6 9 wceq 
 |-  x = (/)
11 cc0 
 |-  0
12 vz 
 |-  z
13 cxr 
 |-  RR*
14 vi 
 |-  i
15 4 4 cxp 
 |-  ( RR X. RR )
16 15 6 5 co 
 |-  ( ( RR X. RR ) ^m x )
17 cn 
 |-  NN
18 16 17 5 co 
 |-  ( ( ( RR X. RR ) ^m x ) ^m NN )
19 3 cv 
 |-  y
20 vj 
 |-  j
21 vk 
 |-  k
22 cico 
 |-  [,)
23 14 cv 
 |-  i
24 20 cv 
 |-  j
25 24 23 cfv 
 |-  ( i ` j )
26 22 25 ccom 
 |-  ( [,) o. ( i ` j ) )
27 21 cv 
 |-  k
28 27 26 cfv 
 |-  ( ( [,) o. ( i ` j ) ) ` k )
29 21 6 28 cixp 
 |-  X_ k e. x ( ( [,) o. ( i ` j ) ) ` k )
30 20 17 29 ciun 
 |-  U_ j e. NN X_ k e. x ( ( [,) o. ( i ` j ) ) ` k )
31 19 30 wss 
 |-  y C_ U_ j e. NN X_ k e. x ( ( [,) o. ( i ` j ) ) ` k )
32 12 cv 
 |-  z
33 csumge0 
 |-  sum^
34 cvol 
 |-  vol
35 28 34 cfv 
 |-  ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) )
36 6 35 21 cprod 
 |-  prod_ k e. x ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) )
37 20 17 36 cmpt 
 |-  ( j e. NN |-> prod_ k e. x ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) )
38 37 33 cfv 
 |-  ( sum^ ` ( j e. NN |-> prod_ k e. x ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) )
39 32 38 wceq 
 |-  z = ( sum^ ` ( j e. NN |-> prod_ k e. x ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) )
40 31 39 wa 
 |-  ( 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 ) ) ) ) )
41 40 14 18 wrex 
 |-  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 ) ) ) ) )
42 41 12 13 crab 
 |-  { 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 ) ) ) ) ) }
43 clt 
 |-  <
44 42 13 43 cinf 
 |-  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* , < )
45 10 11 44 cif 
 |-  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* , < ) )
46 3 8 45 cmpt 
 |-  ( 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* , < ) ) )
47 1 2 46 cmpt 
 |-  ( 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* , < ) ) ) )
48 0 47 wceq 
 |-  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* , < ) ) ) )