ovnlecvr

Description: Given a subset of multidimensional reals and a set of half-open intervals that covers it, the Lebesgue outer measure of the set is bounded by the generalized sum of the pre-measure of the half-open intervals. The statement would also be true with X the empty set, but covers are not used for the zero-dimensional case. (Contributed by Glauco Siliprandi, 11-Oct-2020)

	Ref	Expression
Hypotheses	ovnlecvr.x	$⊢ φ \to X \in Fin$
	ovnlecvr.n0	$⊢ φ \to X \neq \emptyset$
	ovnlecvr.l	$⊢ L = (i \in ({ℝ^{2}}^{X}) ⟼ \prod_{k \in X} vol (([.) \circ i) (k)))$
	ovnlecvr.i	$⊢ φ \to I : ℕ ⟶ {ℝ^{2}}^{X}$
	ovnlecvr.ss	$⊢ φ \to A \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ I (j)) (k)$
Assertion	ovnlecvr	$⊢ φ \to voln* (X) (A) \leq sum^((j \in ℕ ⟼ L (I (j))))$

Proof

Step	Hyp	Ref	Expression
1		ovnlecvr.x	$⊢ φ \to X \in Fin$
2		ovnlecvr.n0	$⊢ φ \to X \neq \emptyset$
3		ovnlecvr.l	$⊢ L = (i \in ({ℝ^{2}}^{X}) ⟼ \prod_{k \in X} vol (([.) \circ i) (k)))$
4		ovnlecvr.i	$⊢ φ \to I : ℕ ⟶ {ℝ^{2}}^{X}$
5		ovnlecvr.ss	$⊢ φ \to A \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ I (j)) (k)$
6	4	ffvelrnda	$⊢ (φ \land j \in ℕ) \to I (j) \in ({ℝ^{2}}^{X})$
7		elmapi	$⊢ I (j) \in ({ℝ^{2}}^{X}) \to I (j) : X ⟶ ℝ^{2}$
8	6 7	syl	$⊢ (φ \land j \in ℕ) \to I (j) : X ⟶ ℝ^{2}$
9	8	hoissrrn	$⊢ (φ \land j \in ℕ) \to \underset{k \in X}{⨉} ([.) \circ I (j)) (k) \subseteq ℝ^{X}$
10	9	ralrimiva	$⊢ φ \to \forall j \in ℕ \underset{k \in X}{⨉} ([.) \circ I (j)) (k) \subseteq ℝ^{X}$
11		iunss	$⊢ ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ I (j)) (k) \subseteq ℝ^{X} \leftrightarrow \forall j \in ℕ \underset{k \in X}{⨉} ([.) \circ I (j)) (k) \subseteq ℝ^{X}$
12	10 11	sylibr	$⊢ φ \to ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ I (j)) (k) \subseteq ℝ^{X}$
13	5 12	sstrd	$⊢ φ \to A \subseteq ℝ^{X}$
14		eqid	$⊢ \{z \in ℝ^{} \| \exists i \in ({({ℝ^{2}}^{X})}^{ℕ}) (A \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ i (j)) (k) \land z = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ i (j)) (k)))))\} = \{z \in ℝ^{} \| \exists i \in ({({ℝ^{2}}^{X})}^{ℕ}) (A \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ i (j)) (k) \land z = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ i (j)) (k)))))\}$
15	1 2 13 14	ovnn0val	$⊢ φ \to voln* (X) (A) = sup (\{z \in ℝ^{} \| \exists i \in ({({ℝ^{2}}^{X})}^{ℕ}) (A \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ i (j)) (k) \land z = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ i (j)) (k)))))\} ℝ^{} <)$
16		ssrab2	$⊢ \{z \in ℝ^{} \| \exists i \in ({({ℝ^{2}}^{X})}^{ℕ}) (A \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ i (j)) (k) \land z = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ i (j)) (k)))))\} \subseteq ℝ^{}$
17	16	a1i	$⊢ φ \to \{z \in ℝ^{} \| \exists i \in ({({ℝ^{2}}^{X})}^{ℕ}) (A \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ i (j)) (k) \land z = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ i (j)) (k)))))\} \subseteq ℝ^{}$
18		nnex	$⊢ ℕ \in V$
19	18	a1i	$⊢ φ \to ℕ \in V$
20		icossicc	$⊢ [0, +∞) \subseteq [0, +∞]$
21		nfv	$⊢ Ⅎ k (φ \land j \in ℕ)$
22	1	adantr	$⊢ (φ \land j \in ℕ) \to X \in Fin$
23	21 22 3 8	hoiprodcl2	$⊢ (φ \land j \in ℕ) \to L (I (j)) \in [0, +∞)$
24	20 23	sselid	$⊢ (φ \land j \in ℕ) \to L (I (j)) \in [0, +∞]$
25		eqid	$⊢ (j \in ℕ ⟼ L (I (j))) = (j \in ℕ ⟼ L (I (j)))$
26	24 25	fmptd	$⊢ φ \to (j \in ℕ ⟼ L (I (j))) : ℕ ⟶ [0, +∞]$
27	19 26	sge0xrcl	$⊢ φ \to sum^((j \in ℕ ⟼ L (I (j)))) \in ℝ^{*}$
28		ovex	$⊢ {ℝ^{2}}^{X} \in V$
29	28 18	pm3.2i	$⊢ ({ℝ^{2}}^{X} \in V \land ℕ \in V)$
30		elmapg	$⊢ ({ℝ^{2}}^{X} \in V \land ℕ \in V) \to (I \in ({({ℝ^{2}}^{X})}^{ℕ}) \leftrightarrow I : ℕ ⟶ {ℝ^{2}}^{X})$
31	29 30	ax-mp	$⊢ I \in ({({ℝ^{2}}^{X})}^{ℕ}) \leftrightarrow I : ℕ ⟶ {ℝ^{2}}^{X}$
32	4 31	sylibr	$⊢ φ \to I \in ({({ℝ^{2}}^{X})}^{ℕ})$
33		coeq2	$⊢ i = I (j) \to [.) \circ i = [.) \circ I (j)$
34	33	fveq1d	$⊢ i = I (j) \to ([.) \circ i) (k) = ([.) \circ I (j)) (k)$
35	34	fveq2d	$⊢ i = I (j) \to vol (([.) \circ i) (k)) = vol (([.) \circ I (j)) (k))$
36	35	prodeq2ad	$⊢ i = I (j) \to \prod_{k \in X} vol (([.) \circ i) (k)) = \prod_{k \in X} vol (([.) \circ I (j)) (k))$
37		prodex	$⊢ \prod_{k \in X} vol (([.) \circ I (j)) (k)) \in V$
38	37	a1i	$⊢ (φ \land j \in ℕ) \to \prod_{k \in X} vol (([.) \circ I (j)) (k)) \in V$
39	3 36 6 38	fvmptd3	$⊢ (φ \land j \in ℕ) \to L (I (j)) = \prod_{k \in X} vol (([.) \circ I (j)) (k))$
40	39	mpteq2dva	$⊢ φ \to (j \in ℕ ⟼ L (I (j))) = (j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ I (j)) (k)))$
41	40	fveq2d	$⊢ φ \to sum^((j \in ℕ ⟼ L (I (j)))) = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ I (j)) (k))))$
42	5 41	jca	$⊢ φ \to (A \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ I (j)) (k) \land sum^((j \in ℕ ⟼ L (I (j)))) = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ I (j)) (k)))))$
43		nfv	$⊢ Ⅎ k i = I$
44		fveq1	$⊢ i = I \to i (j) = I (j)$
45	44	coeq2d	$⊢ i = I \to [.) \circ i (j) = [.) \circ I (j)$
46	45	fveq1d	$⊢ i = I \to ([.) \circ i (j)) (k) = ([.) \circ I (j)) (k)$
47	46	adantr	$⊢ (i = I \land k \in X) \to ([.) \circ i (j)) (k) = ([.) \circ I (j)) (k)$
48	43 47	ixpeq2d	$⊢ i = I \to \underset{k \in X}{⨉} ([.) \circ i (j)) (k) = \underset{k \in X}{⨉} ([.) \circ I (j)) (k)$
49	48	iuneq2d	$⊢ i = I \to ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ i (j)) (k) = ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ I (j)) (k)$
50	49	sseq2d	$⊢ i = I \to (A \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ i (j)) (k) \leftrightarrow A \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ I (j)) (k))$
51	46	fveq2d	$⊢ i = I \to vol (([.) \circ i (j)) (k)) = vol (([.) \circ I (j)) (k))$
52	51	prodeq2ad	$⊢ i = I \to \prod_{k \in X} vol (([.) \circ i (j)) (k)) = \prod_{k \in X} vol (([.) \circ I (j)) (k))$
53	52	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)))$
54	53	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))))$
55	54	eqeq2d	$⊢ i = I \to (sum^((j \in ℕ ⟼ L (I (j)))) = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ i (j)) (k)))) \leftrightarrow sum^((j \in ℕ ⟼ L (I (j)))) = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ I (j)) (k)))))$
56	50 55	anbi12d	$⊢ i = I \to ((A \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ i (j)) (k) \land sum^((j \in ℕ ⟼ L (I (j)))) = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ i (j)) (k))))) \leftrightarrow (A \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ I (j)) (k) \land sum^((j \in ℕ ⟼ L (I (j)))) = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ I (j)) (k))))))$
57	56	rspcev	$⊢ (I \in ({({ℝ^{2}}^{X})}^{ℕ}) \land (A \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ I (j)) (k) \land sum^((j \in ℕ ⟼ L (I (j)))) = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ I (j)) (k)))))) \to \exists i \in ({({ℝ^{2}}^{X})}^{ℕ}) (A \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ i (j)) (k) \land sum^((j \in ℕ ⟼ L (I (j)))) = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ i (j)) (k)))))$
58	32 42 57	syl2anc	$⊢ φ \to \exists i \in ({({ℝ^{2}}^{X})}^{ℕ}) (A \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ i (j)) (k) \land sum^((j \in ℕ ⟼ L (I (j)))) = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ i (j)) (k)))))$
59	27 58	jca	$⊢ φ \to (sum^((j \in ℕ ⟼ L (I (j)))) \in ℝ^{*} \land \exists i \in ({({ℝ^{2}}^{X})}^{ℕ}) (A \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ i (j)) (k) \land sum^((j \in ℕ ⟼ L (I (j)))) = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ i (j)) (k))))))$
60		eqeq1	$⊢ z = sum^((j \in ℕ ⟼ L (I (j)))) \to (z = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ i (j)) (k)))) \leftrightarrow sum^((j \in ℕ ⟼ L (I (j)))) = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ i (j)) (k)))))$
61	60	anbi2d	$⊢ z = sum^((j \in ℕ ⟼ L (I (j)))) \to ((A \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ i (j)) (k) \land z = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ i (j)) (k))))) \leftrightarrow (A \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ i (j)) (k) \land sum^((j \in ℕ ⟼ L (I (j)))) = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ i (j)) (k))))))$
62	61	rexbidv	$⊢ z = sum^((j \in ℕ ⟼ L (I (j)))) \to (\exists i \in ({({ℝ^{2}}^{X})}^{ℕ}) (A \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ i (j)) (k) \land z = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ i (j)) (k))))) \leftrightarrow \exists i \in ({({ℝ^{2}}^{X})}^{ℕ}) (A \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ i (j)) (k) \land sum^((j \in ℕ ⟼ L (I (j)))) = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ i (j)) (k))))))$
63	62	elrab	$⊢ sum^((j \in ℕ ⟼ L (I (j)))) \in \{z \in ℝ^{} \| \exists i \in ({({ℝ^{2}}^{X})}^{ℕ}) (A \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ i (j)) (k) \land z = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ i (j)) (k)))))\} \leftrightarrow (sum^((j \in ℕ ⟼ L (I (j)))) \in ℝ^{} \land \exists i \in ({({ℝ^{2}}^{X})}^{ℕ}) (A \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ i (j)) (k) \land sum^((j \in ℕ ⟼ L (I (j)))) = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ i (j)) (k))))))$
64	59 63	sylibr	$⊢ φ \to sum^((j \in ℕ ⟼ L (I (j)))) \in \{z \in ℝ^{*} \| \exists i \in ({({ℝ^{2}}^{X})}^{ℕ}) (A \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ i (j)) (k) \land z = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ i (j)) (k)))))\}$
65		infxrlb	$⊢ (\{z \in ℝ^{} \| \exists i \in ({({ℝ^{2}}^{X})}^{ℕ}) (A \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ i (j)) (k) \land z = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ i (j)) (k)))))\} \subseteq ℝ^{} \land sum^((j \in ℕ ⟼ L (I (j)))) \in \{z \in ℝ^{} \| \exists i \in ({({ℝ^{2}}^{X})}^{ℕ}) (A \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ i (j)) (k) \land z = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ i (j)) (k)))))\}) \to sup (\{z \in ℝ^{} \| \exists i \in ({({ℝ^{2}}^{X})}^{ℕ}) (A \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ i (j)) (k) \land z = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ i (j)) (k)))))\} ℝ^{*} <) \leq sum^((j \in ℕ ⟼ L (I (j))))$
66	17 64 65	syl2anc	$⊢ φ \to sup (\{z \in ℝ^{} \| \exists i \in ({({ℝ^{2}}^{X})}^{ℕ}) (A \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ i (j)) (k) \land z = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ i (j)) (k)))))\} ℝ^{} <) \leq sum^((j \in ℕ ⟼ L (I (j))))$
67	15 66	eqbrtrd	$⊢ φ \to voln* (X) (A) \leq sum^((j \in ℕ ⟼ L (I (j))))$

Metamath Proof Explorer

Theorem ovnlecvr

Proof