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	$⊢ φ \to X \in Fin$
	ovn0lem.n0	$⊢ φ \to X \neq \emptyset$
	ovn0lem.m	$⊢ M = \{z \in ℝ^{*} \| \exists i \in ({({ℝ^{2}}^{X})}^{ℕ}) z = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ i (j)) (k))))\}$
	ovn0lem.infm	$⊢ φ \to inf (M ℝ^{*} <) \in [0, +∞]$
	ovn0lem.i	$⊢ I = (j \in ℕ ⟼ (l \in X ⟼ ⟨1, 0⟩))$
Assertion	ovn0lem	$⊢ φ \to inf (M ℝ^{*} <) = 0$

Proof

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

Metamath Proof Explorer

Theorem ovn0lem

Proof