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	$⊢ φ \to X \in Fin$
	vonsn.2	$⊢ φ \to A \in (ℝ^{X})$
Assertion	vonsn	$⊢ φ \to voln (X) (\{A\}) = 0$

Proof

Step	Hyp	Ref	Expression
1		vonsn.1	$⊢ φ \to X \in Fin$
2		vonsn.2	$⊢ φ \to A \in (ℝ^{X})$
3		fveq2	$⊢ X = \emptyset \to voln (X) = voln (\emptyset)$
4	3	fveq1d	$⊢ X = \emptyset \to voln (X) (\{A\}) = voln (\emptyset) (\{A\})$
5	4	adantl	$⊢ (φ \land X = \emptyset) \to voln (X) (\{A\}) = voln (\emptyset) (\{A\})$
6		0fi	$⊢ \emptyset \in Fin$
7	6	a1i	$⊢ (φ \land X = \emptyset) \to \emptyset \in Fin$
8	2	adantr	$⊢ (φ \land X = \emptyset) \to A \in (ℝ^{X})$
9		oveq2	$⊢ X = \emptyset \to ℝ^{X} = ℝ^{\emptyset}$
10	9	adantl	$⊢ (φ \land X = \emptyset) \to ℝ^{X} = ℝ^{\emptyset}$
11	8 10	eleqtrd	$⊢ (φ \land X = \emptyset) \to A \in (ℝ^{\emptyset})$
12	7 11	snvonmbl	$⊢ (φ \land X = \emptyset) \to \{A\} \in dom voln (\emptyset)$
13	12	von0val	$⊢ (φ \land X = \emptyset) \to voln (\emptyset) (\{A\}) = 0$
14	5 13	eqtrd	$⊢ (φ \land X = \emptyset) \to voln (X) (\{A\}) = 0$
15		neqne	$⊢ \neg X = \emptyset \to X \neq \emptyset$
16	15	adantl	$⊢ (φ \land \neg X = \emptyset) \to X \neq \emptyset$
17	2	rrxsnicc	$⊢ φ \to \underset{k \in X}{⨉} [A (k), A (k)] = \{A\}$
18	17	eqcomd	$⊢ φ \to \{A\} = \underset{k \in X}{⨉} [A (k), A (k)]$
19	18	fveq2d	$⊢ φ \to voln (X) (\{A\}) = voln (X) (\underset{k \in X}{⨉} [A (k), A (k)])$
20	19	adantr	$⊢ (φ \land X \neq \emptyset) \to voln (X) (\{A\}) = voln (X) (\underset{k \in X}{⨉} [A (k), A (k)])$
21	1	adantr	$⊢ (φ \land X \neq \emptyset) \to X \in Fin$
22		simpr	$⊢ (φ \land X \neq \emptyset) \to X \neq \emptyset$
23		elmapi	$⊢ A \in (ℝ^{X}) \to A : X ⟶ ℝ$
24	2 23	syl	$⊢ φ \to A : X ⟶ ℝ$
25	24	adantr	$⊢ (φ \land X \neq \emptyset) \to A : X ⟶ ℝ$
26		eqid	$⊢ \underset{k \in X}{⨉} [A (k), A (k)] = \underset{k \in X}{⨉} [A (k), A (k)]$
27	21 22 25 25 26	vonn0icc	$⊢ (φ \land X \neq \emptyset) \to voln (X) (\underset{k \in X}{⨉} [A (k), A (k)]) = \prod_{k \in X} vol ([A (k), A (k)])$
28	24	ffvelcdmda	$⊢ (φ \land k \in X) \to A (k) \in ℝ$
29	28	rexrd	$⊢ (φ \land k \in X) \to A (k) \in ℝ^{*}$
30		iccid	$⊢ A (k) \in ℝ^{*} \to [A (k), A (k)] = \{A (k)\}$
31	29 30	syl	$⊢ (φ \land k \in X) \to [A (k), A (k)] = \{A (k)\}$
32	31	fveq2d	$⊢ (φ \land k \in X) \to vol ([A (k), A (k)]) = vol (\{A (k)\})$
33		volsn	$⊢ A (k) \in ℝ \to vol (\{A (k)\}) = 0$
34	28 33	syl	$⊢ (φ \land k \in X) \to vol (\{A (k)\}) = 0$
35	32 34	eqtrd	$⊢ (φ \land k \in X) \to vol ([A (k), A (k)]) = 0$
36	35	prodeq2dv	$⊢ φ \to \prod_{k \in X} vol ([A (k), A (k)]) = \prod_{k \in X} 0$
37	36	adantr	$⊢ (φ \land X \neq \emptyset) \to \prod_{k \in X} vol ([A (k), A (k)]) = \prod_{k \in X} 0$
38		0cnd	$⊢ φ \to 0 \in ℂ$
39		fprodconst	$⊢ (X \in Fin \land 0 \in ℂ) \to \prod_{k \in X} 0 = 0^{\|X\|}$
40	1 38 39	syl2anc	$⊢ φ \to \prod_{k \in X} 0 = 0^{\|X\|}$
41	40	adantr	$⊢ (φ \land X \neq \emptyset) \to \prod_{k \in X} 0 = 0^{\|X\|}$
42		hashnncl	$⊢ X \in Fin \to (\|X\| \in ℕ \leftrightarrow X \neq \emptyset)$
43	1 42	syl	$⊢ φ \to (\|X\| \in ℕ \leftrightarrow X \neq \emptyset)$
44	43	adantr	$⊢ (φ \land X \neq \emptyset) \to (\|X\| \in ℕ \leftrightarrow X \neq \emptyset)$
45	22 44	mpbird	$⊢ (φ \land X \neq \emptyset) \to \|X\| \in ℕ$
46		0exp	$⊢ \|X\| \in ℕ \to 0^{\|X\|} = 0$
47	45 46	syl	$⊢ (φ \land X \neq \emptyset) \to 0^{\|X\|} = 0$
48	37 41 47	3eqtrd	$⊢ (φ \land X \neq \emptyset) \to \prod_{k \in X} vol ([A (k), A (k)]) = 0$
49	20 27 48	3eqtrd	$⊢ (φ \land X \neq \emptyset) \to voln (X) (\{A\}) = 0$
50	16 49	syldan	$⊢ (φ \land \neg X = \emptyset) \to voln (X) (\{A\}) = 0$
51	14 50	pm2.61dan	$⊢ φ \to voln (X) (\{A\}) = 0$

Metamath Proof Explorer

Theorem vonsn

Proof