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		0fi	|- (/) 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	ffvelcdmda	|- ( ( 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 )