ovnhoilem1

Description: The Lebesgue outer measure of a multidimensional half-open interval is less than or equal to the product of its length in each dimension. First part of the proof of Proposition 115D (b) of Fremlin1 p. 30. (Contributed by Glauco Siliprandi, 21-Nov-2020)

	Ref	Expression
Hypotheses	ovnhoilem1.x	$⊢ φ \to X \in Fin$
	ovnhoilem1.a	$⊢ φ \to A : X ⟶ ℝ$
	ovnhoilem1.b	$⊢ φ \to B : X ⟶ ℝ$
	ovnhoilem1.c	$⊢ I = \underset{k \in X}{⨉} [A (k), B (k))$
	ovnhoilem1.m	$⊢ M = \{z \in ℝ^{*} \| \exists i \in ({({ℝ^{2}}^{X})}^{ℕ}) (I \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)))))\}$
	ovnhoilem1.h	$⊢ H = (j \in ℕ ⟼ (k \in X ⟼ if (j = 1, ⟨A (k), B (k)⟩, ⟨0, 0⟩)))$
Assertion	ovnhoilem1	$⊢ φ \to voln* (X) (I) \leq \prod_{k \in X} vol ([A (k), B (k)))$

Proof

Step	Hyp	Ref	Expression
1		ovnhoilem1.x	$⊢ φ \to X \in Fin$
2		ovnhoilem1.a	$⊢ φ \to A : X ⟶ ℝ$
3		ovnhoilem1.b	$⊢ φ \to B : X ⟶ ℝ$
4		ovnhoilem1.c	$⊢ I = \underset{k \in X}{⨉} [A (k), B (k))$
5		ovnhoilem1.m	$⊢ M = \{z \in ℝ^{*} \| \exists i \in ({({ℝ^{2}}^{X})}^{ℕ}) (I \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)))))\}$
6		ovnhoilem1.h	$⊢ H = (j \in ℕ ⟼ (k \in X ⟼ if (j = 1, ⟨A (k), B (k)⟩, ⟨0, 0⟩)))$
7	4	a1i	$⊢ φ \to I = \underset{k \in X}{⨉} [A (k), B (k))$
8		nfv	$⊢ Ⅎ k φ$
9	2	ffvelcdmda	$⊢ (φ \land k \in X) \to A (k) \in ℝ$
10	3	ffvelcdmda	$⊢ (φ \land k \in X) \to B (k) \in ℝ$
11	10	rexrd	$⊢ (φ \land k \in X) \to B (k) \in ℝ^{*}$
12	8 9 11	hoissrrn2	$⊢ φ \to \underset{k \in X}{⨉} [A (k), B (k)) \subseteq ℝ^{X}$
13	7 12	eqsstrd	$⊢ φ \to I \subseteq ℝ^{X}$
14	1 13 5	ovnval2	$⊢ φ \to voln* (X) (I) = if (X = \emptyset, 0, inf (M ℝ^{*} <))$
15		iftrue	$⊢ X = \emptyset \to if (X = \emptyset, 0, inf (M ℝ^{*} <)) = 0$
16	15	adantl	$⊢ (φ \land X = \emptyset) \to if (X = \emptyset, 0, inf (M ℝ^{*} <)) = 0$
17		0xr	$⊢ 0 \in ℝ^{*}$
18	17	a1i	$⊢ φ \to 0 \in ℝ^{*}$
19		pnfxr	$⊢ +∞ \in ℝ^{*}$
20	19	a1i	$⊢ φ \to +∞ \in ℝ^{*}$
21	8 1 9 10	hoiprodcl3	$⊢ φ \to \prod_{k \in X} vol ([A (k), B (k))) \in [0, +∞)$
22		icogelb	$⊢ (0 \in ℝ^{} \land +∞ \in ℝ^{} \land \prod_{k \in X} vol ([A (k), B (k))) \in [0, +∞)) \to 0 \leq \prod_{k \in X} vol ([A (k), B (k)))$
23	18 20 21 22	syl3anc	$⊢ φ \to 0 \leq \prod_{k \in X} vol ([A (k), B (k)))$
24	23	adantr	$⊢ (φ \land X = \emptyset) \to 0 \leq \prod_{k \in X} vol ([A (k), B (k)))$
25	16 24	eqbrtrd	$⊢ (φ \land X = \emptyset) \to if (X = \emptyset, 0, inf (M ℝ^{*} <)) \leq \prod_{k \in X} vol ([A (k), B (k)))$
26		iffalse	$⊢ \neg X = \emptyset \to if (X = \emptyset, 0, inf (M ℝ^{} <)) = inf (M ℝ^{} <)$
27	26	adantl	$⊢ (φ \land \neg X = \emptyset) \to if (X = \emptyset, 0, inf (M ℝ^{} <)) = inf (M ℝ^{} <)$
28		ssrab2	$⊢ \{z \in ℝ^{} \| \exists i \in ({({ℝ^{2}}^{X})}^{ℕ}) (I \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 ℝ^{}$
29	5 28	eqsstri	$⊢ M \subseteq ℝ^{*}$
30	29	a1i	$⊢ (φ \land \neg X = \emptyset) \to M \subseteq ℝ^{*}$
31		icossxr	$⊢ [0, +∞) \subseteq ℝ^{*}$
32	31 21	sselid	$⊢ φ \to \prod_{k \in X} vol ([A (k), B (k))) \in ℝ^{*}$
33	32	adantr	$⊢ (φ \land \neg X = \emptyset) \to \prod_{k \in X} vol ([A (k), B (k))) \in ℝ^{*}$
34		opelxpi	$⊢ (A (k) \in ℝ \land B (k) \in ℝ) \to ⟨A (k), B (k)⟩ \in ℝ^{2}$
35	9 10 34	syl2anc	$⊢ (φ \land k \in X) \to ⟨A (k), B (k)⟩ \in ℝ^{2}$
36		0re	$⊢ 0 \in ℝ$
37		opelxpi	$⊢ (0 \in ℝ \land 0 \in ℝ) \to ⟨0, 0⟩ \in ℝ^{2}$
38	36 36 37	mp2an	$⊢ ⟨0, 0⟩ \in ℝ^{2}$
39	38	a1i	$⊢ (φ \land k \in X) \to ⟨0, 0⟩ \in ℝ^{2}$
40	35 39	ifcld	$⊢ (φ \land k \in X) \to if (j = 1, ⟨A (k), B (k)⟩, ⟨0, 0⟩) \in ℝ^{2}$
41	40	fmpttd	$⊢ φ \to (k \in X ⟼ if (j = 1, ⟨A (k), B (k)⟩, ⟨0, 0⟩)) : X ⟶ ℝ^{2}$
42		reex	$⊢ ℝ \in V$
43	42 42	xpex	$⊢ ℝ^{2} \in V$
44	1 43	jctil	$⊢ φ \to (ℝ^{2} \in V \land X \in Fin)$
45		elmapg	$⊢ (ℝ^{2} \in V \land X \in Fin) \to ((k \in X ⟼ if (j = 1, ⟨A (k), B (k)⟩, ⟨0, 0⟩)) \in ({ℝ^{2}}^{X}) \leftrightarrow (k \in X ⟼ if (j = 1, ⟨A (k), B (k)⟩, ⟨0, 0⟩)) : X ⟶ ℝ^{2})$
46	44 45	syl	$⊢ φ \to ((k \in X ⟼ if (j = 1, ⟨A (k), B (k)⟩, ⟨0, 0⟩)) \in ({ℝ^{2}}^{X}) \leftrightarrow (k \in X ⟼ if (j = 1, ⟨A (k), B (k)⟩, ⟨0, 0⟩)) : X ⟶ ℝ^{2})$
47	41 46	mpbird	$⊢ φ \to (k \in X ⟼ if (j = 1, ⟨A (k), B (k)⟩, ⟨0, 0⟩)) \in ({ℝ^{2}}^{X})$
48	47	adantr	$⊢ (φ \land j \in ℕ) \to (k \in X ⟼ if (j = 1, ⟨A (k), B (k)⟩, ⟨0, 0⟩)) \in ({ℝ^{2}}^{X})$
49	48 6	fmptd	$⊢ φ \to H : ℕ ⟶ {ℝ^{2}}^{X}$
50		ovex	$⊢ {ℝ^{2}}^{X} \in V$
51		nnex	$⊢ ℕ \in V$
52	50 51	elmap	$⊢ H \in ({({ℝ^{2}}^{X})}^{ℕ}) \leftrightarrow H : ℕ ⟶ {ℝ^{2}}^{X}$
53	49 52	sylibr	$⊢ φ \to H \in ({({ℝ^{2}}^{X})}^{ℕ})$
54	53	adantr	$⊢ (φ \land \neg X = \emptyset) \to H \in ({({ℝ^{2}}^{X})}^{ℕ})$
55		eqidd	$⊢ φ \to \underset{k \in X}{⨉} [A (k), B (k)) = \underset{k \in X}{⨉} [A (k), B (k))$
56	35	fmpttd	$⊢ φ \to (k \in X ⟼ ⟨A (k), B (k)⟩) : X ⟶ ℝ^{2}$
57		iftrue	$⊢ j = 1 \to if (j = 1, ⟨A (k), B (k)⟩, ⟨0, 0⟩) = ⟨A (k), B (k)⟩$
58	57	mpteq2dv	$⊢ j = 1 \to (k \in X ⟼ if (j = 1, ⟨A (k), B (k)⟩, ⟨0, 0⟩)) = (k \in X ⟼ ⟨A (k), B (k)⟩)$
59		1nn	$⊢ 1 \in ℕ$
60	59	a1i	$⊢ φ \to 1 \in ℕ$
61		mptexg	$⊢ X \in Fin \to (k \in X ⟼ ⟨A (k), B (k)⟩) \in V$
62	1 61	syl	$⊢ φ \to (k \in X ⟼ ⟨A (k), B (k)⟩) \in V$
63	6 58 60 62	fvmptd3	$⊢ φ \to H (1) = (k \in X ⟼ ⟨A (k), B (k)⟩)$
64	63	feq1d	$⊢ φ \to (H (1) : X ⟶ ℝ^{2} \leftrightarrow (k \in X ⟼ ⟨A (k), B (k)⟩) : X ⟶ ℝ^{2})$
65	56 64	mpbird	$⊢ φ \to H (1) : X ⟶ ℝ^{2}$
66	65	adantr	$⊢ (φ \land k \in X) \to H (1) : X ⟶ ℝ^{2}$
67		simpr	$⊢ (φ \land k \in X) \to k \in X$
68	66 67	fvovco	$⊢ (φ \land k \in X) \to ([.) \circ H (1)) (k) = [1^{st} (H (1) (k)), 2^{nd} (H (1) (k)))$
69	35	elexd	$⊢ (φ \land k \in X) \to ⟨A (k), B (k)⟩ \in V$
70	63 69	fvmpt2d	$⊢ (φ \land k \in X) \to H (1) (k) = ⟨A (k), B (k)⟩$
71	70	fveq2d	$⊢ (φ \land k \in X) \to 1^{st} (H (1) (k)) = 1^{st} (⟨A (k), B (k)⟩)$
72		fvex	$⊢ A (k) \in V$
73		fvex	$⊢ B (k) \in V$
74	72 73	op1st	$⊢ 1^{st} (⟨A (k), B (k)⟩) = A (k)$
75	74	a1i	$⊢ (φ \land k \in X) \to 1^{st} (⟨A (k), B (k)⟩) = A (k)$
76	71 75	eqtrd	$⊢ (φ \land k \in X) \to 1^{st} (H (1) (k)) = A (k)$
77	70	fveq2d	$⊢ (φ \land k \in X) \to 2^{nd} (H (1) (k)) = 2^{nd} (⟨A (k), B (k)⟩)$
78	72 73	op2nd	$⊢ 2^{nd} (⟨A (k), B (k)⟩) = B (k)$
79	78	a1i	$⊢ (φ \land k \in X) \to 2^{nd} (⟨A (k), B (k)⟩) = B (k)$
80	77 79	eqtrd	$⊢ (φ \land k \in X) \to 2^{nd} (H (1) (k)) = B (k)$
81	76 80	oveq12d	$⊢ (φ \land k \in X) \to [1^{st} (H (1) (k)), 2^{nd} (H (1) (k))) = [A (k), B (k))$
82	68 81	eqtrd	$⊢ (φ \land k \in X) \to ([.) \circ H (1)) (k) = [A (k), B (k))$
83	82	ixpeq2dva	$⊢ φ \to \underset{k \in X}{⨉} ([.) \circ H (1)) (k) = \underset{k \in X}{⨉} [A (k), B (k))$
84	55 7 83	3eqtr4d	$⊢ φ \to I = \underset{k \in X}{⨉} ([.) \circ H (1)) (k)$
85		fveq2	$⊢ j = 1 \to H (j) = H (1)$
86	85	coeq2d	$⊢ j = 1 \to [.) \circ H (j) = [.) \circ H (1)$
87	86	fveq1d	$⊢ j = 1 \to ([.) \circ H (j)) (k) = ([.) \circ H (1)) (k)$
88	87	ixpeq2dv	$⊢ j = 1 \to \underset{k \in X}{⨉} ([.) \circ H (j)) (k) = \underset{k \in X}{⨉} ([.) \circ H (1)) (k)$
89	88	ssiun2s	$⊢ 1 \in ℕ \to \underset{k \in X}{⨉} ([.) \circ H (1)) (k) \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ H (j)) (k)$
90	59 89	ax-mp	$⊢ \underset{k \in X}{⨉} ([.) \circ H (1)) (k) \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ H (j)) (k)$
91	84 90	eqsstrdi	$⊢ φ \to I \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ H (j)) (k)$
92	91	adantr	$⊢ (φ \land \neg X = \emptyset) \to I \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ H (j)) (k)$
93	82	fveq2d	$⊢ (φ \land k \in X) \to vol (([.) \circ H (1)) (k)) = vol ([A (k), B (k)))$
94	93	eqcomd	$⊢ (φ \land k \in X) \to vol ([A (k), B (k))) = vol (([.) \circ H (1)) (k))$
95	94	prodeq2dv	$⊢ φ \to \prod_{k \in X} vol ([A (k), B (k))) = \prod_{k \in X} vol (([.) \circ H (1)) (k))$
96	95	adantr	$⊢ (φ \land \neg X = \emptyset) \to \prod_{k \in X} vol ([A (k), B (k))) = \prod_{k \in X} vol (([.) \circ H (1)) (k))$
97		1red	$⊢ φ \to 1 \in ℝ$
98		icossicc	$⊢ [0, +∞) \subseteq [0, +∞]$
99	8 1 65	hoiprodcl	$⊢ φ \to \prod_{k \in X} vol (([.) \circ H (1)) (k)) \in [0, +∞)$
100	98 99	sselid	$⊢ φ \to \prod_{k \in X} vol (([.) \circ H (1)) (k)) \in [0, +∞]$
101	87	fveq2d	$⊢ j = 1 \to vol (([.) \circ H (j)) (k)) = vol (([.) \circ H (1)) (k))$
102	101	prodeq2ad	$⊢ j = 1 \to \prod_{k \in X} vol (([.) \circ H (j)) (k)) = \prod_{k \in X} vol (([.) \circ H (1)) (k))$
103	97 100 102	sge0snmpt	$⊢ φ \to sum^((j \in \{1\} ⟼ \prod_{k \in X} vol (([.) \circ H (j)) (k)))) = \prod_{k \in X} vol (([.) \circ H (1)) (k))$
104	103	eqcomd	$⊢ φ \to \prod_{k \in X} vol (([.) \circ H (1)) (k)) = sum^((j \in \{1\} ⟼ \prod_{k \in X} vol (([.) \circ H (j)) (k))))$
105	104	adantr	$⊢ (φ \land \neg X = \emptyset) \to \prod_{k \in X} vol (([.) \circ H (1)) (k)) = sum^((j \in \{1\} ⟼ \prod_{k \in X} vol (([.) \circ H (j)) (k))))$
106		nfv	$⊢ Ⅎ j (φ \land \neg X = \emptyset)$
107	51	a1i	$⊢ (φ \land \neg X = \emptyset) \to ℕ \in V$
108		snssi	$⊢ 1 \in ℕ \to \{1\} \subseteq ℕ$
109	59 108	ax-mp	$⊢ \{1\} \subseteq ℕ$
110	109	a1i	$⊢ (φ \land \neg X = \emptyset) \to \{1\} \subseteq ℕ$
111		nfv	$⊢ Ⅎ k ((φ \land \neg X = \emptyset) \land j \in \{1\})$
112	1	ad2antrr	$⊢ ((φ \land \neg X = \emptyset) \land j \in \{1\}) \to X \in Fin$
113		simpl	$⊢ (φ \land j \in \{1\}) \to φ$
114		elsni	$⊢ j \in \{1\} \to j = 1$
115	114	adantl	$⊢ (φ \land j \in \{1\}) \to j = 1$
116	65	adantr	$⊢ (φ \land j = 1) \to H (1) : X ⟶ ℝ^{2}$
117	85	adantl	$⊢ (φ \land j = 1) \to H (j) = H (1)$
118	117	feq1d	$⊢ (φ \land j = 1) \to (H (j) : X ⟶ ℝ^{2} \leftrightarrow H (1) : X ⟶ ℝ^{2})$
119	116 118	mpbird	$⊢ (φ \land j = 1) \to H (j) : X ⟶ ℝ^{2}$
120	113 115 119	syl2anc	$⊢ (φ \land j \in \{1\}) \to H (j) : X ⟶ ℝ^{2}$
121	120	adantlr	$⊢ ((φ \land \neg X = \emptyset) \land j \in \{1\}) \to H (j) : X ⟶ ℝ^{2}$
122	111 112 121	hoiprodcl	$⊢ ((φ \land \neg X = \emptyset) \land j \in \{1\}) \to \prod_{k \in X} vol (([.) \circ H (j)) (k)) \in [0, +∞)$
123	98 122	sselid	$⊢ ((φ \land \neg X = \emptyset) \land j \in \{1\}) \to \prod_{k \in X} vol (([.) \circ H (j)) (k)) \in [0, +∞]$
124	39	fmpttd	$⊢ φ \to (k \in X ⟼ ⟨0, 0⟩) : X ⟶ ℝ^{2}$
125	124	adantr	$⊢ (φ \land j \in (ℕ ∖ \{1\})) \to (k \in X ⟼ ⟨0, 0⟩) : X ⟶ ℝ^{2}$
126		simpl	$⊢ (φ \land j \in (ℕ ∖ \{1\})) \to φ$
127		eldifi	$⊢ j \in (ℕ ∖ \{1\}) \to j \in ℕ$
128	127	adantl	$⊢ (φ \land j \in (ℕ ∖ \{1\})) \to j \in ℕ$
129	6	a1i	$⊢ φ \to H = (j \in ℕ ⟼ (k \in X ⟼ if (j = 1, ⟨A (k), B (k)⟩, ⟨0, 0⟩)))$
130	48	elexd	$⊢ (φ \land j \in ℕ) \to (k \in X ⟼ if (j = 1, ⟨A (k), B (k)⟩, ⟨0, 0⟩)) \in V$
131	129 130	fvmpt2d	$⊢ (φ \land j \in ℕ) \to H (j) = (k \in X ⟼ if (j = 1, ⟨A (k), B (k)⟩, ⟨0, 0⟩))$
132	126 128 131	syl2anc	$⊢ (φ \land j \in (ℕ ∖ \{1\})) \to H (j) = (k \in X ⟼ if (j = 1, ⟨A (k), B (k)⟩, ⟨0, 0⟩))$
133		eldifsni	$⊢ j \in (ℕ ∖ \{1\}) \to j \neq 1$
134	133	neneqd	$⊢ j \in (ℕ ∖ \{1\}) \to \neg j = 1$
135	134	iffalsed	$⊢ j \in (ℕ ∖ \{1\}) \to if (j = 1, ⟨A (k), B (k)⟩, ⟨0, 0⟩) = ⟨0, 0⟩$
136	135	mpteq2dv	$⊢ j \in (ℕ ∖ \{1\}) \to (k \in X ⟼ if (j = 1, ⟨A (k), B (k)⟩, ⟨0, 0⟩)) = (k \in X ⟼ ⟨0, 0⟩)$
137	136	adantl	$⊢ (φ \land j \in (ℕ ∖ \{1\})) \to (k \in X ⟼ if (j = 1, ⟨A (k), B (k)⟩, ⟨0, 0⟩)) = (k \in X ⟼ ⟨0, 0⟩)$
138	132 137	eqtrd	$⊢ (φ \land j \in (ℕ ∖ \{1\})) \to H (j) = (k \in X ⟼ ⟨0, 0⟩)$
139	138	feq1d	$⊢ (φ \land j \in (ℕ ∖ \{1\})) \to (H (j) : X ⟶ ℝ^{2} \leftrightarrow (k \in X ⟼ ⟨0, 0⟩) : X ⟶ ℝ^{2})$
140	125 139	mpbird	$⊢ (φ \land j \in (ℕ ∖ \{1\})) \to H (j) : X ⟶ ℝ^{2}$
141	140	adantr	$⊢ ((φ \land j \in (ℕ ∖ \{1\})) \land k \in X) \to H (j) : X ⟶ ℝ^{2}$
142		simpr	$⊢ ((φ \land j \in (ℕ ∖ \{1\})) \land k \in X) \to k \in X$
143	141 142	fvovco	$⊢ ((φ \land j \in (ℕ ∖ \{1\})) \land k \in X) \to ([.) \circ H (j)) (k) = [1^{st} (H (j) (k)), 2^{nd} (H (j) (k)))$
144	38	elexi	$⊢ ⟨0, 0⟩ \in V$
145	144	a1i	$⊢ ((φ \land j \in (ℕ ∖ \{1\})) \land k \in X) \to ⟨0, 0⟩ \in V$
146	138 145	fvmpt2d	$⊢ ((φ \land j \in (ℕ ∖ \{1\})) \land k \in X) \to H (j) (k) = ⟨0, 0⟩$
147	146	fveq2d	$⊢ ((φ \land j \in (ℕ ∖ \{1\})) \land k \in X) \to 1^{st} (H (j) (k)) = 1^{st} (⟨0, 0⟩)$
148	17	elexi	$⊢ 0 \in V$
149	148 148	op1st	$⊢ 1^{st} (⟨0, 0⟩) = 0$
150	149	a1i	$⊢ ((φ \land j \in (ℕ ∖ \{1\})) \land k \in X) \to 1^{st} (⟨0, 0⟩) = 0$
151	147 150	eqtrd	$⊢ ((φ \land j \in (ℕ ∖ \{1\})) \land k \in X) \to 1^{st} (H (j) (k)) = 0$
152	146	fveq2d	$⊢ ((φ \land j \in (ℕ ∖ \{1\})) \land k \in X) \to 2^{nd} (H (j) (k)) = 2^{nd} (⟨0, 0⟩)$
153	148 148	op2nd	$⊢ 2^{nd} (⟨0, 0⟩) = 0$
154	153	a1i	$⊢ ((φ \land j \in (ℕ ∖ \{1\})) \land k \in X) \to 2^{nd} (⟨0, 0⟩) = 0$
155	152 154	eqtrd	$⊢ ((φ \land j \in (ℕ ∖ \{1\})) \land k \in X) \to 2^{nd} (H (j) (k)) = 0$
156	151 155	oveq12d	$⊢ ((φ \land j \in (ℕ ∖ \{1\})) \land k \in X) \to [1^{st} (H (j) (k)), 2^{nd} (H (j) (k))) = [0, 0)$
157		0le0	$⊢ 0 \leq 0$
158		ico0	$⊢ (0 \in ℝ^{} \land 0 \in ℝ^{}) \to ([0, 0) = \emptyset \leftrightarrow 0 \leq 0)$
159	17 17 158	mp2an	$⊢ [0, 0) = \emptyset \leftrightarrow 0 \leq 0$
160	157 159	mpbir	$⊢ [0, 0) = \emptyset$
161	160	a1i	$⊢ ((φ \land j \in (ℕ ∖ \{1\})) \land k \in X) \to [0, 0) = \emptyset$
162	143 156 161	3eqtrd	$⊢ ((φ \land j \in (ℕ ∖ \{1\})) \land k \in X) \to ([.) \circ H (j)) (k) = \emptyset$
163	162	fveq2d	$⊢ ((φ \land j \in (ℕ ∖ \{1\})) \land k \in X) \to vol (([.) \circ H (j)) (k)) = vol (\emptyset)$
164		vol0	$⊢ vol (\emptyset) = 0$
165	164	a1i	$⊢ ((φ \land j \in (ℕ ∖ \{1\})) \land k \in X) \to vol (\emptyset) = 0$
166	163 165	eqtrd	$⊢ ((φ \land j \in (ℕ ∖ \{1\})) \land k \in X) \to vol (([.) \circ H (j)) (k)) = 0$
167	166	prodeq2dv	$⊢ (φ \land j \in (ℕ ∖ \{1\})) \to \prod_{k \in X} vol (([.) \circ H (j)) (k)) = \prod_{k \in X} 0$
168	167	adantlr	$⊢ ((φ \land \neg X = \emptyset) \land j \in (ℕ ∖ \{1\})) \to \prod_{k \in X} vol (([.) \circ H (j)) (k)) = \prod_{k \in X} 0$
169		0cnd	$⊢ φ \to 0 \in ℂ$
170		fprodconst	$⊢ (X \in Fin \land 0 \in ℂ) \to \prod_{k \in X} 0 = 0^{\|X\|}$
171	1 169 170	syl2anc	$⊢ φ \to \prod_{k \in X} 0 = 0^{\|X\|}$
172	171	ad2antrr	$⊢ ((φ \land \neg X = \emptyset) \land j \in (ℕ ∖ \{1\})) \to \prod_{k \in X} 0 = 0^{\|X\|}$
173		neqne	$⊢ \neg X = \emptyset \to X \neq \emptyset$
174	173	adantl	$⊢ (φ \land \neg X = \emptyset) \to X \neq \emptyset$
175	1	adantr	$⊢ (φ \land \neg X = \emptyset) \to X \in Fin$
176		hashnncl	$⊢ X \in Fin \to (\|X\| \in ℕ \leftrightarrow X \neq \emptyset)$
177	175 176	syl	$⊢ (φ \land \neg X = \emptyset) \to (\|X\| \in ℕ \leftrightarrow X \neq \emptyset)$
178	174 177	mpbird	$⊢ (φ \land \neg X = \emptyset) \to \|X\| \in ℕ$
179		0exp	$⊢ \|X\| \in ℕ \to 0^{\|X\|} = 0$
180	178 179	syl	$⊢ (φ \land \neg X = \emptyset) \to 0^{\|X\|} = 0$
181	180	adantr	$⊢ ((φ \land \neg X = \emptyset) \land j \in (ℕ ∖ \{1\})) \to 0^{\|X\|} = 0$
182	168 172 181	3eqtrd	$⊢ ((φ \land \neg X = \emptyset) \land j \in (ℕ ∖ \{1\})) \to \prod_{k \in X} vol (([.) \circ H (j)) (k)) = 0$
183	106 107 110 123 182	sge0ss	$⊢ (φ \land \neg X = \emptyset) \to sum^((j \in \{1\} ⟼ \prod_{k \in X} vol (([.) \circ H (j)) (k)))) = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ H (j)) (k))))$
184	96 105 183	3eqtrd	$⊢ (φ \land \neg X = \emptyset) \to \prod_{k \in X} vol ([A (k), B (k))) = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ H (j)) (k))))$
185	92 184	jca	$⊢ (φ \land \neg X = \emptyset) \to (I \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ H (j)) (k) \land \prod_{k \in X} vol ([A (k), B (k))) = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ H (j)) (k)))))$
186		nfcv	$⊢ \underline{Ⅎ} k i$
187		nfcv	$⊢ \underline{Ⅎ} k ℕ$
188		nfmpt1	$⊢ \underline{Ⅎ} k (k \in X ⟼ if (j = 1, ⟨A (k), B (k)⟩, ⟨0, 0⟩))$
189	187 188	nfmpt	$⊢ \underline{Ⅎ} k (j \in ℕ ⟼ (k \in X ⟼ if (j = 1, ⟨A (k), B (k)⟩, ⟨0, 0⟩)))$
190	6 189	nfcxfr	$⊢ \underline{Ⅎ} k H$
191	186 190	nfeq	$⊢ Ⅎ k i = H$
192		fveq1	$⊢ i = H \to i (j) = H (j)$
193	192	coeq2d	$⊢ i = H \to [.) \circ i (j) = [.) \circ H (j)$
194	193	fveq1d	$⊢ i = H \to ([.) \circ i (j)) (k) = ([.) \circ H (j)) (k)$
195	194	adantr	$⊢ (i = H \land k \in X) \to ([.) \circ i (j)) (k) = ([.) \circ H (j)) (k)$
196	191 195	ixpeq2d	$⊢ i = H \to \underset{k \in X}{⨉} ([.) \circ i (j)) (k) = \underset{k \in X}{⨉} ([.) \circ H (j)) (k)$
197	196	iuneq2d	$⊢ i = H \to ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ i (j)) (k) = ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ H (j)) (k)$
198	197	sseq2d	$⊢ i = H \to (I \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ i (j)) (k) \leftrightarrow I \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ H (j)) (k))$
199	194	fveq2d	$⊢ i = H \to vol (([.) \circ i (j)) (k)) = vol (([.) \circ H (j)) (k))$
200	199	a1d	$⊢ i = H \to (k \in X \to vol (([.) \circ i (j)) (k)) = vol (([.) \circ H (j)) (k)))$
201	191 200	ralrimi	$⊢ i = H \to \forall k \in X vol (([.) \circ i (j)) (k)) = vol (([.) \circ H (j)) (k))$
202	201	prodeq2d	$⊢ i = H \to \prod_{k \in X} vol (([.) \circ i (j)) (k)) = \prod_{k \in X} vol (([.) \circ H (j)) (k))$
203	202	mpteq2dv	$⊢ i = H \to (j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ i (j)) (k))) = (j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ H (j)) (k)))$
204	203	fveq2d	$⊢ i = H \to sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ i (j)) (k)))) = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ H (j)) (k))))$
205	204	eqeq2d	$⊢ i = H \to (\prod_{k \in X} vol ([A (k), B (k))) = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ i (j)) (k)))) \leftrightarrow \prod_{k \in X} vol ([A (k), B (k))) = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ H (j)) (k)))))$
206	198 205	anbi12d	$⊢ i = H \to ((I \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ i (j)) (k) \land \prod_{k \in X} vol ([A (k), B (k))) = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ i (j)) (k))))) \leftrightarrow (I \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ H (j)) (k) \land \prod_{k \in X} vol ([A (k), B (k))) = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ H (j)) (k))))))$
207	206	rspcev	$⊢ (H \in ({({ℝ^{2}}^{X})}^{ℕ}) \land (I \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ H (j)) (k) \land \prod_{k \in X} vol ([A (k), B (k))) = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ H (j)) (k)))))) \to \exists i \in ({({ℝ^{2}}^{X})}^{ℕ}) (I \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ i (j)) (k) \land \prod_{k \in X} vol ([A (k), B (k))) = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ i (j)) (k)))))$
208	54 185 207	syl2anc	$⊢ (φ \land \neg X = \emptyset) \to \exists i \in ({({ℝ^{2}}^{X})}^{ℕ}) (I \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ i (j)) (k) \land \prod_{k \in X} vol ([A (k), B (k))) = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ i (j)) (k)))))$
209	33 208	jca	$⊢ (φ \land \neg X = \emptyset) \to (\prod_{k \in X} vol ([A (k), B (k))) \in ℝ^{*} \land \exists i \in ({({ℝ^{2}}^{X})}^{ℕ}) (I \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ i (j)) (k) \land \prod_{k \in X} vol ([A (k), B (k))) = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ i (j)) (k))))))$
210		eqeq1	$⊢ z = \prod_{k \in X} vol ([A (k), B (k))) \to (z = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ i (j)) (k)))) \leftrightarrow \prod_{k \in X} vol ([A (k), B (k))) = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ i (j)) (k)))))$
211	210	anbi2d	$⊢ z = \prod_{k \in X} vol ([A (k), B (k))) \to ((I \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 (I \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ i (j)) (k) \land \prod_{k \in X} vol ([A (k), B (k))) = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ i (j)) (k))))))$
212	211	rexbidv	$⊢ z = \prod_{k \in X} vol ([A (k), B (k))) \to (\exists i \in ({({ℝ^{2}}^{X})}^{ℕ}) (I \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})}^{ℕ}) (I \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ i (j)) (k) \land \prod_{k \in X} vol ([A (k), B (k))) = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ i (j)) (k))))))$
213	212	elrab	$⊢ \prod_{k \in X} vol ([A (k), B (k))) \in \{z \in ℝ^{} \| \exists i \in ({({ℝ^{2}}^{X})}^{ℕ}) (I \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 (\prod_{k \in X} vol ([A (k), B (k))) \in ℝ^{} \land \exists i \in ({({ℝ^{2}}^{X})}^{ℕ}) (I \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ i (j)) (k) \land \prod_{k \in X} vol ([A (k), B (k))) = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ i (j)) (k))))))$
214	209 213	sylibr	$⊢ (φ \land \neg X = \emptyset) \to \prod_{k \in X} vol ([A (k), B (k))) \in \{z \in ℝ^{*} \| \exists i \in ({({ℝ^{2}}^{X})}^{ℕ}) (I \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)))))\}$
215	5	eqcomi	$⊢ \{z \in ℝ^{*} \| \exists i \in ({({ℝ^{2}}^{X})}^{ℕ}) (I \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)))))\} = M$
216	215	a1i	$⊢ (φ \land \neg X = \emptyset) \to \{z \in ℝ^{*} \| \exists i \in ({({ℝ^{2}}^{X})}^{ℕ}) (I \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)))))\} = M$
217	214 216	eleqtrd	$⊢ (φ \land \neg X = \emptyset) \to \prod_{k \in X} vol ([A (k), B (k))) \in M$
218		infxrlb	$⊢ (M \subseteq ℝ^{} \land \prod_{k \in X} vol ([A (k), B (k))) \in M) \to inf (M ℝ^{} <) \leq \prod_{k \in X} vol ([A (k), B (k)))$
219	30 217 218	syl2anc	$⊢ (φ \land \neg X = \emptyset) \to inf (M ℝ^{*} <) \leq \prod_{k \in X} vol ([A (k), B (k)))$
220	27 219	eqbrtrd	$⊢ (φ \land \neg X = \emptyset) \to if (X = \emptyset, 0, inf (M ℝ^{*} <)) \leq \prod_{k \in X} vol ([A (k), B (k)))$
221	25 220	pm2.61dan	$⊢ φ \to if (X = \emptyset, 0, inf (M ℝ^{*} <)) \leq \prod_{k \in X} vol ([A (k), B (k)))$
222	14 221	eqbrtrd	$⊢ φ \to voln* (X) (I) \leq \prod_{k \in X} vol ([A (k), B (k)))$

Metamath Proof Explorer

Theorem ovnhoilem1

Proof