Definition df-ovoln 40751

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.)

Assertion

Ref	Expression
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 = (Σ^ ` ( j e. NN |-> prod_ k e. x ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) } , RR* , < ) ) ) )

Distinct variable group:   x, k, y, z, i, j

Detailed syntax breakdown of Definition df-ovoln

Step	Hyp	Ref	Expression
1		covoln 40750	. 2 class voln*
2		vx	. . 3 setvar x
3		cfn 7955	. . 3 class Fin
4		vy	. . . 4 setvar y
5		cr 9935	. . . . . 6 class RR
6	2	cv 1482	. . . . . 6 class x
7		cmap 7857	. . . . . 6 class ^m
8	5, 6, 7	co 6650	. . . . 5 class ( RR ^m x )
9	8	cpw 4158	. . . 4 class ~P ( RR ^m x )
10		c0 3915	. . . . . 6 class (/)
11	6, 10	wceq 1483	. . . . 5 wff x = (/)
12		cc0 9936	. . . . 5 class 0
13	4	cv 1482	. . . . . . . . . 10 class y
14		vj	. . . . . . . . . . 11 setvar j
15		cn 11020	. . . . . . . . . . 11 class NN
16		vk	. . . . . . . . . . . 12 setvar k
17	16	cv 1482	. . . . . . . . . . . . 13 class k
18		cico 12177	. . . . . . . . . . . . . 14 class [,)
19	14	cv 1482	. . . . . . . . . . . . . . 15 class j
20		vi	. . . . . . . . . . . . . . . 16 setvar i
21	20	cv 1482	. . . . . . . . . . . . . . 15 class i
22	19, 21	cfv 5888	. . . . . . . . . . . . . 14 class ( i ` j )
23	18, 22	ccom 5118	. . . . . . . . . . . . 13 class ( [,) o. ( i ` j ) )
24	17, 23	cfv 5888	. . . . . . . . . . . 12 class ( ( [,) o. ( i ` j ) ) ` k )
25	16, 6, 24	cixp 7908	. . . . . . . . . . 11 class X_ k e. x ( ( [,) o. ( i ` j ) ) ` k )
26	14, 15, 25	ciun 4520	. . . . . . . . . 10 class U_ j e. NN X_ k e. x ( ( [,) o. ( i ` j ) ) ` k )
27	13, 26	wss 3574	. . . . . . . . 9 wff y C_ U_ j e. NN X_ k e. x ( ( [,) o. ( i ` j ) ) ` k )
28		vz	. . . . . . . . . . 11 setvar z
29	28	cv 1482	. . . . . . . . . 10 class z
30		cvol 23232	. . . . . . . . . . . . . 14 class vol
31	24, 30	cfv 5888	. . . . . . . . . . . . 13 class ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) )
32	6, 31, 16	cprod 14635	. . . . . . . . . . . 12 class prod_ k e. x ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) )
33	14, 15, 32	cmpt 4729	. . . . . . . . . . 11 class ( j e. NN |-> prod_ k e. x ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) )
34		csumge0 40579	. . . . . . . . . . 11 class Σ^
35	33, 34	cfv 5888	. . . . . . . . . 10 class (Σ^ ` ( j e. NN |-> prod_ k e. x ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) )
36	29, 35	wceq 1483	. . . . . . . . 9 wff z = (Σ^ ` ( j e. NN |-> prod_ k e. x ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) )
37	27, 36	wa 384	. . . . . . . 8 wff ( y C_ U_ j e. NN X_ k e. x ( ( [,) o. ( i ` j ) ) ` k ) /\ z = (Σ^ ` ( j e. NN |-> prod_ k e. x ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) )
38	5, 5	cxp 5112	. . . . . . . . . 10 class ( RR X. RR )
39	38, 6, 7	co 6650	. . . . . . . . 9 class ( ( RR X. RR ) ^m x )
40	39, 15, 7	co 6650	. . . . . . . 8 class ( ( ( RR X. RR ) ^m x ) ^m NN )
41	37, 20, 40	wrex 2913	. . . . . . 7 wff 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 = (Σ^ ` ( j e. NN |-> prod_ k e. x ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) )
42		cxr 10073	. . . . . . 7 class RR*
43	41, 28, 42	crab 2916	. . . . . 6 class { 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 = (Σ^ ` ( j e. NN |-> prod_ k e. x ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) }
44		clt 10074	. . . . . 6 class <
45	43, 42, 44	cinf 8347	. . . . 5 class 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 = (Σ^ ` ( j e. NN |-> prod_ k e. x ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) } , RR* , < )
46	11, 12, 45	cif 4086	. . . 4 class 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 = (Σ^ ` ( j e. NN |-> prod_ k e. x ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) } , RR* , < ) )
47	4, 9, 46	cmpt 4729	. . 3 class ( 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 = (Σ^ ` ( j e. NN |-> prod_ k e. x ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) } , RR* , < ) ) )
48	2, 3, 47	cmpt 4729	. 2 class ( 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 = (Σ^ ` ( j e. NN |-> prod_ k e. x ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) } , RR* , < ) ) ) )
49	1, 48	wceq 1483	1 wff 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 = (Σ^ ` ( j e. NN |-> prod_ k e. x ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) } , RR* , < ) ) ) )

This definition is referenced by:  ovnval  40755