ovolval3

Description: The value of the Lebesgue outer measure for subsets of the reals, expressed using sum^ and vol o. (,) . See ovolval and ovolval2 for alternative expressions. (Contributed by Glauco Siliprandi, 3-Mar-2021)

	Ref	Expression
Hypotheses	ovolval3.a	$⊢ φ \to A \subseteq ℝ$
	ovolval3.m	$⊢ M = \{y \in ℝ^{*} \| \exists f \in ({(\leq \cap ℝ^{2})}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ f) \land y = sum^((vol \circ (.)) \circ f))\}$
Assertion	ovolval3	$⊢ φ \to {vol}^{} (A) = inf (M ℝ^{} <)$

Proof

Step	Hyp	Ref	Expression
1		ovolval3.a	$⊢ φ \to A \subseteq ℝ$
2		ovolval3.m	$⊢ M = \{y \in ℝ^{*} \| \exists f \in ({(\leq \cap ℝ^{2})}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ f) \land y = sum^((vol \circ (.)) \circ f))\}$
3		eqid	$⊢ \{y \in ℝ^{} \| \exists f \in ({(\leq \cap ℝ^{2})}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ f) \land y = sum^((abs \circ -) \circ f))\} = \{y \in ℝ^{} \| \exists f \in ({(\leq \cap ℝ^{2})}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ f) \land y = sum^((abs \circ -) \circ f))\}$
4	1 3	ovolval2	$⊢ φ \to {vol}^{} (A) = inf (\{y \in ℝ^{} \| \exists f \in ({(\leq \cap ℝ^{2})}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ f) \land y = sum^((abs \circ -) \circ f))\} ℝ^{*} <)$
5		reex	$⊢ ℝ \in V$
6	5 5	xpex	$⊢ ℝ^{2} \in V$
7		inss2	$⊢ \leq \cap ℝ^{2} \subseteq ℝ^{2}$
8		mapss	$⊢ (ℝ^{2} \in V \land \leq \cap ℝ^{2} \subseteq ℝ^{2}) \to {(\leq \cap ℝ^{2})}^{ℕ} \subseteq {ℝ^{2}}^{ℕ}$
9	6 7 8	mp2an	$⊢ {(\leq \cap ℝ^{2})}^{ℕ} \subseteq {ℝ^{2}}^{ℕ}$
10	9	sseli	$⊢ f \in ({(\leq \cap ℝ^{2})}^{ℕ}) \to f \in ({ℝ^{2}}^{ℕ})$
11		elmapi	$⊢ f \in ({ℝ^{2}}^{ℕ}) \to f : ℕ ⟶ ℝ^{2}$
12	10 11	syl	$⊢ f \in ({(\leq \cap ℝ^{2})}^{ℕ}) \to f : ℕ ⟶ ℝ^{2}$
13	12	ffvelcdmda	$⊢ (f \in ({(\leq \cap ℝ^{2})}^{ℕ}) \land n \in ℕ) \to f (n) \in ℝ^{2}$
14		1st2nd2	$⊢ f (n) \in ℝ^{2} \to f (n) = ⟨1^{st} (f (n)), 2^{nd} (f (n))⟩$
15	13 14	syl	$⊢ (f \in ({(\leq \cap ℝ^{2})}^{ℕ}) \land n \in ℕ) \to f (n) = ⟨1^{st} (f (n)), 2^{nd} (f (n))⟩$
16	15	fveq2d	$⊢ (f \in ({(\leq \cap ℝ^{2})}^{ℕ}) \land n \in ℕ) \to (.) (f (n)) = (.) (⟨1^{st} (f (n)), 2^{nd} (f (n))⟩)$
17		df-ov	$⊢ (1^{st} (f (n)), 2^{nd} (f (n))) = (.) (⟨1^{st} (f (n)), 2^{nd} (f (n))⟩)$
18	17	eqcomi	$⊢ (.) (⟨1^{st} (f (n)), 2^{nd} (f (n))⟩) = (1^{st} (f (n)), 2^{nd} (f (n)))$
19	18	a1i	$⊢ (f \in ({(\leq \cap ℝ^{2})}^{ℕ}) \land n \in ℕ) \to (.) (⟨1^{st} (f (n)), 2^{nd} (f (n))⟩) = (1^{st} (f (n)), 2^{nd} (f (n)))$
20	16 19	eqtrd	$⊢ (f \in ({(\leq \cap ℝ^{2})}^{ℕ}) \land n \in ℕ) \to (.) (f (n)) = (1^{st} (f (n)), 2^{nd} (f (n)))$
21	20	fveq2d	$⊢ (f \in ({(\leq \cap ℝ^{2})}^{ℕ}) \land n \in ℕ) \to vol ((.) (f (n))) = vol ((1^{st} (f (n)), 2^{nd} (f (n))))$
22		xp1st	$⊢ f (n) \in ℝ^{2} \to 1^{st} (f (n)) \in ℝ$
23	13 22	syl	$⊢ (f \in ({(\leq \cap ℝ^{2})}^{ℕ}) \land n \in ℕ) \to 1^{st} (f (n)) \in ℝ$
24		xp2nd	$⊢ f (n) \in ℝ^{2} \to 2^{nd} (f (n)) \in ℝ$
25	13 24	syl	$⊢ (f \in ({(\leq \cap ℝ^{2})}^{ℕ}) \land n \in ℕ) \to 2^{nd} (f (n)) \in ℝ$
26		elmapi	$⊢ f \in ({(\leq \cap ℝ^{2})}^{ℕ}) \to f : ℕ ⟶ \leq \cap ℝ^{2}$
27	26	adantr	$⊢ (f \in ({(\leq \cap ℝ^{2})}^{ℕ}) \land n \in ℕ) \to f : ℕ ⟶ \leq \cap ℝ^{2}$
28		simpr	$⊢ (f \in ({(\leq \cap ℝ^{2})}^{ℕ}) \land n \in ℕ) \to n \in ℕ$
29		ovolfcl	$⊢ (f : ℕ ⟶ \leq \cap ℝ^{2} \land n \in ℕ) \to (1^{st} (f (n)) \in ℝ \land 2^{nd} (f (n)) \in ℝ \land 1^{st} (f (n)) \leq 2^{nd} (f (n)))$
30	27 28 29	syl2anc	$⊢ (f \in ({(\leq \cap ℝ^{2})}^{ℕ}) \land n \in ℕ) \to (1^{st} (f (n)) \in ℝ \land 2^{nd} (f (n)) \in ℝ \land 1^{st} (f (n)) \leq 2^{nd} (f (n)))$
31	30	simp3d	$⊢ (f \in ({(\leq \cap ℝ^{2})}^{ℕ}) \land n \in ℕ) \to 1^{st} (f (n)) \leq 2^{nd} (f (n))$
32		volioo	$⊢ (1^{st} (f (n)) \in ℝ \land 2^{nd} (f (n)) \in ℝ \land 1^{st} (f (n)) \leq 2^{nd} (f (n))) \to vol ((1^{st} (f (n)), 2^{nd} (f (n)))) = 2^{nd} (f (n)) - 1^{st} (f (n))$
33	23 25 31 32	syl3anc	$⊢ (f \in ({(\leq \cap ℝ^{2})}^{ℕ}) \land n \in ℕ) \to vol ((1^{st} (f (n)), 2^{nd} (f (n)))) = 2^{nd} (f (n)) - 1^{st} (f (n))$
34	21 33	eqtrd	$⊢ (f \in ({(\leq \cap ℝ^{2})}^{ℕ}) \land n \in ℕ) \to vol ((.) (f (n))) = 2^{nd} (f (n)) - 1^{st} (f (n))$
35		ioof	$⊢ (.) : ℝ^{} \times ℝ^{} ⟶ 𝒫 ℝ$
36		ffun	$⊢ (.) : ℝ^{} \times ℝ^{} ⟶ 𝒫 ℝ \to Fun (.)$
37	35 36	ax-mp	$⊢ Fun (.)$
38	37	a1i	$⊢ (f \in ({(\leq \cap ℝ^{2})}^{ℕ}) \land n \in ℕ) \to Fun (.)$
39		rexpssxrxp	$⊢ ℝ^{2} \subseteq ℝ^{} \times ℝ^{}$
40	39 13	sselid	$⊢ (f \in ({(\leq \cap ℝ^{2})}^{ℕ}) \land n \in ℕ) \to f (n) \in (ℝ^{} \times ℝ^{})$
41	35	fdmi	$⊢ dom (.) = ℝ^{} \times ℝ^{}$
42	41	eqcomi	$⊢ ℝ^{} \times ℝ^{} = dom (.)$
43	42	a1i	$⊢ (f \in ({(\leq \cap ℝ^{2})}^{ℕ}) \land n \in ℕ) \to ℝ^{} \times ℝ^{} = dom (.)$
44	40 43	eleqtrd	$⊢ (f \in ({(\leq \cap ℝ^{2})}^{ℕ}) \land n \in ℕ) \to f (n) \in dom (.)$
45		fvco	$⊢ (Fun (.) \land f (n) \in dom (.)) \to (vol \circ (.)) (f (n)) = vol ((.) (f (n)))$
46	38 44 45	syl2anc	$⊢ (f \in ({(\leq \cap ℝ^{2})}^{ℕ}) \land n \in ℕ) \to (vol \circ (.)) (f (n)) = vol ((.) (f (n)))$
47	15	fveq2d	$⊢ (f \in ({(\leq \cap ℝ^{2})}^{ℕ}) \land n \in ℕ) \to (abs \circ -) (f (n)) = (abs \circ -) (⟨1^{st} (f (n)), 2^{nd} (f (n))⟩)$
48		df-ov	$⊢ 1^{st} (f (n)) (abs \circ -) 2^{nd} (f (n)) = (abs \circ -) (⟨1^{st} (f (n)), 2^{nd} (f (n))⟩)$
49	48	eqcomi	$⊢ (abs \circ -) (⟨1^{st} (f (n)), 2^{nd} (f (n))⟩) = 1^{st} (f (n)) (abs \circ -) 2^{nd} (f (n))$
50	49	a1i	$⊢ (f \in ({(\leq \cap ℝ^{2})}^{ℕ}) \land n \in ℕ) \to (abs \circ -) (⟨1^{st} (f (n)), 2^{nd} (f (n))⟩) = 1^{st} (f (n)) (abs \circ -) 2^{nd} (f (n))$
51	23	recnd	$⊢ (f \in ({(\leq \cap ℝ^{2})}^{ℕ}) \land n \in ℕ) \to 1^{st} (f (n)) \in ℂ$
52	25	recnd	$⊢ (f \in ({(\leq \cap ℝ^{2})}^{ℕ}) \land n \in ℕ) \to 2^{nd} (f (n)) \in ℂ$
53		eqid	$⊢ abs \circ - = abs \circ -$
54	53	cnmetdval	$⊢ (1^{st} (f (n)) \in ℂ \land 2^{nd} (f (n)) \in ℂ) \to 1^{st} (f (n)) (abs \circ -) 2^{nd} (f (n)) = \|1^{st} (f (n)) - 2^{nd} (f (n))\|$
55	51 52 54	syl2anc	$⊢ (f \in ({(\leq \cap ℝ^{2})}^{ℕ}) \land n \in ℕ) \to 1^{st} (f (n)) (abs \circ -) 2^{nd} (f (n)) = \|1^{st} (f (n)) - 2^{nd} (f (n))\|$
56		abssub	$⊢ (1^{st} (f (n)) \in ℂ \land 2^{nd} (f (n)) \in ℂ) \to \|1^{st} (f (n)) - 2^{nd} (f (n))\| = \|2^{nd} (f (n)) - 1^{st} (f (n))\|$
57	51 52 56	syl2anc	$⊢ (f \in ({(\leq \cap ℝ^{2})}^{ℕ}) \land n \in ℕ) \to \|1^{st} (f (n)) - 2^{nd} (f (n))\| = \|2^{nd} (f (n)) - 1^{st} (f (n))\|$
58	23 25 31	abssubge0d	$⊢ (f \in ({(\leq \cap ℝ^{2})}^{ℕ}) \land n \in ℕ) \to \|2^{nd} (f (n)) - 1^{st} (f (n))\| = 2^{nd} (f (n)) - 1^{st} (f (n))$
59	55 57 58	3eqtrd	$⊢ (f \in ({(\leq \cap ℝ^{2})}^{ℕ}) \land n \in ℕ) \to 1^{st} (f (n)) (abs \circ -) 2^{nd} (f (n)) = 2^{nd} (f (n)) - 1^{st} (f (n))$
60	47 50 59	3eqtrd	$⊢ (f \in ({(\leq \cap ℝ^{2})}^{ℕ}) \land n \in ℕ) \to (abs \circ -) (f (n)) = 2^{nd} (f (n)) - 1^{st} (f (n))$
61	34 46 60	3eqtr4d	$⊢ (f \in ({(\leq \cap ℝ^{2})}^{ℕ}) \land n \in ℕ) \to (vol \circ (.)) (f (n)) = (abs \circ -) (f (n))$
62	61	mpteq2dva	$⊢ f \in ({(\leq \cap ℝ^{2})}^{ℕ}) \to (n \in ℕ ⟼ (vol \circ (.)) (f (n))) = (n \in ℕ ⟼ (abs \circ -) (f (n)))$
63		volioof	$⊢ (vol \circ (.)) : ℝ^{} \times ℝ^{} ⟶ [0, +∞]$
64	63	a1i	$⊢ f \in ({(\leq \cap ℝ^{2})}^{ℕ}) \to (vol \circ (.)) : ℝ^{} \times ℝ^{} ⟶ [0, +∞]$
65	39	a1i	$⊢ f \in ({(\leq \cap ℝ^{2})}^{ℕ}) \to ℝ^{2} \subseteq ℝ^{} \times ℝ^{}$
66	12 65	fssd	$⊢ f \in ({(\leq \cap ℝ^{2})}^{ℕ}) \to f : ℕ ⟶ ℝ^{} \times ℝ^{}$
67		fcompt	$⊢ ((vol \circ (.)) : ℝ^{} \times ℝ^{} ⟶ [0, +∞] \land f : ℕ ⟶ ℝ^{} \times ℝ^{}) \to (vol \circ (.)) \circ f = (n \in ℕ ⟼ (vol \circ (.)) (f (n)))$
68	64 66 67	syl2anc	$⊢ f \in ({(\leq \cap ℝ^{2})}^{ℕ}) \to (vol \circ (.)) \circ f = (n \in ℕ ⟼ (vol \circ (.)) (f (n)))$
69		absf	$⊢ abs : ℂ ⟶ ℝ$
70		subf	$⊢ - : ℂ \times ℂ ⟶ ℂ$
71		fco	$⊢ (abs : ℂ ⟶ ℝ \land - : ℂ \times ℂ ⟶ ℂ) \to (abs \circ -) : ℂ \times ℂ ⟶ ℝ$
72	69 70 71	mp2an	$⊢ (abs \circ -) : ℂ \times ℂ ⟶ ℝ$
73	72	a1i	$⊢ f \in ({(\leq \cap ℝ^{2})}^{ℕ}) \to (abs \circ -) : ℂ \times ℂ ⟶ ℝ$
74		rr2sscn2	$⊢ ℝ^{2} \subseteq ℂ \times ℂ$
75	74	a1i	$⊢ f \in ({(\leq \cap ℝ^{2})}^{ℕ}) \to ℝ^{2} \subseteq ℂ \times ℂ$
76	12 75	fssd	$⊢ f \in ({(\leq \cap ℝ^{2})}^{ℕ}) \to f : ℕ ⟶ ℂ \times ℂ$
77		fcompt	$⊢ ((abs \circ -) : ℂ \times ℂ ⟶ ℝ \land f : ℕ ⟶ ℂ \times ℂ) \to (abs \circ -) \circ f = (n \in ℕ ⟼ (abs \circ -) (f (n)))$
78	73 76 77	syl2anc	$⊢ f \in ({(\leq \cap ℝ^{2})}^{ℕ}) \to (abs \circ -) \circ f = (n \in ℕ ⟼ (abs \circ -) (f (n)))$
79	62 68 78	3eqtr4d	$⊢ f \in ({(\leq \cap ℝ^{2})}^{ℕ}) \to (vol \circ (.)) \circ f = (abs \circ -) \circ f$
80	79	fveq2d	$⊢ f \in ({(\leq \cap ℝ^{2})}^{ℕ}) \to sum^((vol \circ (.)) \circ f) = sum^((abs \circ -) \circ f)$
81	80	eqeq2d	$⊢ f \in ({(\leq \cap ℝ^{2})}^{ℕ}) \to (y = sum^((vol \circ (.)) \circ f) \leftrightarrow y = sum^((abs \circ -) \circ f))$
82	81	anbi2d	$⊢ f \in ({(\leq \cap ℝ^{2})}^{ℕ}) \to ((A \subseteq ⋃ ran ((.) \circ f) \land y = sum^((vol \circ (.)) \circ f)) \leftrightarrow (A \subseteq ⋃ ran ((.) \circ f) \land y = sum^((abs \circ -) \circ f)))$
83	82	rexbiia	$⊢ \exists f \in ({(\leq \cap ℝ^{2})}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ f) \land y = sum^((vol \circ (.)) \circ f)) \leftrightarrow \exists f \in ({(\leq \cap ℝ^{2})}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ f) \land y = sum^((abs \circ -) \circ f))$
84	83	rabbii	$⊢ \{y \in ℝ^{} \| \exists f \in ({(\leq \cap ℝ^{2})}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ f) \land y = sum^((vol \circ (.)) \circ f))\} = \{y \in ℝ^{} \| \exists f \in ({(\leq \cap ℝ^{2})}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ f) \land y = sum^((abs \circ -) \circ f))\}$
85	2 84	eqtr2i	$⊢ \{y \in ℝ^{*} \| \exists f \in ({(\leq \cap ℝ^{2})}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ f) \land y = sum^((abs \circ -) \circ f))\} = M$
86	85	infeq1i	$⊢ inf (\{y \in ℝ^{} \| \exists f \in ({(\leq \cap ℝ^{2})}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ f) \land y = sum^((abs \circ -) \circ f))\} ℝ^{} <) = inf (M ℝ^{*} <)$
87	86	a1i	$⊢ φ \to inf (\{y \in ℝ^{} \| \exists f \in ({(\leq \cap ℝ^{2})}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ f) \land y = sum^((abs \circ -) \circ f))\} ℝ^{} <) = inf (M ℝ^{*} <)$
88	4 87	eqtrd	$⊢ φ \to {vol}^{} (A) = inf (M ℝ^{} <)$

Metamath Proof Explorer

Theorem ovolval3

Proof