ovolval5lem3

Description: The value of the Lebesgue outer measure for subsets of the reals, using covers of left-closed right-open intervals are used, instead of open intervals. (Contributed by Glauco Siliprandi, 3-Mar-2021)

	Ref	Expression
Hypotheses	ovolval5lem3.m	$⊢ M = \{y \in ℝ^{*} \| \exists f \in ({ℝ^{2}}^{ℕ}) (A \subseteq ⋃ ran ([.) \circ f) \land y = sum^((vol \circ [.)) \circ f))\}$
	ovolval5lem3.q	$⊢ Q = \{z \in ℝ^{*} \| \exists f \in ({ℝ^{2}}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ f) \land z = sum^((vol \circ (.)) \circ f))\}$
Assertion	ovolval5lem3	$⊢ inf (Q ℝ^{} <) = inf (M ℝ^{} <)$

Proof

Step	Hyp	Ref	Expression
1		ovolval5lem3.m	$⊢ M = \{y \in ℝ^{*} \| \exists f \in ({ℝ^{2}}^{ℕ}) (A \subseteq ⋃ ran ([.) \circ f) \land y = sum^((vol \circ [.)) \circ f))\}$
2		ovolval5lem3.q	$⊢ Q = \{z \in ℝ^{*} \| \exists f \in ({ℝ^{2}}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ f) \land z = sum^((vol \circ (.)) \circ f))\}$
3	2	ssrab3	$⊢ Q \subseteq ℝ^{*}$
4		infxrcl	$⊢ Q \subseteq ℝ^{} \to inf (Q ℝ^{} <) \in ℝ^{*}$
5	3 4	mp1i	$⊢ ⊤ \to inf (Q ℝ^{} <) \in ℝ^{}$
6	1	ssrab3	$⊢ M \subseteq ℝ^{*}$
7		infxrcl	$⊢ M \subseteq ℝ^{} \to inf (M ℝ^{} <) \in ℝ^{*}$
8	6 7	mp1i	$⊢ ⊤ \to inf (M ℝ^{} <) \in ℝ^{}$
9	3	a1i	$⊢ ⊤ \to Q \subseteq ℝ^{*}$
10	6	a1i	$⊢ ⊤ \to M \subseteq ℝ^{*}$
11	1	reqabi	$⊢ y \in M \leftrightarrow (y \in ℝ^{*} \land \exists f \in ({ℝ^{2}}^{ℕ}) (A \subseteq ⋃ ran ([.) \circ f) \land y = sum^((vol \circ [.)) \circ f)))$
12	11	simprbi	$⊢ y \in M \to \exists f \in ({ℝ^{2}}^{ℕ}) (A \subseteq ⋃ ran ([.) \circ f) \land y = sum^((vol \circ [.)) \circ f))$
13		coeq2	$⊢ g = f \to (.) \circ g = (.) \circ f$
14	13	rneqd	$⊢ g = f \to ran ((.) \circ g) = ran ((.) \circ f)$
15	14	unieqd	$⊢ g = f \to ⋃ ran ((.) \circ g) = ⋃ ran ((.) \circ f)$
16	15	sseq2d	$⊢ g = f \to (A \subseteq ⋃ ran ((.) \circ g) \leftrightarrow A \subseteq ⋃ ran ((.) \circ f))$
17		coeq2	$⊢ g = f \to (vol \circ (.)) \circ g = (vol \circ (.)) \circ f$
18	17	fveq2d	$⊢ g = f \to sum^((vol \circ (.)) \circ g) = sum^((vol \circ (.)) \circ f)$
19	18	eqeq2d	$⊢ g = f \to (z = sum^((vol \circ (.)) \circ g) \leftrightarrow z = sum^((vol \circ (.)) \circ f))$
20	16 19	anbi12d	$⊢ g = f \to ((A \subseteq ⋃ ran ((.) \circ g) \land z = sum^((vol \circ (.)) \circ g)) \leftrightarrow (A \subseteq ⋃ ran ((.) \circ f) \land z = sum^((vol \circ (.)) \circ f)))$
21	20	cbvrexvw	$⊢ \exists g \in ({ℝ^{2}}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ g) \land z = sum^((vol \circ (.)) \circ g)) \leftrightarrow \exists f \in ({ℝ^{2}}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ f) \land z = sum^((vol \circ (.)) \circ f))$
22	21	rabbii	$⊢ \{z \in ℝ^{} \| \exists g \in ({ℝ^{2}}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ g) \land z = sum^((vol \circ (.)) \circ g))\} = \{z \in ℝ^{} \| \exists f \in ({ℝ^{2}}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ f) \land z = sum^((vol \circ (.)) \circ f))\}$
23	2 22	eqtr4i	$⊢ Q = \{z \in ℝ^{*} \| \exists g \in ({ℝ^{2}}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ g) \land z = sum^((vol \circ (.)) \circ g))\}$
24		simp3r	$⊢ (w \in ℝ^{+} \land f \in ({ℝ^{2}}^{ℕ}) \land (A \subseteq ⋃ ran ([.) \circ f) \land y = sum^((vol \circ [.)) \circ f))) \to y = sum^((vol \circ [.)) \circ f)$
25		eqid	$⊢ sum^((vol \circ (.)) \circ (m \in ℕ ⟼ ⟨1^{st} (f (m)) - (\frac{w}{2^{m}}), 2^{nd} (f (m))⟩)) = sum^((vol \circ (.)) \circ (m \in ℕ ⟼ ⟨1^{st} (f (m)) - (\frac{w}{2^{m}}), 2^{nd} (f (m))⟩))$
26		elmapi	$⊢ f \in ({ℝ^{2}}^{ℕ}) \to f : ℕ ⟶ ℝ^{2}$
27	26	3ad2ant2	$⊢ (w \in ℝ^{+} \land f \in ({ℝ^{2}}^{ℕ}) \land (A \subseteq ⋃ ran ([.) \circ f) \land y = sum^((vol \circ [.)) \circ f))) \to f : ℕ ⟶ ℝ^{2}$
28		simp3l	$⊢ (w \in ℝ^{+} \land f \in ({ℝ^{2}}^{ℕ}) \land (A \subseteq ⋃ ran ([.) \circ f) \land y = sum^((vol \circ [.)) \circ f))) \to A \subseteq ⋃ ran ([.) \circ f)$
29		simp1	$⊢ (w \in ℝ^{+} \land f \in ({ℝ^{2}}^{ℕ}) \land (A \subseteq ⋃ ran ([.) \circ f) \land y = sum^((vol \circ [.)) \circ f))) \to w \in ℝ^{+}$
30		2fveq3	$⊢ m = n \to 1^{st} (f (m)) = 1^{st} (f (n))$
31		oveq2	$⊢ m = n \to 2^{m} = 2^{n}$
32	31	oveq2d	$⊢ m = n \to \frac{w}{2^{m}} = \frac{w}{2^{n}}$
33	30 32	oveq12d	$⊢ m = n \to 1^{st} (f (m)) - (\frac{w}{2^{m}}) = 1^{st} (f (n)) - (\frac{w}{2^{n}})$
34		2fveq3	$⊢ m = n \to 2^{nd} (f (m)) = 2^{nd} (f (n))$
35	33 34	opeq12d	$⊢ m = n \to ⟨1^{st} (f (m)) - (\frac{w}{2^{m}}), 2^{nd} (f (m))⟩ = ⟨1^{st} (f (n)) - (\frac{w}{2^{n}}), 2^{nd} (f (n))⟩$
36	35	cbvmptv	$⊢ (m \in ℕ ⟼ ⟨1^{st} (f (m)) - (\frac{w}{2^{m}}), 2^{nd} (f (m))⟩) = (n \in ℕ ⟼ ⟨1^{st} (f (n)) - (\frac{w}{2^{n}}), 2^{nd} (f (n))⟩)$
37	23 24 25 27 28 29 36	ovolval5lem2	$⊢ (w \in ℝ^{+} \land f \in ({ℝ^{2}}^{ℕ}) \land (A \subseteq ⋃ ran ([.) \circ f) \land y = sum^((vol \circ [.)) \circ f))) \to \exists z \in Q z \leq y +_{𝑒} w$
38	37	rexlimdv3a	$⊢ w \in ℝ^{+} \to (\exists f \in ({ℝ^{2}}^{ℕ}) (A \subseteq ⋃ ran ([.) \circ f) \land y = sum^((vol \circ [.)) \circ f)) \to \exists z \in Q z \leq y +_{𝑒} w)$
39	12 38	mpan9	$⊢ (y \in M \land w \in ℝ^{+}) \to \exists z \in Q z \leq y +_{𝑒} w$
40	39	3adant1	$⊢ (⊤ \land y \in M \land w \in ℝ^{+}) \to \exists z \in Q z \leq y +_{𝑒} w$
41	9 10 40	infleinf	$⊢ ⊤ \to inf (Q ℝ^{} <) \leq inf (M ℝ^{} <)$
42		eqeq1	$⊢ z = y \to (z = sum^((vol \circ (.)) \circ f) \leftrightarrow y = sum^((vol \circ (.)) \circ f))$
43	42	anbi2d	$⊢ z = y \to ((A \subseteq ⋃ ran ((.) \circ f) \land z = sum^((vol \circ (.)) \circ f)) \leftrightarrow (A \subseteq ⋃ ran ((.) \circ f) \land y = sum^((vol \circ (.)) \circ f)))$
44	43	rexbidv	$⊢ z = y \to (\exists f \in ({ℝ^{2}}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ f) \land z = sum^((vol \circ (.)) \circ f)) \leftrightarrow \exists f \in ({ℝ^{2}}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ f) \land y = sum^((vol \circ (.)) \circ f)))$
45	44	cbvrabv	$⊢ \{z \in ℝ^{} \| \exists f \in ({ℝ^{2}}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ f) \land z = sum^((vol \circ (.)) \circ f))\} = \{y \in ℝ^{} \| \exists f \in ({ℝ^{2}}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ f) \land y = sum^((vol \circ (.)) \circ f))\}$
46		simpr	$⊢ (f \in ({ℝ^{2}}^{ℕ}) \land A \subseteq ⋃ ran ((.) \circ f)) \to A \subseteq ⋃ ran ((.) \circ f)$
47		ioossico	$⊢ (1^{st} (f (n)), 2^{nd} (f (n))) \subseteq [1^{st} (f (n)), 2^{nd} (f (n)))$
48	47	a1i	$⊢ (f \in ({ℝ^{2}}^{ℕ}) \land n \in ℕ) \to (1^{st} (f (n)), 2^{nd} (f (n))) \subseteq [1^{st} (f (n)), 2^{nd} (f (n)))$
49	26	adantr	$⊢ (f \in ({ℝ^{2}}^{ℕ}) \land n \in ℕ) \to f : ℕ ⟶ ℝ^{2}$
50		simpr	$⊢ (f \in ({ℝ^{2}}^{ℕ}) \land n \in ℕ) \to n \in ℕ$
51	49 50	fvovco	$⊢ (f \in ({ℝ^{2}}^{ℕ}) \land n \in ℕ) \to ((.) \circ f) (n) = (1^{st} (f (n)), 2^{nd} (f (n)))$
52	49 50	fvovco	$⊢ (f \in ({ℝ^{2}}^{ℕ}) \land n \in ℕ) \to ([.) \circ f) (n) = [1^{st} (f (n)), 2^{nd} (f (n)))$
53	48 51 52	3sstr4d	$⊢ (f \in ({ℝ^{2}}^{ℕ}) \land n \in ℕ) \to ((.) \circ f) (n) \subseteq ([.) \circ f) (n)$
54	53	ralrimiva	$⊢ f \in ({ℝ^{2}}^{ℕ}) \to \forall n \in ℕ ((.) \circ f) (n) \subseteq ([.) \circ f) (n)$
55		ss2iun	$⊢ \forall n \in ℕ ((.) \circ f) (n) \subseteq ([.) \circ f) (n) \to ⋃_{n \in ℕ} ((.) \circ f) (n) \subseteq ⋃_{n \in ℕ} ([.) \circ f) (n)$
56	54 55	syl	$⊢ f \in ({ℝ^{2}}^{ℕ}) \to ⋃_{n \in ℕ} ((.) \circ f) (n) \subseteq ⋃_{n \in ℕ} ([.) \circ f) (n)$
57		ioof	$⊢ (.) : ℝ^{} \times ℝ^{} ⟶ 𝒫 ℝ$
58	57	a1i	$⊢ f \in ({ℝ^{2}}^{ℕ}) \to (.) : ℝ^{} \times ℝ^{} ⟶ 𝒫 ℝ$
59		rexpssxrxp	$⊢ ℝ^{2} \subseteq ℝ^{} \times ℝ^{}$
60	59	a1i	$⊢ f \in ({ℝ^{2}}^{ℕ}) \to ℝ^{2} \subseteq ℝ^{} \times ℝ^{}$
61	58 60 26	fcoss	$⊢ f \in ({ℝ^{2}}^{ℕ}) \to ((.) \circ f) : ℕ ⟶ 𝒫 ℝ$
62	61	ffnd	$⊢ f \in ({ℝ^{2}}^{ℕ}) \to ((.) \circ f) Fn ℕ$
63		fniunfv	$⊢ ((.) \circ f) Fn ℕ \to ⋃_{n \in ℕ} ((.) \circ f) (n) = ⋃ ran ((.) \circ f)$
64	62 63	syl	$⊢ f \in ({ℝ^{2}}^{ℕ}) \to ⋃_{n \in ℕ} ((.) \circ f) (n) = ⋃ ran ((.) \circ f)$
65		icof	$⊢ [.) : ℝ^{} \times ℝ^{} ⟶ 𝒫 ℝ^{*}$
66	65	a1i	$⊢ f \in ({ℝ^{2}}^{ℕ}) \to [.) : ℝ^{} \times ℝ^{} ⟶ 𝒫 ℝ^{*}$
67	66 60 26	fcoss	$⊢ f \in ({ℝ^{2}}^{ℕ}) \to ([.) \circ f) : ℕ ⟶ 𝒫 ℝ^{*}$
68	67	ffnd	$⊢ f \in ({ℝ^{2}}^{ℕ}) \to ([.) \circ f) Fn ℕ$
69		fniunfv	$⊢ ([.) \circ f) Fn ℕ \to ⋃_{n \in ℕ} ([.) \circ f) (n) = ⋃ ran ([.) \circ f)$
70	68 69	syl	$⊢ f \in ({ℝ^{2}}^{ℕ}) \to ⋃_{n \in ℕ} ([.) \circ f) (n) = ⋃ ran ([.) \circ f)$
71	56 64 70	3sstr3d	$⊢ f \in ({ℝ^{2}}^{ℕ}) \to ⋃ ran ((.) \circ f) \subseteq ⋃ ran ([.) \circ f)$
72	71	adantr	$⊢ (f \in ({ℝ^{2}}^{ℕ}) \land A \subseteq ⋃ ran ((.) \circ f)) \to ⋃ ran ((.) \circ f) \subseteq ⋃ ran ([.) \circ f)$
73	46 72	sstrd	$⊢ (f \in ({ℝ^{2}}^{ℕ}) \land A \subseteq ⋃ ran ((.) \circ f)) \to A \subseteq ⋃ ran ([.) \circ f)$
74		simpr	$⊢ (f \in ({ℝ^{2}}^{ℕ}) \land y = sum^((vol \circ (.)) \circ f)) \to y = sum^((vol \circ (.)) \circ f)$
75	26	voliooicof	$⊢ f \in ({ℝ^{2}}^{ℕ}) \to (vol \circ (.)) \circ f = (vol \circ [.)) \circ f$
76	75	fveq2d	$⊢ f \in ({ℝ^{2}}^{ℕ}) \to sum^((vol \circ (.)) \circ f) = sum^((vol \circ [.)) \circ f)$
77	76	adantr	$⊢ (f \in ({ℝ^{2}}^{ℕ}) \land y = sum^((vol \circ (.)) \circ f)) \to sum^((vol \circ (.)) \circ f) = sum^((vol \circ [.)) \circ f)$
78	74 77	eqtrd	$⊢ (f \in ({ℝ^{2}}^{ℕ}) \land y = sum^((vol \circ (.)) \circ f)) \to y = sum^((vol \circ [.)) \circ f)$
79	73 78	anim12dan	$⊢ (f \in ({ℝ^{2}}^{ℕ}) \land (A \subseteq ⋃ ran ((.) \circ f) \land y = sum^((vol \circ (.)) \circ f))) \to (A \subseteq ⋃ ran ([.) \circ f) \land y = sum^((vol \circ [.)) \circ f))$
80	79	ex	$⊢ f \in ({ℝ^{2}}^{ℕ}) \to ((A \subseteq ⋃ ran ((.) \circ f) \land y = sum^((vol \circ (.)) \circ f)) \to (A \subseteq ⋃ ran ([.) \circ f) \land y = sum^((vol \circ [.)) \circ f)))$
81	80	reximia	$⊢ \exists f \in ({ℝ^{2}}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ f) \land y = sum^((vol \circ (.)) \circ f)) \to \exists f \in ({ℝ^{2}}^{ℕ}) (A \subseteq ⋃ ran ([.) \circ f) \land y = sum^((vol \circ [.)) \circ f))$
82	81	a1i	$⊢ y \in ℝ^{*} \to (\exists f \in ({ℝ^{2}}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ f) \land y = sum^((vol \circ (.)) \circ f)) \to \exists f \in ({ℝ^{2}}^{ℕ}) (A \subseteq ⋃ ran ([.) \circ f) \land y = sum^((vol \circ [.)) \circ f)))$
83	82	ss2rabi	$⊢ \{y \in ℝ^{} \| \exists f \in ({ℝ^{2}}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ f) \land y = sum^((vol \circ (.)) \circ f))\} \subseteq \{y \in ℝ^{} \| \exists f \in ({ℝ^{2}}^{ℕ}) (A \subseteq ⋃ ran ([.) \circ f) \land y = sum^((vol \circ [.)) \circ f))\}$
84	45 83	eqsstri	$⊢ \{z \in ℝ^{} \| \exists f \in ({ℝ^{2}}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ f) \land z = sum^((vol \circ (.)) \circ f))\} \subseteq \{y \in ℝ^{} \| \exists f \in ({ℝ^{2}}^{ℕ}) (A \subseteq ⋃ ran ([.) \circ f) \land y = sum^((vol \circ [.)) \circ f))\}$
85	84 2 1	3sstr4i	$⊢ Q \subseteq M$
86		infxrss	$⊢ (Q \subseteq M \land M \subseteq ℝ^{}) \to inf (M ℝ^{} <) \leq inf (Q ℝ^{*} <)$
87	85 6 86	mp2an	$⊢ inf (M ℝ^{} <) \leq inf (Q ℝ^{} <)$
88	87	a1i	$⊢ ⊤ \to inf (M ℝ^{} <) \leq inf (Q ℝ^{} <)$
89	5 8 41 88	xrletrid	$⊢ ⊤ \to inf (Q ℝ^{} <) = inf (M ℝ^{} <)$
90	89	mptru	$⊢ inf (Q ℝ^{} <) = inf (M ℝ^{} <)$

Metamath Proof Explorer

Theorem ovolval5lem3

Proof