hoidmvlelem4

Description: The dimensional volume of a multidimensional half-open interval is less than or equal the generalized sum of the dimensional volumes of countable half-open intervals that cover it. Induction step of Lemma 115B of Fremlin1 p. 29, case nonempty interval and dimension of the space greater than 1 . (Contributed by Glauco Siliprandi, 21-Nov-2020)

	Ref	Expression
Hypotheses	hoidmvlelem4.l	$⊢ L = (x \in Fin ⟼ (a \in (ℝ^{x}), b \in (ℝ^{x}) ⟼ if (x = \emptyset, 0, \prod_{k \in x} vol ([a (k), b (k))))))$
	hoidmvlelem4.x	$⊢ φ \to X \in Fin$
	hoidmvlelem4.y	$⊢ φ \to Y \subseteq X$
	hoidmvlelem4.n	$⊢ φ \to Y \neq \emptyset$
	hoidmvlelem4.z	$⊢ φ \to Z \in (X ∖ Y)$
	hoidmvlelem4.w	$⊢ W = Y \cup \{Z\}$
	hoidmvlelem4.a	$⊢ φ \to A : W ⟶ ℝ$
	hoidmvlelem4.b	$⊢ φ \to B : W ⟶ ℝ$
	hoidmvlelem4.k	$⊢ (φ \land k \in W) \to A (k) < B (k)$
	hoidmvlelem4.c	$⊢ φ \to C : ℕ ⟶ ℝ^{W}$
	hoidmvlelem4.d	$⊢ φ \to D : ℕ ⟶ ℝ^{W}$
	hoidmvlelem4.r	$⊢ φ \to sum^((j \in ℕ ⟼ C (j) L (W) D (j))) \in ℝ$
	hoidmvlelem4.h	$⊢ H = (x \in ℝ ⟼ (c \in (ℝ^{W}) ⟼ (j \in W ⟼ if (j \in Y, c (j), if (c (j) \leq x, c (j), x)))))$
	hoidmvlelem4.14	$⊢ G = ({A ↾}_{Y}) L (Y) ({B ↾}_{Y})$
	hoidmvlelem4.e	$⊢ φ \to E \in ℝ^{+}$
	hoidmvlelem4.u	$⊢ U = \{z \in [A (Z), B (Z)] \| G (z - A (Z)) \leq (1 + E) sum^((j \in ℕ ⟼ C (j) L (W) H (z) (D (j))))\}$
	hoidmvlelem4.s	$⊢ S = sup (U ℝ <)$
	hoidmvlelem4.i	$⊢ φ \to \forall e \in (ℝ^{Y}) \forall f \in (ℝ^{Y}) \forall g \in ({(ℝ^{Y})}^{ℕ}) \forall h \in ({(ℝ^{Y})}^{ℕ}) (\underset{k \in Y}{⨉} [e (k), f (k)) \subseteq ⋃_{j \in ℕ} \underset{k \in Y}{⨉} [g (j) (k), h (j) (k)) \to e L (Y) f \leq sum^((j \in ℕ ⟼ g (j) L (Y) h (j))))$
	hoidmvlelem4.i2	$⊢ φ \to \underset{k \in W}{⨉} [A (k), B (k)) \subseteq ⋃_{j \in ℕ} \underset{k \in W}{⨉} [C (j) (k), D (j) (k))$
Assertion	hoidmvlelem4	$⊢ φ \to A L (W) B \leq (1 + E) sum^((j \in ℕ ⟼ C (j) L (W) D (j)))$

Proof

Step	Hyp	Ref	Expression
1		hoidmvlelem4.l	$⊢ L = (x \in Fin ⟼ (a \in (ℝ^{x}), b \in (ℝ^{x}) ⟼ if (x = \emptyset, 0, \prod_{k \in x} vol ([a (k), b (k))))))$
2		hoidmvlelem4.x	$⊢ φ \to X \in Fin$
3		hoidmvlelem4.y	$⊢ φ \to Y \subseteq X$
4		hoidmvlelem4.n	$⊢ φ \to Y \neq \emptyset$
5		hoidmvlelem4.z	$⊢ φ \to Z \in (X ∖ Y)$
6		hoidmvlelem4.w	$⊢ W = Y \cup \{Z\}$
7		hoidmvlelem4.a	$⊢ φ \to A : W ⟶ ℝ$
8		hoidmvlelem4.b	$⊢ φ \to B : W ⟶ ℝ$
9		hoidmvlelem4.k	$⊢ (φ \land k \in W) \to A (k) < B (k)$
10		hoidmvlelem4.c	$⊢ φ \to C : ℕ ⟶ ℝ^{W}$
11		hoidmvlelem4.d	$⊢ φ \to D : ℕ ⟶ ℝ^{W}$
12		hoidmvlelem4.r	$⊢ φ \to sum^((j \in ℕ ⟼ C (j) L (W) D (j))) \in ℝ$
13		hoidmvlelem4.h	$⊢ H = (x \in ℝ ⟼ (c \in (ℝ^{W}) ⟼ (j \in W ⟼ if (j \in Y, c (j), if (c (j) \leq x, c (j), x)))))$
14		hoidmvlelem4.14	$⊢ G = ({A ↾}_{Y}) L (Y) ({B ↾}_{Y})$
15		hoidmvlelem4.e	$⊢ φ \to E \in ℝ^{+}$
16		hoidmvlelem4.u	$⊢ U = \{z \in [A (Z), B (Z)] \| G (z - A (Z)) \leq (1 + E) sum^((j \in ℕ ⟼ C (j) L (W) H (z) (D (j))))\}$
17		hoidmvlelem4.s	$⊢ S = sup (U ℝ <)$
18		hoidmvlelem4.i	$⊢ φ \to \forall e \in (ℝ^{Y}) \forall f \in (ℝ^{Y}) \forall g \in ({(ℝ^{Y})}^{ℕ}) \forall h \in ({(ℝ^{Y})}^{ℕ}) (\underset{k \in Y}{⨉} [e (k), f (k)) \subseteq ⋃_{j \in ℕ} \underset{k \in Y}{⨉} [g (j) (k), h (j) (k)) \to e L (Y) f \leq sum^((j \in ℕ ⟼ g (j) L (Y) h (j))))$
19		hoidmvlelem4.i2	$⊢ φ \to \underset{k \in W}{⨉} [A (k), B (k)) \subseteq ⋃_{j \in ℕ} \underset{k \in W}{⨉} [C (j) (k), D (j) (k))$
20		rge0ssre	$⊢ [0, +∞) \subseteq ℝ$
21	5	eldifad	$⊢ φ \to Z \in X$
22		snssi	$⊢ Z \in X \to \{Z\} \subseteq X$
23	21 22	syl	$⊢ φ \to \{Z\} \subseteq X$
24	3 23	unssd	$⊢ φ \to Y \cup \{Z\} \subseteq X$
25	6 24	eqsstrid	$⊢ φ \to W \subseteq X$
26		ssfi	$⊢ (X \in Fin \land W \subseteq X) \to W \in Fin$
27	2 25 26	syl2anc	$⊢ φ \to W \in Fin$
28	1 27 7 8	hoidmvcl	$⊢ φ \to A L (W) B \in [0, +∞)$
29	20 28	sselid	$⊢ φ \to A L (W) B \in ℝ$
30		1red	$⊢ φ \to 1 \in ℝ$
31	15	rpred	$⊢ φ \to E \in ℝ$
32	30 31	readdcld	$⊢ φ \to 1 + E \in ℝ$
33		nfv	$⊢ Ⅎ j φ$
34		nnex	$⊢ ℕ \in V$
35	34	a1i	$⊢ φ \to ℕ \in V$
36		icossicc	$⊢ [0, +∞) \subseteq [0, +∞]$
37	27	adantr	$⊢ (φ \land j \in ℕ) \to W \in Fin$
38	10	ffvelrnda	$⊢ (φ \land j \in ℕ) \to C (j) \in (ℝ^{W})$
39		elmapi	$⊢ C (j) \in (ℝ^{W}) \to C (j) : W ⟶ ℝ$
40	38 39	syl	$⊢ (φ \land j \in ℕ) \to C (j) : W ⟶ ℝ$
41		eleq1	$⊢ j = h \to (j \in Y \leftrightarrow h \in Y)$
42		fveq2	$⊢ j = h \to c (j) = c (h)$
43	42	breq1d	$⊢ j = h \to (c (j) \leq x \leftrightarrow c (h) \leq x)$
44	43 42	ifbieq1d	$⊢ j = h \to if (c (j) \leq x, c (j), x) = if (c (h) \leq x, c (h), x)$
45	41 42 44	ifbieq12d	$⊢ j = h \to if (j \in Y, c (j), if (c (j) \leq x, c (j), x)) = if (h \in Y, c (h), if (c (h) \leq x, c (h), x))$
46	45	cbvmptv	$⊢ (j \in W ⟼ if (j \in Y, c (j), if (c (j) \leq x, c (j), x))) = (h \in W ⟼ if (h \in Y, c (h), if (c (h) \leq x, c (h), x)))$
47	46	mpteq2i	$⊢ (c \in (ℝ^{W}) ⟼ (j \in W ⟼ if (j \in Y, c (j), if (c (j) \leq x, c (j), x)))) = (c \in (ℝ^{W}) ⟼ (h \in W ⟼ if (h \in Y, c (h), if (c (h) \leq x, c (h), x))))$
48	47	mpteq2i	$⊢ (x \in ℝ ⟼ (c \in (ℝ^{W}) ⟼ (j \in W ⟼ if (j \in Y, c (j), if (c (j) \leq x, c (j), x))))) = (x \in ℝ ⟼ (c \in (ℝ^{W}) ⟼ (h \in W ⟼ if (h \in Y, c (h), if (c (h) \leq x, c (h), x)))))$
49	13 48	eqtri	$⊢ H = (x \in ℝ ⟼ (c \in (ℝ^{W}) ⟼ (h \in W ⟼ if (h \in Y, c (h), if (c (h) \leq x, c (h), x)))))$
50		snidg	$⊢ Z \in (X ∖ Y) \to Z \in \{Z\}$
51	5 50	syl	$⊢ φ \to Z \in \{Z\}$
52		elun2	$⊢ Z \in \{Z\} \to Z \in (Y \cup \{Z\})$
53	51 52	syl	$⊢ φ \to Z \in (Y \cup \{Z\})$
54	6	a1i	$⊢ φ \to W = Y \cup \{Z\}$
55	54	eqcomd	$⊢ φ \to Y \cup \{Z\} = W$
56	53 55	eleqtrd	$⊢ φ \to Z \in W$
57	8 56	ffvelrnd	$⊢ φ \to B (Z) \in ℝ$
58	57	adantr	$⊢ (φ \land j \in ℕ) \to B (Z) \in ℝ$
59	11	ffvelrnda	$⊢ (φ \land j \in ℕ) \to D (j) \in (ℝ^{W})$
60		elmapi	$⊢ D (j) \in (ℝ^{W}) \to D (j) : W ⟶ ℝ$
61	59 60	syl	$⊢ (φ \land j \in ℕ) \to D (j) : W ⟶ ℝ$
62	49 58 37 61	hsphoif	$⊢ (φ \land j \in ℕ) \to H (B (Z)) (D (j)) : W ⟶ ℝ$
63	1 37 40 62	hoidmvcl	$⊢ (φ \land j \in ℕ) \to C (j) L (W) H (B (Z)) (D (j)) \in [0, +∞)$
64	36 63	sselid	$⊢ (φ \land j \in ℕ) \to C (j) L (W) H (B (Z)) (D (j)) \in [0, +∞]$
65	33 35 64	sge0clmpt	$⊢ φ \to sum^((j \in ℕ ⟼ C (j) L (W) H (B (Z)) (D (j)))) \in [0, +∞]$
66	33 35 64	sge0xrclmpt	$⊢ φ \to sum^((j \in ℕ ⟼ C (j) L (W) H (B (Z)) (D (j)))) \in ℝ^{*}$
67		pnfxr	$⊢ +∞ \in ℝ^{*}$
68	67	a1i	$⊢ φ \to +∞ \in ℝ^{*}$
69	12	rexrd	$⊢ φ \to sum^((j \in ℕ ⟼ C (j) L (W) D (j))) \in ℝ^{*}$
70	1 37 40 61	hoidmvcl	$⊢ (φ \land j \in ℕ) \to C (j) L (W) D (j) \in [0, +∞)$
71	36 70	sselid	$⊢ (φ \land j \in ℕ) \to C (j) L (W) D (j) \in [0, +∞]$
72	5	eldifbd	$⊢ φ \to \neg Z \in Y$
73	56 72	eldifd	$⊢ φ \to Z \in (W ∖ Y)$
74	73	adantr	$⊢ (φ \land j \in ℕ) \to Z \in (W ∖ Y)$
75	1 37 74 6 58 49 40 61	hsphoidmvle	$⊢ (φ \land j \in ℕ) \to C (j) L (W) H (B (Z)) (D (j)) \leq C (j) L (W) D (j)$
76	33 35 64 71 75	sge0lempt	$⊢ φ \to sum^((j \in ℕ ⟼ C (j) L (W) H (B (Z)) (D (j)))) \leq sum^((j \in ℕ ⟼ C (j) L (W) D (j)))$
77	12	ltpnfd	$⊢ φ \to sum^((j \in ℕ ⟼ C (j) L (W) D (j))) < +∞$
78	66 69 68 76 77	xrlelttrd	$⊢ φ \to sum^((j \in ℕ ⟼ C (j) L (W) H (B (Z)) (D (j)))) < +∞$
79	66 68 78	xrltned	$⊢ φ \to sum^((j \in ℕ ⟼ C (j) L (W) H (B (Z)) (D (j)))) \neq +∞$
80		ge0xrre	$⊢ (sum^((j \in ℕ ⟼ C (j) L (W) H (B (Z)) (D (j)))) \in [0, +∞] \land sum^((j \in ℕ ⟼ C (j) L (W) H (B (Z)) (D (j)))) \neq +∞) \to sum^((j \in ℕ ⟼ C (j) L (W) H (B (Z)) (D (j)))) \in ℝ$
81	65 79 80	syl2anc	$⊢ φ \to sum^((j \in ℕ ⟼ C (j) L (W) H (B (Z)) (D (j)))) \in ℝ$
82	32 81	remulcld	$⊢ φ \to (1 + E) sum^((j \in ℕ ⟼ C (j) L (W) H (B (Z)) (D (j)))) \in ℝ$
83	32 12	remulcld	$⊢ φ \to (1 + E) sum^((j \in ℕ ⟼ C (j) L (W) D (j))) \in ℝ$
84	56	ancli	$⊢ φ \to (φ \land Z \in W)$
85		eleq1	$⊢ k = Z \to (k \in W \leftrightarrow Z \in W)$
86	85	anbi2d	$⊢ k = Z \to ((φ \land k \in W) \leftrightarrow (φ \land Z \in W))$
87		fveq2	$⊢ k = Z \to A (k) = A (Z)$
88		fveq2	$⊢ k = Z \to B (k) = B (Z)$
89	87 88	breq12d	$⊢ k = Z \to (A (k) < B (k) \leftrightarrow A (Z) < B (Z))$
90	86 89	imbi12d	$⊢ k = Z \to (((φ \land k \in W) \to A (k) < B (k)) \leftrightarrow ((φ \land Z \in W) \to A (Z) < B (Z)))$
91	90 9	vtoclg	$⊢ Z \in W \to ((φ \land Z \in W) \to A (Z) < B (Z))$
92	56 84 91	sylc	$⊢ φ \to A (Z) < B (Z)$
93	1 2 3 5 6 7 8 10 11 12 13 14 15 16 17 92	hoidmvlelem1	$⊢ φ \to S \in U$
94	57	rexrd	$⊢ φ \to B (Z) \in ℝ^{*}$
95		iccssxr	$⊢ [A (Z), B (Z)] \subseteq ℝ^{*}$
96		ssrab2	$⊢ \{z \in [A (Z), B (Z)] \| G (z - A (Z)) \leq (1 + E) sum^((j \in ℕ ⟼ C (j) L (W) H (z) (D (j))))\} \subseteq [A (Z), B (Z)]$
97	16 96	eqsstri	$⊢ U \subseteq [A (Z), B (Z)]$
98	97 93	sselid	$⊢ φ \to S \in [A (Z), B (Z)]$
99	95 98	sselid	$⊢ φ \to S \in ℝ^{*}$
100		simpl	$⊢ (φ \land \neg B (Z) \leq S) \to φ$
101		simpr	$⊢ (φ \land \neg B (Z) \leq S) \to \neg B (Z) \leq S$
102	7 56	ffvelrnd	$⊢ φ \to A (Z) \in ℝ$
103	102 57	iccssred	$⊢ φ \to [A (Z), B (Z)] \subseteq ℝ$
104	103 98	sseldd	$⊢ φ \to S \in ℝ$
105	104	adantr	$⊢ (φ \land \neg B (Z) \leq S) \to S \in ℝ$
106	100 57	syl	$⊢ (φ \land \neg B (Z) \leq S) \to B (Z) \in ℝ$
107	105 106	ltnled	$⊢ (φ \land \neg B (Z) \leq S) \to (S < B (Z) \leftrightarrow \neg B (Z) \leq S)$
108	101 107	mpbird	$⊢ (φ \land \neg B (Z) \leq S) \to S < B (Z)$
109	2	adantr	$⊢ (φ \land S < B (Z)) \to X \in Fin$
110	3	adantr	$⊢ (φ \land S < B (Z)) \to Y \subseteq X$
111	5	adantr	$⊢ (φ \land S < B (Z)) \to Z \in (X ∖ Y)$
112	7	adantr	$⊢ (φ \land S < B (Z)) \to A : W ⟶ ℝ$
113	8	adantr	$⊢ (φ \land S < B (Z)) \to B : W ⟶ ℝ$
114	9	adantlr	$⊢ ((φ \land S < B (Z)) \land k \in W) \to A (k) < B (k)$
115		eqid	$⊢ (y \in Y ⟼ 0) = (y \in Y ⟼ 0)$
116	10	adantr	$⊢ (φ \land S < B (Z)) \to C : ℕ ⟶ ℝ^{W}$
117		fveq2	$⊢ i = j \to C (i) = C (j)$
118	117	fveq1d	$⊢ i = j \to C (i) (Z) = C (j) (Z)$
119		fveq2	$⊢ i = j \to D (i) = D (j)$
120	119	fveq1d	$⊢ i = j \to D (i) (Z) = D (j) (Z)$
121	118 120	oveq12d	$⊢ i = j \to [C (i) (Z), D (i) (Z)) = [C (j) (Z), D (j) (Z))$
122	121	eleq2d	$⊢ i = j \to (S \in [C (i) (Z), D (i) (Z)) \leftrightarrow S \in [C (j) (Z), D (j) (Z)))$
123	117	reseq1d	$⊢ i = j \to {C (i) ↾}_{Y} = {C (j) ↾}_{Y}$
124	122 123	ifbieq1d	$⊢ i = j \to if (S \in [C (i) (Z), D (i) (Z)), {C (i) ↾}_{Y}, (y \in Y ⟼ 0)) = if (S \in [C (j) (Z), D (j) (Z)), {C (j) ↾}_{Y}, (y \in Y ⟼ 0))$
125	124	cbvmptv	$⊢ (i \in ℕ ⟼ if (S \in [C (i) (Z), D (i) (Z)), {C (i) ↾}_{Y}, (y \in Y ⟼ 0))) = (j \in ℕ ⟼ if (S \in [C (j) (Z), D (j) (Z)), {C (j) ↾}_{Y}, (y \in Y ⟼ 0)))$
126	11	adantr	$⊢ (φ \land S < B (Z)) \to D : ℕ ⟶ ℝ^{W}$
127	119	reseq1d	$⊢ i = j \to {D (i) ↾}_{Y} = {D (j) ↾}_{Y}$
128	122 127	ifbieq1d	$⊢ i = j \to if (S \in [C (i) (Z), D (i) (Z)), {D (i) ↾}_{Y}, (y \in Y ⟼ 0)) = if (S \in [C (j) (Z), D (j) (Z)), {D (j) ↾}_{Y}, (y \in Y ⟼ 0))$
129	128	cbvmptv	$⊢ (i \in ℕ ⟼ if (S \in [C (i) (Z), D (i) (Z)), {D (i) ↾}_{Y}, (y \in Y ⟼ 0))) = (j \in ℕ ⟼ if (S \in [C (j) (Z), D (j) (Z)), {D (j) ↾}_{Y}, (y \in Y ⟼ 0)))$
130	12	adantr	$⊢ (φ \land S < B (Z)) \to sum^((j \in ℕ ⟼ C (j) L (W) D (j))) \in ℝ$
131	15	adantr	$⊢ (φ \land S < B (Z)) \to E \in ℝ^{+}$
132	93	adantr	$⊢ (φ \land S < B (Z)) \to S \in U$
133		simpr	$⊢ (φ \land S < B (Z)) \to S < B (Z)$
134		biid	$⊢ S \in [C (i) (Z), D (i) (Z)) \leftrightarrow S \in [C (i) (Z), D (i) (Z))$
135		eqidd	$⊢ w = y \to 0 = 0$
136	135	cbvmptv	$⊢ (w \in Y ⟼ 0) = (y \in Y ⟼ 0)$
137	134 136	ifbieq2i	$⊢ if (S \in [C (i) (Z), D (i) (Z)), {C (i) ↾}_{Y}, (w \in Y ⟼ 0)) = if (S \in [C (i) (Z), D (i) (Z)), {C (i) ↾}_{Y}, (y \in Y ⟼ 0))$
138	137	mpteq2i	$⊢ (i \in ℕ ⟼ if (S \in [C (i) (Z), D (i) (Z)), {C (i) ↾}_{Y}, (w \in Y ⟼ 0))) = (i \in ℕ ⟼ if (S \in [C (i) (Z), D (i) (Z)), {C (i) ↾}_{Y}, (y \in Y ⟼ 0)))$
139	138	a1i	$⊢ l = j \to (i \in ℕ ⟼ if (S \in [C (i) (Z), D (i) (Z)), {C (i) ↾}_{Y}, (w \in Y ⟼ 0))) = (i \in ℕ ⟼ if (S \in [C (i) (Z), D (i) (Z)), {C (i) ↾}_{Y}, (y \in Y ⟼ 0)))$
140		id	$⊢ l = j \to l = j$
141	139 140	fveq12d	$⊢ l = j \to (i \in ℕ ⟼ if (S \in [C (i) (Z), D (i) (Z)), {C (i) ↾}_{Y}, (w \in Y ⟼ 0))) (l) = (i \in ℕ ⟼ if (S \in [C (i) (Z), D (i) (Z)), {C (i) ↾}_{Y}, (y \in Y ⟼ 0))) (j)$
142	134 136	ifbieq2i	$⊢ if (S \in [C (i) (Z), D (i) (Z)), {D (i) ↾}_{Y}, (w \in Y ⟼ 0)) = if (S \in [C (i) (Z), D (i) (Z)), {D (i) ↾}_{Y}, (y \in Y ⟼ 0))$
143	142	mpteq2i	$⊢ (i \in ℕ ⟼ if (S \in [C (i) (Z), D (i) (Z)), {D (i) ↾}_{Y}, (w \in Y ⟼ 0))) = (i \in ℕ ⟼ if (S \in [C (i) (Z), D (i) (Z)), {D (i) ↾}_{Y}, (y \in Y ⟼ 0)))$
144	143	a1i	$⊢ l = j \to (i \in ℕ ⟼ if (S \in [C (i) (Z), D (i) (Z)), {D (i) ↾}_{Y}, (w \in Y ⟼ 0))) = (i \in ℕ ⟼ if (S \in [C (i) (Z), D (i) (Z)), {D (i) ↾}_{Y}, (y \in Y ⟼ 0)))$
145	144 140	fveq12d	$⊢ l = j \to (i \in ℕ ⟼ if (S \in [C (i) (Z), D (i) (Z)), {D (i) ↾}_{Y}, (w \in Y ⟼ 0))) (l) = (i \in ℕ ⟼ if (S \in [C (i) (Z), D (i) (Z)), {D (i) ↾}_{Y}, (y \in Y ⟼ 0))) (j)$
146	141 145	oveq12d	$⊢ l = j \to (i \in ℕ ⟼ if (S \in [C (i) (Z), D (i) (Z)), {C (i) ↾}_{Y}, (w \in Y ⟼ 0))) (l) L (Y) (i \in ℕ ⟼ if (S \in [C (i) (Z), D (i) (Z)), {D (i) ↾}_{Y}, (w \in Y ⟼ 0))) (l) = (i \in ℕ ⟼ if (S \in [C (i) (Z), D (i) (Z)), {C (i) ↾}_{Y}, (y \in Y ⟼ 0))) (j) L (Y) (i \in ℕ ⟼ if (S \in [C (i) (Z), D (i) (Z)), {D (i) ↾}_{Y}, (y \in Y ⟼ 0))) (j)$
147	146	cbvmptv	$⊢ (l \in ℕ ⟼ (i \in ℕ ⟼ if (S \in [C (i) (Z), D (i) (Z)), {C (i) ↾}_{Y}, (w \in Y ⟼ 0))) (l) L (Y) (i \in ℕ ⟼ if (S \in [C (i) (Z), D (i) (Z)), {D (i) ↾}_{Y}, (w \in Y ⟼ 0))) (l)) = (j \in ℕ ⟼ (i \in ℕ ⟼ if (S \in [C (i) (Z), D (i) (Z)), {C (i) ↾}_{Y}, (y \in Y ⟼ 0))) (j) L (Y) (i \in ℕ ⟼ if (S \in [C (i) (Z), D (i) (Z)), {D (i) ↾}_{Y}, (y \in Y ⟼ 0))) (j))$
148	18	adantr	$⊢ (φ \land S < B (Z)) \to \forall e \in (ℝ^{Y}) \forall f \in (ℝ^{Y}) \forall g \in ({(ℝ^{Y})}^{ℕ}) \forall h \in ({(ℝ^{Y})}^{ℕ}) (\underset{k \in Y}{⨉} [e (k), f (k)) \subseteq ⋃_{j \in ℕ} \underset{k \in Y}{⨉} [g (j) (k), h (j) (k)) \to e L (Y) f \leq sum^((j \in ℕ ⟼ g (j) L (Y) h (j))))$
149	19	adantr	$⊢ (φ \land S < B (Z)) \to \underset{k \in W}{⨉} [A (k), B (k)) \subseteq ⋃_{j \in ℕ} \underset{k \in W}{⨉} [C (j) (k), D (j) (k))$
150		eqid	$⊢ (x \in \underset{y \in Y}{⨉} [A (y), B (y)) ⟼ (y \in W ⟼ if (y \in Y, x (y), S))) = (x \in \underset{y \in Y}{⨉} [A (y), B (y)) ⟼ (y \in W ⟼ if (y \in Y, x (y), S)))$
151		fveq2	$⊢ y = k \to A (y) = A (k)$
152		fveq2	$⊢ y = k \to B (y) = B (k)$
153	151 152	oveq12d	$⊢ y = k \to [A (y), B (y)) = [A (k), B (k))$
154	153	cbvixpv	$⊢ \underset{y \in Y}{⨉} [A (y), B (y)) = \underset{k \in Y}{⨉} [A (k), B (k))$
155		eleq1	$⊢ y = k \to (y \in Y \leftrightarrow k \in Y)$
156		fveq2	$⊢ y = k \to x (y) = x (k)$
157	155 156	ifbieq1d	$⊢ y = k \to if (y \in Y, x (y), S) = if (k \in Y, x (k), S)$
158	157	cbvmptv	$⊢ (y \in W ⟼ if (y \in Y, x (y), S)) = (k \in W ⟼ if (k \in Y, x (k), S))$
159	154 158	mpteq12i	$⊢ (x \in \underset{y \in Y}{⨉} [A (y), B (y)) ⟼ (y \in W ⟼ if (y \in Y, x (y), S))) = (x \in \underset{k \in Y}{⨉} [A (k), B (k)) ⟼ (k \in W ⟼ if (k \in Y, x (k), S)))$
160	150 159	eqtri	$⊢ (x \in \underset{y \in Y}{⨉} [A (y), B (y)) ⟼ (y \in W ⟼ if (y \in Y, x (y), S))) = (x \in \underset{k \in Y}{⨉} [A (k), B (k)) ⟼ (k \in W ⟼ if (k \in Y, x (k), S)))$
161	1 109 110 111 6 112 113 114 115 116 125 126 129 130 13 14 131 16 132 133 147 148 149 160	hoidmvlelem3	$⊢ (φ \land S < B (Z)) \to \exists u \in U S < u$
162	100 108 161	syl2anc	$⊢ (φ \land \neg B (Z) \leq S) \to \exists u \in U S < u$
163	97	a1i	$⊢ φ \to U \subseteq [A (Z), B (Z)]$
164	163 103	sstrd	$⊢ φ \to U \subseteq ℝ$
165	164	adantr	$⊢ (φ \land u \in U) \to U \subseteq ℝ$
166		ne0i	$⊢ u \in U \to U \neq \emptyset$
167	166	adantl	$⊢ (φ \land u \in U) \to U \neq \emptyset$
168	102	rexrd	$⊢ φ \to A (Z) \in ℝ^{*}$
169	168	adantr	$⊢ (φ \land u \in U) \to A (Z) \in ℝ^{*}$
170	94	adantr	$⊢ (φ \land u \in U) \to B (Z) \in ℝ^{*}$
171	163	sselda	$⊢ (φ \land u \in U) \to u \in [A (Z), B (Z)]$
172		iccleub	$⊢ (A (Z) \in ℝ^{} \land B (Z) \in ℝ^{} \land u \in [A (Z), B (Z)]) \to u \leq B (Z)$
173	169 170 171 172	syl3anc	$⊢ (φ \land u \in U) \to u \leq B (Z)$
174	173	ralrimiva	$⊢ φ \to \forall u \in U u \leq B (Z)$
175		brralrspcev	$⊢ (B (Z) \in ℝ \land \forall u \in U u \leq B (Z)) \to \exists y \in ℝ \forall u \in U u \leq y$
176	57 174 175	syl2anc	$⊢ φ \to \exists y \in ℝ \forall u \in U u \leq y$
177	176	adantr	$⊢ (φ \land u \in U) \to \exists y \in ℝ \forall u \in U u \leq y$
178		simpr	$⊢ (φ \land u \in U) \to u \in U$
179		suprub	$⊢ ((U \subseteq ℝ \land U \neq \emptyset \land \exists y \in ℝ \forall u \in U u \leq y) \land u \in U) \to u \leq sup (U ℝ <)$
180	165 167 177 178 179	syl31anc	$⊢ (φ \land u \in U) \to u \leq sup (U ℝ <)$
181	180 17	breqtrrdi	$⊢ (φ \land u \in U) \to u \leq S$
182	181	ralrimiva	$⊢ φ \to \forall u \in U u \leq S$
183	165 178	sseldd	$⊢ (φ \land u \in U) \to u \in ℝ$
184	104	adantr	$⊢ (φ \land u \in U) \to S \in ℝ$
185	183 184	lenltd	$⊢ (φ \land u \in U) \to (u \leq S \leftrightarrow \neg S < u)$
186	185	ralbidva	$⊢ φ \to (\forall u \in U u \leq S \leftrightarrow \forall u \in U \neg S < u)$
187	182 186	mpbid	$⊢ φ \to \forall u \in U \neg S < u$
188		ralnex	$⊢ \forall u \in U \neg S < u \leftrightarrow \neg \exists u \in U S < u$
189	187 188	sylib	$⊢ φ \to \neg \exists u \in U S < u$
190	189	adantr	$⊢ (φ \land S < B (Z)) \to \neg \exists u \in U S < u$
191	100 108 190	syl2anc	$⊢ (φ \land \neg B (Z) \leq S) \to \neg \exists u \in U S < u$
192	162 191	condan	$⊢ φ \to B (Z) \leq S$
193		iccleub	$⊢ (A (Z) \in ℝ^{} \land B (Z) \in ℝ^{} \land S \in [A (Z), B (Z)]) \to S \leq B (Z)$
194	168 94 98 193	syl3anc	$⊢ φ \to S \leq B (Z)$
195	94 99 192 194	xrletrid	$⊢ φ \to B (Z) = S$
196	16	eqcomi	$⊢ \{z \in [A (Z), B (Z)] \| G (z - A (Z)) \leq (1 + E) sum^((j \in ℕ ⟼ C (j) L (W) H (z) (D (j))))\} = U$
197	196	a1i	$⊢ φ \to \{z \in [A (Z), B (Z)] \| G (z - A (Z)) \leq (1 + E) sum^((j \in ℕ ⟼ C (j) L (W) H (z) (D (j))))\} = U$
198	195 197	eleq12d	$⊢ φ \to (B (Z) \in \{z \in [A (Z), B (Z)] \| G (z - A (Z)) \leq (1 + E) sum^((j \in ℕ ⟼ C (j) L (W) H (z) (D (j))))\} \leftrightarrow S \in U)$
199	93 198	mpbird	$⊢ φ \to B (Z) \in \{z \in [A (Z), B (Z)] \| G (z - A (Z)) \leq (1 + E) sum^((j \in ℕ ⟼ C (j) L (W) H (z) (D (j))))\}$
200		oveq1	$⊢ z = B (Z) \to z - A (Z) = B (Z) - A (Z)$
201	200	oveq2d	$⊢ z = B (Z) \to G (z - A (Z)) = G (B (Z) - A (Z))$
202		fveq2	$⊢ z = B (Z) \to H (z) = H (B (Z))$
203	202	fveq1d	$⊢ z = B (Z) \to H (z) (D (j)) = H (B (Z)) (D (j))$
204	203	oveq2d	$⊢ z = B (Z) \to C (j) L (W) H (z) (D (j)) = C (j) L (W) H (B (Z)) (D (j))$
205	204	mpteq2dv	$⊢ z = B (Z) \to (j \in ℕ ⟼ C (j) L (W) H (z) (D (j))) = (j \in ℕ ⟼ C (j) L (W) H (B (Z)) (D (j)))$
206	205	fveq2d	$⊢ z = B (Z) \to sum^((j \in ℕ ⟼ C (j) L (W) H (z) (D (j)))) = sum^((j \in ℕ ⟼ C (j) L (W) H (B (Z)) (D (j))))$
207	206	oveq2d	$⊢ z = B (Z) \to (1 + E) sum^((j \in ℕ ⟼ C (j) L (W) H (z) (D (j)))) = (1 + E) sum^((j \in ℕ ⟼ C (j) L (W) H (B (Z)) (D (j))))$
208	201 207	breq12d	$⊢ z = B (Z) \to (G (z - A (Z)) \leq (1 + E) sum^((j \in ℕ ⟼ C (j) L (W) H (z) (D (j)))) \leftrightarrow G (B (Z) - A (Z)) \leq (1 + E) sum^((j \in ℕ ⟼ C (j) L (W) H (B (Z)) (D (j)))))$
209	208	elrab	$⊢ B (Z) \in \{z \in [A (Z), B (Z)] \| G (z - A (Z)) \leq (1 + E) sum^((j \in ℕ ⟼ C (j) L (W) H (z) (D (j))))\} \leftrightarrow (B (Z) \in [A (Z), B (Z)] \land G (B (Z) - A (Z)) \leq (1 + E) sum^((j \in ℕ ⟼ C (j) L (W) H (B (Z)) (D (j)))))$
210	199 209	sylib	$⊢ φ \to (B (Z) \in [A (Z), B (Z)] \land G (B (Z) - A (Z)) \leq (1 + E) sum^((j \in ℕ ⟼ C (j) L (W) H (B (Z)) (D (j)))))$
211	210	simprd	$⊢ φ \to G (B (Z) - A (Z)) \leq (1 + E) sum^((j \in ℕ ⟼ C (j) L (W) H (B (Z)) (D (j))))$
212	2 3	ssfid	$⊢ φ \to Y \in Fin$
213		eqid	$⊢ \prod_{k \in Y} vol ([A (k), B (k))) = \prod_{k \in Y} vol ([A (k), B (k)))$
214	1 212 5 72 6 7 8 213	hoiprodp1	$⊢ φ \to A L (W) B = \prod_{k \in Y} vol ([A (k), B (k))) vol ([A (Z), B (Z)))$
215		eqidd	$⊢ φ \to \prod_{k \in Y} (B (k) - A (k)) = \prod_{k \in Y} (B (k) - A (k))$
216	7	adantr	$⊢ (φ \land k \in Y) \to A : W ⟶ ℝ$
217		ssun1	$⊢ Y \subseteq Y \cup \{Z\}$
218	6	eqcomi	$⊢ Y \cup \{Z\} = W$
219	217 218	sseqtri	$⊢ Y \subseteq W$
220		simpr	$⊢ (φ \land k \in Y) \to k \in Y$
221	219 220	sselid	$⊢ (φ \land k \in Y) \to k \in W$
222	216 221	ffvelrnd	$⊢ (φ \land k \in Y) \to A (k) \in ℝ$
223	8	adantr	$⊢ (φ \land k \in Y) \to B : W ⟶ ℝ$
224	223 221	ffvelrnd	$⊢ (φ \land k \in Y) \to B (k) \in ℝ$
225	221 9	syldan	$⊢ (φ \land k \in Y) \to A (k) < B (k)$
226	222 224 225	volicon0	$⊢ (φ \land k \in Y) \to vol ([A (k), B (k))) = B (k) - A (k)$
227	226	prodeq2dv	$⊢ φ \to \prod_{k \in Y} vol ([A (k), B (k))) = \prod_{k \in Y} (B (k) - A (k))$
228	14	a1i	$⊢ φ \to G = ({A ↾}_{Y}) L (Y) ({B ↾}_{Y})$
229	219	a1i	$⊢ φ \to Y \subseteq W$
230	7 229	fssresd	$⊢ φ \to ({A ↾}_{Y}) : Y ⟶ ℝ$
231	8 229	fssresd	$⊢ φ \to ({B ↾}_{Y}) : Y ⟶ ℝ$
232	1 212 4 230 231	hoidmvn0val	$⊢ φ \to ({A ↾}_{Y}) L (Y) ({B ↾}_{Y}) = \prod_{k \in Y} vol ([({A ↾}_{Y}) (k), ({B ↾}_{Y}) (k)))$
233		fvres	$⊢ k \in Y \to ({A ↾}_{Y}) (k) = A (k)$
234		fvres	$⊢ k \in Y \to ({B ↾}_{Y}) (k) = B (k)$
235	233 234	oveq12d	$⊢ k \in Y \to [({A ↾}_{Y}) (k), ({B ↾}_{Y}) (k)) = [A (k), B (k))$
236	235	fveq2d	$⊢ k \in Y \to vol ([({A ↾}_{Y}) (k), ({B ↾}_{Y}) (k))) = vol ([A (k), B (k)))$
237	236	adantl	$⊢ (φ \land k \in Y) \to vol ([({A ↾}_{Y}) (k), ({B ↾}_{Y}) (k))) = vol ([A (k), B (k)))$
238		volico	$⊢ (A (k) \in ℝ \land B (k) \in ℝ) \to vol ([A (k), B (k))) = if (A (k) < B (k), B (k) - A (k), 0)$
239	222 224 238	syl2anc	$⊢ (φ \land k \in Y) \to vol ([A (k), B (k))) = if (A (k) < B (k), B (k) - A (k), 0)$
240	239 226	eqtr3d	$⊢ (φ \land k \in Y) \to if (A (k) < B (k), B (k) - A (k), 0) = B (k) - A (k)$
241	237 239 240	3eqtrd	$⊢ (φ \land k \in Y) \to vol ([({A ↾}_{Y}) (k), ({B ↾}_{Y}) (k))) = B (k) - A (k)$
242	241	prodeq2dv	$⊢ φ \to \prod_{k \in Y} vol ([({A ↾}_{Y}) (k), ({B ↾}_{Y}) (k))) = \prod_{k \in Y} (B (k) - A (k))$
243	228 232 242	3eqtrd	$⊢ φ \to G = \prod_{k \in Y} (B (k) - A (k))$
244	215 227 243	3eqtr4d	$⊢ φ \to \prod_{k \in Y} vol ([A (k), B (k))) = G$
245	102 57 92	volicon0	$⊢ φ \to vol ([A (Z), B (Z))) = B (Z) - A (Z)$
246	244 245	oveq12d	$⊢ φ \to \prod_{k \in Y} vol ([A (k), B (k))) vol ([A (Z), B (Z))) = G (B (Z) - A (Z))$
247	214 246	eqtrd	$⊢ φ \to A L (W) B = G (B (Z) - A (Z))$
248	247	breq1d	$⊢ φ \to (A L (W) B \leq (1 + E) sum^((j \in ℕ ⟼ C (j) L (W) H (B (Z)) (D (j)))) \leftrightarrow G (B (Z) - A (Z)) \leq (1 + E) sum^((j \in ℕ ⟼ C (j) L (W) H (B (Z)) (D (j)))))$
249	211 248	mpbird	$⊢ φ \to A L (W) B \leq (1 + E) sum^((j \in ℕ ⟼ C (j) L (W) H (B (Z)) (D (j))))$
250		0le1	$⊢ 0 \leq 1$
251	250	a1i	$⊢ φ \to 0 \leq 1$
252	15	rpge0d	$⊢ φ \to 0 \leq E$
253	30 31 251 252	addge0d	$⊢ φ \to 0 \leq 1 + E$
254	81 12 32 253 76	lemul2ad	$⊢ φ \to (1 + E) sum^((j \in ℕ ⟼ C (j) L (W) H (B (Z)) (D (j)))) \leq (1 + E) sum^((j \in ℕ ⟼ C (j) L (W) D (j)))$
255	29 82 83 249 254	letrd	$⊢ φ \to A L (W) B \leq (1 + E) sum^((j \in ℕ ⟼ C (j) L (W) D (j)))$

Metamath Proof Explorer

Theorem hoidmvlelem4

Proof