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

Proof

Step	Hyp	Ref	Expression
1		ovolval3.a	⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
2		ovolval3.m	⊢ 𝑀 = { 𝑦 ∈ ℝ^* ∣ ∃ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = ( Σ^{^} ‘ ( ( vol ∘ (,) ) ∘ 𝑓 ) ) ) }
3		eqid	⊢ { 𝑦 ∈ ℝ^* ∣ ∃ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = ( Σ^{^} ‘ ( ( abs ∘ − ) ∘ 𝑓 ) ) ) } = { 𝑦 ∈ ℝ^* ∣ ∃ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = ( Σ^{^} ‘ ( ( abs ∘ − ) ∘ 𝑓 ) ) ) }
4	1 3	ovolval2	⊢ ( 𝜑 → ( vol* ‘ 𝐴 ) = inf ( { 𝑦 ∈ ℝ^* ∣ ∃ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = ( Σ^{^} ‘ ( ( abs ∘ − ) ∘ 𝑓 ) ) ) } , ℝ^* , < ) )
5		reex	⊢ ℝ ∈ V
6	5 5	xpex	⊢ ( ℝ × ℝ ) ∈ V
7		inss2	⊢ ( ≤ ∩ ( ℝ × ℝ ) ) ⊆ ( ℝ × ℝ )
8		mapss	⊢ ( ( ( ℝ × ℝ ) ∈ V ∧ ( ≤ ∩ ( ℝ × ℝ ) ) ⊆ ( ℝ × ℝ ) ) → ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ⊆ ( ( ℝ × ℝ ) ↑_m ℕ ) )
9	6 7 8	mp2an	⊢ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ⊆ ( ( ℝ × ℝ ) ↑_m ℕ )
10	9	sseli	⊢ ( 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) → 𝑓 ∈ ( ( ℝ × ℝ ) ↑_m ℕ ) )
11		elmapi	⊢ ( 𝑓 ∈ ( ( ℝ × ℝ ) ↑_m ℕ ) → 𝑓 : ℕ ⟶ ( ℝ × ℝ ) )
12	10 11	syl	⊢ ( 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) → 𝑓 : ℕ ⟶ ( ℝ × ℝ ) )
13	12	ffvelrnda	⊢ ( ( 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ∧ 𝑛 ∈ ℕ ) → ( 𝑓 ‘ 𝑛 ) ∈ ( ℝ × ℝ ) )
14		1st2nd2	⊢ ( ( 𝑓 ‘ 𝑛 ) ∈ ( ℝ × ℝ ) → ( 𝑓 ‘ 𝑛 ) = ⟨ ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) , ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) ⟩ )
15	13 14	syl	⊢ ( ( 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ∧ 𝑛 ∈ ℕ ) → ( 𝑓 ‘ 𝑛 ) = ⟨ ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) , ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) ⟩ )
16	15	fveq2d	⊢ ( ( 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ∧ 𝑛 ∈ ℕ ) → ( (,) ‘ ( 𝑓 ‘ 𝑛 ) ) = ( (,) ‘ ⟨ ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) , ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) ⟩ ) )
17		df-ov	⊢ ( ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) (,) ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) ) = ( (,) ‘ ⟨ ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) , ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) ⟩ )
18	17	eqcomi	⊢ ( (,) ‘ ⟨ ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) , ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) ⟩ ) = ( ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) (,) ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) )
19	18	a1i	⊢ ( ( 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ∧ 𝑛 ∈ ℕ ) → ( (,) ‘ ⟨ ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) , ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) ⟩ ) = ( ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) (,) ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) ) )
20	16 19	eqtrd	⊢ ( ( 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ∧ 𝑛 ∈ ℕ ) → ( (,) ‘ ( 𝑓 ‘ 𝑛 ) ) = ( ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) (,) ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) ) )
21	20	fveq2d	⊢ ( ( 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ∧ 𝑛 ∈ ℕ ) → ( vol ‘ ( (,) ‘ ( 𝑓 ‘ 𝑛 ) ) ) = ( vol ‘ ( ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) (,) ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) ) ) )
22		xp1st	⊢ ( ( 𝑓 ‘ 𝑛 ) ∈ ( ℝ × ℝ ) → ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ∈ ℝ )
23	13 22	syl	⊢ ( ( 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ∧ 𝑛 ∈ ℕ ) → ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ∈ ℝ )
24		xp2nd	⊢ ( ( 𝑓 ‘ 𝑛 ) ∈ ( ℝ × ℝ ) → ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) ∈ ℝ )
25	13 24	syl	⊢ ( ( 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ∧ 𝑛 ∈ ℕ ) → ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) ∈ ℝ )
26		elmapi	⊢ ( 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) → 𝑓 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) )
27	26	adantr	⊢ ( ( 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ∧ 𝑛 ∈ ℕ ) → 𝑓 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) )
28		simpr	⊢ ( ( 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ∧ 𝑛 ∈ ℕ ) → 𝑛 ∈ ℕ )
29		ovolfcl	⊢ ( ( 𝑓 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑛 ∈ ℕ ) → ( ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ∈ ℝ ∧ ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) ∈ ℝ ∧ ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ≤ ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) ) )
30	27 28 29	syl2anc	⊢ ( ( 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ∧ 𝑛 ∈ ℕ ) → ( ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ∈ ℝ ∧ ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) ∈ ℝ ∧ ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ≤ ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) ) )
31	30	simp3d	⊢ ( ( 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ∧ 𝑛 ∈ ℕ ) → ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ≤ ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) )
32		volioo	⊢ ( ( ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ∈ ℝ ∧ ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) ∈ ℝ ∧ ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ≤ ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) ) → ( vol ‘ ( ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) (,) ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) ) ) = ( ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) − ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ) )
33	23 25 31 32	syl3anc	⊢ ( ( 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ∧ 𝑛 ∈ ℕ ) → ( vol ‘ ( ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) (,) ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) ) ) = ( ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) − ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ) )
34	21 33	eqtrd	⊢ ( ( 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ∧ 𝑛 ∈ ℕ ) → ( vol ‘ ( (,) ‘ ( 𝑓 ‘ 𝑛 ) ) ) = ( ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) − ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ) )
35		ioof	⊢ (,) : ( ℝ^* × ℝ^* ) ⟶ 𝒫 ℝ
36		ffun	⊢ ( (,) : ( ℝ^* × ℝ^* ) ⟶ 𝒫 ℝ → Fun (,) )
37	35 36	ax-mp	⊢ Fun (,)
38	37	a1i	⊢ ( ( 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ∧ 𝑛 ∈ ℕ ) → Fun (,) )
39		rexpssxrxp	⊢ ( ℝ × ℝ ) ⊆ ( ℝ^* × ℝ^* )
40	39 13	sselid	⊢ ( ( 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ∧ 𝑛 ∈ ℕ ) → ( 𝑓 ‘ 𝑛 ) ∈ ( ℝ^* × ℝ^* ) )
41	35	fdmi	⊢ dom (,) = ( ℝ^* × ℝ^* )
42	41	eqcomi	⊢ ( ℝ^* × ℝ^* ) = dom (,)
43	42	a1i	⊢ ( ( 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ∧ 𝑛 ∈ ℕ ) → ( ℝ^* × ℝ^* ) = dom (,) )
44	40 43	eleqtrd	⊢ ( ( 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ∧ 𝑛 ∈ ℕ ) → ( 𝑓 ‘ 𝑛 ) ∈ dom (,) )
45		fvco	⊢ ( ( Fun (,) ∧ ( 𝑓 ‘ 𝑛 ) ∈ dom (,) ) → ( ( vol ∘ (,) ) ‘ ( 𝑓 ‘ 𝑛 ) ) = ( vol ‘ ( (,) ‘ ( 𝑓 ‘ 𝑛 ) ) ) )
46	38 44 45	syl2anc	⊢ ( ( 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ∧ 𝑛 ∈ ℕ ) → ( ( vol ∘ (,) ) ‘ ( 𝑓 ‘ 𝑛 ) ) = ( vol ‘ ( (,) ‘ ( 𝑓 ‘ 𝑛 ) ) ) )
47	15	fveq2d	⊢ ( ( 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ∧ 𝑛 ∈ ℕ ) → ( ( abs ∘ − ) ‘ ( 𝑓 ‘ 𝑛 ) ) = ( ( abs ∘ − ) ‘ ⟨ ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) , ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) ⟩ ) )
48		df-ov	⊢ ( ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ( abs ∘ − ) ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) ) = ( ( abs ∘ − ) ‘ ⟨ ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) , ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) ⟩ )
49	48	eqcomi	⊢ ( ( abs ∘ − ) ‘ ⟨ ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) , ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) ⟩ ) = ( ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ( abs ∘ − ) ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) )
50	49	a1i	⊢ ( ( 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ∧ 𝑛 ∈ ℕ ) → ( ( abs ∘ − ) ‘ ⟨ ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) , ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) ⟩ ) = ( ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ( abs ∘ − ) ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) ) )
51	23	recnd	⊢ ( ( 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ∧ 𝑛 ∈ ℕ ) → ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ∈ ℂ )
52	25	recnd	⊢ ( ( 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ∧ 𝑛 ∈ ℕ ) → ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) ∈ ℂ )
53		eqid	⊢ ( abs ∘ − ) = ( abs ∘ − )
54	53	cnmetdval	⊢ ( ( ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ∈ ℂ ∧ ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) ∈ ℂ ) → ( ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ( abs ∘ − ) ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) ) = ( abs ‘ ( ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) − ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) ) ) )
55	51 52 54	syl2anc	⊢ ( ( 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ∧ 𝑛 ∈ ℕ ) → ( ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ( abs ∘ − ) ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) ) = ( abs ‘ ( ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) − ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) ) ) )
56		abssub	⊢ ( ( ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ∈ ℂ ∧ ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) ∈ ℂ ) → ( abs ‘ ( ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) − ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) ) ) = ( abs ‘ ( ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) − ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ) ) )
57	51 52 56	syl2anc	⊢ ( ( 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ∧ 𝑛 ∈ ℕ ) → ( abs ‘ ( ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) − ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) ) ) = ( abs ‘ ( ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) − ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ) ) )
58	23 25 31	abssubge0d	⊢ ( ( 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ∧ 𝑛 ∈ ℕ ) → ( abs ‘ ( ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) − ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ) ) = ( ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) − ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ) )
59	55 57 58	3eqtrd	⊢ ( ( 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ∧ 𝑛 ∈ ℕ ) → ( ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ( abs ∘ − ) ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) ) = ( ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) − ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ) )
60	47 50 59	3eqtrd	⊢ ( ( 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ∧ 𝑛 ∈ ℕ ) → ( ( abs ∘ − ) ‘ ( 𝑓 ‘ 𝑛 ) ) = ( ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) − ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ) )
61	34 46 60	3eqtr4d	⊢ ( ( 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ∧ 𝑛 ∈ ℕ ) → ( ( vol ∘ (,) ) ‘ ( 𝑓 ‘ 𝑛 ) ) = ( ( abs ∘ − ) ‘ ( 𝑓 ‘ 𝑛 ) ) )
62	61	mpteq2dva	⊢ ( 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) → ( 𝑛 ∈ ℕ ↦ ( ( vol ∘ (,) ) ‘ ( 𝑓 ‘ 𝑛 ) ) ) = ( 𝑛 ∈ ℕ ↦ ( ( abs ∘ − ) ‘ ( 𝑓 ‘ 𝑛 ) ) ) )
63		volioof	⊢ ( vol ∘ (,) ) : ( ℝ^* × ℝ^* ) ⟶ ( 0 [,] +∞ )
64	63	a1i	⊢ ( 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) → ( vol ∘ (,) ) : ( ℝ^* × ℝ^* ) ⟶ ( 0 [,] +∞ ) )
65	39	a1i	⊢ ( 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) → ( ℝ × ℝ ) ⊆ ( ℝ^* × ℝ^* ) )
66	12 65	fssd	⊢ ( 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) → 𝑓 : ℕ ⟶ ( ℝ^* × ℝ^* ) )
67		fcompt	⊢ ( ( ( vol ∘ (,) ) : ( ℝ^* × ℝ^* ) ⟶ ( 0 [,] +∞ ) ∧ 𝑓 : ℕ ⟶ ( ℝ^* × ℝ^* ) ) → ( ( vol ∘ (,) ) ∘ 𝑓 ) = ( 𝑛 ∈ ℕ ↦ ( ( vol ∘ (,) ) ‘ ( 𝑓 ‘ 𝑛 ) ) ) )
68	64 66 67	syl2anc	⊢ ( 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) → ( ( vol ∘ (,) ) ∘ 𝑓 ) = ( 𝑛 ∈ ℕ ↦ ( ( vol ∘ (,) ) ‘ ( 𝑓 ‘ 𝑛 ) ) ) )
69		absf	⊢ abs : ℂ ⟶ ℝ
70		subf	⊢ − : ( ℂ × ℂ ) ⟶ ℂ
71		fco	⊢ ( ( abs : ℂ ⟶ ℝ ∧ − : ( ℂ × ℂ ) ⟶ ℂ ) → ( abs ∘ − ) : ( ℂ × ℂ ) ⟶ ℝ )
72	69 70 71	mp2an	⊢ ( abs ∘ − ) : ( ℂ × ℂ ) ⟶ ℝ
73	72	a1i	⊢ ( 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) → ( abs ∘ − ) : ( ℂ × ℂ ) ⟶ ℝ )
74		rr2sscn2	⊢ ( ℝ × ℝ ) ⊆ ( ℂ × ℂ )
75	74	a1i	⊢ ( 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) → ( ℝ × ℝ ) ⊆ ( ℂ × ℂ ) )
76	12 75	fssd	⊢ ( 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) → 𝑓 : ℕ ⟶ ( ℂ × ℂ ) )
77		fcompt	⊢ ( ( ( abs ∘ − ) : ( ℂ × ℂ ) ⟶ ℝ ∧ 𝑓 : ℕ ⟶ ( ℂ × ℂ ) ) → ( ( abs ∘ − ) ∘ 𝑓 ) = ( 𝑛 ∈ ℕ ↦ ( ( abs ∘ − ) ‘ ( 𝑓 ‘ 𝑛 ) ) ) )
78	73 76 77	syl2anc	⊢ ( 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) → ( ( abs ∘ − ) ∘ 𝑓 ) = ( 𝑛 ∈ ℕ ↦ ( ( abs ∘ − ) ‘ ( 𝑓 ‘ 𝑛 ) ) ) )
79	62 68 78	3eqtr4d	⊢ ( 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) → ( ( vol ∘ (,) ) ∘ 𝑓 ) = ( ( abs ∘ − ) ∘ 𝑓 ) )
80	79	fveq2d	⊢ ( 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) → ( Σ^{^} ‘ ( ( vol ∘ (,) ) ∘ 𝑓 ) ) = ( Σ^{^} ‘ ( ( abs ∘ − ) ∘ 𝑓 ) ) )
81	80	eqeq2d	⊢ ( 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) → ( 𝑦 = ( Σ^{^} ‘ ( ( vol ∘ (,) ) ∘ 𝑓 ) ) ↔ 𝑦 = ( Σ^{^} ‘ ( ( abs ∘ − ) ∘ 𝑓 ) ) ) )
82	81	anbi2d	⊢ ( 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) → ( ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = ( Σ^{^} ‘ ( ( vol ∘ (,) ) ∘ 𝑓 ) ) ) ↔ ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = ( Σ^{^} ‘ ( ( abs ∘ − ) ∘ 𝑓 ) ) ) ) )
83	82	rexbiia	⊢ ( ∃ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = ( Σ^{^} ‘ ( ( vol ∘ (,) ) ∘ 𝑓 ) ) ) ↔ ∃ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = ( Σ^{^} ‘ ( ( abs ∘ − ) ∘ 𝑓 ) ) ) )
84	83	rabbii	⊢ { 𝑦 ∈ ℝ^* ∣ ∃ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = ( Σ^{^} ‘ ( ( vol ∘ (,) ) ∘ 𝑓 ) ) ) } = { 𝑦 ∈ ℝ^* ∣ ∃ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = ( Σ^{^} ‘ ( ( abs ∘ − ) ∘ 𝑓 ) ) ) }
85	2 84	eqtr2i	⊢ { 𝑦 ∈ ℝ^* ∣ ∃ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = ( Σ^{^} ‘ ( ( abs ∘ − ) ∘ 𝑓 ) ) ) } = 𝑀
86	85	infeq1i	⊢ inf ( { 𝑦 ∈ ℝ^* ∣ ∃ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = ( Σ^{^} ‘ ( ( abs ∘ − ) ∘ 𝑓 ) ) ) } , ℝ^* , < ) = inf ( 𝑀 , ℝ^* , < )
87	86	a1i	⊢ ( 𝜑 → inf ( { 𝑦 ∈ ℝ^* ∣ ∃ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = ( Σ^{^} ‘ ( ( abs ∘ − ) ∘ 𝑓 ) ) ) } , ℝ^* , < ) = inf ( 𝑀 , ℝ^* , < ) )
88	4 87	eqtrd	⊢ ( 𝜑 → ( vol* ‘ 𝐴 ) = inf ( 𝑀 , ℝ^* , < ) )

Metamath Proof Explorer

Theorem ovolval3

Proof