ovncvr2

Description: B and T are the left and right side of a cover of A . This cover is made of n-dimensional half-open intervals and approximates the n-dimensional Lebesgue outer volume of A . (Contributed by Glauco Siliprandi, 24-Dec-2020)

	Ref	Expression
Hypotheses	ovncvr2.x	$⊢ φ \to X \in Fin$
	ovncvr2.a	$⊢ φ \to A \subseteq ℝ^{X}$
	ovncvr2.e	$⊢ φ \to E \in ℝ^{+}$
	ovncvr2.c	$⊢ C = (a \in 𝒫 (ℝ^{X}) ⟼ \{l \in ({({ℝ^{2}}^{X})}^{ℕ}) \| a \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ l (j)) (k)\})$
	ovncvr2.l	$⊢ L = (h \in ({ℝ^{2}}^{X}) ⟼ \prod_{k \in X} vol (([.) \circ h) (k)))$
	ovncvr2.d	$⊢ D = (a \in 𝒫 (ℝ^{X}) ⟼ (r \in ℝ^{+} ⟼ \{i \in C (a) \| sum^((j \in ℕ ⟼ L (i (j)))) \leq voln* (X) (a) +_{𝑒} r\}))$
	ovncvr2.i	$⊢ φ \to I \in D (A) (E)$
	ovncvr2.b	$⊢ B = (j \in ℕ ⟼ (k \in X ⟼ 1^{st} (I (j) (k))))$
	ovncvr2.t	$⊢ T = (j \in ℕ ⟼ (k \in X ⟼ 2^{nd} (I (j) (k))))$
Assertion	ovncvr2	$⊢ φ \to (((B : ℕ ⟶ ℝ^{X} \land T : ℕ ⟶ ℝ^{X}) \land A \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} [B (j) (k), T (j) (k))) \land sum^((j \in ℕ ⟼ \prod_{k \in X} vol ([B (j) (k), T (j) (k))))) \leq voln* (X) (A) +_{𝑒} E)$

Proof

Step	Hyp	Ref	Expression
1		ovncvr2.x	$⊢ φ \to X \in Fin$
2		ovncvr2.a	$⊢ φ \to A \subseteq ℝ^{X}$
3		ovncvr2.e	$⊢ φ \to E \in ℝ^{+}$
4		ovncvr2.c	$⊢ C = (a \in 𝒫 (ℝ^{X}) ⟼ \{l \in ({({ℝ^{2}}^{X})}^{ℕ}) \| a \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ l (j)) (k)\})$
5		ovncvr2.l	$⊢ L = (h \in ({ℝ^{2}}^{X}) ⟼ \prod_{k \in X} vol (([.) \circ h) (k)))$
6		ovncvr2.d	$⊢ D = (a \in 𝒫 (ℝ^{X}) ⟼ (r \in ℝ^{+} ⟼ \{i \in C (a) \| sum^((j \in ℕ ⟼ L (i (j)))) \leq voln* (X) (a) +_{𝑒} r\}))$
7		ovncvr2.i	$⊢ φ \to I \in D (A) (E)$
8		ovncvr2.b	$⊢ B = (j \in ℕ ⟼ (k \in X ⟼ 1^{st} (I (j) (k))))$
9		ovncvr2.t	$⊢ T = (j \in ℕ ⟼ (k \in X ⟼ 2^{nd} (I (j) (k))))$
10		sseq1	$⊢ a = A \to (a \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ l (j)) (k) \leftrightarrow A \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ l (j)) (k))$
11	10	rabbidv	$⊢ a = A \to \{l \in ({({ℝ^{2}}^{X})}^{ℕ}) \| a \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ l (j)) (k)\} = \{l \in ({({ℝ^{2}}^{X})}^{ℕ}) \| A \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ l (j)) (k)\}$
12		ovexd	$⊢ φ \to ℝ^{X} \in V$
13	12 2	ssexd	$⊢ φ \to A \in V$
14		elpwg	$⊢ A \in V \to (A \in 𝒫 (ℝ^{X}) \leftrightarrow A \subseteq ℝ^{X})$
15	13 14	syl	$⊢ φ \to (A \in 𝒫 (ℝ^{X}) \leftrightarrow A \subseteq ℝ^{X})$
16	2 15	mpbird	$⊢ φ \to A \in 𝒫 (ℝ^{X})$
17		ovex	$⊢ {({ℝ^{2}}^{X})}^{ℕ} \in V$
18	17	rabex	$⊢ \{l \in ({({ℝ^{2}}^{X})}^{ℕ}) \| A \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ l (j)) (k)\} \in V$
19	18	a1i	$⊢ φ \to \{l \in ({({ℝ^{2}}^{X})}^{ℕ}) \| A \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ l (j)) (k)\} \in V$
20	4 11 16 19	fvmptd3	$⊢ φ \to C (A) = \{l \in ({({ℝ^{2}}^{X})}^{ℕ}) \| A \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ l (j)) (k)\}$
21		ssrab2	$⊢ \{l \in ({({ℝ^{2}}^{X})}^{ℕ}) \| A \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ l (j)) (k)\} \subseteq {({ℝ^{2}}^{X})}^{ℕ}$
22	21	a1i	$⊢ φ \to \{l \in ({({ℝ^{2}}^{X})}^{ℕ}) \| A \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ l (j)) (k)\} \subseteq {({ℝ^{2}}^{X})}^{ℕ}$
23	20 22	eqsstrd	$⊢ φ \to C (A) \subseteq {({ℝ^{2}}^{X})}^{ℕ}$
24		fveq2	$⊢ a = A \to C (a) = C (A)$
25	24	eleq2d	$⊢ a = A \to (i \in C (a) \leftrightarrow i \in C (A))$
26		fveq2	$⊢ a = A \to voln* (X) (a) = voln* (X) (A)$
27	26	oveq1d	$⊢ a = A \to voln* (X) (a) +_{𝑒} r = voln* (X) (A) +_{𝑒} r$
28	27	breq2d	$⊢ a = A \to (sum^((j \in ℕ ⟼ L (i (j)))) \leq voln* (X) (a) +_{𝑒} r \leftrightarrow sum^((j \in ℕ ⟼ L (i (j)))) \leq voln* (X) (A) +_{𝑒} r)$
29	25 28	anbi12d	$⊢ a = A \to ((i \in C (a) \land sum^((j \in ℕ ⟼ L (i (j)))) \leq voln* (X) (a) +_{𝑒} r) \leftrightarrow (i \in C (A) \land sum^((j \in ℕ ⟼ L (i (j)))) \leq voln* (X) (A) +_{𝑒} r))$
30	29	rabbidva2	$⊢ a = A \to \{i \in C (a) \| sum^((j \in ℕ ⟼ L (i (j)))) \leq voln* (X) (a) +_{𝑒} r\} = \{i \in C (A) \| sum^((j \in ℕ ⟼ L (i (j)))) \leq voln* (X) (A) +_{𝑒} r\}$
31	30	mpteq2dv	$⊢ a = A \to (r \in ℝ^{+} ⟼ \{i \in C (a) \| sum^((j \in ℕ ⟼ L (i (j)))) \leq voln* (X) (a) +_{𝑒} r\}) = (r \in ℝ^{+} ⟼ \{i \in C (A) \| sum^((j \in ℕ ⟼ L (i (j)))) \leq voln* (X) (A) +_{𝑒} r\})$
32		rpex	$⊢ ℝ^{+} \in V$
33	32	mptex	$⊢ (r \in ℝ^{+} ⟼ \{i \in C (A) \| sum^((j \in ℕ ⟼ L (i (j)))) \leq voln* (X) (A) +_{𝑒} r\}) \in V$
34	33	a1i	$⊢ φ \to (r \in ℝ^{+} ⟼ \{i \in C (A) \| sum^((j \in ℕ ⟼ L (i (j)))) \leq voln* (X) (A) +_{𝑒} r\}) \in V$
35	6 31 16 34	fvmptd3	$⊢ φ \to D (A) = (r \in ℝ^{+} ⟼ \{i \in C (A) \| sum^((j \in ℕ ⟼ L (i (j)))) \leq voln* (X) (A) +_{𝑒} r\})$
36		oveq2	$⊢ r = E \to voln* (X) (A) +_{𝑒} r = voln* (X) (A) +_{𝑒} E$
37	36	breq2d	$⊢ r = E \to (sum^((j \in ℕ ⟼ L (i (j)))) \leq voln* (X) (A) +_{𝑒} r \leftrightarrow sum^((j \in ℕ ⟼ L (i (j)))) \leq voln* (X) (A) +_{𝑒} E)$
38	37	rabbidv	$⊢ r = E \to \{i \in C (A) \| sum^((j \in ℕ ⟼ L (i (j)))) \leq voln* (X) (A) +_{𝑒} r\} = \{i \in C (A) \| sum^((j \in ℕ ⟼ L (i (j)))) \leq voln* (X) (A) +_{𝑒} E\}$
39	38	adantl	$⊢ (φ \land r = E) \to \{i \in C (A) \| sum^((j \in ℕ ⟼ L (i (j)))) \leq voln* (X) (A) +_{𝑒} r\} = \{i \in C (A) \| sum^((j \in ℕ ⟼ L (i (j)))) \leq voln* (X) (A) +_{𝑒} E\}$
40		fvex	$⊢ C (A) \in V$
41	40	rabex	$⊢ \{i \in C (A) \| sum^((j \in ℕ ⟼ L (i (j)))) \leq voln* (X) (A) +_{𝑒} E\} \in V$
42	41	a1i	$⊢ φ \to \{i \in C (A) \| sum^((j \in ℕ ⟼ L (i (j)))) \leq voln* (X) (A) +_{𝑒} E\} \in V$
43	35 39 3 42	fvmptd	$⊢ φ \to D (A) (E) = \{i \in C (A) \| sum^((j \in ℕ ⟼ L (i (j)))) \leq voln* (X) (A) +_{𝑒} E\}$
44	7 43	eleqtrd	$⊢ φ \to I \in \{i \in C (A) \| sum^((j \in ℕ ⟼ L (i (j)))) \leq voln* (X) (A) +_{𝑒} E\}$
45		fveq1	$⊢ i = I \to i (j) = I (j)$
46	45	fveq2d	$⊢ i = I \to L (i (j)) = L (I (j))$
47	46	mpteq2dv	$⊢ i = I \to (j \in ℕ ⟼ L (i (j))) = (j \in ℕ ⟼ L (I (j)))$
48	47	fveq2d	$⊢ i = I \to sum^((j \in ℕ ⟼ L (i (j)))) = sum^((j \in ℕ ⟼ L (I (j))))$
49	48	breq1d	$⊢ i = I \to (sum^((j \in ℕ ⟼ L (i (j)))) \leq voln* (X) (A) +_{𝑒} E \leftrightarrow sum^((j \in ℕ ⟼ L (I (j)))) \leq voln* (X) (A) +_{𝑒} E)$
50	49	elrab	$⊢ I \in \{i \in C (A) \| sum^((j \in ℕ ⟼ L (i (j)))) \leq voln* (X) (A) +_{𝑒} E\} \leftrightarrow (I \in C (A) \land sum^((j \in ℕ ⟼ L (I (j)))) \leq voln* (X) (A) +_{𝑒} E)$
51	44 50	sylib	$⊢ φ \to (I \in C (A) \land sum^((j \in ℕ ⟼ L (I (j)))) \leq voln* (X) (A) +_{𝑒} E)$
52	51	simpld	$⊢ φ \to I \in C (A)$
53	23 52	sseldd	$⊢ φ \to I \in ({({ℝ^{2}}^{X})}^{ℕ})$
54		elmapi	$⊢ I \in ({({ℝ^{2}}^{X})}^{ℕ}) \to I : ℕ ⟶ {ℝ^{2}}^{X}$
55	53 54	syl	$⊢ φ \to I : ℕ ⟶ {ℝ^{2}}^{X}$
56	55	adantr	$⊢ (φ \land j \in ℕ) \to I : ℕ ⟶ {ℝ^{2}}^{X}$
57		simpr	$⊢ (φ \land j \in ℕ) \to j \in ℕ$
58	56 57	ffvelrnd	$⊢ (φ \land j \in ℕ) \to I (j) \in ({ℝ^{2}}^{X})$
59		elmapi	$⊢ I (j) \in ({ℝ^{2}}^{X}) \to I (j) : X ⟶ ℝ^{2}$
60	58 59	syl	$⊢ (φ \land j \in ℕ) \to I (j) : X ⟶ ℝ^{2}$
61	60	ffvelrnda	$⊢ ((φ \land j \in ℕ) \land k \in X) \to I (j) (k) \in ℝ^{2}$
62		xp1st	$⊢ I (j) (k) \in ℝ^{2} \to 1^{st} (I (j) (k)) \in ℝ$
63	61 62	syl	$⊢ ((φ \land j \in ℕ) \land k \in X) \to 1^{st} (I (j) (k)) \in ℝ$
64	63	fmpttd	$⊢ (φ \land j \in ℕ) \to (k \in X ⟼ 1^{st} (I (j) (k))) : X ⟶ ℝ$
65		reex	$⊢ ℝ \in V$
66	65	a1i	$⊢ φ \to ℝ \in V$
67		elmapg	$⊢ (ℝ \in V \land X \in Fin) \to ((k \in X ⟼ 1^{st} (I (j) (k))) \in (ℝ^{X}) \leftrightarrow (k \in X ⟼ 1^{st} (I (j) (k))) : X ⟶ ℝ)$
68	66 1 67	syl2anc	$⊢ φ \to ((k \in X ⟼ 1^{st} (I (j) (k))) \in (ℝ^{X}) \leftrightarrow (k \in X ⟼ 1^{st} (I (j) (k))) : X ⟶ ℝ)$
69	68	adantr	$⊢ (φ \land j \in ℕ) \to ((k \in X ⟼ 1^{st} (I (j) (k))) \in (ℝ^{X}) \leftrightarrow (k \in X ⟼ 1^{st} (I (j) (k))) : X ⟶ ℝ)$
70	64 69	mpbird	$⊢ (φ \land j \in ℕ) \to (k \in X ⟼ 1^{st} (I (j) (k))) \in (ℝ^{X})$
71	70	fmpttd	$⊢ φ \to (j \in ℕ ⟼ (k \in X ⟼ 1^{st} (I (j) (k)))) : ℕ ⟶ ℝ^{X}$
72	8	a1i	$⊢ φ \to B = (j \in ℕ ⟼ (k \in X ⟼ 1^{st} (I (j) (k))))$
73	72	feq1d	$⊢ φ \to (B : ℕ ⟶ ℝ^{X} \leftrightarrow (j \in ℕ ⟼ (k \in X ⟼ 1^{st} (I (j) (k)))) : ℕ ⟶ ℝ^{X})$
74	71 73	mpbird	$⊢ φ \to B : ℕ ⟶ ℝ^{X}$
75		xp2nd	$⊢ I (j) (k) \in ℝ^{2} \to 2^{nd} (I (j) (k)) \in ℝ$
76	61 75	syl	$⊢ ((φ \land j \in ℕ) \land k \in X) \to 2^{nd} (I (j) (k)) \in ℝ$
77	76	fmpttd	$⊢ (φ \land j \in ℕ) \to (k \in X ⟼ 2^{nd} (I (j) (k))) : X ⟶ ℝ$
78		elmapg	$⊢ (ℝ \in V \land X \in Fin) \to ((k \in X ⟼ 2^{nd} (I (j) (k))) \in (ℝ^{X}) \leftrightarrow (k \in X ⟼ 2^{nd} (I (j) (k))) : X ⟶ ℝ)$
79	66 1 78	syl2anc	$⊢ φ \to ((k \in X ⟼ 2^{nd} (I (j) (k))) \in (ℝ^{X}) \leftrightarrow (k \in X ⟼ 2^{nd} (I (j) (k))) : X ⟶ ℝ)$
80	79	adantr	$⊢ (φ \land j \in ℕ) \to ((k \in X ⟼ 2^{nd} (I (j) (k))) \in (ℝ^{X}) \leftrightarrow (k \in X ⟼ 2^{nd} (I (j) (k))) : X ⟶ ℝ)$
81	77 80	mpbird	$⊢ (φ \land j \in ℕ) \to (k \in X ⟼ 2^{nd} (I (j) (k))) \in (ℝ^{X})$
82	81	fmpttd	$⊢ φ \to (j \in ℕ ⟼ (k \in X ⟼ 2^{nd} (I (j) (k)))) : ℕ ⟶ ℝ^{X}$
83	9	a1i	$⊢ φ \to T = (j \in ℕ ⟼ (k \in X ⟼ 2^{nd} (I (j) (k))))$
84	83	feq1d	$⊢ φ \to (T : ℕ ⟶ ℝ^{X} \leftrightarrow (j \in ℕ ⟼ (k \in X ⟼ 2^{nd} (I (j) (k)))) : ℕ ⟶ ℝ^{X})$
85	82 84	mpbird	$⊢ φ \to T : ℕ ⟶ ℝ^{X}$
86	74 85	jca	$⊢ φ \to (B : ℕ ⟶ ℝ^{X} \land T : ℕ ⟶ ℝ^{X})$
87	52 20	eleqtrd	$⊢ φ \to I \in \{l \in ({({ℝ^{2}}^{X})}^{ℕ}) \| A \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ l (j)) (k)\}$
88		fveq1	$⊢ l = I \to l (j) = I (j)$
89	88	coeq2d	$⊢ l = I \to [.) \circ l (j) = [.) \circ I (j)$
90	89	fveq1d	$⊢ l = I \to ([.) \circ l (j)) (k) = ([.) \circ I (j)) (k)$
91	90	ixpeq2dv	$⊢ l = I \to \underset{k \in X}{⨉} ([.) \circ l (j)) (k) = \underset{k \in X}{⨉} ([.) \circ I (j)) (k)$
92	91	adantr	$⊢ (l = I \land j \in ℕ) \to \underset{k \in X}{⨉} ([.) \circ l (j)) (k) = \underset{k \in X}{⨉} ([.) \circ I (j)) (k)$
93	92	iuneq2dv	$⊢ l = I \to ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ l (j)) (k) = ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ I (j)) (k)$
94	93	sseq2d	$⊢ l = I \to (A \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ l (j)) (k) \leftrightarrow A \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ I (j)) (k))$
95	94	elrab	$⊢ I \in \{l \in ({({ℝ^{2}}^{X})}^{ℕ}) \| A \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ l (j)) (k)\} \leftrightarrow (I \in ({({ℝ^{2}}^{X})}^{ℕ}) \land A \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ I (j)) (k))$
96	87 95	sylib	$⊢ φ \to (I \in ({({ℝ^{2}}^{X})}^{ℕ}) \land A \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ I (j)) (k))$
97	96	simprd	$⊢ φ \to A \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ I (j)) (k)$
98	60	adantr	$⊢ ((φ \land j \in ℕ) \land k \in X) \to I (j) : X ⟶ ℝ^{2}$
99		simpr	$⊢ ((φ \land j \in ℕ) \land k \in X) \to k \in X$
100	98 99	fvovco	$⊢ ((φ \land j \in ℕ) \land k \in X) \to ([.) \circ I (j)) (k) = [1^{st} (I (j) (k)), 2^{nd} (I (j) (k)))$
101		mptexg	$⊢ X \in Fin \to (k \in X ⟼ 1^{st} (I (j) (k))) \in V$
102	1 101	syl	$⊢ φ \to (k \in X ⟼ 1^{st} (I (j) (k))) \in V$
103	102	adantr	$⊢ (φ \land j \in ℕ) \to (k \in X ⟼ 1^{st} (I (j) (k))) \in V$
104	72 103	fvmpt2d	$⊢ (φ \land j \in ℕ) \to B (j) = (k \in X ⟼ 1^{st} (I (j) (k)))$
105		fvexd	$⊢ ((φ \land j \in ℕ) \land k \in X) \to 1^{st} (I (j) (k)) \in V$
106	104 105	fvmpt2d	$⊢ ((φ \land j \in ℕ) \land k \in X) \to B (j) (k) = 1^{st} (I (j) (k))$
107	106	eqcomd	$⊢ ((φ \land j \in ℕ) \land k \in X) \to 1^{st} (I (j) (k)) = B (j) (k)$
108		mptexg	$⊢ X \in Fin \to (k \in X ⟼ 2^{nd} (I (j) (k))) \in V$
109	1 108	syl	$⊢ φ \to (k \in X ⟼ 2^{nd} (I (j) (k))) \in V$
110	109	adantr	$⊢ (φ \land j \in ℕ) \to (k \in X ⟼ 2^{nd} (I (j) (k))) \in V$
111	83 110	fvmpt2d	$⊢ (φ \land j \in ℕ) \to T (j) = (k \in X ⟼ 2^{nd} (I (j) (k)))$
112		fvexd	$⊢ ((φ \land j \in ℕ) \land k \in X) \to 2^{nd} (I (j) (k)) \in V$
113	111 112	fvmpt2d	$⊢ ((φ \land j \in ℕ) \land k \in X) \to T (j) (k) = 2^{nd} (I (j) (k))$
114	113	eqcomd	$⊢ ((φ \land j \in ℕ) \land k \in X) \to 2^{nd} (I (j) (k)) = T (j) (k)$
115	107 114	oveq12d	$⊢ ((φ \land j \in ℕ) \land k \in X) \to [1^{st} (I (j) (k)), 2^{nd} (I (j) (k))) = [B (j) (k), T (j) (k))$
116	100 115	eqtrd	$⊢ ((φ \land j \in ℕ) \land k \in X) \to ([.) \circ I (j)) (k) = [B (j) (k), T (j) (k))$
117	116	ixpeq2dva	$⊢ (φ \land j \in ℕ) \to \underset{k \in X}{⨉} ([.) \circ I (j)) (k) = \underset{k \in X}{⨉} [B (j) (k), T (j) (k))$
118	117	iuneq2dv	$⊢ φ \to ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ I (j)) (k) = ⋃_{j \in ℕ} \underset{k \in X}{⨉} [B (j) (k), T (j) (k))$
119	97 118	sseqtrd	$⊢ φ \to A \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} [B (j) (k), T (j) (k))$
120	5	a1i	$⊢ (φ \land j \in ℕ) \to L = (h \in ({ℝ^{2}}^{X}) ⟼ \prod_{k \in X} vol (([.) \circ h) (k)))$
121		coeq2	$⊢ h = I (j) \to [.) \circ h = [.) \circ I (j)$
122	121	fveq1d	$⊢ h = I (j) \to ([.) \circ h) (k) = ([.) \circ I (j)) (k)$
123	122	ad2antlr	$⊢ ((φ \land h = I (j)) \land k \in X) \to ([.) \circ h) (k) = ([.) \circ I (j)) (k)$
124	123	adantllr	$⊢ (((φ \land j \in ℕ) \land h = I (j)) \land k \in X) \to ([.) \circ h) (k) = ([.) \circ I (j)) (k)$
125	100	adantlr	$⊢ (((φ \land j \in ℕ) \land h = I (j)) \land k \in X) \to ([.) \circ I (j)) (k) = [1^{st} (I (j) (k)), 2^{nd} (I (j) (k)))$
126	115	adantlr	$⊢ (((φ \land j \in ℕ) \land h = I (j)) \land k \in X) \to [1^{st} (I (j) (k)), 2^{nd} (I (j) (k))) = [B (j) (k), T (j) (k))$
127	124 125 126	3eqtrd	$⊢ (((φ \land j \in ℕ) \land h = I (j)) \land k \in X) \to ([.) \circ h) (k) = [B (j) (k), T (j) (k))$
128	127	fveq2d	$⊢ (((φ \land j \in ℕ) \land h = I (j)) \land k \in X) \to vol (([.) \circ h) (k)) = vol ([B (j) (k), T (j) (k)))$
129	128	prodeq2dv	$⊢ ((φ \land j \in ℕ) \land h = I (j)) \to \prod_{k \in X} vol (([.) \circ h) (k)) = \prod_{k \in X} vol ([B (j) (k), T (j) (k)))$
130	1	adantr	$⊢ (φ \land j \in ℕ) \to X \in Fin$
131	8	fvmpt2	$⊢ (j \in ℕ \land (k \in X ⟼ 1^{st} (I (j) (k))) \in V) \to B (j) = (k \in X ⟼ 1^{st} (I (j) (k)))$
132	57 103 131	syl2anc	$⊢ (φ \land j \in ℕ) \to B (j) = (k \in X ⟼ 1^{st} (I (j) (k)))$
133	132	feq1d	$⊢ (φ \land j \in ℕ) \to (B (j) : X ⟶ ℝ \leftrightarrow (k \in X ⟼ 1^{st} (I (j) (k))) : X ⟶ ℝ)$
134	64 133	mpbird	$⊢ (φ \land j \in ℕ) \to B (j) : X ⟶ ℝ$
135	134	adantr	$⊢ ((φ \land j \in ℕ) \land k \in X) \to B (j) : X ⟶ ℝ$
136	135 99	ffvelrnd	$⊢ ((φ \land j \in ℕ) \land k \in X) \to B (j) (k) \in ℝ$
137	9	fvmpt2	$⊢ (j \in ℕ \land (k \in X ⟼ 2^{nd} (I (j) (k))) \in V) \to T (j) = (k \in X ⟼ 2^{nd} (I (j) (k)))$
138	57 110 137	syl2anc	$⊢ (φ \land j \in ℕ) \to T (j) = (k \in X ⟼ 2^{nd} (I (j) (k)))$
139	138	feq1d	$⊢ (φ \land j \in ℕ) \to (T (j) : X ⟶ ℝ \leftrightarrow (k \in X ⟼ 2^{nd} (I (j) (k))) : X ⟶ ℝ)$
140	77 139	mpbird	$⊢ (φ \land j \in ℕ) \to T (j) : X ⟶ ℝ$
141	140	adantr	$⊢ ((φ \land j \in ℕ) \land k \in X) \to T (j) : X ⟶ ℝ$
142	141 99	ffvelrnd	$⊢ ((φ \land j \in ℕ) \land k \in X) \to T (j) (k) \in ℝ$
143		volicore	$⊢ (B (j) (k) \in ℝ \land T (j) (k) \in ℝ) \to vol ([B (j) (k), T (j) (k))) \in ℝ$
144	136 142 143	syl2anc	$⊢ ((φ \land j \in ℕ) \land k \in X) \to vol ([B (j) (k), T (j) (k))) \in ℝ$
145	130 144	fprodrecl	$⊢ (φ \land j \in ℕ) \to \prod_{k \in X} vol ([B (j) (k), T (j) (k))) \in ℝ$
146	120 129 58 145	fvmptd	$⊢ (φ \land j \in ℕ) \to L (I (j)) = \prod_{k \in X} vol ([B (j) (k), T (j) (k)))$
147	146	eqcomd	$⊢ (φ \land j \in ℕ) \to \prod_{k \in X} vol ([B (j) (k), T (j) (k))) = L (I (j))$
148	147	mpteq2dva	$⊢ φ \to (j \in ℕ ⟼ \prod_{k \in X} vol ([B (j) (k), T (j) (k)))) = (j \in ℕ ⟼ L (I (j)))$
149	148	fveq2d	$⊢ φ \to sum^((j \in ℕ ⟼ \prod_{k \in X} vol ([B (j) (k), T (j) (k))))) = sum^((j \in ℕ ⟼ L (I (j))))$
150	51	simprd	$⊢ φ \to sum^((j \in ℕ ⟼ L (I (j)))) \leq voln* (X) (A) +_{𝑒} E$
151	149 150	eqbrtrd	$⊢ φ \to sum^((j \in ℕ ⟼ \prod_{k \in X} vol ([B (j) (k), T (j) (k))))) \leq voln* (X) (A) +_{𝑒} E$
152	86 119 151	jca31	$⊢ φ \to (((B : ℕ ⟶ ℝ^{X} \land T : ℕ ⟶ ℝ^{X}) \land A \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} [B (j) (k), T (j) (k))) \land sum^((j \in ℕ ⟼ \prod_{k \in X} vol ([B (j) (k), T (j) (k))))) \leq voln* (X) (A) +_{𝑒} E)$

Metamath Proof Explorer

Theorem ovncvr2

Proof