| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | eqid 2737 | . . 3
⊢
((ℂfld ↾s ℝ)
↑s 𝐼) = ((ℂfld
↾s ℝ) ↑s 𝐼) | 
| 2 |  | eqid 2737 | . . 3
⊢
(dist‘((ℂfld ↾s ℝ)
↑s 𝐼)) = (dist‘((ℂfld
↾s ℝ) ↑s 𝐼)) | 
| 3 |  | rrntotbnd.1 | . . 3
⊢ 𝑋 = (ℝ ↑m
𝐼) | 
| 4 | 1, 2, 3 | repwsmet 37841 | . 2
⊢ (𝐼 ∈ Fin →
(dist‘((ℂfld ↾s ℝ)
↑s 𝐼)) ∈ (Met‘𝑋)) | 
| 5 | 3 | rrnmet 37836 | . 2
⊢ (𝐼 ∈ Fin →
(ℝn‘𝐼) ∈ (Met‘𝑋)) | 
| 6 |  | hashcl 14395 | . . . 4
⊢ (𝐼 ∈ Fin →
(♯‘𝐼) ∈
ℕ0) | 
| 7 |  | nn0re 12535 | . . . . 5
⊢
((♯‘𝐼)
∈ ℕ0 → (♯‘𝐼) ∈ ℝ) | 
| 8 |  | nn0ge0 12551 | . . . . 5
⊢
((♯‘𝐼)
∈ ℕ0 → 0 ≤ (♯‘𝐼)) | 
| 9 | 7, 8 | resqrtcld 15456 | . . . 4
⊢
((♯‘𝐼)
∈ ℕ0 → (√‘(♯‘𝐼)) ∈
ℝ) | 
| 10 | 6, 9 | syl 17 | . . 3
⊢ (𝐼 ∈ Fin →
(√‘(♯‘𝐼)) ∈ ℝ) | 
| 11 | 7, 8 | sqrtge0d 15459 | . . . 4
⊢
((♯‘𝐼)
∈ ℕ0 → 0 ≤ (√‘(♯‘𝐼))) | 
| 12 | 6, 11 | syl 17 | . . 3
⊢ (𝐼 ∈ Fin → 0 ≤
(√‘(♯‘𝐼))) | 
| 13 | 10, 12 | ge0p1rpd 13107 | . 2
⊢ (𝐼 ∈ Fin →
((√‘(♯‘𝐼)) + 1) ∈
ℝ+) | 
| 14 |  | 1rp 13038 | . . 3
⊢ 1 ∈
ℝ+ | 
| 15 | 14 | a1i 11 | . 2
⊢ (𝐼 ∈ Fin → 1 ∈
ℝ+) | 
| 16 |  | metcl 24342 | . . . . 5
⊢
(((ℝn‘𝐼) ∈ (Met‘𝑋) ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝑥(ℝn‘𝐼)𝑦) ∈ ℝ) | 
| 17 | 16 | 3expb 1121 | . . . 4
⊢
(((ℝn‘𝐼) ∈ (Met‘𝑋) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥(ℝn‘𝐼)𝑦) ∈ ℝ) | 
| 18 | 5, 17 | sylan 580 | . . 3
⊢ ((𝐼 ∈ Fin ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥(ℝn‘𝐼)𝑦) ∈ ℝ) | 
| 19 | 10 | adantr 480 | . . . 4
⊢ ((𝐼 ∈ Fin ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) →
(√‘(♯‘𝐼)) ∈ ℝ) | 
| 20 | 4 | adantr 480 | . . . . . 6
⊢ ((𝐼 ∈ Fin ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) →
(dist‘((ℂfld ↾s ℝ)
↑s 𝐼)) ∈ (Met‘𝑋)) | 
| 21 |  | simprl 771 | . . . . . 6
⊢ ((𝐼 ∈ Fin ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → 𝑥 ∈ 𝑋) | 
| 22 |  | simprr 773 | . . . . . 6
⊢ ((𝐼 ∈ Fin ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → 𝑦 ∈ 𝑋) | 
| 23 |  | metcl 24342 | . . . . . . 7
⊢
(((dist‘((ℂfld ↾s ℝ)
↑s 𝐼)) ∈ (Met‘𝑋) ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝑥(dist‘((ℂfld
↾s ℝ) ↑s 𝐼))𝑦) ∈ ℝ) | 
| 24 |  | metge0 24355 | . . . . . . 7
⊢
(((dist‘((ℂfld ↾s ℝ)
↑s 𝐼)) ∈ (Met‘𝑋) ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → 0 ≤ (𝑥(dist‘((ℂfld
↾s ℝ) ↑s 𝐼))𝑦)) | 
| 25 | 23, 24 | jca 511 | . . . . . 6
⊢
(((dist‘((ℂfld ↾s ℝ)
↑s 𝐼)) ∈ (Met‘𝑋) ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → ((𝑥(dist‘((ℂfld
↾s ℝ) ↑s 𝐼))𝑦) ∈ ℝ ∧ 0 ≤ (𝑥(dist‘((ℂfld
↾s ℝ) ↑s 𝐼))𝑦))) | 
| 26 | 20, 21, 22, 25 | syl3anc 1373 | . . . . 5
⊢ ((𝐼 ∈ Fin ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((𝑥(dist‘((ℂfld
↾s ℝ) ↑s 𝐼))𝑦) ∈ ℝ ∧ 0 ≤ (𝑥(dist‘((ℂfld
↾s ℝ) ↑s 𝐼))𝑦))) | 
| 27 | 26 | simpld 494 | . . . 4
⊢ ((𝐼 ∈ Fin ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥(dist‘((ℂfld
↾s ℝ) ↑s 𝐼))𝑦) ∈ ℝ) | 
| 28 | 19, 27 | remulcld 11291 | . . 3
⊢ ((𝐼 ∈ Fin ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) →
((√‘(♯‘𝐼)) · (𝑥(dist‘((ℂfld
↾s ℝ) ↑s 𝐼))𝑦)) ∈ ℝ) | 
| 29 |  | peano2re 11434 | . . . . . 6
⊢
((√‘(♯‘𝐼)) ∈ ℝ →
((√‘(♯‘𝐼)) + 1) ∈ ℝ) | 
| 30 | 10, 29 | syl 17 | . . . . 5
⊢ (𝐼 ∈ Fin →
((√‘(♯‘𝐼)) + 1) ∈ ℝ) | 
| 31 | 30 | adantr 480 | . . . 4
⊢ ((𝐼 ∈ Fin ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) →
((√‘(♯‘𝐼)) + 1) ∈ ℝ) | 
| 32 | 31, 27 | remulcld 11291 | . . 3
⊢ ((𝐼 ∈ Fin ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) →
(((√‘(♯‘𝐼)) + 1) · (𝑥(dist‘((ℂfld
↾s ℝ) ↑s 𝐼))𝑦)) ∈ ℝ) | 
| 33 |  | id 22 | . . . . 5
⊢ (𝐼 ∈ Fin → 𝐼 ∈ Fin) | 
| 34 | 1, 2, 3, 33 | rrnequiv 37842 | . . . 4
⊢ ((𝐼 ∈ Fin ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((𝑥(dist‘((ℂfld
↾s ℝ) ↑s 𝐼))𝑦) ≤ (𝑥(ℝn‘𝐼)𝑦) ∧ (𝑥(ℝn‘𝐼)𝑦) ≤ ((√‘(♯‘𝐼)) · (𝑥(dist‘((ℂfld
↾s ℝ) ↑s 𝐼))𝑦)))) | 
| 35 | 34 | simprd 495 | . . 3
⊢ ((𝐼 ∈ Fin ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥(ℝn‘𝐼)𝑦) ≤ ((√‘(♯‘𝐼)) · (𝑥(dist‘((ℂfld
↾s ℝ) ↑s 𝐼))𝑦))) | 
| 36 | 19 | lep1d 12199 | . . . 4
⊢ ((𝐼 ∈ Fin ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) →
(√‘(♯‘𝐼)) ≤ ((√‘(♯‘𝐼)) + 1)) | 
| 37 |  | lemul1a 12121 | . . . 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 1375 | . . 3
⊢ ((𝐼 ∈ Fin ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) →
((√‘(♯‘𝐼)) · (𝑥(dist‘((ℂfld
↾s ℝ) ↑s 𝐼))𝑦)) ≤ (((√‘(♯‘𝐼)) + 1) · (𝑥(dist‘((ℂfld
↾s ℝ) ↑s 𝐼))𝑦))) | 
| 39 | 18, 28, 32, 35, 38 | letrd 11418 | . 2
⊢ ((𝐼 ∈ Fin ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥(ℝn‘𝐼)𝑦) ≤ (((√‘(♯‘𝐼)) + 1) · (𝑥(dist‘((ℂfld
↾s ℝ) ↑s 𝐼))𝑦))) | 
| 40 | 34 | simpld 494 | . . 3
⊢ ((𝐼 ∈ Fin ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥(dist‘((ℂfld
↾s ℝ) ↑s 𝐼))𝑦) ≤ (𝑥(ℝn‘𝐼)𝑦)) | 
| 41 | 18 | recnd 11289 | . . . 4
⊢ ((𝐼 ∈ Fin ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥(ℝn‘𝐼)𝑦) ∈ ℂ) | 
| 42 | 41 | mullidd 11279 | . . 3
⊢ ((𝐼 ∈ Fin ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (1 · (𝑥(ℝn‘𝐼)𝑦)) = (𝑥(ℝn‘𝐼)𝑦)) | 
| 43 | 40, 42 | breqtrrd 5171 | . 2
⊢ ((𝐼 ∈ Fin ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥(dist‘((ℂfld
↾s ℝ) ↑s 𝐼))𝑦) ≤ (1 · (𝑥(ℝn‘𝐼)𝑦))) | 
| 44 |  | eqid 2737 | . 2
⊢
((dist‘((ℂfld ↾s ℝ)
↑s 𝐼)) ↾ (𝑌 × 𝑌)) = ((dist‘((ℂfld
↾s ℝ) ↑s 𝐼)) ↾ (𝑌 × 𝑌)) | 
| 45 |  | rrntotbnd.2 | . 2
⊢ 𝑀 =
((ℝn‘𝐼) ↾ (𝑌 × 𝑌)) | 
| 46 |  | ax-resscn 11212 | . . 3
⊢ ℝ
⊆ ℂ | 
| 47 | 1, 44 | cnpwstotbnd 37804 | . . 3
⊢ ((ℝ
⊆ ℂ ∧ 𝐼
∈ Fin) → (((dist‘((ℂfld ↾s
ℝ) ↑s 𝐼)) ↾ (𝑌 × 𝑌)) ∈ (TotBnd‘𝑌) ↔
((dist‘((ℂfld ↾s ℝ)
↑s 𝐼)) ↾ (𝑌 × 𝑌)) ∈ (Bnd‘𝑌))) | 
| 48 | 46, 47 | mpan 690 | . 2
⊢ (𝐼 ∈ Fin →
(((dist‘((ℂfld ↾s ℝ)
↑s 𝐼)) ↾ (𝑌 × 𝑌)) ∈ (TotBnd‘𝑌) ↔
((dist‘((ℂfld ↾s ℝ)
↑s 𝐼)) ↾ (𝑌 × 𝑌)) ∈ (Bnd‘𝑌))) | 
| 49 | 4, 5, 13, 15, 39, 43, 44, 45, 48 | equivbnd2 37799 | 1
⊢ (𝐼 ∈ Fin → (𝑀 ∈ (TotBnd‘𝑌) ↔ 𝑀 ∈ (Bnd‘𝑌))) |