Metamath Proof Explorer

Theorem ovn0

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

Ref Expression
Hypothesis ovn0.1 
|- ( ph -> X e. Fin )
Assertion ovn0 
|- ( ph -> ( ( voln* ` X ) ` (/) ) = 0 )

Proof

Step Hyp Ref Expression
1 ovn0.1 
 |-  ( ph -> X e. Fin )
2 0ss 
 |-  (/) C_ ( RR ^m X )
3 2 a1i 
 |-  ( ph -> (/) C_ ( RR ^m X ) )
4 0ss 
 |-  (/) C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k )
5 4 a1i 
 |-  ( z = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) -> (/) C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) )
6 id 
 |-  ( 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 ) ) ) ) )
7 5 6 jca 
 |-  ( z = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) -> ( (/) 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 simpr 
 |-  ( ( (/) 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 = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) )
9 7 8 impbii 
 |-  ( z = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) <-> ( (/) 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 rexbii 
 |-  ( 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 ) ( (/) 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 ) ) ) ) ) )
11 10 rgenw 
 |-  A. 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 ) ) ) ) <-> E. i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ( (/) 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 ) ) ) ) ) )
12 rabbi 
 |-  ( A. 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 ) ) ) ) <-> E. i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ( (/) 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 ) 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 ) ( (/) 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 ) ) ) ) ) } )
13 11 12 mpbi 
 |-  { 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 ) ) ) ) } = { z e. RR* | E. i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ( (/) 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 ) ) ) ) ) }
14 1 3 13 ovnval2 
 |-  ( ph -> ( ( voln* ` X ) ` (/) ) = if ( X = (/) , 0 , inf ( { 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 ) ) ) ) } , RR* , < ) ) )
15 simpr 
 |-  ( ( ph /\ X = (/) ) -> X = (/) )
16 15 iftrued 
 |-  ( ( ph /\ X = (/) ) -> if ( X = (/) , 0 , inf ( { 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 ) ) ) ) } , RR* , < ) ) = 0 )
17 iffalse 
 |-  ( -. X = (/) -> if ( X = (/) , 0 , inf ( { 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 ) ) ) ) } , RR* , < ) ) = inf ( { 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 ) ) ) ) } , RR* , < ) )
18 17 adantl 
 |-  ( ( ph /\ -. X = (/) ) -> if ( X = (/) , 0 , inf ( { 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 ) ) ) ) } , RR* , < ) ) = inf ( { 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 ) ) ) ) } , RR* , < ) )
19 1 adantr 
 |-  ( ( ph /\ -. X = (/) ) -> X e. Fin )
20 neqne 
 |-  ( -. X = (/) -> X =/= (/) )
21 20 adantl 
 |-  ( ( ph /\ -. X = (/) ) -> X =/= (/) )
22 eqid 
 |-  { 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 ) ) ) ) } = { 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 ) ) ) ) }
23 14 17 sylan9eq 
 |-  ( ( ph /\ -. X = (/) ) -> ( ( voln* ` X ) ` (/) ) = inf ( { 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 ) ) ) ) } , RR* , < ) )
24 23 eqcomd 
 |-  ( ( ph /\ -. X = (/) ) -> inf ( { 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 ) ) ) ) } , RR* , < ) = ( ( voln* ` X ) ` (/) ) )
25 1 ovnf 
 |-  ( ph -> ( voln* ` X ) : ~P ( RR ^m X ) --> ( 0 [,] +oo ) )
26 0elpw 
 |-  (/) e. ~P ( RR ^m X )
27 26 a1i 
 |-  ( ph -> (/) e. ~P ( RR ^m X ) )
28 25 27 ffvelrnd 
 |-  ( ph -> ( ( voln* ` X ) ` (/) ) e. ( 0 [,] +oo ) )
29 28 adantr 
 |-  ( ( ph /\ -. X = (/) ) -> ( ( voln* ` X ) ` (/) ) e. ( 0 [,] +oo ) )
30 24 29 eqeltrd 
 |-  ( ( ph /\ -. X = (/) ) -> inf ( { 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 ) ) ) ) } , RR* , < ) e. ( 0 [,] +oo ) )
31 eqidd 
 |-  ( m = l -> <. 1 , 0 >. = <. 1 , 0 >. )
32 31 cbvmptv 
 |-  ( m e. X |-> <. 1 , 0 >. ) = ( l e. X |-> <. 1 , 0 >. )
33 32 a1i 
 |-  ( h = j -> ( m e. X |-> <. 1 , 0 >. ) = ( l e. X |-> <. 1 , 0 >. ) )
34 33 cbvmptv 
 |-  ( h e. NN |-> ( m e. X |-> <. 1 , 0 >. ) ) = ( j e. NN |-> ( l e. X |-> <. 1 , 0 >. ) )
35 19 21 22 30 34 ovn0lem 
 |-  ( ( ph /\ -. X = (/) ) -> inf ( { 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 ) ) ) ) } , RR* , < ) = 0 )
36 18 35 eqtrd 
 |-  ( ( ph /\ -. X = (/) ) -> if ( X = (/) , 0 , inf ( { 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 ) ) ) ) } , RR* , < ) ) = 0 )
37 16 36 pm2.61dan 
 |-  ( ph -> if ( X = (/) , 0 , inf ( { 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 ) ) ) ) } , RR* , < ) ) = 0 )
38 14 37 eqtrd 
 |-  ( ph -> ( ( voln* ` X ) ` (/) ) = 0 )