ovnlecvr2

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. (Contributed by Glauco Siliprandi, 24-Dec-2020)

	Ref	Expression
Hypotheses	ovnlecvr2.x	$⊢ φ \to X \in Fin$
	ovnlecvr2.c	$⊢ φ \to C : ℕ ⟶ ℝ^{X}$
	ovnlecvr2.d	$⊢ φ \to D : ℕ ⟶ ℝ^{X}$
	ovnlecvr2.s	$⊢ φ \to A \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} [C (j) (k), D (j) (k))$
	ovnlecvr2.l	$⊢ L = (x \in Fin ⟼ (a \in (ℝ^{x}), b \in (ℝ^{x}) ⟼ if (x = \emptyset, 0, \prod_{k \in x} vol ([a (k), b (k))))))$
Assertion	ovnlecvr2	$⊢ φ \to voln* (X) (A) \leq sum^((j \in ℕ ⟼ C (j) L (X) D (j)))$

Proof

Step	Hyp	Ref	Expression
1		ovnlecvr2.x	$⊢ φ \to X \in Fin$
2		ovnlecvr2.c	$⊢ φ \to C : ℕ ⟶ ℝ^{X}$
3		ovnlecvr2.d	$⊢ φ \to D : ℕ ⟶ ℝ^{X}$
4		ovnlecvr2.s	$⊢ φ \to A \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} [C (j) (k), D (j) (k))$
5		ovnlecvr2.l	$⊢ L = (x \in Fin ⟼ (a \in (ℝ^{x}), b \in (ℝ^{x}) ⟼ if (x = \emptyset, 0, \prod_{k \in x} vol ([a (k), b (k))))))$
6		fveq2	$⊢ X = \emptyset \to voln* (X) = voln* (\emptyset)$
7	6	fveq1d	$⊢ X = \emptyset \to voln* (X) (A) = voln* (\emptyset) (A)$
8	7	adantl	$⊢ (φ \land X = \emptyset) \to voln* (X) (A) = voln* (\emptyset) (A)$
9	4	adantr	$⊢ (φ \land X = \emptyset) \to A \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} [C (j) (k), D (j) (k))$
10		1nn	$⊢ 1 \in ℕ$
11		ne0i	$⊢ 1 \in ℕ \to ℕ \neq \emptyset$
12	10 11	ax-mp	$⊢ ℕ \neq \emptyset$
13	12	a1i	$⊢ φ \to ℕ \neq \emptyset$
14		iunconst	$⊢ ℕ \neq \emptyset \to ⋃_{j \in ℕ} \{\emptyset\} = \{\emptyset\}$
15	13 14	syl	$⊢ φ \to ⋃_{j \in ℕ} \{\emptyset\} = \{\emptyset\}$
16	15	adantr	$⊢ (φ \land X = \emptyset) \to ⋃_{j \in ℕ} \{\emptyset\} = \{\emptyset\}$
17		ixpeq1	$⊢ X = \emptyset \to \underset{k \in X}{⨉} [C (j) (k), D (j) (k)) = \underset{k \in \emptyset}{⨉} [C (j) (k), D (j) (k))$
18		ixp0x	$⊢ \underset{k \in \emptyset}{⨉} [C (j) (k), D (j) (k)) = \{\emptyset\}$
19	18	a1i	$⊢ X = \emptyset \to \underset{k \in \emptyset}{⨉} [C (j) (k), D (j) (k)) = \{\emptyset\}$
20	17 19	eqtrd	$⊢ X = \emptyset \to \underset{k \in X}{⨉} [C (j) (k), D (j) (k)) = \{\emptyset\}$
21	20	adantr	$⊢ (X = \emptyset \land j \in ℕ) \to \underset{k \in X}{⨉} [C (j) (k), D (j) (k)) = \{\emptyset\}$
22	21	iuneq2dv	$⊢ X = \emptyset \to ⋃_{j \in ℕ} \underset{k \in X}{⨉} [C (j) (k), D (j) (k)) = ⋃_{j \in ℕ} \{\emptyset\}$
23	22	adantl	$⊢ (φ \land X = \emptyset) \to ⋃_{j \in ℕ} \underset{k \in X}{⨉} [C (j) (k), D (j) (k)) = ⋃_{j \in ℕ} \{\emptyset\}$
24		reex	$⊢ ℝ \in V$
25		mapdm0	$⊢ ℝ \in V \to ℝ^{\emptyset} = \{\emptyset\}$
26	24 25	ax-mp	$⊢ ℝ^{\emptyset} = \{\emptyset\}$
27	26	a1i	$⊢ (φ \land X = \emptyset) \to ℝ^{\emptyset} = \{\emptyset\}$
28	16 23 27	3eqtr4d	$⊢ (φ \land X = \emptyset) \to ⋃_{j \in ℕ} \underset{k \in X}{⨉} [C (j) (k), D (j) (k)) = ℝ^{\emptyset}$
29	9 28	sseqtrd	$⊢ (φ \land X = \emptyset) \to A \subseteq ℝ^{\emptyset}$
30	29	ovn0val	$⊢ (φ \land X = \emptyset) \to voln* (\emptyset) (A) = 0$
31	8 30	eqtrd	$⊢ (φ \land X = \emptyset) \to voln* (X) (A) = 0$
32		nfv	$⊢ Ⅎ j φ$
33		nnex	$⊢ ℕ \in V$
34	33	a1i	$⊢ φ \to ℕ \in V$
35		icossicc	$⊢ [0, +∞) \subseteq [0, +∞]$
36	1	adantr	$⊢ (φ \land j \in ℕ) \to X \in Fin$
37	2	ffvelcdmda	$⊢ (φ \land j \in ℕ) \to C (j) \in (ℝ^{X})$
38		elmapi	$⊢ C (j) \in (ℝ^{X}) \to C (j) : X ⟶ ℝ$
39	37 38	syl	$⊢ (φ \land j \in ℕ) \to C (j) : X ⟶ ℝ$
40	3	ffvelcdmda	$⊢ (φ \land j \in ℕ) \to D (j) \in (ℝ^{X})$
41		elmapi	$⊢ D (j) \in (ℝ^{X}) \to D (j) : X ⟶ ℝ$
42	40 41	syl	$⊢ (φ \land j \in ℕ) \to D (j) : X ⟶ ℝ$
43	5 36 39 42	hoidmvcl	$⊢ (φ \land j \in ℕ) \to C (j) L (X) D (j) \in [0, +∞)$
44	35 43	sselid	$⊢ (φ \land j \in ℕ) \to C (j) L (X) D (j) \in [0, +∞]$
45	32 34 44	sge0ge0mpt	$⊢ φ \to 0 \leq sum^((j \in ℕ ⟼ C (j) L (X) D (j)))$
46	45	adantr	$⊢ (φ \land X = \emptyset) \to 0 \leq sum^((j \in ℕ ⟼ C (j) L (X) D (j)))$
47	31 46	eqbrtrd	$⊢ (φ \land X = \emptyset) \to voln* (X) (A) \leq sum^((j \in ℕ ⟼ C (j) L (X) D (j)))$
48		simpl	$⊢ (φ \land \neg X = \emptyset) \to φ$
49		neqne	$⊢ \neg X = \emptyset \to X \neq \emptyset$
50	49	adantl	$⊢ (φ \land \neg X = \emptyset) \to X \neq \emptyset$
51	1	adantr	$⊢ (φ \land X \neq \emptyset) \to X \in Fin$
52		simpr	$⊢ (φ \land X \neq \emptyset) \to X \neq \emptyset$
53	39	ffvelcdmda	$⊢ ((φ \land j \in ℕ) \land k \in X) \to C (j) (k) \in ℝ$
54	42	ffvelcdmda	$⊢ ((φ \land j \in ℕ) \land k \in X) \to D (j) (k) \in ℝ$
55	54	rexrd	$⊢ ((φ \land j \in ℕ) \land k \in X) \to D (j) (k) \in ℝ^{*}$
56		icossre	$⊢ (C (j) (k) \in ℝ \land D (j) (k) \in ℝ^{*}) \to [C (j) (k), D (j) (k)) \subseteq ℝ$
57	53 55 56	syl2anc	$⊢ ((φ \land j \in ℕ) \land k \in X) \to [C (j) (k), D (j) (k)) \subseteq ℝ$
58	57	ralrimiva	$⊢ (φ \land j \in ℕ) \to \forall k \in X [C (j) (k), D (j) (k)) \subseteq ℝ$
59		ss2ixp	$⊢ \forall k \in X [C (j) (k), D (j) (k)) \subseteq ℝ \to \underset{k \in X}{⨉} [C (j) (k), D (j) (k)) \subseteq \underset{k \in X}{⨉} ℝ$
60	58 59	syl	$⊢ (φ \land j \in ℕ) \to \underset{k \in X}{⨉} [C (j) (k), D (j) (k)) \subseteq \underset{k \in X}{⨉} ℝ$
61	24	a1i	$⊢ φ \to ℝ \in V$
62		ixpconstg	$⊢ (X \in Fin \land ℝ \in V) \to \underset{k \in X}{⨉} ℝ = ℝ^{X}$
63	1 61 62	syl2anc	$⊢ φ \to \underset{k \in X}{⨉} ℝ = ℝ^{X}$
64	63	adantr	$⊢ (φ \land j \in ℕ) \to \underset{k \in X}{⨉} ℝ = ℝ^{X}$
65	60 64	sseqtrd	$⊢ (φ \land j \in ℕ) \to \underset{k \in X}{⨉} [C (j) (k), D (j) (k)) \subseteq ℝ^{X}$
66	65	ralrimiva	$⊢ φ \to \forall j \in ℕ \underset{k \in X}{⨉} [C (j) (k), D (j) (k)) \subseteq ℝ^{X}$
67		iunss	$⊢ ⋃_{j \in ℕ} \underset{k \in X}{⨉} [C (j) (k), D (j) (k)) \subseteq ℝ^{X} \leftrightarrow \forall j \in ℕ \underset{k \in X}{⨉} [C (j) (k), D (j) (k)) \subseteq ℝ^{X}$
68	66 67	sylibr	$⊢ φ \to ⋃_{j \in ℕ} \underset{k \in X}{⨉} [C (j) (k), D (j) (k)) \subseteq ℝ^{X}$
69	4 68	sstrd	$⊢ φ \to A \subseteq ℝ^{X}$
70	69	adantr	$⊢ (φ \land X \neq \emptyset) \to A \subseteq ℝ^{X}$
71		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)))))\}$
72	51 52 70 71	ovnn0val	$⊢ (φ \land X \neq \emptyset) \to voln* (X) (A) = inf (\{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)))))\} ℝ^{} <)$
73		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 ℝ^{}$
74	73	a1i	$⊢ (φ \land X \neq \emptyset) \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 ℝ^{}$
75	32 34 44	sge0xrclmpt	$⊢ φ \to sum^((j \in ℕ ⟼ C (j) L (X) D (j))) \in ℝ^{*}$
76	75	adantr	$⊢ (φ \land X \neq \emptyset) \to sum^((j \in ℕ ⟼ C (j) L (X) D (j))) \in ℝ^{*}$
77		opelxpi	$⊢ (C (j) (k) \in ℝ \land D (j) (k) \in ℝ) \to ⟨C (j) (k), D (j) (k)⟩ \in ℝ^{2}$
78	53 54 77	syl2anc	$⊢ ((φ \land j \in ℕ) \land k \in X) \to ⟨C (j) (k), D (j) (k)⟩ \in ℝ^{2}$
79	78	fmpttd	$⊢ (φ \land j \in ℕ) \to (k \in X ⟼ ⟨C (j) (k), D (j) (k)⟩) : X ⟶ ℝ^{2}$
80	24 24	xpex	$⊢ ℝ^{2} \in V$
81	80	a1i	$⊢ (φ \land j \in ℕ) \to ℝ^{2} \in V$
82		elmapg	$⊢ (ℝ^{2} \in V \land X \in Fin) \to ((k \in X ⟼ ⟨C (j) (k), D (j) (k)⟩) \in ({ℝ^{2}}^{X}) \leftrightarrow (k \in X ⟼ ⟨C (j) (k), D (j) (k)⟩) : X ⟶ ℝ^{2})$
83	81 36 82	syl2anc	$⊢ (φ \land j \in ℕ) \to ((k \in X ⟼ ⟨C (j) (k), D (j) (k)⟩) \in ({ℝ^{2}}^{X}) \leftrightarrow (k \in X ⟼ ⟨C (j) (k), D (j) (k)⟩) : X ⟶ ℝ^{2})$
84	79 83	mpbird	$⊢ (φ \land j \in ℕ) \to (k \in X ⟼ ⟨C (j) (k), D (j) (k)⟩) \in ({ℝ^{2}}^{X})$
85	84	fmpttd	$⊢ φ \to (j \in ℕ ⟼ (k \in X ⟼ ⟨C (j) (k), D (j) (k)⟩)) : ℕ ⟶ {ℝ^{2}}^{X}$
86		ovexd	$⊢ φ \to {ℝ^{2}}^{X} \in V$
87		elmapg	$⊢ ({ℝ^{2}}^{X} \in V \land ℕ \in V) \to ((j \in ℕ ⟼ (k \in X ⟼ ⟨C (j) (k), D (j) (k)⟩)) \in ({({ℝ^{2}}^{X})}^{ℕ}) \leftrightarrow (j \in ℕ ⟼ (k \in X ⟼ ⟨C (j) (k), D (j) (k)⟩)) : ℕ ⟶ {ℝ^{2}}^{X})$
88	86 34 87	syl2anc	$⊢ φ \to ((j \in ℕ ⟼ (k \in X ⟼ ⟨C (j) (k), D (j) (k)⟩)) \in ({({ℝ^{2}}^{X})}^{ℕ}) \leftrightarrow (j \in ℕ ⟼ (k \in X ⟼ ⟨C (j) (k), D (j) (k)⟩)) : ℕ ⟶ {ℝ^{2}}^{X})$
89	85 88	mpbird	$⊢ φ \to (j \in ℕ ⟼ (k \in X ⟼ ⟨C (j) (k), D (j) (k)⟩)) \in ({({ℝ^{2}}^{X})}^{ℕ})$
90	89	adantr	$⊢ (φ \land X \neq \emptyset) \to (j \in ℕ ⟼ (k \in X ⟼ ⟨C (j) (k), D (j) (k)⟩)) \in ({({ℝ^{2}}^{X})}^{ℕ})$
91		simpr	$⊢ (φ \land j \in ℕ) \to j \in ℕ$
92		mptexg	$⊢ X \in Fin \to (k \in X ⟼ ⟨C (j) (k), D (j) (k)⟩) \in V$
93	1 92	syl	$⊢ φ \to (k \in X ⟼ ⟨C (j) (k), D (j) (k)⟩) \in V$
94	93	adantr	$⊢ (φ \land j \in ℕ) \to (k \in X ⟼ ⟨C (j) (k), D (j) (k)⟩) \in V$
95		eqid	$⊢ (j \in ℕ ⟼ (k \in X ⟼ ⟨C (j) (k), D (j) (k)⟩)) = (j \in ℕ ⟼ (k \in X ⟼ ⟨C (j) (k), D (j) (k)⟩))$
96	95	fvmpt2	$⊢ (j \in ℕ \land (k \in X ⟼ ⟨C (j) (k), D (j) (k)⟩) \in V) \to (j \in ℕ ⟼ (k \in X ⟼ ⟨C (j) (k), D (j) (k)⟩)) (j) = (k \in X ⟼ ⟨C (j) (k), D (j) (k)⟩)$
97	91 94 96	syl2anc	$⊢ (φ \land j \in ℕ) \to (j \in ℕ ⟼ (k \in X ⟼ ⟨C (j) (k), D (j) (k)⟩)) (j) = (k \in X ⟼ ⟨C (j) (k), D (j) (k)⟩)$
98	97	coeq2d	$⊢ (φ \land j \in ℕ) \to [.) \circ (j \in ℕ ⟼ (k \in X ⟼ ⟨C (j) (k), D (j) (k)⟩)) (j) = [.) \circ (k \in X ⟼ ⟨C (j) (k), D (j) (k)⟩)$
99	98	fveq1d	$⊢ (φ \land j \in ℕ) \to ([.) \circ (j \in ℕ ⟼ (k \in X ⟼ ⟨C (j) (k), D (j) (k)⟩)) (j)) (k) = ([.) \circ (k \in X ⟼ ⟨C (j) (k), D (j) (k)⟩)) (k)$
100	99	adantr	$⊢ ((φ \land j \in ℕ) \land k \in X) \to ([.) \circ (j \in ℕ ⟼ (k \in X ⟼ ⟨C (j) (k), D (j) (k)⟩)) (j)) (k) = ([.) \circ (k \in X ⟼ ⟨C (j) (k), D (j) (k)⟩)) (k)$
101	79	adantr	$⊢ ((φ \land j \in ℕ) \land k \in X) \to (k \in X ⟼ ⟨C (j) (k), D (j) (k)⟩) : X ⟶ ℝ^{2}$
102		simpr	$⊢ ((φ \land j \in ℕ) \land k \in X) \to k \in X$
103	101 102	fvovco	$⊢ ((φ \land j \in ℕ) \land k \in X) \to ([.) \circ (k \in X ⟼ ⟨C (j) (k), D (j) (k)⟩)) (k) = [1^{st} ((k \in X ⟼ ⟨C (j) (k), D (j) (k)⟩) (k)), 2^{nd} ((k \in X ⟼ ⟨C (j) (k), D (j) (k)⟩) (k)))$
104		simpr	$⊢ (φ \land k \in X) \to k \in X$
105		opex	$⊢ ⟨C (j) (k), D (j) (k)⟩ \in V$
106	105	a1i	$⊢ (φ \land k \in X) \to ⟨C (j) (k), D (j) (k)⟩ \in V$
107		eqid	$⊢ (k \in X ⟼ ⟨C (j) (k), D (j) (k)⟩) = (k \in X ⟼ ⟨C (j) (k), D (j) (k)⟩)$
108	107	fvmpt2	$⊢ (k \in X \land ⟨C (j) (k), D (j) (k)⟩ \in V) \to (k \in X ⟼ ⟨C (j) (k), D (j) (k)⟩) (k) = ⟨C (j) (k), D (j) (k)⟩$
109	104 106 108	syl2anc	$⊢ (φ \land k \in X) \to (k \in X ⟼ ⟨C (j) (k), D (j) (k)⟩) (k) = ⟨C (j) (k), D (j) (k)⟩$
110	109	fveq2d	$⊢ (φ \land k \in X) \to 1^{st} ((k \in X ⟼ ⟨C (j) (k), D (j) (k)⟩) (k)) = 1^{st} (⟨C (j) (k), D (j) (k)⟩)$
111		fvex	$⊢ C (j) (k) \in V$
112		fvex	$⊢ D (j) (k) \in V$
113		op1stg	$⊢ (C (j) (k) \in V \land D (j) (k) \in V) \to 1^{st} (⟨C (j) (k), D (j) (k)⟩) = C (j) (k)$
114	111 112 113	mp2an	$⊢ 1^{st} (⟨C (j) (k), D (j) (k)⟩) = C (j) (k)$
115	114	a1i	$⊢ (φ \land k \in X) \to 1^{st} (⟨C (j) (k), D (j) (k)⟩) = C (j) (k)$
116	110 115	eqtrd	$⊢ (φ \land k \in X) \to 1^{st} ((k \in X ⟼ ⟨C (j) (k), D (j) (k)⟩) (k)) = C (j) (k)$
117	109	fveq2d	$⊢ (φ \land k \in X) \to 2^{nd} ((k \in X ⟼ ⟨C (j) (k), D (j) (k)⟩) (k)) = 2^{nd} (⟨C (j) (k), D (j) (k)⟩)$
118	111 112	op2nd	$⊢ 2^{nd} (⟨C (j) (k), D (j) (k)⟩) = D (j) (k)$
119	118	a1i	$⊢ (φ \land k \in X) \to 2^{nd} (⟨C (j) (k), D (j) (k)⟩) = D (j) (k)$
120	117 119	eqtrd	$⊢ (φ \land k \in X) \to 2^{nd} ((k \in X ⟼ ⟨C (j) (k), D (j) (k)⟩) (k)) = D (j) (k)$
121	116 120	oveq12d	$⊢ (φ \land k \in X) \to [1^{st} ((k \in X ⟼ ⟨C (j) (k), D (j) (k)⟩) (k)), 2^{nd} ((k \in X ⟼ ⟨C (j) (k), D (j) (k)⟩) (k))) = [C (j) (k), D (j) (k))$
122	121	adantlr	$⊢ ((φ \land j \in ℕ) \land k \in X) \to [1^{st} ((k \in X ⟼ ⟨C (j) (k), D (j) (k)⟩) (k)), 2^{nd} ((k \in X ⟼ ⟨C (j) (k), D (j) (k)⟩) (k))) = [C (j) (k), D (j) (k))$
123	100 103 122	3eqtrrd	$⊢ ((φ \land j \in ℕ) \land k \in X) \to [C (j) (k), D (j) (k)) = ([.) \circ (j \in ℕ ⟼ (k \in X ⟼ ⟨C (j) (k), D (j) (k)⟩)) (j)) (k)$
124	123	ixpeq2dva	$⊢ (φ \land j \in ℕ) \to \underset{k \in X}{⨉} [C (j) (k), D (j) (k)) = \underset{k \in X}{⨉} ([.) \circ (j \in ℕ ⟼ (k \in X ⟼ ⟨C (j) (k), D (j) (k)⟩)) (j)) (k)$
125	124	iuneq2dv	$⊢ φ \to ⋃_{j \in ℕ} \underset{k \in X}{⨉} [C (j) (k), D (j) (k)) = ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ (j \in ℕ ⟼ (k \in X ⟼ ⟨C (j) (k), D (j) (k)⟩)) (j)) (k)$
126	4 125	sseqtrd	$⊢ φ \to A \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ (j \in ℕ ⟼ (k \in X ⟼ ⟨C (j) (k), D (j) (k)⟩)) (j)) (k)$
127	126	adantr	$⊢ (φ \land X \neq \emptyset) \to A \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ (j \in ℕ ⟼ (k \in X ⟼ ⟨C (j) (k), D (j) (k)⟩)) (j)) (k)$
128		eqidd	$⊢ (φ \land X \neq \emptyset) \to sum^((j \in ℕ ⟼ \prod_{k \in X} vol ([C (j) (k), D (j) (k))))) = sum^((j \in ℕ ⟼ \prod_{k \in X} vol ([C (j) (k), D (j) (k)))))$
129	51	adantr	$⊢ ((φ \land X \neq \emptyset) \land j \in ℕ) \to X \in Fin$
130	52	adantr	$⊢ ((φ \land X \neq \emptyset) \land j \in ℕ) \to X \neq \emptyset$
131	39	adantlr	$⊢ ((φ \land X \neq \emptyset) \land j \in ℕ) \to C (j) : X ⟶ ℝ$
132	42	adantlr	$⊢ ((φ \land X \neq \emptyset) \land j \in ℕ) \to D (j) : X ⟶ ℝ$
133	5 129 130 131 132	hoidmvn0val	$⊢ ((φ \land X \neq \emptyset) \land j \in ℕ) \to C (j) L (X) D (j) = \prod_{k \in X} vol ([C (j) (k), D (j) (k)))$
134	133	mpteq2dva	$⊢ (φ \land X \neq \emptyset) \to (j \in ℕ ⟼ C (j) L (X) D (j)) = (j \in ℕ ⟼ \prod_{k \in X} vol ([C (j) (k), D (j) (k))))$
135	134	fveq2d	$⊢ (φ \land X \neq \emptyset) \to sum^((j \in ℕ ⟼ C (j) L (X) D (j))) = sum^((j \in ℕ ⟼ \prod_{k \in X} vol ([C (j) (k), D (j) (k)))))$
136	123	eqcomd	$⊢ ((φ \land j \in ℕ) \land k \in X) \to ([.) \circ (j \in ℕ ⟼ (k \in X ⟼ ⟨C (j) (k), D (j) (k)⟩)) (j)) (k) = [C (j) (k), D (j) (k))$
137	136	fveq2d	$⊢ ((φ \land j \in ℕ) \land k \in X) \to vol (([.) \circ (j \in ℕ ⟼ (k \in X ⟼ ⟨C (j) (k), D (j) (k)⟩)) (j)) (k)) = vol ([C (j) (k), D (j) (k)))$
138	137	prodeq2dv	$⊢ (φ \land j \in ℕ) \to \prod_{k \in X} vol (([.) \circ (j \in ℕ ⟼ (k \in X ⟼ ⟨C (j) (k), D (j) (k)⟩)) (j)) (k)) = \prod_{k \in X} vol ([C (j) (k), D (j) (k)))$
139	138	mpteq2dva	$⊢ φ \to (j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ (j \in ℕ ⟼ (k \in X ⟼ ⟨C (j) (k), D (j) (k)⟩)) (j)) (k))) = (j \in ℕ ⟼ \prod_{k \in X} vol ([C (j) (k), D (j) (k))))$
140	139	fveq2d	$⊢ φ \to sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ (j \in ℕ ⟼ (k \in X ⟼ ⟨C (j) (k), D (j) (k)⟩)) (j)) (k)))) = sum^((j \in ℕ ⟼ \prod_{k \in X} vol ([C (j) (k), D (j) (k)))))$
141	140	adantr	$⊢ (φ \land X \neq \emptyset) \to sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ (j \in ℕ ⟼ (k \in X ⟼ ⟨C (j) (k), D (j) (k)⟩)) (j)) (k)))) = sum^((j \in ℕ ⟼ \prod_{k \in X} vol ([C (j) (k), D (j) (k)))))$
142	128 135 141	3eqtr4d	$⊢ (φ \land X \neq \emptyset) \to sum^((j \in ℕ ⟼ C (j) L (X) D (j))) = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ (j \in ℕ ⟼ (k \in X ⟼ ⟨C (j) (k), D (j) (k)⟩)) (j)) (k))))$
143	127 142	jca	$⊢ (φ \land X \neq \emptyset) \to (A \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ (j \in ℕ ⟼ (k \in X ⟼ ⟨C (j) (k), D (j) (k)⟩)) (j)) (k) \land sum^((j \in ℕ ⟼ C (j) L (X) D (j))) = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ (j \in ℕ ⟼ (k \in X ⟼ ⟨C (j) (k), D (j) (k)⟩)) (j)) (k)))))$
144		nfcv	$⊢ \underline{Ⅎ} j i$
145		nfmpt1	$⊢ \underline{Ⅎ} j (j \in ℕ ⟼ (k \in X ⟼ ⟨C (j) (k), D (j) (k)⟩))$
146	144 145	nfeq	$⊢ Ⅎ j i = (j \in ℕ ⟼ (k \in X ⟼ ⟨C (j) (k), D (j) (k)⟩))$
147		nfcv	$⊢ \underline{Ⅎ} k i$
148		nfcv	$⊢ \underline{Ⅎ} k ℕ$
149		nfmpt1	$⊢ \underline{Ⅎ} k (k \in X ⟼ ⟨C (j) (k), D (j) (k)⟩)$
150	148 149	nfmpt	$⊢ \underline{Ⅎ} k (j \in ℕ ⟼ (k \in X ⟼ ⟨C (j) (k), D (j) (k)⟩))$
151	147 150	nfeq	$⊢ Ⅎ k i = (j \in ℕ ⟼ (k \in X ⟼ ⟨C (j) (k), D (j) (k)⟩))$
152		fveq1	$⊢ i = (j \in ℕ ⟼ (k \in X ⟼ ⟨C (j) (k), D (j) (k)⟩)) \to i (j) = (j \in ℕ ⟼ (k \in X ⟼ ⟨C (j) (k), D (j) (k)⟩)) (j)$
153	152	coeq2d	$⊢ i = (j \in ℕ ⟼ (k \in X ⟼ ⟨C (j) (k), D (j) (k)⟩)) \to [.) \circ i (j) = [.) \circ (j \in ℕ ⟼ (k \in X ⟼ ⟨C (j) (k), D (j) (k)⟩)) (j)$
154	153	fveq1d	$⊢ i = (j \in ℕ ⟼ (k \in X ⟼ ⟨C (j) (k), D (j) (k)⟩)) \to ([.) \circ i (j)) (k) = ([.) \circ (j \in ℕ ⟼ (k \in X ⟼ ⟨C (j) (k), D (j) (k)⟩)) (j)) (k)$
155	154	adantr	$⊢ (i = (j \in ℕ ⟼ (k \in X ⟼ ⟨C (j) (k), D (j) (k)⟩)) \land k \in X) \to ([.) \circ i (j)) (k) = ([.) \circ (j \in ℕ ⟼ (k \in X ⟼ ⟨C (j) (k), D (j) (k)⟩)) (j)) (k)$
156	151 155	ixpeq2d	$⊢ i = (j \in ℕ ⟼ (k \in X ⟼ ⟨C (j) (k), D (j) (k)⟩)) \to \underset{k \in X}{⨉} ([.) \circ i (j)) (k) = \underset{k \in X}{⨉} ([.) \circ (j \in ℕ ⟼ (k \in X ⟼ ⟨C (j) (k), D (j) (k)⟩)) (j)) (k)$
157	156	adantr	$⊢ (i = (j \in ℕ ⟼ (k \in X ⟼ ⟨C (j) (k), D (j) (k)⟩)) \land j \in ℕ) \to \underset{k \in X}{⨉} ([.) \circ i (j)) (k) = \underset{k \in X}{⨉} ([.) \circ (j \in ℕ ⟼ (k \in X ⟼ ⟨C (j) (k), D (j) (k)⟩)) (j)) (k)$
158	146 157	iuneq2df	$⊢ i = (j \in ℕ ⟼ (k \in X ⟼ ⟨C (j) (k), D (j) (k)⟩)) \to ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ i (j)) (k) = ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ (j \in ℕ ⟼ (k \in X ⟼ ⟨C (j) (k), D (j) (k)⟩)) (j)) (k)$
159	158	sseq2d	$⊢ i = (j \in ℕ ⟼ (k \in X ⟼ ⟨C (j) (k), D (j) (k)⟩)) \to (A \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ i (j)) (k) \leftrightarrow A \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ (j \in ℕ ⟼ (k \in X ⟼ ⟨C (j) (k), D (j) (k)⟩)) (j)) (k))$
160		nfv	$⊢ Ⅎ k j \in ℕ$
161	151 160	nfan	$⊢ Ⅎ k (i = (j \in ℕ ⟼ (k \in X ⟼ ⟨C (j) (k), D (j) (k)⟩)) \land j \in ℕ)$
162	154	fveq2d	$⊢ i = (j \in ℕ ⟼ (k \in X ⟼ ⟨C (j) (k), D (j) (k)⟩)) \to vol (([.) \circ i (j)) (k)) = vol (([.) \circ (j \in ℕ ⟼ (k \in X ⟼ ⟨C (j) (k), D (j) (k)⟩)) (j)) (k))$
163	162	a1d	$⊢ i = (j \in ℕ ⟼ (k \in X ⟼ ⟨C (j) (k), D (j) (k)⟩)) \to (k \in X \to vol (([.) \circ i (j)) (k)) = vol (([.) \circ (j \in ℕ ⟼ (k \in X ⟼ ⟨C (j) (k), D (j) (k)⟩)) (j)) (k)))$
164	163	adantr	$⊢ (i = (j \in ℕ ⟼ (k \in X ⟼ ⟨C (j) (k), D (j) (k)⟩)) \land j \in ℕ) \to (k \in X \to vol (([.) \circ i (j)) (k)) = vol (([.) \circ (j \in ℕ ⟼ (k \in X ⟼ ⟨C (j) (k), D (j) (k)⟩)) (j)) (k)))$
165	161 164	ralrimi	$⊢ (i = (j \in ℕ ⟼ (k \in X ⟼ ⟨C (j) (k), D (j) (k)⟩)) \land j \in ℕ) \to \forall k \in X vol (([.) \circ i (j)) (k)) = vol (([.) \circ (j \in ℕ ⟼ (k \in X ⟼ ⟨C (j) (k), D (j) (k)⟩)) (j)) (k))$
166	165	prodeq2d	$⊢ (i = (j \in ℕ ⟼ (k \in X ⟼ ⟨C (j) (k), D (j) (k)⟩)) \land j \in ℕ) \to \prod_{k \in X} vol (([.) \circ i (j)) (k)) = \prod_{k \in X} vol (([.) \circ (j \in ℕ ⟼ (k \in X ⟼ ⟨C (j) (k), D (j) (k)⟩)) (j)) (k))$
167	146 166	mpteq2da	$⊢ i = (j \in ℕ ⟼ (k \in X ⟼ ⟨C (j) (k), D (j) (k)⟩)) \to (j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ i (j)) (k))) = (j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ (j \in ℕ ⟼ (k \in X ⟼ ⟨C (j) (k), D (j) (k)⟩)) (j)) (k)))$
168	167	fveq2d	$⊢ i = (j \in ℕ ⟼ (k \in X ⟼ ⟨C (j) (k), D (j) (k)⟩)) \to sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ i (j)) (k)))) = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ (j \in ℕ ⟼ (k \in X ⟼ ⟨C (j) (k), D (j) (k)⟩)) (j)) (k))))$
169	168	eqeq2d	$⊢ i = (j \in ℕ ⟼ (k \in X ⟼ ⟨C (j) (k), D (j) (k)⟩)) \to (sum^((j \in ℕ ⟼ C (j) L (X) D (j))) = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ i (j)) (k)))) \leftrightarrow sum^((j \in ℕ ⟼ C (j) L (X) D (j))) = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ (j \in ℕ ⟼ (k \in X ⟼ ⟨C (j) (k), D (j) (k)⟩)) (j)) (k)))))$
170	159 169	anbi12d	$⊢ i = (j \in ℕ ⟼ (k \in X ⟼ ⟨C (j) (k), D (j) (k)⟩)) \to ((A \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ i (j)) (k) \land sum^((j \in ℕ ⟼ C (j) L (X) D (j))) = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ i (j)) (k))))) \leftrightarrow (A \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ (j \in ℕ ⟼ (k \in X ⟼ ⟨C (j) (k), D (j) (k)⟩)) (j)) (k) \land sum^((j \in ℕ ⟼ C (j) L (X) D (j))) = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ (j \in ℕ ⟼ (k \in X ⟼ ⟨C (j) (k), D (j) (k)⟩)) (j)) (k))))))$
171	170	rspcev	$⊢ ((j \in ℕ ⟼ (k \in X ⟼ ⟨C (j) (k), D (j) (k)⟩)) \in ({({ℝ^{2}}^{X})}^{ℕ}) \land (A \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ (j \in ℕ ⟼ (k \in X ⟼ ⟨C (j) (k), D (j) (k)⟩)) (j)) (k) \land sum^((j \in ℕ ⟼ C (j) L (X) D (j))) = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ (j \in ℕ ⟼ (k \in X ⟼ ⟨C (j) (k), D (j) (k)⟩)) (j)) (k)))))) \to \exists i \in ({({ℝ^{2}}^{X})}^{ℕ}) (A \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ i (j)) (k) \land sum^((j \in ℕ ⟼ C (j) L (X) D (j))) = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ i (j)) (k)))))$
172	90 143 171	syl2anc	$⊢ (φ \land X \neq \emptyset) \to \exists i \in ({({ℝ^{2}}^{X})}^{ℕ}) (A \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ i (j)) (k) \land sum^((j \in ℕ ⟼ C (j) L (X) D (j))) = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ i (j)) (k)))))$
173	76 172	jca	$⊢ (φ \land X \neq \emptyset) \to (sum^((j \in ℕ ⟼ C (j) L (X) D (j))) \in ℝ^{*} \land \exists i \in ({({ℝ^{2}}^{X})}^{ℕ}) (A \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ i (j)) (k) \land sum^((j \in ℕ ⟼ C (j) L (X) D (j))) = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ i (j)) (k))))))$
174		eqeq1	$⊢ z = sum^((j \in ℕ ⟼ C (j) L (X) D (j))) \to (z = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ i (j)) (k)))) \leftrightarrow sum^((j \in ℕ ⟼ C (j) L (X) D (j))) = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ i (j)) (k)))))$
175	174	anbi2d	$⊢ z = sum^((j \in ℕ ⟼ C (j) L (X) D (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 ℕ ⟼ C (j) L (X) D (j))) = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ i (j)) (k))))))$
176	175	rexbidv	$⊢ z = sum^((j \in ℕ ⟼ C (j) L (X) D (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 ℕ ⟼ C (j) L (X) D (j))) = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ i (j)) (k))))))$
177	176	elrab	$⊢ sum^((j \in ℕ ⟼ C (j) L (X) D (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 ℕ ⟼ C (j) L (X) D (j))) \in ℝ^{} \land \exists i \in ({({ℝ^{2}}^{X})}^{ℕ}) (A \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ i (j)) (k) \land sum^((j \in ℕ ⟼ C (j) L (X) D (j))) = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ i (j)) (k))))))$
178	173 177	sylibr	$⊢ (φ \land X \neq \emptyset) \to sum^((j \in ℕ ⟼ C (j) L (X) D (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)))))\}$
179		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 ℕ ⟼ C (j) L (X) D (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 inf (\{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 ℕ ⟼ C (j) L (X) D (j)))$
180	74 178 179	syl2anc	$⊢ (φ \land X \neq \emptyset) \to inf (\{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 ℕ ⟼ C (j) L (X) D (j)))$
181	72 180	eqbrtrd	$⊢ (φ \land X \neq \emptyset) \to voln* (X) (A) \leq sum^((j \in ℕ ⟼ C (j) L (X) D (j)))$
182	48 50 181	syl2anc	$⊢ (φ \land \neg X = \emptyset) \to voln* (X) (A) \leq sum^((j \in ℕ ⟼ C (j) L (X) D (j)))$
183	47 182	pm2.61dan	$⊢ φ \to voln* (X) (A) \leq sum^((j \in ℕ ⟼ C (j) L (X) D (j)))$

Metamath Proof Explorer

Theorem ovnlecvr2

Proof