ovolval2

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

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

Proof

Step	Hyp	Ref	Expression
1		ovolval2.a	$⊢ φ \to A \subseteq ℝ$
2		ovolval2.m	$⊢ M = \{y \in ℝ^{*} \| \exists f \in ({(\leq \cap ℝ^{2})}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ f) \land y = sum^((abs \circ -) \circ f))\}$
3		eqid	$⊢ \{y \in ℝ^{} \| \exists f \in ({(\leq \cap ℝ^{2})}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ f) \land y = sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <))\} = \{y \in ℝ^{} \| \exists f \in ({(\leq \cap ℝ^{2})}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ f) \land y = sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <))\}$
4	3	ovolval	$⊢ A \subseteq ℝ \to {vol}^{} (A) = inf (\{y \in ℝ^{} \| \exists f \in ({(\leq \cap ℝ^{2})}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ f) \land y = sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <))\} ℝ^{} <)$
5	1 4	syl	$⊢ φ \to {vol}^{} (A) = inf (\{y \in ℝ^{} \| \exists f \in ({(\leq \cap ℝ^{2})}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ f) \land y = sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <))\} ℝ^{} <)$
6	3	a1i	$⊢ φ \to \{y \in ℝ^{} \| \exists f \in ({(\leq \cap ℝ^{2})}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ f) \land y = sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <))\} = \{y \in ℝ^{} \| \exists f \in ({(\leq \cap ℝ^{2})}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ f) \land y = sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <))\}$
7		reex	$⊢ ℝ \in V$
8	7 7	xpex	$⊢ ℝ^{2} \in V$
9		inss2	$⊢ \leq \cap ℝ^{2} \subseteq ℝ^{2}$
10		mapss	$⊢ (ℝ^{2} \in V \land \leq \cap ℝ^{2} \subseteq ℝ^{2}) \to {(\leq \cap ℝ^{2})}^{ℕ} \subseteq {ℝ^{2}}^{ℕ}$
11	8 9 10	mp2an	$⊢ {(\leq \cap ℝ^{2})}^{ℕ} \subseteq {ℝ^{2}}^{ℕ}$
12	11	sseli	$⊢ f \in ({(\leq \cap ℝ^{2})}^{ℕ}) \to f \in ({ℝ^{2}}^{ℕ})$
13		1zzd	$⊢ f \in ({ℝ^{2}}^{ℕ}) \to 1 \in ℤ$
14	12 13	syl	$⊢ f \in ({(\leq \cap ℝ^{2})}^{ℕ}) \to 1 \in ℤ$
15	14	adantl	$⊢ (φ \land f \in ({(\leq \cap ℝ^{2})}^{ℕ})) \to 1 \in ℤ$
16		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
17		absfico	$⊢ abs : ℂ ⟶ [0, +∞)$
18		subf	$⊢ - : ℂ \times ℂ ⟶ ℂ$
19		fco	$⊢ (abs : ℂ ⟶ [0, +∞) \land - : ℂ \times ℂ ⟶ ℂ) \to (abs \circ -) : ℂ \times ℂ ⟶ [0, +∞)$
20	17 18 19	mp2an	$⊢ (abs \circ -) : ℂ \times ℂ ⟶ [0, +∞)$
21	20	a1i	$⊢ f \in ({(\leq \cap ℝ^{2})}^{ℕ}) \to (abs \circ -) : ℂ \times ℂ ⟶ [0, +∞)$
22		rr2sscn2	$⊢ ℝ^{2} \subseteq ℂ \times ℂ$
23	22	a1i	$⊢ f \in ({(\leq \cap ℝ^{2})}^{ℕ}) \to ℝ^{2} \subseteq ℂ \times ℂ$
24		elmapi	$⊢ f \in ({ℝ^{2}}^{ℕ}) \to f : ℕ ⟶ ℝ^{2}$
25	12 24	syl	$⊢ f \in ({(\leq \cap ℝ^{2})}^{ℕ}) \to f : ℕ ⟶ ℝ^{2}$
26	21 23 25	fcoss	$⊢ f \in ({(\leq \cap ℝ^{2})}^{ℕ}) \to ((abs \circ -) \circ f) : ℕ ⟶ [0, +∞)$
27	26	adantl	$⊢ (φ \land f \in ({(\leq \cap ℝ^{2})}^{ℕ})) \to ((abs \circ -) \circ f) : ℕ ⟶ [0, +∞)$
28		eqid	$⊢ seq 1 (+ ((abs \circ -) \circ f)) = seq 1 (+ ((abs \circ -) \circ f))$
29	15 16 27 28	sge0seq	$⊢ (φ \land f \in ({(\leq \cap ℝ^{2})}^{ℕ})) \to sum^((abs \circ -) \circ f) = sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{*} <)$
30	29	eqcomd	$⊢ (φ \land f \in ({(\leq \cap ℝ^{2})}^{ℕ})) \to sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{*} <) = sum^((abs \circ -) \circ f)$
31	30	eqeq2d	$⊢ (φ \land f \in ({(\leq \cap ℝ^{2})}^{ℕ})) \to (y = sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{*} <) \leftrightarrow y = sum^((abs \circ -) \circ f))$
32	31	anbi2d	$⊢ (φ \land f \in ({(\leq \cap ℝ^{2})}^{ℕ})) \to ((A \subseteq ⋃ ran ((.) \circ f) \land y = sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{*} <)) \leftrightarrow (A \subseteq ⋃ ran ((.) \circ f) \land y = sum^((abs \circ -) \circ f)))$
33	32	rexbidva	$⊢ φ \to (\exists f \in ({(\leq \cap ℝ^{2})}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ f) \land y = sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{*} <)) \leftrightarrow \exists f \in ({(\leq \cap ℝ^{2})}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ f) \land y = sum^((abs \circ -) \circ f)))$
34	33	rabbidv	$⊢ φ \to \{y \in ℝ^{} \| \exists f \in ({(\leq \cap ℝ^{2})}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ f) \land y = sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <))\} = \{y \in ℝ^{*} \| \exists f \in ({(\leq \cap ℝ^{2})}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ f) \land y = sum^((abs \circ -) \circ f))\}$
35	2	eqcomi	$⊢ \{y \in ℝ^{*} \| \exists f \in ({(\leq \cap ℝ^{2})}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ f) \land y = sum^((abs \circ -) \circ f))\} = M$
36	35	a1i	$⊢ φ \to \{y \in ℝ^{*} \| \exists f \in ({(\leq \cap ℝ^{2})}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ f) \land y = sum^((abs \circ -) \circ f))\} = M$
37	6 34 36	3eqtrd	$⊢ φ \to \{y \in ℝ^{} \| \exists f \in ({(\leq \cap ℝ^{2})}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ f) \land y = sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <))\} = M$
38	37	infeq1d	$⊢ φ \to inf (\{y \in ℝ^{} \| \exists f \in ({(\leq \cap ℝ^{2})}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ f) \land y = sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <))\} ℝ^{} <) = inf (M ℝ^{} <)$
39	5 38	eqtrd	$⊢ φ \to {vol}^{} (A) = inf (M ℝ^{} <)$

Metamath Proof Explorer

Theorem ovolval2

Proof