Theorem ovn0lem

Description: For any finite dimension, the Lebesgue outer measure of the empty set is zero. This is step (a)(ii) of the proof of Proposition 115D (a) of Fremlin1 p. 30. (Contributed by Glauco Siliprandi, 11-Oct-2020)

	Ref	Expression
Hypotheses	ovn0lem.x	|- ( ph -> X e. Fin )
	ovn0lem.n0	|- ( ph -> X =/= (/) )
	ovn0lem.m	|- M = { z e. RR* | E. i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) z = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) }
	ovn0lem.infm	|- ( ph -> inf ( M , RR* , < ) e. ( 0 [,] +oo ) )
	ovn0lem.i	|- I = ( j e. NN |-> ( l e. X |-> <. 1 , 0 >. ) )
Assertion	ovn0lem	|- ( ph -> inf ( M , RR* , < ) = 0 )

Proof

Step	Hyp	Ref	Expression
1		ovn0lem.x	|- ( ph -> X e. Fin )
2		ovn0lem.n0	|- ( ph -> X =/= (/) )
3		ovn0lem.m	|- M = { z e. RR* | E. i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) z = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) }
4		ovn0lem.infm	|- ( ph -> inf ( M , RR* , < ) e. ( 0 [,] +oo ) )
5		ovn0lem.i	|- I = ( j e. NN |-> ( l e. X |-> <. 1 , 0 >. ) )
6		iccssxr	|- ( 0 [,] +oo ) C_ RR*
7	6 4	sseldi	|- ( ph -> inf ( M , RR* , < ) e. RR* )
8		0xr	|- 0 e. RR*
9	8	a1i	|- ( ph -> 0 e. RR* )
10		ssrab2	|- { z e. RR* | E. i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) z = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) } C_ RR*
11	3 10	eqsstri	|- M C_ RR*
12	11	a1i	|- ( ph -> M C_ RR* )
13		1re	|- 1 e. RR
14		0re	|- 0 e. RR
15	13 14	pm3.2i	|- ( 1 e. RR /\ 0 e. RR )
16		opelxp	|- ( <. 1 , 0 >. e. ( RR X. RR ) <-> ( 1 e. RR /\ 0 e. RR ) )
17	15 16	mpbir	|- <. 1 , 0 >. e. ( RR X. RR )
18	17	a1i	|- ( ( ph /\ l e. X ) -> <. 1 , 0 >. e. ( RR X. RR ) )
19		eqid	|- ( l e. X |-> <. 1 , 0 >. ) = ( l e. X |-> <. 1 , 0 >. )
20	18 19	fmptd	|- ( ph -> ( l e. X |-> <. 1 , 0 >. ) : X --> ( RR X. RR ) )
21		reex	|- RR e. _V
22	21 21	xpex	|- ( RR X. RR ) e. _V
23	22	a1i	|- ( ph -> ( RR X. RR ) e. _V )
24		elmapg	|- ( ( ( RR X. RR ) e. _V /\ X e. Fin ) -> ( ( l e. X |-> <. 1 , 0 >. ) e. ( ( RR X. RR ) ^m X ) <-> ( l e. X |-> <. 1 , 0 >. ) : X --> ( RR X. RR ) ) )
25	23 1 24	syl2anc	|- ( ph -> ( ( l e. X |-> <. 1 , 0 >. ) e. ( ( RR X. RR ) ^m X ) <-> ( l e. X |-> <. 1 , 0 >. ) : X --> ( RR X. RR ) ) )
26	20 25	mpbird	|- ( ph -> ( l e. X |-> <. 1 , 0 >. ) e. ( ( RR X. RR ) ^m X ) )
27	26	adantr	|- ( ( ph /\ j e. NN ) -> ( l e. X |-> <. 1 , 0 >. ) e. ( ( RR X. RR ) ^m X ) )
28	27 5	fmptd	|- ( ph -> I : NN --> ( ( RR X. RR ) ^m X ) )
29		ovexd	|- ( ph -> ( ( RR X. RR ) ^m X ) e. _V )
30		nnex	|- NN e. _V
31	30	a1i	|- ( ph -> NN e. _V )
32		elmapg	|- ( ( ( ( RR X. RR ) ^m X ) e. _V /\ NN e. _V ) -> ( I e. ( ( ( RR X. RR ) ^m X ) ^m NN ) <-> I : NN --> ( ( RR X. RR ) ^m X ) ) )
33	29 31 32	syl2anc	|- ( ph -> ( I e. ( ( ( RR X. RR ) ^m X ) ^m NN ) <-> I : NN --> ( ( RR X. RR ) ^m X ) ) )
34	28 33	mpbird	|- ( ph -> I e. ( ( ( RR X. RR ) ^m X ) ^m NN ) )
35		n0	|- ( X =/= (/) <-> E. l l e. X )
36	2 35	sylib	|- ( ph -> E. l l e. X )
37	36	adantr	|- ( ( ph /\ j e. NN ) -> E. l l e. X )
38		nfv	|- F/ k ( ( ph /\ j e. NN ) /\ l e. X )
39		nfcv	|- F/_ k ( vol ` ( ( [,) o. ( I ` j ) ) ` l ) )
40	1	ad2antrr	|- ( ( ( ph /\ j e. NN ) /\ l e. X ) -> X e. Fin )
41	28	ffvelrnda	|- ( ( ph /\ j e. NN ) -> ( I ` j ) e. ( ( RR X. RR ) ^m X ) )
42		elmapi	|- ( ( I ` j ) e. ( ( RR X. RR ) ^m X ) -> ( I ` j ) : X --> ( RR X. RR ) )
43	41 42	syl	|- ( ( ph /\ j e. NN ) -> ( I ` j ) : X --> ( RR X. RR ) )
44	43	adantr	|- ( ( ( ph /\ j e. NN ) /\ k e. X ) -> ( I ` j ) : X --> ( RR X. RR ) )
45		simpr	|- ( ( ( ph /\ j e. NN ) /\ k e. X ) -> k e. X )
46	44 45	fvovco	|- ( ( ( ph /\ j e. NN ) /\ k e. X ) -> ( ( [,) o. ( I ` j ) ) ` k ) = ( ( 1st ` ( ( I ` j ) ` k ) ) [,) ( 2nd ` ( ( I ` j ) ` k ) ) ) )
47		simpr	|- ( ( ph /\ j e. NN ) -> j e. NN )
48	27	elexd	|- ( ( ph /\ j e. NN ) -> ( l e. X |-> <. 1 , 0 >. ) e. _V )
49	5	fvmpt2	|- ( ( j e. NN /\ ( l e. X |-> <. 1 , 0 >. ) e. _V ) -> ( I ` j ) = ( l e. X |-> <. 1 , 0 >. ) )
50	47 48 49	syl2anc	|- ( ( ph /\ j e. NN ) -> ( I ` j ) = ( l e. X |-> <. 1 , 0 >. ) )
51	50	adantr	|- ( ( ( ph /\ j e. NN ) /\ k e. X ) -> ( I ` j ) = ( l e. X |-> <. 1 , 0 >. ) )
52		eqidd	|- ( ( ( ( ph /\ j e. NN ) /\ k e. X ) /\ l = k ) -> <. 1 , 0 >. = <. 1 , 0 >. )
53	17	elexi	|- <. 1 , 0 >. e. _V
54	53	a1i	|- ( ( ( ph /\ j e. NN ) /\ k e. X ) -> <. 1 , 0 >. e. _V )
55	51 52 45 54	fvmptd	|- ( ( ( ph /\ j e. NN ) /\ k e. X ) -> ( ( I ` j ) ` k ) = <. 1 , 0 >. )
56	55	fveq2d	|- ( ( ( ph /\ j e. NN ) /\ k e. X ) -> ( 1st ` ( ( I ` j ) ` k ) ) = ( 1st ` <. 1 , 0 >. ) )
57	13	elexi	|- 1 e. _V
58	8	elexi	|- 0 e. _V
59	57 58	op1st	|- ( 1st ` <. 1 , 0 >. ) = 1
60	59	a1i	|- ( ( ( ph /\ j e. NN ) /\ k e. X ) -> ( 1st ` <. 1 , 0 >. ) = 1 )
61	56 60	eqtrd	|- ( ( ( ph /\ j e. NN ) /\ k e. X ) -> ( 1st ` ( ( I ` j ) ` k ) ) = 1 )
62	55	fveq2d	|- ( ( ( ph /\ j e. NN ) /\ k e. X ) -> ( 2nd ` ( ( I ` j ) ` k ) ) = ( 2nd ` <. 1 , 0 >. ) )
63	57 58	op2nd	|- ( 2nd ` <. 1 , 0 >. ) = 0
64	63	a1i	|- ( ( ( ph /\ j e. NN ) /\ k e. X ) -> ( 2nd ` <. 1 , 0 >. ) = 0 )
65	62 64	eqtrd	|- ( ( ( ph /\ j e. NN ) /\ k e. X ) -> ( 2nd ` ( ( I ` j ) ` k ) ) = 0 )
66	61 65	oveq12d	|- ( ( ( ph /\ j e. NN ) /\ k e. X ) -> ( ( 1st ` ( ( I ` j ) ` k ) ) [,) ( 2nd ` ( ( I ` j ) ` k ) ) ) = ( 1 [,) 0 ) )
67		0le1	|- 0 <_ 1
68		1xr	|- 1 e. RR*
69		ico0	|- ( ( 1 e. RR* /\ 0 e. RR* ) -> ( ( 1 [,) 0 ) = (/) <-> 0 <_ 1 ) )
70	68 8 69	mp2an	|- ( ( 1 [,) 0 ) = (/) <-> 0 <_ 1 )
71	67 70	mpbir	|- ( 1 [,) 0 ) = (/)
72	71	a1i	|- ( ( ( ph /\ j e. NN ) /\ k e. X ) -> ( 1 [,) 0 ) = (/) )
73	46 66 72	3eqtrd	|- ( ( ( ph /\ j e. NN ) /\ k e. X ) -> ( ( [,) o. ( I ` j ) ) ` k ) = (/) )
74	73	fveq2d	|- ( ( ( ph /\ j e. NN ) /\ k e. X ) -> ( vol ` ( ( [,) o. ( I ` j ) ) ` k ) ) = ( vol ` (/) ) )
75		vol0	|- ( vol ` (/) ) = 0
76	75	a1i	|- ( ( ( ph /\ j e. NN ) /\ k e. X ) -> ( vol ` (/) ) = 0 )
77	74 76	eqtrd	|- ( ( ( ph /\ j e. NN ) /\ k e. X ) -> ( vol ` ( ( [,) o. ( I ` j ) ) ` k ) ) = 0 )
78		0cn	|- 0 e. CC
79	78	a1i	|- ( ( ( ph /\ j e. NN ) /\ k e. X ) -> 0 e. CC )
80	77 79	eqeltrd	|- ( ( ( ph /\ j e. NN ) /\ k e. X ) -> ( vol ` ( ( [,) o. ( I ` j ) ) ` k ) ) e. CC )
81	80	adantlr	|- ( ( ( ( ph /\ j e. NN ) /\ l e. X ) /\ k e. X ) -> ( vol ` ( ( [,) o. ( I ` j ) ) ` k ) ) e. CC )
82		2fveq3	|- ( k = l -> ( vol ` ( ( [,) o. ( I ` j ) ) ` k ) ) = ( vol ` ( ( [,) o. ( I ` j ) ) ` l ) ) )
83		simpr	|- ( ( ( ph /\ j e. NN ) /\ l e. X ) -> l e. X )
84		eleq1w	|- ( k = l -> ( k e. X <-> l e. X ) )
85	84	anbi2d	|- ( k = l -> ( ( ( ph /\ j e. NN ) /\ k e. X ) <-> ( ( ph /\ j e. NN ) /\ l e. X ) ) )
86	82	eqeq1d	|- ( k = l -> ( ( vol ` ( ( [,) o. ( I ` j ) ) ` k ) ) = 0 <-> ( vol ` ( ( [,) o. ( I ` j ) ) ` l ) ) = 0 ) )
87	85 86	imbi12d	|- ( k = l -> ( ( ( ( ph /\ j e. NN ) /\ k e. X ) -> ( vol ` ( ( [,) o. ( I ` j ) ) ` k ) ) = 0 ) <-> ( ( ( ph /\ j e. NN ) /\ l e. X ) -> ( vol ` ( ( [,) o. ( I ` j ) ) ` l ) ) = 0 ) ) )
88	87 77	chvarvv	|- ( ( ( ph /\ j e. NN ) /\ l e. X ) -> ( vol ` ( ( [,) o. ( I ` j ) ) ` l ) ) = 0 )
89	38 39 40 81 82 83 88	fprod0	|- ( ( ( ph /\ j e. NN ) /\ l e. X ) -> prod_ k e. X ( vol ` ( ( [,) o. ( I ` j ) ) ` k ) ) = 0 )
90	89	ex	|- ( ( ph /\ j e. NN ) -> ( l e. X -> prod_ k e. X ( vol ` ( ( [,) o. ( I ` j ) ) ` k ) ) = 0 ) )
91	90	exlimdv	|- ( ( ph /\ j e. NN ) -> ( E. l l e. X -> prod_ k e. X ( vol ` ( ( [,) o. ( I ` j ) ) ` k ) ) = 0 ) )
92	37 91	mpd	|- ( ( ph /\ j e. NN ) -> prod_ k e. X ( vol ` ( ( [,) o. ( I ` j ) ) ` k ) ) = 0 )
93	92	mpteq2dva	|- ( ph -> ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( I ` j ) ) ` k ) ) ) = ( j e. NN |-> 0 ) )
94	93	fveq2d	|- ( ph -> ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( I ` j ) ) ` k ) ) ) ) = ( sum^ ` ( j e. NN |-> 0 ) ) )
95		nfv	|- F/ j ph
96	95 31	sge0z	|- ( ph -> ( sum^ ` ( j e. NN |-> 0 ) ) = 0 )
97		eqidd	|- ( ph -> 0 = 0 )
98	94 96 97	3eqtrrd	|- ( ph -> 0 = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( I ` j ) ) ` k ) ) ) ) )
99		fveq1	|- ( i = I -> ( i ` j ) = ( I ` j ) )
100	99	coeq2d	|- ( i = I -> ( [,) o. ( i ` j ) ) = ( [,) o. ( I ` j ) ) )
101	100	fveq1d	|- ( i = I -> ( ( [,) o. ( i ` j ) ) ` k ) = ( ( [,) o. ( I ` j ) ) ` k ) )
102	101	fveq2d	|- ( i = I -> ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) = ( vol ` ( ( [,) o. ( I ` j ) ) ` k ) ) )
103	102	ralrimivw	|- ( i = I -> A. k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) = ( vol ` ( ( [,) o. ( I ` j ) ) ` k ) ) )
104	103	prodeq2d	|- ( i = I -> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) = prod_ k e. X ( vol ` ( ( [,) o. ( I ` j ) ) ` k ) ) )
105	104	mpteq2dv	|- ( i = I -> ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) = ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( I ` j ) ) ` k ) ) ) )
106	105	fveq2d	|- ( i = I -> ( 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 ) ) ) ) )
107	106	rspceeqv	|- ( ( I e. ( ( ( RR X. RR ) ^m X ) ^m NN ) /\ 0 = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( I ` j ) ) ` k ) ) ) ) ) -> E. i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) 0 = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) )
108	34 98 107	syl2anc	|- ( ph -> E. i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) 0 = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) )
109	9 108	jca	|- ( ph -> ( 0 e. RR* /\ E. i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) 0 = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) )
110		eqeq1	|- ( z = 0 -> ( z = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) <-> 0 = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) )
111	110	rexbidv	|- ( z = 0 -> ( E. i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) z = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) <-> E. i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) 0 = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) )
112	111 3	elrab2	|- ( 0 e. M <-> ( 0 e. RR* /\ E. i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) 0 = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) )
113	109 112	sylibr	|- ( ph -> 0 e. M )
114		infxrlb	|- ( ( M C_ RR* /\ 0 e. M ) -> inf ( M , RR* , < ) <_ 0 )
115	12 113 114	syl2anc	|- ( ph -> inf ( M , RR* , < ) <_ 0 )
116		pnfxr	|- +oo e. RR*
117	116	a1i	|- ( ph -> +oo e. RR* )
118		iccgelb	|- ( ( 0 e. RR* /\ +oo e. RR* /\ inf ( M , RR* , < ) e. ( 0 [,] +oo ) ) -> 0 <_ inf ( M , RR* , < ) )
119	9 117 4 118	syl3anc	|- ( ph -> 0 <_ inf ( M , RR* , < ) )
120	7 9 115 119	xrletrid	|- ( ph -> inf ( M , RR* , < ) = 0 )