Step | Hyp | Ref
| Expression |
1 | | rrxtopnfi.1 |
. . 3
⊢ (𝜑 → 𝐼 ∈ Fin) |
2 | 1 | rrxtopn 39177 |
. 2
⊢ (𝜑 →
(TopOpen‘(ℝ^‘𝐼)) = (MetOpen‘(𝑓 ∈ (Base‘(ℝ^‘𝐼)), 𝑔 ∈ (Base‘(ℝ^‘𝐼)) ↦
(√‘(ℝfld Σg (𝑥 ∈ 𝐼 ↦ (((𝑓‘𝑥) − (𝑔‘𝑥))↑2))))))) |
3 | | eqid 2610 |
. . . . 5
⊢
(ℝ^‘𝐼) =
(ℝ^‘𝐼) |
4 | | eqid 2610 |
. . . . 5
⊢
(Base‘(ℝ^‘𝐼)) = (Base‘(ℝ^‘𝐼)) |
5 | 1, 3, 4 | rrxbasefi 39179 |
. . . 4
⊢ (𝜑 →
(Base‘(ℝ^‘𝐼)) = (ℝ ↑𝑚
𝐼)) |
6 | 5 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝑓 ∈ (Base‘(ℝ^‘𝐼))) →
(Base‘(ℝ^‘𝐼)) = (ℝ ↑𝑚
𝐼)) |
7 | | simpl 472 |
. . . . 5
⊢ ((𝜑 ∧ (𝑓 ∈ (Base‘(ℝ^‘𝐼)) ∧ 𝑔 ∈ (Base‘(ℝ^‘𝐼)))) → 𝜑) |
8 | | simprl 790 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑓 ∈ (Base‘(ℝ^‘𝐼)) ∧ 𝑔 ∈ (Base‘(ℝ^‘𝐼)))) → 𝑓 ∈ (Base‘(ℝ^‘𝐼))) |
9 | | simpr 476 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑓 ∈ (Base‘(ℝ^‘𝐼))) → 𝑓 ∈ (Base‘(ℝ^‘𝐼))) |
10 | 9, 6 | eleqtrd 2690 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑓 ∈ (Base‘(ℝ^‘𝐼))) → 𝑓 ∈ (ℝ ↑𝑚
𝐼)) |
11 | 8, 10 | syldan 486 |
. . . . 5
⊢ ((𝜑 ∧ (𝑓 ∈ (Base‘(ℝ^‘𝐼)) ∧ 𝑔 ∈ (Base‘(ℝ^‘𝐼)))) → 𝑓 ∈ (ℝ ↑𝑚
𝐼)) |
12 | | simprr 792 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑓 ∈ (Base‘(ℝ^‘𝐼)) ∧ 𝑔 ∈ (Base‘(ℝ^‘𝐼)))) → 𝑔 ∈ (Base‘(ℝ^‘𝐼))) |
13 | | simpr 476 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑔 ∈ (Base‘(ℝ^‘𝐼))) → 𝑔 ∈ (Base‘(ℝ^‘𝐼))) |
14 | 5 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑔 ∈ (Base‘(ℝ^‘𝐼))) →
(Base‘(ℝ^‘𝐼)) = (ℝ ↑𝑚
𝐼)) |
15 | 13, 14 | eleqtrd 2690 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑔 ∈ (Base‘(ℝ^‘𝐼))) → 𝑔 ∈ (ℝ ↑𝑚
𝐼)) |
16 | 12, 15 | syldan 486 |
. . . . 5
⊢ ((𝜑 ∧ (𝑓 ∈ (Base‘(ℝ^‘𝐼)) ∧ 𝑔 ∈ (Base‘(ℝ^‘𝐼)))) → 𝑔 ∈ (ℝ ↑𝑚
𝐼)) |
17 | | elmapi 7765 |
. . . . . . . . . . . . . 14
⊢ (𝑓 ∈ (ℝ
↑𝑚 𝐼) → 𝑓:𝐼⟶ℝ) |
18 | 17 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝑓 ∈ (ℝ
↑𝑚 𝐼) ∧ 𝑔 ∈ (ℝ ↑𝑚
𝐼)) → 𝑓:𝐼⟶ℝ) |
19 | 18 | ffvelrnda 6267 |
. . . . . . . . . . . 12
⊢ (((𝑓 ∈ (ℝ
↑𝑚 𝐼) ∧ 𝑔 ∈ (ℝ ↑𝑚
𝐼)) ∧ 𝑥 ∈ 𝐼) → (𝑓‘𝑥) ∈ ℝ) |
20 | | elmapi 7765 |
. . . . . . . . . . . . . 14
⊢ (𝑔 ∈ (ℝ
↑𝑚 𝐼) → 𝑔:𝐼⟶ℝ) |
21 | 20 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((𝑓 ∈ (ℝ
↑𝑚 𝐼) ∧ 𝑔 ∈ (ℝ ↑𝑚
𝐼)) → 𝑔:𝐼⟶ℝ) |
22 | 21 | ffvelrnda 6267 |
. . . . . . . . . . . 12
⊢ (((𝑓 ∈ (ℝ
↑𝑚 𝐼) ∧ 𝑔 ∈ (ℝ ↑𝑚
𝐼)) ∧ 𝑥 ∈ 𝐼) → (𝑔‘𝑥) ∈ ℝ) |
23 | 19, 22 | resubcld 10337 |
. . . . . . . . . . 11
⊢ (((𝑓 ∈ (ℝ
↑𝑚 𝐼) ∧ 𝑔 ∈ (ℝ ↑𝑚
𝐼)) ∧ 𝑥 ∈ 𝐼) → ((𝑓‘𝑥) − (𝑔‘𝑥)) ∈ ℝ) |
24 | 23 | resqcld 12897 |
. . . . . . . . . 10
⊢ (((𝑓 ∈ (ℝ
↑𝑚 𝐼) ∧ 𝑔 ∈ (ℝ ↑𝑚
𝐼)) ∧ 𝑥 ∈ 𝐼) → (((𝑓‘𝑥) − (𝑔‘𝑥))↑2) ∈ ℝ) |
25 | | eqid 2610 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝐼 ↦ (((𝑓‘𝑥) − (𝑔‘𝑥))↑2)) = (𝑥 ∈ 𝐼 ↦ (((𝑓‘𝑥) − (𝑔‘𝑥))↑2)) |
26 | 24, 25 | fmptd 6292 |
. . . . . . . . 9
⊢ ((𝑓 ∈ (ℝ
↑𝑚 𝐼) ∧ 𝑔 ∈ (ℝ ↑𝑚
𝐼)) → (𝑥 ∈ 𝐼 ↦ (((𝑓‘𝑥) − (𝑔‘𝑥))↑2)):𝐼⟶ℝ) |
27 | 26 | 3adant1 1072 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑓 ∈ (ℝ ↑𝑚
𝐼) ∧ 𝑔 ∈ (ℝ ↑𝑚
𝐼)) → (𝑥 ∈ 𝐼 ↦ (((𝑓‘𝑥) − (𝑔‘𝑥))↑2)):𝐼⟶ℝ) |
28 | 1 | 3ad2ant1 1075 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑓 ∈ (ℝ ↑𝑚
𝐼) ∧ 𝑔 ∈ (ℝ ↑𝑚
𝐼)) → 𝐼 ∈ Fin) |
29 | | 0red 9920 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑓 ∈ (ℝ ↑𝑚
𝐼) ∧ 𝑔 ∈ (ℝ ↑𝑚
𝐼)) → 0 ∈
ℝ) |
30 | 27, 28, 29 | fidmfisupp 38385 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑓 ∈ (ℝ ↑𝑚
𝐼) ∧ 𝑔 ∈ (ℝ ↑𝑚
𝐼)) → (𝑥 ∈ 𝐼 ↦ (((𝑓‘𝑥) − (𝑔‘𝑥))↑2)) finSupp 0) |
31 | | regsumsupp 19787 |
. . . . . . . 8
⊢ (((𝑥 ∈ 𝐼 ↦ (((𝑓‘𝑥) − (𝑔‘𝑥))↑2)):𝐼⟶ℝ ∧ (𝑥 ∈ 𝐼 ↦ (((𝑓‘𝑥) − (𝑔‘𝑥))↑2)) finSupp 0 ∧ 𝐼 ∈ Fin) → (ℝfld
Σg (𝑥 ∈ 𝐼 ↦ (((𝑓‘𝑥) − (𝑔‘𝑥))↑2))) = Σ𝑘 ∈ ((𝑥 ∈ 𝐼 ↦ (((𝑓‘𝑥) − (𝑔‘𝑥))↑2)) supp 0)((𝑥 ∈ 𝐼 ↦ (((𝑓‘𝑥) − (𝑔‘𝑥))↑2))‘𝑘)) |
32 | 27, 30, 28, 31 | syl3anc 1318 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑓 ∈ (ℝ ↑𝑚
𝐼) ∧ 𝑔 ∈ (ℝ ↑𝑚
𝐼)) →
(ℝfld Σg (𝑥 ∈ 𝐼 ↦ (((𝑓‘𝑥) − (𝑔‘𝑥))↑2))) = Σ𝑘 ∈ ((𝑥 ∈ 𝐼 ↦ (((𝑓‘𝑥) − (𝑔‘𝑥))↑2)) supp 0)((𝑥 ∈ 𝐼 ↦ (((𝑓‘𝑥) − (𝑔‘𝑥))↑2))‘𝑘)) |
33 | | ax-resscn 9872 |
. . . . . . . . . . . . . . 15
⊢ ℝ
⊆ ℂ |
34 | 33 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝑓 ∈ (ℝ
↑𝑚 𝐼) → ℝ ⊆
ℂ) |
35 | 17, 34 | fssd 5970 |
. . . . . . . . . . . . 13
⊢ (𝑓 ∈ (ℝ
↑𝑚 𝐼) → 𝑓:𝐼⟶ℂ) |
36 | 35 | 3ad2ant2 1076 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑓 ∈ (ℝ ↑𝑚
𝐼) ∧ 𝑔 ∈ (ℝ ↑𝑚
𝐼)) → 𝑓:𝐼⟶ℂ) |
37 | 36 | ffvelrnda 6267 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑓 ∈ (ℝ ↑𝑚
𝐼) ∧ 𝑔 ∈ (ℝ ↑𝑚
𝐼)) ∧ 𝑥 ∈ 𝐼) → (𝑓‘𝑥) ∈ ℂ) |
38 | 33 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝑔 ∈ (ℝ
↑𝑚 𝐼) → ℝ ⊆
ℂ) |
39 | 20, 38 | fssd 5970 |
. . . . . . . . . . . . 13
⊢ (𝑔 ∈ (ℝ
↑𝑚 𝐼) → 𝑔:𝐼⟶ℂ) |
40 | 39 | 3ad2ant3 1077 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑓 ∈ (ℝ ↑𝑚
𝐼) ∧ 𝑔 ∈ (ℝ ↑𝑚
𝐼)) → 𝑔:𝐼⟶ℂ) |
41 | 40 | ffvelrnda 6267 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑓 ∈ (ℝ ↑𝑚
𝐼) ∧ 𝑔 ∈ (ℝ ↑𝑚
𝐼)) ∧ 𝑥 ∈ 𝐼) → (𝑔‘𝑥) ∈ ℂ) |
42 | 37, 41 | subcld 10271 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑓 ∈ (ℝ ↑𝑚
𝐼) ∧ 𝑔 ∈ (ℝ ↑𝑚
𝐼)) ∧ 𝑥 ∈ 𝐼) → ((𝑓‘𝑥) − (𝑔‘𝑥)) ∈ ℂ) |
43 | 42 | sqcld 12868 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑓 ∈ (ℝ ↑𝑚
𝐼) ∧ 𝑔 ∈ (ℝ ↑𝑚
𝐼)) ∧ 𝑥 ∈ 𝐼) → (((𝑓‘𝑥) − (𝑔‘𝑥))↑2) ∈ ℂ) |
44 | 43, 25 | fmptd 6292 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑓 ∈ (ℝ ↑𝑚
𝐼) ∧ 𝑔 ∈ (ℝ ↑𝑚
𝐼)) → (𝑥 ∈ 𝐼 ↦ (((𝑓‘𝑥) − (𝑔‘𝑥))↑2)):𝐼⟶ℂ) |
45 | 28, 44 | fsumsupp0 38645 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑓 ∈ (ℝ ↑𝑚
𝐼) ∧ 𝑔 ∈ (ℝ ↑𝑚
𝐼)) → Σ𝑘 ∈ ((𝑥 ∈ 𝐼 ↦ (((𝑓‘𝑥) − (𝑔‘𝑥))↑2)) supp 0)((𝑥 ∈ 𝐼 ↦ (((𝑓‘𝑥) − (𝑔‘𝑥))↑2))‘𝑘) = Σ𝑘 ∈ 𝐼 ((𝑥 ∈ 𝐼 ↦ (((𝑓‘𝑥) − (𝑔‘𝑥))↑2))‘𝑘)) |
46 | | eqidd 2611 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑓 ∈ (ℝ ↑𝑚
𝐼) ∧ 𝑔 ∈ (ℝ ↑𝑚
𝐼)) ∧ 𝑘 ∈ 𝐼) → (𝑥 ∈ 𝐼 ↦ (((𝑓‘𝑥) − (𝑔‘𝑥))↑2)) = (𝑥 ∈ 𝐼 ↦ (((𝑓‘𝑥) − (𝑔‘𝑥))↑2))) |
47 | | fveq2 6103 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑘 → (𝑓‘𝑥) = (𝑓‘𝑘)) |
48 | | fveq2 6103 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑘 → (𝑔‘𝑥) = (𝑔‘𝑘)) |
49 | 47, 48 | oveq12d 6567 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑘 → ((𝑓‘𝑥) − (𝑔‘𝑥)) = ((𝑓‘𝑘) − (𝑔‘𝑘))) |
50 | 49 | oveq1d 6564 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑘 → (((𝑓‘𝑥) − (𝑔‘𝑥))↑2) = (((𝑓‘𝑘) − (𝑔‘𝑘))↑2)) |
51 | 50 | adantl 481 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑓 ∈ (ℝ ↑𝑚
𝐼) ∧ 𝑔 ∈ (ℝ ↑𝑚
𝐼)) ∧ 𝑘 ∈ 𝐼) ∧ 𝑥 = 𝑘) → (((𝑓‘𝑥) − (𝑔‘𝑥))↑2) = (((𝑓‘𝑘) − (𝑔‘𝑘))↑2)) |
52 | | simpr 476 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑓 ∈ (ℝ ↑𝑚
𝐼) ∧ 𝑔 ∈ (ℝ ↑𝑚
𝐼)) ∧ 𝑘 ∈ 𝐼) → 𝑘 ∈ 𝐼) |
53 | | ovex 6577 |
. . . . . . . . . 10
⊢ (((𝑓‘𝑘) − (𝑔‘𝑘))↑2) ∈ V |
54 | 53 | a1i 11 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑓 ∈ (ℝ ↑𝑚
𝐼) ∧ 𝑔 ∈ (ℝ ↑𝑚
𝐼)) ∧ 𝑘 ∈ 𝐼) → (((𝑓‘𝑘) − (𝑔‘𝑘))↑2) ∈ V) |
55 | 46, 51, 52, 54 | fvmptd 6197 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑓 ∈ (ℝ ↑𝑚
𝐼) ∧ 𝑔 ∈ (ℝ ↑𝑚
𝐼)) ∧ 𝑘 ∈ 𝐼) → ((𝑥 ∈ 𝐼 ↦ (((𝑓‘𝑥) − (𝑔‘𝑥))↑2))‘𝑘) = (((𝑓‘𝑘) − (𝑔‘𝑘))↑2)) |
56 | 55 | sumeq2dv 14281 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑓 ∈ (ℝ ↑𝑚
𝐼) ∧ 𝑔 ∈ (ℝ ↑𝑚
𝐼)) → Σ𝑘 ∈ 𝐼 ((𝑥 ∈ 𝐼 ↦ (((𝑓‘𝑥) − (𝑔‘𝑥))↑2))‘𝑘) = Σ𝑘 ∈ 𝐼 (((𝑓‘𝑘) − (𝑔‘𝑘))↑2)) |
57 | 32, 45, 56 | 3eqtrd 2648 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑓 ∈ (ℝ ↑𝑚
𝐼) ∧ 𝑔 ∈ (ℝ ↑𝑚
𝐼)) →
(ℝfld Σg (𝑥 ∈ 𝐼 ↦ (((𝑓‘𝑥) − (𝑔‘𝑥))↑2))) = Σ𝑘 ∈ 𝐼 (((𝑓‘𝑘) − (𝑔‘𝑘))↑2)) |
58 | 57 | fveq2d 6107 |
. . . . 5
⊢ ((𝜑 ∧ 𝑓 ∈ (ℝ ↑𝑚
𝐼) ∧ 𝑔 ∈ (ℝ ↑𝑚
𝐼)) →
(√‘(ℝfld Σg (𝑥 ∈ 𝐼 ↦ (((𝑓‘𝑥) − (𝑔‘𝑥))↑2)))) = (√‘Σ𝑘 ∈ 𝐼 (((𝑓‘𝑘) − (𝑔‘𝑘))↑2))) |
59 | 7, 11, 16, 58 | syl3anc 1318 |
. . . 4
⊢ ((𝜑 ∧ (𝑓 ∈ (Base‘(ℝ^‘𝐼)) ∧ 𝑔 ∈ (Base‘(ℝ^‘𝐼)))) →
(√‘(ℝfld Σg (𝑥 ∈ 𝐼 ↦ (((𝑓‘𝑥) − (𝑔‘𝑥))↑2)))) = (√‘Σ𝑘 ∈ 𝐼 (((𝑓‘𝑘) − (𝑔‘𝑘))↑2))) |
60 | 5, 6, 59 | mpt2eq123dva 6614 |
. . 3
⊢ (𝜑 → (𝑓 ∈ (Base‘(ℝ^‘𝐼)), 𝑔 ∈ (Base‘(ℝ^‘𝐼)) ↦
(√‘(ℝfld Σg (𝑥 ∈ 𝐼 ↦ (((𝑓‘𝑥) − (𝑔‘𝑥))↑2))))) = (𝑓 ∈ (ℝ ↑𝑚
𝐼), 𝑔 ∈ (ℝ ↑𝑚
𝐼) ↦
(√‘Σ𝑘
∈ 𝐼 (((𝑓‘𝑘) − (𝑔‘𝑘))↑2)))) |
61 | 60 | fveq2d 6107 |
. 2
⊢ (𝜑 → (MetOpen‘(𝑓 ∈
(Base‘(ℝ^‘𝐼)), 𝑔 ∈ (Base‘(ℝ^‘𝐼)) ↦
(√‘(ℝfld Σg (𝑥 ∈ 𝐼 ↦ (((𝑓‘𝑥) − (𝑔‘𝑥))↑2)))))) = (MetOpen‘(𝑓 ∈ (ℝ
↑𝑚 𝐼), 𝑔 ∈ (ℝ ↑𝑚
𝐼) ↦
(√‘Σ𝑘
∈ 𝐼 (((𝑓‘𝑘) − (𝑔‘𝑘))↑2))))) |
62 | 2, 61 | eqtrd 2644 |
1
⊢ (𝜑 →
(TopOpen‘(ℝ^‘𝐼)) = (MetOpen‘(𝑓 ∈ (ℝ ↑𝑚
𝐼), 𝑔 ∈ (ℝ ↑𝑚
𝐼) ↦
(√‘Σ𝑘
∈ 𝐼 (((𝑓‘𝑘) − (𝑔‘𝑘))↑2))))) |