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	⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
	ovolval2.m	⊢ 𝑀 = { 𝑦 ∈ ℝ^* ∣ ∃ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = ( Σ^{^} ‘ ( ( abs ∘ − ) ∘ 𝑓 ) ) ) }
Assertion	ovolval2	⊢ ( 𝜑 → ( vol* ‘ 𝐴 ) = inf ( 𝑀 , ℝ^* , < ) )

Proof

Step	Hyp	Ref	Expression
1		ovolval2.a	⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
2		ovolval2.m	⊢ 𝑀 = { 𝑦 ∈ ℝ^* ∣ ∃ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = ( Σ^{^} ‘ ( ( abs ∘ − ) ∘ 𝑓 ) ) ) }
3		eqid	⊢ { 𝑦 ∈ ℝ^* ∣ ∃ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ^* , < ) ) } = { 𝑦 ∈ ℝ^* ∣ ∃ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ^* , < ) ) }
4	3	ovolval	⊢ ( 𝐴 ⊆ ℝ → ( vol* ‘ 𝐴 ) = inf ( { 𝑦 ∈ ℝ^* ∣ ∃ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ^* , < ) ) } , ℝ^* , < ) )
5	1 4	syl	⊢ ( 𝜑 → ( vol* ‘ 𝐴 ) = inf ( { 𝑦 ∈ ℝ^* ∣ ∃ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ^* , < ) ) } , ℝ^* , < ) )
6	3	a1i	⊢ ( 𝜑 → { 𝑦 ∈ ℝ^* ∣ ∃ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ^* , < ) ) } = { 𝑦 ∈ ℝ^* ∣ ∃ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ^* , < ) ) } )
7		reex	⊢ ℝ ∈ V
8	7 7	xpex	⊢ ( ℝ × ℝ ) ∈ V
9		inss2	⊢ ( ≤ ∩ ( ℝ × ℝ ) ) ⊆ ( ℝ × ℝ )
10		mapss	⊢ ( ( ( ℝ × ℝ ) ∈ V ∧ ( ≤ ∩ ( ℝ × ℝ ) ) ⊆ ( ℝ × ℝ ) ) → ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ⊆ ( ( ℝ × ℝ ) ↑_m ℕ ) )
11	8 9 10	mp2an	⊢ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ⊆ ( ( ℝ × ℝ ) ↑_m ℕ )
12	11	sseli	⊢ ( 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) → 𝑓 ∈ ( ( ℝ × ℝ ) ↑_m ℕ ) )
13		1zzd	⊢ ( 𝑓 ∈ ( ( ℝ × ℝ ) ↑_m ℕ ) → 1 ∈ ℤ )
14	12 13	syl	⊢ ( 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) → 1 ∈ ℤ )
15	14	adantl	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ) → 1 ∈ ℤ )
16		nnuz	⊢ ℕ = ( ℤ_≥ ‘ 1 )
17		absfico	⊢ abs : ℂ ⟶ ( 0 [,) +∞ )
18		subf	⊢ − : ( ℂ × ℂ ) ⟶ ℂ
19		fco	⊢ ( ( abs : ℂ ⟶ ( 0 [,) +∞ ) ∧ − : ( ℂ × ℂ ) ⟶ ℂ ) → ( abs ∘ − ) : ( ℂ × ℂ ) ⟶ ( 0 [,) +∞ ) )
20	17 18 19	mp2an	⊢ ( abs ∘ − ) : ( ℂ × ℂ ) ⟶ ( 0 [,) +∞ )
21	20	a1i	⊢ ( 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) → ( abs ∘ − ) : ( ℂ × ℂ ) ⟶ ( 0 [,) +∞ ) )
22		rr2sscn2	⊢ ( ℝ × ℝ ) ⊆ ( ℂ × ℂ )
23	22	a1i	⊢ ( 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) → ( ℝ × ℝ ) ⊆ ( ℂ × ℂ ) )
24		elmapi	⊢ ( 𝑓 ∈ ( ( ℝ × ℝ ) ↑_m ℕ ) → 𝑓 : ℕ ⟶ ( ℝ × ℝ ) )
25	12 24	syl	⊢ ( 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) → 𝑓 : ℕ ⟶ ( ℝ × ℝ ) )
26	21 23 25	fcoss	⊢ ( 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) → ( ( abs ∘ − ) ∘ 𝑓 ) : ℕ ⟶ ( 0 [,) +∞ ) )
27	26	adantl	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ) → ( ( abs ∘ − ) ∘ 𝑓 ) : ℕ ⟶ ( 0 [,) +∞ ) )
28		eqid	⊢ seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) = seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) )
29	15 16 27 28	sge0seq	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ) → ( Σ^{^} ‘ ( ( abs ∘ − ) ∘ 𝑓 ) ) = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ^* , < ) )
30	29	eqcomd	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ) → sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ^* , < ) = ( Σ^{^} ‘ ( ( abs ∘ − ) ∘ 𝑓 ) ) )
31	30	eqeq2d	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ) → ( 𝑦 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ^* , < ) ↔ 𝑦 = ( Σ^{^} ‘ ( ( abs ∘ − ) ∘ 𝑓 ) ) ) )
32	31	anbi2d	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ) → ( ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ^* , < ) ) ↔ ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = ( Σ^{^} ‘ ( ( abs ∘ − ) ∘ 𝑓 ) ) ) ) )
33	32	rexbidva	⊢ ( 𝜑 → ( ∃ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ^* , < ) ) ↔ ∃ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = ( Σ^{^} ‘ ( ( abs ∘ − ) ∘ 𝑓 ) ) ) ) )
34	33	rabbidv	⊢ ( 𝜑 → { 𝑦 ∈ ℝ^* ∣ ∃ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ^* , < ) ) } = { 𝑦 ∈ ℝ^* ∣ ∃ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = ( Σ^{^} ‘ ( ( abs ∘ − ) ∘ 𝑓 ) ) ) } )
35	2	eqcomi	⊢ { 𝑦 ∈ ℝ^* ∣ ∃ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = ( Σ^{^} ‘ ( ( abs ∘ − ) ∘ 𝑓 ) ) ) } = 𝑀
36	35	a1i	⊢ ( 𝜑 → { 𝑦 ∈ ℝ^* ∣ ∃ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = ( Σ^{^} ‘ ( ( abs ∘ − ) ∘ 𝑓 ) ) ) } = 𝑀 )
37	6 34 36	3eqtrd	⊢ ( 𝜑 → { 𝑦 ∈ ℝ^* ∣ ∃ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ^* , < ) ) } = 𝑀 )
38	37	infeq1d	⊢ ( 𝜑 → inf ( { 𝑦 ∈ ℝ^* ∣ ∃ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ^* , < ) ) } , ℝ^* , < ) = inf ( 𝑀 , ℝ^* , < ) )
39	5 38	eqtrd	⊢ ( 𝜑 → ( vol* ‘ 𝐴 ) = inf ( 𝑀 , ℝ^* , < ) )

Metamath Proof Explorer

Theorem ovolval2

Proof