Step | Hyp | Ref
| Expression |
1 | | eqid 2622 |
. . 3
⊢
((ℂfld ↾s ℝ)
↑s 𝐼) = ((ℂfld
↾s ℝ) ↑s 𝐼) |
2 | | eqid 2622 |
. . 3
⊢
(dist‘((ℂfld ↾s ℝ)
↑s 𝐼)) = (dist‘((ℂfld
↾s ℝ) ↑s 𝐼)) |
3 | | rrntotbnd.1 |
. . 3
⊢ 𝑋 = (ℝ
↑𝑚 𝐼) |
4 | 1, 2, 3 | repwsmet 33633 |
. 2
⊢ (𝐼 ∈ Fin →
(dist‘((ℂfld ↾s ℝ)
↑s 𝐼)) ∈ (Met‘𝑋)) |
5 | 3 | rrnmet 33628 |
. 2
⊢ (𝐼 ∈ Fin →
(ℝn‘𝐼) ∈ (Met‘𝑋)) |
6 | | hashcl 13147 |
. . . 4
⊢ (𝐼 ∈ Fin →
(#‘𝐼) ∈
ℕ0) |
7 | | nn0re 11301 |
. . . . 5
⊢
((#‘𝐼) ∈
ℕ0 → (#‘𝐼) ∈ ℝ) |
8 | | nn0ge0 11318 |
. . . . 5
⊢
((#‘𝐼) ∈
ℕ0 → 0 ≤ (#‘𝐼)) |
9 | 7, 8 | resqrtcld 14156 |
. . . 4
⊢
((#‘𝐼) ∈
ℕ0 → (√‘(#‘𝐼)) ∈ ℝ) |
10 | 6, 9 | syl 17 |
. . 3
⊢ (𝐼 ∈ Fin →
(√‘(#‘𝐼))
∈ ℝ) |
11 | 7, 8 | sqrtge0d 14159 |
. . . 4
⊢
((#‘𝐼) ∈
ℕ0 → 0 ≤ (√‘(#‘𝐼))) |
12 | 6, 11 | syl 17 |
. . 3
⊢ (𝐼 ∈ Fin → 0 ≤
(√‘(#‘𝐼))) |
13 | 10, 12 | ge0p1rpd 11902 |
. 2
⊢ (𝐼 ∈ Fin →
((√‘(#‘𝐼)) + 1) ∈
ℝ+) |
14 | | 1rp 11836 |
. . 3
⊢ 1 ∈
ℝ+ |
15 | 14 | a1i 11 |
. 2
⊢ (𝐼 ∈ Fin → 1 ∈
ℝ+) |
16 | | metcl 22137 |
. . . . 5
⊢
(((ℝn‘𝐼) ∈ (Met‘𝑋) ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝑥(ℝn‘𝐼)𝑦) ∈ ℝ) |
17 | 16 | 3expb 1266 |
. . . 4
⊢
(((ℝn‘𝐼) ∈ (Met‘𝑋) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥(ℝn‘𝐼)𝑦) ∈ ℝ) |
18 | 5, 17 | sylan 488 |
. . 3
⊢ ((𝐼 ∈ Fin ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥(ℝn‘𝐼)𝑦) ∈ ℝ) |
19 | 10 | adantr 481 |
. . . 4
⊢ ((𝐼 ∈ Fin ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (√‘(#‘𝐼)) ∈
ℝ) |
20 | 4 | adantr 481 |
. . . . . 6
⊢ ((𝐼 ∈ Fin ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) →
(dist‘((ℂfld ↾s ℝ)
↑s 𝐼)) ∈ (Met‘𝑋)) |
21 | | simprl 794 |
. . . . . 6
⊢ ((𝐼 ∈ Fin ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → 𝑥 ∈ 𝑋) |
22 | | simprr 796 |
. . . . . 6
⊢ ((𝐼 ∈ Fin ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → 𝑦 ∈ 𝑋) |
23 | | metcl 22137 |
. . . . . . 7
⊢
(((dist‘((ℂfld ↾s ℝ)
↑s 𝐼)) ∈ (Met‘𝑋) ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝑥(dist‘((ℂfld
↾s ℝ) ↑s 𝐼))𝑦) ∈ ℝ) |
24 | | metge0 22150 |
. . . . . . 7
⊢
(((dist‘((ℂfld ↾s ℝ)
↑s 𝐼)) ∈ (Met‘𝑋) ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → 0 ≤ (𝑥(dist‘((ℂfld
↾s ℝ) ↑s 𝐼))𝑦)) |
25 | 23, 24 | jca 554 |
. . . . . 6
⊢
(((dist‘((ℂfld ↾s ℝ)
↑s 𝐼)) ∈ (Met‘𝑋) ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → ((𝑥(dist‘((ℂfld
↾s ℝ) ↑s 𝐼))𝑦) ∈ ℝ ∧ 0 ≤ (𝑥(dist‘((ℂfld
↾s ℝ) ↑s 𝐼))𝑦))) |
26 | 20, 21, 22, 25 | syl3anc 1326 |
. . . . 5
⊢ ((𝐼 ∈ Fin ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((𝑥(dist‘((ℂfld
↾s ℝ) ↑s 𝐼))𝑦) ∈ ℝ ∧ 0 ≤ (𝑥(dist‘((ℂfld
↾s ℝ) ↑s 𝐼))𝑦))) |
27 | 26 | simpld 475 |
. . . 4
⊢ ((𝐼 ∈ Fin ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥(dist‘((ℂfld
↾s ℝ) ↑s 𝐼))𝑦) ∈ ℝ) |
28 | 19, 27 | remulcld 10070 |
. . 3
⊢ ((𝐼 ∈ Fin ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((√‘(#‘𝐼)) · (𝑥(dist‘((ℂfld
↾s ℝ) ↑s 𝐼))𝑦)) ∈ ℝ) |
29 | | peano2re 10209 |
. . . . . 6
⊢
((√‘(#‘𝐼)) ∈ ℝ →
((√‘(#‘𝐼)) + 1) ∈ ℝ) |
30 | 10, 29 | syl 17 |
. . . . 5
⊢ (𝐼 ∈ Fin →
((√‘(#‘𝐼)) + 1) ∈ ℝ) |
31 | 30 | adantr 481 |
. . . 4
⊢ ((𝐼 ∈ Fin ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((√‘(#‘𝐼)) + 1) ∈
ℝ) |
32 | 31, 27 | remulcld 10070 |
. . 3
⊢ ((𝐼 ∈ Fin ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (((√‘(#‘𝐼)) + 1) · (𝑥(dist‘((ℂfld
↾s ℝ) ↑s 𝐼))𝑦)) ∈ ℝ) |
33 | | id 22 |
. . . . 5
⊢ (𝐼 ∈ Fin → 𝐼 ∈ Fin) |
34 | 1, 2, 3, 33 | rrnequiv 33634 |
. . . 4
⊢ ((𝐼 ∈ Fin ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((𝑥(dist‘((ℂfld
↾s ℝ) ↑s 𝐼))𝑦) ≤ (𝑥(ℝn‘𝐼)𝑦) ∧ (𝑥(ℝn‘𝐼)𝑦) ≤ ((√‘(#‘𝐼)) · (𝑥(dist‘((ℂfld
↾s ℝ) ↑s 𝐼))𝑦)))) |
35 | 34 | simprd 479 |
. . 3
⊢ ((𝐼 ∈ Fin ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥(ℝn‘𝐼)𝑦) ≤ ((√‘(#‘𝐼)) · (𝑥(dist‘((ℂfld
↾s ℝ) ↑s 𝐼))𝑦))) |
36 | 19 | lep1d 10955 |
. . . 4
⊢ ((𝐼 ∈ Fin ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (√‘(#‘𝐼)) ≤
((√‘(#‘𝐼)) + 1)) |
37 | | lemul1a 10877 |
. . . 4
⊢
((((√‘(#‘𝐼)) ∈ ℝ ∧
((√‘(#‘𝐼)) + 1) ∈ ℝ ∧ ((𝑥(dist‘((ℂfld
↾s ℝ) ↑s 𝐼))𝑦) ∈ ℝ ∧ 0 ≤ (𝑥(dist‘((ℂfld
↾s ℝ) ↑s 𝐼))𝑦))) ∧ (√‘(#‘𝐼)) ≤
((√‘(#‘𝐼)) + 1)) →
((√‘(#‘𝐼)) · (𝑥(dist‘((ℂfld
↾s ℝ) ↑s 𝐼))𝑦)) ≤ (((√‘(#‘𝐼)) + 1) · (𝑥(dist‘((ℂfld
↾s ℝ) ↑s 𝐼))𝑦))) |
38 | 19, 31, 26, 36, 37 | syl31anc 1329 |
. . 3
⊢ ((𝐼 ∈ Fin ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((√‘(#‘𝐼)) · (𝑥(dist‘((ℂfld
↾s ℝ) ↑s 𝐼))𝑦)) ≤ (((√‘(#‘𝐼)) + 1) · (𝑥(dist‘((ℂfld
↾s ℝ) ↑s 𝐼))𝑦))) |
39 | 18, 28, 32, 35, 38 | letrd 10194 |
. 2
⊢ ((𝐼 ∈ Fin ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥(ℝn‘𝐼)𝑦) ≤ (((√‘(#‘𝐼)) + 1) · (𝑥(dist‘((ℂfld
↾s ℝ) ↑s 𝐼))𝑦))) |
40 | 34 | simpld 475 |
. . 3
⊢ ((𝐼 ∈ Fin ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥(dist‘((ℂfld
↾s ℝ) ↑s 𝐼))𝑦) ≤ (𝑥(ℝn‘𝐼)𝑦)) |
41 | 18 | recnd 10068 |
. . . 4
⊢ ((𝐼 ∈ Fin ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥(ℝn‘𝐼)𝑦) ∈ ℂ) |
42 | 41 | mulid2d 10058 |
. . 3
⊢ ((𝐼 ∈ Fin ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (1 · (𝑥(ℝn‘𝐼)𝑦)) = (𝑥(ℝn‘𝐼)𝑦)) |
43 | 40, 42 | breqtrrd 4681 |
. 2
⊢ ((𝐼 ∈ Fin ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥(dist‘((ℂfld
↾s ℝ) ↑s 𝐼))𝑦) ≤ (1 · (𝑥(ℝn‘𝐼)𝑦))) |
44 | | eqid 2622 |
. 2
⊢
((dist‘((ℂfld ↾s ℝ)
↑s 𝐼)) ↾ (𝑌 × 𝑌)) = ((dist‘((ℂfld
↾s ℝ) ↑s 𝐼)) ↾ (𝑌 × 𝑌)) |
45 | | rrntotbnd.2 |
. 2
⊢ 𝑀 =
((ℝn‘𝐼) ↾ (𝑌 × 𝑌)) |
46 | | ax-resscn 9993 |
. . 3
⊢ ℝ
⊆ ℂ |
47 | 1, 44 | cnpwstotbnd 33596 |
. . 3
⊢ ((ℝ
⊆ ℂ ∧ 𝐼
∈ Fin) → (((dist‘((ℂfld ↾s
ℝ) ↑s 𝐼)) ↾ (𝑌 × 𝑌)) ∈ (TotBnd‘𝑌) ↔
((dist‘((ℂfld ↾s ℝ)
↑s 𝐼)) ↾ (𝑌 × 𝑌)) ∈ (Bnd‘𝑌))) |
48 | 46, 47 | mpan 706 |
. 2
⊢ (𝐼 ∈ Fin →
(((dist‘((ℂfld ↾s ℝ)
↑s 𝐼)) ↾ (𝑌 × 𝑌)) ∈ (TotBnd‘𝑌) ↔
((dist‘((ℂfld ↾s ℝ)
↑s 𝐼)) ↾ (𝑌 × 𝑌)) ∈ (Bnd‘𝑌))) |
49 | 4, 5, 13, 15, 39, 43, 44, 45, 48 | equivbnd2 33591 |
1
⊢ (𝐼 ∈ Fin → (𝑀 ∈ (TotBnd‘𝑌) ↔ 𝑀 ∈ (Bnd‘𝑌))) |