Metamath Proof Explorer


Theorem vonsn

Description: The n-dimensional Lebesgue measure of a singleton is zero. This is the first statement in Proposition 115G (e) of Fremlin1 p. 32. (Contributed by Glauco Siliprandi, 8-Apr-2021)

Ref Expression
Hypotheses vonsn.1
|- ( ph -> X e. Fin )
vonsn.2
|- ( ph -> A e. ( RR ^m X ) )
Assertion vonsn
|- ( ph -> ( ( voln ` X ) ` { A } ) = 0 )

Proof

Step Hyp Ref Expression
1 vonsn.1
 |-  ( ph -> X e. Fin )
2 vonsn.2
 |-  ( ph -> A e. ( RR ^m X ) )
3 fveq2
 |-  ( X = (/) -> ( voln ` X ) = ( voln ` (/) ) )
4 3 fveq1d
 |-  ( X = (/) -> ( ( voln ` X ) ` { A } ) = ( ( voln ` (/) ) ` { A } ) )
5 4 adantl
 |-  ( ( ph /\ X = (/) ) -> ( ( voln ` X ) ` { A } ) = ( ( voln ` (/) ) ` { A } ) )
6 0fin
 |-  (/) e. Fin
7 6 a1i
 |-  ( ( ph /\ X = (/) ) -> (/) e. Fin )
8 2 adantr
 |-  ( ( ph /\ X = (/) ) -> A e. ( RR ^m X ) )
9 oveq2
 |-  ( X = (/) -> ( RR ^m X ) = ( RR ^m (/) ) )
10 9 adantl
 |-  ( ( ph /\ X = (/) ) -> ( RR ^m X ) = ( RR ^m (/) ) )
11 8 10 eleqtrd
 |-  ( ( ph /\ X = (/) ) -> A e. ( RR ^m (/) ) )
12 7 11 snvonmbl
 |-  ( ( ph /\ X = (/) ) -> { A } e. dom ( voln ` (/) ) )
13 12 von0val
 |-  ( ( ph /\ X = (/) ) -> ( ( voln ` (/) ) ` { A } ) = 0 )
14 5 13 eqtrd
 |-  ( ( ph /\ X = (/) ) -> ( ( voln ` X ) ` { A } ) = 0 )
15 neqne
 |-  ( -. X = (/) -> X =/= (/) )
16 15 adantl
 |-  ( ( ph /\ -. X = (/) ) -> X =/= (/) )
17 2 rrxsnicc
 |-  ( ph -> X_ k e. X ( ( A ` k ) [,] ( A ` k ) ) = { A } )
18 17 eqcomd
 |-  ( ph -> { A } = X_ k e. X ( ( A ` k ) [,] ( A ` k ) ) )
19 18 fveq2d
 |-  ( ph -> ( ( voln ` X ) ` { A } ) = ( ( voln ` X ) ` X_ k e. X ( ( A ` k ) [,] ( A ` k ) ) ) )
20 19 adantr
 |-  ( ( ph /\ X =/= (/) ) -> ( ( voln ` X ) ` { A } ) = ( ( voln ` X ) ` X_ k e. X ( ( A ` k ) [,] ( A ` k ) ) ) )
21 1 adantr
 |-  ( ( ph /\ X =/= (/) ) -> X e. Fin )
22 simpr
 |-  ( ( ph /\ X =/= (/) ) -> X =/= (/) )
23 elmapi
 |-  ( A e. ( RR ^m X ) -> A : X --> RR )
24 2 23 syl
 |-  ( ph -> A : X --> RR )
25 24 adantr
 |-  ( ( ph /\ X =/= (/) ) -> A : X --> RR )
26 eqid
 |-  X_ k e. X ( ( A ` k ) [,] ( A ` k ) ) = X_ k e. X ( ( A ` k ) [,] ( A ` k ) )
27 21 22 25 25 26 vonn0icc
 |-  ( ( ph /\ X =/= (/) ) -> ( ( voln ` X ) ` X_ k e. X ( ( A ` k ) [,] ( A ` k ) ) ) = prod_ k e. X ( vol ` ( ( A ` k ) [,] ( A ` k ) ) ) )
28 24 ffvelrnda
 |-  ( ( ph /\ k e. X ) -> ( A ` k ) e. RR )
29 28 rexrd
 |-  ( ( ph /\ k e. X ) -> ( A ` k ) e. RR* )
30 iccid
 |-  ( ( A ` k ) e. RR* -> ( ( A ` k ) [,] ( A ` k ) ) = { ( A ` k ) } )
31 29 30 syl
 |-  ( ( ph /\ k e. X ) -> ( ( A ` k ) [,] ( A ` k ) ) = { ( A ` k ) } )
32 31 fveq2d
 |-  ( ( ph /\ k e. X ) -> ( vol ` ( ( A ` k ) [,] ( A ` k ) ) ) = ( vol ` { ( A ` k ) } ) )
33 volsn
 |-  ( ( A ` k ) e. RR -> ( vol ` { ( A ` k ) } ) = 0 )
34 28 33 syl
 |-  ( ( ph /\ k e. X ) -> ( vol ` { ( A ` k ) } ) = 0 )
35 32 34 eqtrd
 |-  ( ( ph /\ k e. X ) -> ( vol ` ( ( A ` k ) [,] ( A ` k ) ) ) = 0 )
36 35 prodeq2dv
 |-  ( ph -> prod_ k e. X ( vol ` ( ( A ` k ) [,] ( A ` k ) ) ) = prod_ k e. X 0 )
37 36 adantr
 |-  ( ( ph /\ X =/= (/) ) -> prod_ k e. X ( vol ` ( ( A ` k ) [,] ( A ` k ) ) ) = prod_ k e. X 0 )
38 0cnd
 |-  ( ph -> 0 e. CC )
39 fprodconst
 |-  ( ( X e. Fin /\ 0 e. CC ) -> prod_ k e. X 0 = ( 0 ^ ( # ` X ) ) )
40 1 38 39 syl2anc
 |-  ( ph -> prod_ k e. X 0 = ( 0 ^ ( # ` X ) ) )
41 40 adantr
 |-  ( ( ph /\ X =/= (/) ) -> prod_ k e. X 0 = ( 0 ^ ( # ` X ) ) )
42 hashnncl
 |-  ( X e. Fin -> ( ( # ` X ) e. NN <-> X =/= (/) ) )
43 1 42 syl
 |-  ( ph -> ( ( # ` X ) e. NN <-> X =/= (/) ) )
44 43 adantr
 |-  ( ( ph /\ X =/= (/) ) -> ( ( # ` X ) e. NN <-> X =/= (/) ) )
45 22 44 mpbird
 |-  ( ( ph /\ X =/= (/) ) -> ( # ` X ) e. NN )
46 0exp
 |-  ( ( # ` X ) e. NN -> ( 0 ^ ( # ` X ) ) = 0 )
47 45 46 syl
 |-  ( ( ph /\ X =/= (/) ) -> ( 0 ^ ( # ` X ) ) = 0 )
48 37 41 47 3eqtrd
 |-  ( ( ph /\ X =/= (/) ) -> prod_ k e. X ( vol ` ( ( A ` k ) [,] ( A ` k ) ) ) = 0 )
49 20 27 48 3eqtrd
 |-  ( ( ph /\ X =/= (/) ) -> ( ( voln ` X ) ` { A } ) = 0 )
50 16 49 syldan
 |-  ( ( ph /\ -. X = (/) ) -> ( ( voln ` X ) ` { A } ) = 0 )
51 14 50 pm2.61dan
 |-  ( ph -> ( ( voln ` X ) ` { A } ) = 0 )