Step | Hyp | Ref
| Expression |
1 | | ovolval3.a |
. . 3
⊢ (𝜑 → 𝐴 ⊆ ℝ) |
2 | | eqid 2738 |
. . 3
⊢ {𝑦 ∈ ℝ*
∣ ∃𝑓 ∈ ((
≤ ∩ (ℝ × ℝ)) ↑m ℕ)(𝐴 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((abs ∘ − ) ∘ 𝑓)))} = {𝑦 ∈ ℝ* ∣
∃𝑓 ∈ (( ≤
∩ (ℝ × ℝ)) ↑m ℕ)(𝐴 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((abs ∘ − ) ∘ 𝑓)))} |
3 | 1, 2 | ovolval2 44182 |
. 2
⊢ (𝜑 → (vol*‘𝐴) = inf({𝑦 ∈ ℝ* ∣
∃𝑓 ∈ (( ≤
∩ (ℝ × ℝ)) ↑m ℕ)(𝐴 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((abs ∘ − ) ∘ 𝑓)))}, ℝ*, <
)) |
4 | | ovolval3.m |
. . . . 5
⊢ 𝑀 = {𝑦 ∈ ℝ* ∣
∃𝑓 ∈ (( ≤
∩ (ℝ × ℝ)) ↑m ℕ)(𝐴 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓)))} |
5 | | reex 10962 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ℝ
∈ V |
6 | 5, 5 | xpex 7603 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (ℝ
× ℝ) ∈ V |
7 | | inss2 4163 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ( ≤
∩ (ℝ × ℝ)) ⊆ (ℝ ×
ℝ) |
8 | | mapss 8677 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((ℝ × ℝ) ∈ V ∧ ( ≤ ∩ (ℝ ×
ℝ)) ⊆ (ℝ × ℝ)) → (( ≤ ∩ (ℝ
× ℝ)) ↑m ℕ) ⊆ ((ℝ ×
ℝ) ↑m ℕ)) |
9 | 6, 7, 8 | mp2an 689 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (( ≤
∩ (ℝ × ℝ)) ↑m ℕ) ⊆ ((ℝ
× ℝ) ↑m ℕ) |
10 | 9 | sseli 3917 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑓 ∈ (( ≤ ∩ (ℝ
× ℝ)) ↑m ℕ) → 𝑓 ∈ ((ℝ × ℝ)
↑m ℕ)) |
11 | | elmapi 8637 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) → 𝑓:ℕ⟶(ℝ ×
ℝ)) |
12 | 10, 11 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑓 ∈ (( ≤ ∩ (ℝ
× ℝ)) ↑m ℕ) → 𝑓:ℕ⟶(ℝ ×
ℝ)) |
13 | 12 | ffvelrnda 6961 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑓 ∈ (( ≤ ∩ (ℝ
× ℝ)) ↑m ℕ) ∧ 𝑛 ∈ ℕ) → (𝑓‘𝑛) ∈ (ℝ ×
ℝ)) |
14 | | 1st2nd2 7870 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑓‘𝑛) ∈ (ℝ × ℝ) →
(𝑓‘𝑛) = 〈(1st ‘(𝑓‘𝑛)), (2nd ‘(𝑓‘𝑛))〉) |
15 | 13, 14 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑓 ∈ (( ≤ ∩ (ℝ
× ℝ)) ↑m ℕ) ∧ 𝑛 ∈ ℕ) → (𝑓‘𝑛) = 〈(1st ‘(𝑓‘𝑛)), (2nd ‘(𝑓‘𝑛))〉) |
16 | 15 | fveq2d 6778 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑓 ∈ (( ≤ ∩ (ℝ
× ℝ)) ↑m ℕ) ∧ 𝑛 ∈ ℕ) → ((,)‘(𝑓‘𝑛)) = ((,)‘〈(1st
‘(𝑓‘𝑛)), (2nd
‘(𝑓‘𝑛))〉)) |
17 | | df-ov 7278 |
. . . . . . . . . . . . . . . . . 18
⊢
((1st ‘(𝑓‘𝑛))(,)(2nd ‘(𝑓‘𝑛))) = ((,)‘〈(1st
‘(𝑓‘𝑛)), (2nd
‘(𝑓‘𝑛))〉) |
18 | 17 | eqcomi 2747 |
. . . . . . . . . . . . . . . . 17
⊢
((,)‘〈(1st ‘(𝑓‘𝑛)), (2nd ‘(𝑓‘𝑛))〉) = ((1st ‘(𝑓‘𝑛))(,)(2nd ‘(𝑓‘𝑛))) |
19 | 18 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑓 ∈ (( ≤ ∩ (ℝ
× ℝ)) ↑m ℕ) ∧ 𝑛 ∈ ℕ) →
((,)‘〈(1st ‘(𝑓‘𝑛)), (2nd ‘(𝑓‘𝑛))〉) = ((1st ‘(𝑓‘𝑛))(,)(2nd ‘(𝑓‘𝑛)))) |
20 | 16, 19 | eqtrd 2778 |
. . . . . . . . . . . . . . 15
⊢ ((𝑓 ∈ (( ≤ ∩ (ℝ
× ℝ)) ↑m ℕ) ∧ 𝑛 ∈ ℕ) → ((,)‘(𝑓‘𝑛)) = ((1st ‘(𝑓‘𝑛))(,)(2nd ‘(𝑓‘𝑛)))) |
21 | 20 | fveq2d 6778 |
. . . . . . . . . . . . . 14
⊢ ((𝑓 ∈ (( ≤ ∩ (ℝ
× ℝ)) ↑m ℕ) ∧ 𝑛 ∈ ℕ) →
(vol‘((,)‘(𝑓‘𝑛))) = (vol‘((1st
‘(𝑓‘𝑛))(,)(2nd
‘(𝑓‘𝑛))))) |
22 | | xp1st 7863 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑓‘𝑛) ∈ (ℝ × ℝ) →
(1st ‘(𝑓‘𝑛)) ∈ ℝ) |
23 | 13, 22 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝑓 ∈ (( ≤ ∩ (ℝ
× ℝ)) ↑m ℕ) ∧ 𝑛 ∈ ℕ) → (1st
‘(𝑓‘𝑛)) ∈
ℝ) |
24 | | xp2nd 7864 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑓‘𝑛) ∈ (ℝ × ℝ) →
(2nd ‘(𝑓‘𝑛)) ∈ ℝ) |
25 | 13, 24 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝑓 ∈ (( ≤ ∩ (ℝ
× ℝ)) ↑m ℕ) ∧ 𝑛 ∈ ℕ) → (2nd
‘(𝑓‘𝑛)) ∈
ℝ) |
26 | | elmapi 8637 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑓 ∈ (( ≤ ∩ (ℝ
× ℝ)) ↑m ℕ) → 𝑓:ℕ⟶( ≤ ∩ (ℝ ×
ℝ))) |
27 | 26 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑓 ∈ (( ≤ ∩ (ℝ
× ℝ)) ↑m ℕ) ∧ 𝑛 ∈ ℕ) → 𝑓:ℕ⟶( ≤ ∩ (ℝ ×
ℝ))) |
28 | | simpr 485 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑓 ∈ (( ≤ ∩ (ℝ
× ℝ)) ↑m ℕ) ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℕ) |
29 | | ovolfcl 24630 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑓:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝑛 ∈ ℕ) → ((1st
‘(𝑓‘𝑛)) ∈ ℝ ∧
(2nd ‘(𝑓‘𝑛)) ∈ ℝ ∧ (1st
‘(𝑓‘𝑛)) ≤ (2nd
‘(𝑓‘𝑛)))) |
30 | 27, 28, 29 | syl2anc 584 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑓 ∈ (( ≤ ∩ (ℝ
× ℝ)) ↑m ℕ) ∧ 𝑛 ∈ ℕ) → ((1st
‘(𝑓‘𝑛)) ∈ ℝ ∧
(2nd ‘(𝑓‘𝑛)) ∈ ℝ ∧ (1st
‘(𝑓‘𝑛)) ≤ (2nd
‘(𝑓‘𝑛)))) |
31 | 30 | simp3d 1143 |
. . . . . . . . . . . . . . 15
⊢ ((𝑓 ∈ (( ≤ ∩ (ℝ
× ℝ)) ↑m ℕ) ∧ 𝑛 ∈ ℕ) → (1st
‘(𝑓‘𝑛)) ≤ (2nd
‘(𝑓‘𝑛))) |
32 | | volioo 24733 |
. . . . . . . . . . . . . . 15
⊢
(((1st ‘(𝑓‘𝑛)) ∈ ℝ ∧ (2nd
‘(𝑓‘𝑛)) ∈ ℝ ∧
(1st ‘(𝑓‘𝑛)) ≤ (2nd ‘(𝑓‘𝑛))) → (vol‘((1st
‘(𝑓‘𝑛))(,)(2nd
‘(𝑓‘𝑛)))) = ((2nd
‘(𝑓‘𝑛)) − (1st
‘(𝑓‘𝑛)))) |
33 | 23, 25, 31, 32 | syl3anc 1370 |
. . . . . . . . . . . . . 14
⊢ ((𝑓 ∈ (( ≤ ∩ (ℝ
× ℝ)) ↑m ℕ) ∧ 𝑛 ∈ ℕ) →
(vol‘((1st ‘(𝑓‘𝑛))(,)(2nd ‘(𝑓‘𝑛)))) = ((2nd ‘(𝑓‘𝑛)) − (1st ‘(𝑓‘𝑛)))) |
34 | 21, 33 | eqtrd 2778 |
. . . . . . . . . . . . 13
⊢ ((𝑓 ∈ (( ≤ ∩ (ℝ
× ℝ)) ↑m ℕ) ∧ 𝑛 ∈ ℕ) →
(vol‘((,)‘(𝑓‘𝑛))) = ((2nd ‘(𝑓‘𝑛)) − (1st ‘(𝑓‘𝑛)))) |
35 | | ioof 13179 |
. . . . . . . . . . . . . . . 16
⊢
(,):(ℝ* × ℝ*)⟶𝒫
ℝ |
36 | | ffun 6603 |
. . . . . . . . . . . . . . . 16
⊢
((,):(ℝ* × ℝ*)⟶𝒫
ℝ → Fun (,)) |
37 | 35, 36 | ax-mp 5 |
. . . . . . . . . . . . . . 15
⊢ Fun
(,) |
38 | 37 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ ((𝑓 ∈ (( ≤ ∩ (ℝ
× ℝ)) ↑m ℕ) ∧ 𝑛 ∈ ℕ) → Fun
(,)) |
39 | | rexpssxrxp 11020 |
. . . . . . . . . . . . . . . 16
⊢ (ℝ
× ℝ) ⊆ (ℝ* ×
ℝ*) |
40 | 39, 13 | sselid 3919 |
. . . . . . . . . . . . . . 15
⊢ ((𝑓 ∈ (( ≤ ∩ (ℝ
× ℝ)) ↑m ℕ) ∧ 𝑛 ∈ ℕ) → (𝑓‘𝑛) ∈ (ℝ* ×
ℝ*)) |
41 | 35 | fdmi 6612 |
. . . . . . . . . . . . . . . . 17
⊢ dom (,) =
(ℝ* × ℝ*) |
42 | 41 | eqcomi 2747 |
. . . . . . . . . . . . . . . 16
⊢
(ℝ* × ℝ*) = dom
(,) |
43 | 42 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ ((𝑓 ∈ (( ≤ ∩ (ℝ
× ℝ)) ↑m ℕ) ∧ 𝑛 ∈ ℕ) → (ℝ*
× ℝ*) = dom (,)) |
44 | 40, 43 | eleqtrd 2841 |
. . . . . . . . . . . . . 14
⊢ ((𝑓 ∈ (( ≤ ∩ (ℝ
× ℝ)) ↑m ℕ) ∧ 𝑛 ∈ ℕ) → (𝑓‘𝑛) ∈ dom (,)) |
45 | | fvco 6866 |
. . . . . . . . . . . . . 14
⊢ ((Fun (,)
∧ (𝑓‘𝑛) ∈ dom (,)) → ((vol
∘ (,))‘(𝑓‘𝑛)) = (vol‘((,)‘(𝑓‘𝑛)))) |
46 | 38, 44, 45 | syl2anc 584 |
. . . . . . . . . . . . 13
⊢ ((𝑓 ∈ (( ≤ ∩ (ℝ
× ℝ)) ↑m ℕ) ∧ 𝑛 ∈ ℕ) → ((vol ∘
(,))‘(𝑓‘𝑛)) =
(vol‘((,)‘(𝑓‘𝑛)))) |
47 | 15 | fveq2d 6778 |
. . . . . . . . . . . . . 14
⊢ ((𝑓 ∈ (( ≤ ∩ (ℝ
× ℝ)) ↑m ℕ) ∧ 𝑛 ∈ ℕ) → ((abs ∘ −
)‘(𝑓‘𝑛)) = ((abs ∘ −
)‘〈(1st ‘(𝑓‘𝑛)), (2nd ‘(𝑓‘𝑛))〉)) |
48 | | df-ov 7278 |
. . . . . . . . . . . . . . . 16
⊢
((1st ‘(𝑓‘𝑛))(abs ∘ − )(2nd
‘(𝑓‘𝑛))) = ((abs ∘ −
)‘〈(1st ‘(𝑓‘𝑛)), (2nd ‘(𝑓‘𝑛))〉) |
49 | 48 | eqcomi 2747 |
. . . . . . . . . . . . . . 15
⊢ ((abs
∘ − )‘〈(1st ‘(𝑓‘𝑛)), (2nd ‘(𝑓‘𝑛))〉) = ((1st ‘(𝑓‘𝑛))(abs ∘ − )(2nd
‘(𝑓‘𝑛))) |
50 | 49 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ ((𝑓 ∈ (( ≤ ∩ (ℝ
× ℝ)) ↑m ℕ) ∧ 𝑛 ∈ ℕ) → ((abs ∘ −
)‘〈(1st ‘(𝑓‘𝑛)), (2nd ‘(𝑓‘𝑛))〉) = ((1st ‘(𝑓‘𝑛))(abs ∘ − )(2nd
‘(𝑓‘𝑛)))) |
51 | 23 | recnd 11003 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑓 ∈ (( ≤ ∩ (ℝ
× ℝ)) ↑m ℕ) ∧ 𝑛 ∈ ℕ) → (1st
‘(𝑓‘𝑛)) ∈
ℂ) |
52 | 25 | recnd 11003 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑓 ∈ (( ≤ ∩ (ℝ
× ℝ)) ↑m ℕ) ∧ 𝑛 ∈ ℕ) → (2nd
‘(𝑓‘𝑛)) ∈
ℂ) |
53 | | eqid 2738 |
. . . . . . . . . . . . . . . . 17
⊢ (abs
∘ − ) = (abs ∘ − ) |
54 | 53 | cnmetdval 23934 |
. . . . . . . . . . . . . . . 16
⊢
(((1st ‘(𝑓‘𝑛)) ∈ ℂ ∧ (2nd
‘(𝑓‘𝑛)) ∈ ℂ) →
((1st ‘(𝑓‘𝑛))(abs ∘ − )(2nd
‘(𝑓‘𝑛))) =
(abs‘((1st ‘(𝑓‘𝑛)) − (2nd ‘(𝑓‘𝑛))))) |
55 | 51, 52, 54 | syl2anc 584 |
. . . . . . . . . . . . . . 15
⊢ ((𝑓 ∈ (( ≤ ∩ (ℝ
× ℝ)) ↑m ℕ) ∧ 𝑛 ∈ ℕ) → ((1st
‘(𝑓‘𝑛))(abs ∘ −
)(2nd ‘(𝑓‘𝑛))) = (abs‘((1st
‘(𝑓‘𝑛)) − (2nd
‘(𝑓‘𝑛))))) |
56 | | abssub 15038 |
. . . . . . . . . . . . . . . 16
⊢
(((1st ‘(𝑓‘𝑛)) ∈ ℂ ∧ (2nd
‘(𝑓‘𝑛)) ∈ ℂ) →
(abs‘((1st ‘(𝑓‘𝑛)) − (2nd ‘(𝑓‘𝑛)))) = (abs‘((2nd
‘(𝑓‘𝑛)) − (1st
‘(𝑓‘𝑛))))) |
57 | 51, 52, 56 | syl2anc 584 |
. . . . . . . . . . . . . . 15
⊢ ((𝑓 ∈ (( ≤ ∩ (ℝ
× ℝ)) ↑m ℕ) ∧ 𝑛 ∈ ℕ) →
(abs‘((1st ‘(𝑓‘𝑛)) − (2nd ‘(𝑓‘𝑛)))) = (abs‘((2nd
‘(𝑓‘𝑛)) − (1st
‘(𝑓‘𝑛))))) |
58 | 23, 25, 31 | abssubge0d 15143 |
. . . . . . . . . . . . . . 15
⊢ ((𝑓 ∈ (( ≤ ∩ (ℝ
× ℝ)) ↑m ℕ) ∧ 𝑛 ∈ ℕ) →
(abs‘((2nd ‘(𝑓‘𝑛)) − (1st ‘(𝑓‘𝑛)))) = ((2nd ‘(𝑓‘𝑛)) − (1st ‘(𝑓‘𝑛)))) |
59 | 55, 57, 58 | 3eqtrd 2782 |
. . . . . . . . . . . . . 14
⊢ ((𝑓 ∈ (( ≤ ∩ (ℝ
× ℝ)) ↑m ℕ) ∧ 𝑛 ∈ ℕ) → ((1st
‘(𝑓‘𝑛))(abs ∘ −
)(2nd ‘(𝑓‘𝑛))) = ((2nd ‘(𝑓‘𝑛)) − (1st ‘(𝑓‘𝑛)))) |
60 | 47, 50, 59 | 3eqtrd 2782 |
. . . . . . . . . . . . 13
⊢ ((𝑓 ∈ (( ≤ ∩ (ℝ
× ℝ)) ↑m ℕ) ∧ 𝑛 ∈ ℕ) → ((abs ∘ −
)‘(𝑓‘𝑛)) = ((2nd
‘(𝑓‘𝑛)) − (1st
‘(𝑓‘𝑛)))) |
61 | 34, 46, 60 | 3eqtr4d 2788 |
. . . . . . . . . . . 12
⊢ ((𝑓 ∈ (( ≤ ∩ (ℝ
× ℝ)) ↑m ℕ) ∧ 𝑛 ∈ ℕ) → ((vol ∘
(,))‘(𝑓‘𝑛)) = ((abs ∘ −
)‘(𝑓‘𝑛))) |
62 | 61 | mpteq2dva 5174 |
. . . . . . . . . . 11
⊢ (𝑓 ∈ (( ≤ ∩ (ℝ
× ℝ)) ↑m ℕ) → (𝑛 ∈ ℕ ↦ ((vol ∘
(,))‘(𝑓‘𝑛))) = (𝑛 ∈ ℕ ↦ ((abs ∘ −
)‘(𝑓‘𝑛)))) |
63 | | volioof 43528 |
. . . . . . . . . . . . 13
⊢ (vol
∘ (,)):(ℝ* ×
ℝ*)⟶(0[,]+∞) |
64 | 63 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝑓 ∈ (( ≤ ∩ (ℝ
× ℝ)) ↑m ℕ) → (vol ∘
(,)):(ℝ* ×
ℝ*)⟶(0[,]+∞)) |
65 | 39 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝑓 ∈ (( ≤ ∩ (ℝ
× ℝ)) ↑m ℕ) → (ℝ × ℝ)
⊆ (ℝ* × ℝ*)) |
66 | 12, 65 | fssd 6618 |
. . . . . . . . . . . 12
⊢ (𝑓 ∈ (( ≤ ∩ (ℝ
× ℝ)) ↑m ℕ) → 𝑓:ℕ⟶(ℝ* ×
ℝ*)) |
67 | | fcompt 7005 |
. . . . . . . . . . . 12
⊢ (((vol
∘ (,)):(ℝ* ×
ℝ*)⟶(0[,]+∞) ∧ 𝑓:ℕ⟶(ℝ* ×
ℝ*)) → ((vol ∘ (,)) ∘ 𝑓) = (𝑛 ∈ ℕ ↦ ((vol ∘
(,))‘(𝑓‘𝑛)))) |
68 | 64, 66, 67 | syl2anc 584 |
. . . . . . . . . . 11
⊢ (𝑓 ∈ (( ≤ ∩ (ℝ
× ℝ)) ↑m ℕ) → ((vol ∘ (,)) ∘
𝑓) = (𝑛 ∈ ℕ ↦ ((vol ∘
(,))‘(𝑓‘𝑛)))) |
69 | | absf 15049 |
. . . . . . . . . . . . . 14
⊢
abs:ℂ⟶ℝ |
70 | | subf 11223 |
. . . . . . . . . . . . . 14
⊢ −
:(ℂ × ℂ)⟶ℂ |
71 | | fco 6624 |
. . . . . . . . . . . . . 14
⊢
((abs:ℂ⟶ℝ ∧ − :(ℂ ×
ℂ)⟶ℂ) → (abs ∘ − ):(ℂ ×
ℂ)⟶ℝ) |
72 | 69, 70, 71 | mp2an 689 |
. . . . . . . . . . . . 13
⊢ (abs
∘ − ):(ℂ × ℂ)⟶ℝ |
73 | 72 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝑓 ∈ (( ≤ ∩ (ℝ
× ℝ)) ↑m ℕ) → (abs ∘ −
):(ℂ × ℂ)⟶ℝ) |
74 | | rr2sscn2 42905 |
. . . . . . . . . . . . . 14
⊢ (ℝ
× ℝ) ⊆ (ℂ × ℂ) |
75 | 74 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝑓 ∈ (( ≤ ∩ (ℝ
× ℝ)) ↑m ℕ) → (ℝ × ℝ)
⊆ (ℂ × ℂ)) |
76 | 12, 75 | fssd 6618 |
. . . . . . . . . . . 12
⊢ (𝑓 ∈ (( ≤ ∩ (ℝ
× ℝ)) ↑m ℕ) → 𝑓:ℕ⟶(ℂ ×
ℂ)) |
77 | | fcompt 7005 |
. . . . . . . . . . . 12
⊢ (((abs
∘ − ):(ℂ × ℂ)⟶ℝ ∧ 𝑓:ℕ⟶(ℂ ×
ℂ)) → ((abs ∘ − ) ∘ 𝑓) = (𝑛 ∈ ℕ ↦ ((abs ∘ −
)‘(𝑓‘𝑛)))) |
78 | 73, 76, 77 | syl2anc 584 |
. . . . . . . . . . 11
⊢ (𝑓 ∈ (( ≤ ∩ (ℝ
× ℝ)) ↑m ℕ) → ((abs ∘ − )
∘ 𝑓) = (𝑛 ∈ ℕ ↦ ((abs
∘ − )‘(𝑓‘𝑛)))) |
79 | 62, 68, 78 | 3eqtr4d 2788 |
. . . . . . . . . 10
⊢ (𝑓 ∈ (( ≤ ∩ (ℝ
× ℝ)) ↑m ℕ) → ((vol ∘ (,)) ∘
𝑓) = ((abs ∘ −
) ∘ 𝑓)) |
80 | 79 | fveq2d 6778 |
. . . . . . . . 9
⊢ (𝑓 ∈ (( ≤ ∩ (ℝ
× ℝ)) ↑m ℕ) →
(Σ^‘((vol ∘ (,)) ∘ 𝑓)) =
(Σ^‘((abs ∘ − ) ∘ 𝑓))) |
81 | 80 | eqeq2d 2749 |
. . . . . . . 8
⊢ (𝑓 ∈ (( ≤ ∩ (ℝ
× ℝ)) ↑m ℕ) → (𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓)) ↔ 𝑦 =
(Σ^‘((abs ∘ − ) ∘ 𝑓)))) |
82 | 81 | anbi2d 629 |
. . . . . . 7
⊢ (𝑓 ∈ (( ≤ ∩ (ℝ
× ℝ)) ↑m ℕ) → ((𝐴 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓))) ↔ (𝐴 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((abs ∘ − ) ∘ 𝑓))))) |
83 | 82 | rexbiia 3180 |
. . . . . 6
⊢
(∃𝑓 ∈ ((
≤ ∩ (ℝ × ℝ)) ↑m ℕ)(𝐴 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓))) ↔ ∃𝑓 ∈ (( ≤ ∩ (ℝ
× ℝ)) ↑m ℕ)(𝐴 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((abs ∘ − ) ∘ 𝑓)))) |
84 | 83 | rabbii 3408 |
. . . . 5
⊢ {𝑦 ∈ ℝ*
∣ ∃𝑓 ∈ ((
≤ ∩ (ℝ × ℝ)) ↑m ℕ)(𝐴 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓)))} = {𝑦 ∈ ℝ* ∣
∃𝑓 ∈ (( ≤
∩ (ℝ × ℝ)) ↑m ℕ)(𝐴 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((abs ∘ − ) ∘ 𝑓)))} |
85 | 4, 84 | eqtr2i 2767 |
. . . 4
⊢ {𝑦 ∈ ℝ*
∣ ∃𝑓 ∈ ((
≤ ∩ (ℝ × ℝ)) ↑m ℕ)(𝐴 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((abs ∘ − ) ∘ 𝑓)))} = 𝑀 |
86 | 85 | infeq1i 9237 |
. . 3
⊢
inf({𝑦 ∈
ℝ* ∣ ∃𝑓 ∈ (( ≤ ∩ (ℝ ×
ℝ)) ↑m ℕ)(𝐴 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((abs ∘ − ) ∘ 𝑓)))}, ℝ*, <
) = inf(𝑀,
ℝ*, < ) |
87 | 86 | a1i 11 |
. 2
⊢ (𝜑 → inf({𝑦 ∈ ℝ* ∣
∃𝑓 ∈ (( ≤
∩ (ℝ × ℝ)) ↑m ℕ)(𝐴 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((abs ∘ − ) ∘ 𝑓)))}, ℝ*, <
) = inf(𝑀,
ℝ*, < )) |
88 | 3, 87 | eqtrd 2778 |
1
⊢ (𝜑 → (vol*‘𝐴) = inf(𝑀, ℝ*, <
)) |