Step | Hyp | Ref
| Expression |
1 | | rrxtopnfi.1 |
. . 3
⊢ (𝜑 → 𝐼 ∈ Fin) |
2 | 1 | rrxtopn 43454 |
. 2
⊢ (𝜑 →
(TopOpen‘(ℝ^‘𝐼)) = (MetOpen‘(𝑓 ∈ (Base‘(ℝ^‘𝐼)), 𝑔 ∈ (Base‘(ℝ^‘𝐼)) ↦
(√‘(ℝfld Σg (𝑥 ∈ 𝐼 ↦ (((𝑓‘𝑥) − (𝑔‘𝑥))↑2))))))) |
3 | | eqid 2734 |
. . . . 5
⊢
(ℝ^‘𝐼) =
(ℝ^‘𝐼) |
4 | | eqid 2734 |
. . . . 5
⊢
(Base‘(ℝ^‘𝐼)) = (Base‘(ℝ^‘𝐼)) |
5 | 1, 3, 4 | rrxbasefi 24279 |
. . . 4
⊢ (𝜑 →
(Base‘(ℝ^‘𝐼)) = (ℝ ↑m 𝐼)) |
6 | 5 | adantr 484 |
. . . 4
⊢ ((𝜑 ∧ 𝑓 ∈ (Base‘(ℝ^‘𝐼))) →
(Base‘(ℝ^‘𝐼)) = (ℝ ↑m 𝐼)) |
7 | | simpl 486 |
. . . . 5
⊢ ((𝜑 ∧ (𝑓 ∈ (Base‘(ℝ^‘𝐼)) ∧ 𝑔 ∈ (Base‘(ℝ^‘𝐼)))) → 𝜑) |
8 | | simprl 771 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑓 ∈ (Base‘(ℝ^‘𝐼)) ∧ 𝑔 ∈ (Base‘(ℝ^‘𝐼)))) → 𝑓 ∈ (Base‘(ℝ^‘𝐼))) |
9 | | simpr 488 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑓 ∈ (Base‘(ℝ^‘𝐼))) → 𝑓 ∈ (Base‘(ℝ^‘𝐼))) |
10 | 9, 6 | eleqtrd 2836 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑓 ∈ (Base‘(ℝ^‘𝐼))) → 𝑓 ∈ (ℝ ↑m 𝐼)) |
11 | 8, 10 | syldan 594 |
. . . . 5
⊢ ((𝜑 ∧ (𝑓 ∈ (Base‘(ℝ^‘𝐼)) ∧ 𝑔 ∈ (Base‘(ℝ^‘𝐼)))) → 𝑓 ∈ (ℝ ↑m 𝐼)) |
12 | | simprr 773 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑓 ∈ (Base‘(ℝ^‘𝐼)) ∧ 𝑔 ∈ (Base‘(ℝ^‘𝐼)))) → 𝑔 ∈ (Base‘(ℝ^‘𝐼))) |
13 | | simpr 488 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑔 ∈ (Base‘(ℝ^‘𝐼))) → 𝑔 ∈ (Base‘(ℝ^‘𝐼))) |
14 | 5 | adantr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑔 ∈ (Base‘(ℝ^‘𝐼))) →
(Base‘(ℝ^‘𝐼)) = (ℝ ↑m 𝐼)) |
15 | 13, 14 | eleqtrd 2836 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑔 ∈ (Base‘(ℝ^‘𝐼))) → 𝑔 ∈ (ℝ ↑m 𝐼)) |
16 | 12, 15 | syldan 594 |
. . . . 5
⊢ ((𝜑 ∧ (𝑓 ∈ (Base‘(ℝ^‘𝐼)) ∧ 𝑔 ∈ (Base‘(ℝ^‘𝐼)))) → 𝑔 ∈ (ℝ ↑m 𝐼)) |
17 | | elmapi 8519 |
. . . . . . . . . . . . . 14
⊢ (𝑓 ∈ (ℝ
↑m 𝐼)
→ 𝑓:𝐼⟶ℝ) |
18 | 17 | adantr 484 |
. . . . . . . . . . . . 13
⊢ ((𝑓 ∈ (ℝ
↑m 𝐼) ∧
𝑔 ∈ (ℝ
↑m 𝐼))
→ 𝑓:𝐼⟶ℝ) |
19 | 18 | ffvelrnda 6893 |
. . . . . . . . . . . 12
⊢ (((𝑓 ∈ (ℝ
↑m 𝐼) ∧
𝑔 ∈ (ℝ
↑m 𝐼))
∧ 𝑥 ∈ 𝐼) → (𝑓‘𝑥) ∈ ℝ) |
20 | | elmapi 8519 |
. . . . . . . . . . . . . 14
⊢ (𝑔 ∈ (ℝ
↑m 𝐼)
→ 𝑔:𝐼⟶ℝ) |
21 | 20 | adantl 485 |
. . . . . . . . . . . . 13
⊢ ((𝑓 ∈ (ℝ
↑m 𝐼) ∧
𝑔 ∈ (ℝ
↑m 𝐼))
→ 𝑔:𝐼⟶ℝ) |
22 | 21 | ffvelrnda 6893 |
. . . . . . . . . . . 12
⊢ (((𝑓 ∈ (ℝ
↑m 𝐼) ∧
𝑔 ∈ (ℝ
↑m 𝐼))
∧ 𝑥 ∈ 𝐼) → (𝑔‘𝑥) ∈ ℝ) |
23 | 19, 22 | resubcld 11243 |
. . . . . . . . . . 11
⊢ (((𝑓 ∈ (ℝ
↑m 𝐼) ∧
𝑔 ∈ (ℝ
↑m 𝐼))
∧ 𝑥 ∈ 𝐼) → ((𝑓‘𝑥) − (𝑔‘𝑥)) ∈ ℝ) |
24 | 23 | resqcld 13800 |
. . . . . . . . . 10
⊢ (((𝑓 ∈ (ℝ
↑m 𝐼) ∧
𝑔 ∈ (ℝ
↑m 𝐼))
∧ 𝑥 ∈ 𝐼) → (((𝑓‘𝑥) − (𝑔‘𝑥))↑2) ∈ ℝ) |
25 | | eqid 2734 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝐼 ↦ (((𝑓‘𝑥) − (𝑔‘𝑥))↑2)) = (𝑥 ∈ 𝐼 ↦ (((𝑓‘𝑥) − (𝑔‘𝑥))↑2)) |
26 | 24, 25 | fmptd 6920 |
. . . . . . . . 9
⊢ ((𝑓 ∈ (ℝ
↑m 𝐼) ∧
𝑔 ∈ (ℝ
↑m 𝐼))
→ (𝑥 ∈ 𝐼 ↦ (((𝑓‘𝑥) − (𝑔‘𝑥))↑2)):𝐼⟶ℝ) |
27 | 26 | 3adant1 1132 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑓 ∈ (ℝ ↑m 𝐼) ∧ 𝑔 ∈ (ℝ ↑m 𝐼)) → (𝑥 ∈ 𝐼 ↦ (((𝑓‘𝑥) − (𝑔‘𝑥))↑2)):𝐼⟶ℝ) |
28 | 1 | 3ad2ant1 1135 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑓 ∈ (ℝ ↑m 𝐼) ∧ 𝑔 ∈ (ℝ ↑m 𝐼)) → 𝐼 ∈ Fin) |
29 | | 0red 10819 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑓 ∈ (ℝ ↑m 𝐼) ∧ 𝑔 ∈ (ℝ ↑m 𝐼)) → 0 ∈
ℝ) |
30 | 27, 28, 29 | fidmfisupp 42364 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑓 ∈ (ℝ ↑m 𝐼) ∧ 𝑔 ∈ (ℝ ↑m 𝐼)) → (𝑥 ∈ 𝐼 ↦ (((𝑓‘𝑥) − (𝑔‘𝑥))↑2)) finSupp 0) |
31 | | regsumsupp 20556 |
. . . . . . . 8
⊢ (((𝑥 ∈ 𝐼 ↦ (((𝑓‘𝑥) − (𝑔‘𝑥))↑2)):𝐼⟶ℝ ∧ (𝑥 ∈ 𝐼 ↦ (((𝑓‘𝑥) − (𝑔‘𝑥))↑2)) finSupp 0 ∧ 𝐼 ∈ Fin) → (ℝfld
Σg (𝑥 ∈ 𝐼 ↦ (((𝑓‘𝑥) − (𝑔‘𝑥))↑2))) = Σ𝑘 ∈ ((𝑥 ∈ 𝐼 ↦ (((𝑓‘𝑥) − (𝑔‘𝑥))↑2)) supp 0)((𝑥 ∈ 𝐼 ↦ (((𝑓‘𝑥) − (𝑔‘𝑥))↑2))‘𝑘)) |
32 | 27, 30, 28, 31 | syl3anc 1373 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑓 ∈ (ℝ ↑m 𝐼) ∧ 𝑔 ∈ (ℝ ↑m 𝐼)) → (ℝfld
Σg (𝑥 ∈ 𝐼 ↦ (((𝑓‘𝑥) − (𝑔‘𝑥))↑2))) = Σ𝑘 ∈ ((𝑥 ∈ 𝐼 ↦ (((𝑓‘𝑥) − (𝑔‘𝑥))↑2)) supp 0)((𝑥 ∈ 𝐼 ↦ (((𝑓‘𝑥) − (𝑔‘𝑥))↑2))‘𝑘)) |
33 | | ax-resscn 10769 |
. . . . . . . . . . . . . . 15
⊢ ℝ
⊆ ℂ |
34 | 33 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝑓 ∈ (ℝ
↑m 𝐼)
→ ℝ ⊆ ℂ) |
35 | 17, 34 | fssd 6552 |
. . . . . . . . . . . . 13
⊢ (𝑓 ∈ (ℝ
↑m 𝐼)
→ 𝑓:𝐼⟶ℂ) |
36 | 35 | 3ad2ant2 1136 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑓 ∈ (ℝ ↑m 𝐼) ∧ 𝑔 ∈ (ℝ ↑m 𝐼)) → 𝑓:𝐼⟶ℂ) |
37 | 36 | ffvelrnda 6893 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑓 ∈ (ℝ ↑m 𝐼) ∧ 𝑔 ∈ (ℝ ↑m 𝐼)) ∧ 𝑥 ∈ 𝐼) → (𝑓‘𝑥) ∈ ℂ) |
38 | 33 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝑔 ∈ (ℝ
↑m 𝐼)
→ ℝ ⊆ ℂ) |
39 | 20, 38 | fssd 6552 |
. . . . . . . . . . . . 13
⊢ (𝑔 ∈ (ℝ
↑m 𝐼)
→ 𝑔:𝐼⟶ℂ) |
40 | 39 | 3ad2ant3 1137 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑓 ∈ (ℝ ↑m 𝐼) ∧ 𝑔 ∈ (ℝ ↑m 𝐼)) → 𝑔:𝐼⟶ℂ) |
41 | 40 | ffvelrnda 6893 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑓 ∈ (ℝ ↑m 𝐼) ∧ 𝑔 ∈ (ℝ ↑m 𝐼)) ∧ 𝑥 ∈ 𝐼) → (𝑔‘𝑥) ∈ ℂ) |
42 | 37, 41 | subcld 11172 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑓 ∈ (ℝ ↑m 𝐼) ∧ 𝑔 ∈ (ℝ ↑m 𝐼)) ∧ 𝑥 ∈ 𝐼) → ((𝑓‘𝑥) − (𝑔‘𝑥)) ∈ ℂ) |
43 | 42 | sqcld 13697 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑓 ∈ (ℝ ↑m 𝐼) ∧ 𝑔 ∈ (ℝ ↑m 𝐼)) ∧ 𝑥 ∈ 𝐼) → (((𝑓‘𝑥) − (𝑔‘𝑥))↑2) ∈ ℂ) |
44 | 43, 25 | fmptd 6920 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑓 ∈ (ℝ ↑m 𝐼) ∧ 𝑔 ∈ (ℝ ↑m 𝐼)) → (𝑥 ∈ 𝐼 ↦ (((𝑓‘𝑥) − (𝑔‘𝑥))↑2)):𝐼⟶ℂ) |
45 | 28, 44 | fsumsupp0 42748 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑓 ∈ (ℝ ↑m 𝐼) ∧ 𝑔 ∈ (ℝ ↑m 𝐼)) → Σ𝑘 ∈ ((𝑥 ∈ 𝐼 ↦ (((𝑓‘𝑥) − (𝑔‘𝑥))↑2)) supp 0)((𝑥 ∈ 𝐼 ↦ (((𝑓‘𝑥) − (𝑔‘𝑥))↑2))‘𝑘) = Σ𝑘 ∈ 𝐼 ((𝑥 ∈ 𝐼 ↦ (((𝑓‘𝑥) − (𝑔‘𝑥))↑2))‘𝑘)) |
46 | | eqidd 2735 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑓 ∈ (ℝ ↑m 𝐼) ∧ 𝑔 ∈ (ℝ ↑m 𝐼)) ∧ 𝑘 ∈ 𝐼) → (𝑥 ∈ 𝐼 ↦ (((𝑓‘𝑥) − (𝑔‘𝑥))↑2)) = (𝑥 ∈ 𝐼 ↦ (((𝑓‘𝑥) − (𝑔‘𝑥))↑2))) |
47 | | fveq2 6706 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑘 → (𝑓‘𝑥) = (𝑓‘𝑘)) |
48 | | fveq2 6706 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑘 → (𝑔‘𝑥) = (𝑔‘𝑘)) |
49 | 47, 48 | oveq12d 7220 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑘 → ((𝑓‘𝑥) − (𝑔‘𝑥)) = ((𝑓‘𝑘) − (𝑔‘𝑘))) |
50 | 49 | oveq1d 7217 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑘 → (((𝑓‘𝑥) − (𝑔‘𝑥))↑2) = (((𝑓‘𝑘) − (𝑔‘𝑘))↑2)) |
51 | 50 | adantl 485 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑓 ∈ (ℝ ↑m 𝐼) ∧ 𝑔 ∈ (ℝ ↑m 𝐼)) ∧ 𝑘 ∈ 𝐼) ∧ 𝑥 = 𝑘) → (((𝑓‘𝑥) − (𝑔‘𝑥))↑2) = (((𝑓‘𝑘) − (𝑔‘𝑘))↑2)) |
52 | | simpr 488 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑓 ∈ (ℝ ↑m 𝐼) ∧ 𝑔 ∈ (ℝ ↑m 𝐼)) ∧ 𝑘 ∈ 𝐼) → 𝑘 ∈ 𝐼) |
53 | | ovexd 7237 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑓 ∈ (ℝ ↑m 𝐼) ∧ 𝑔 ∈ (ℝ ↑m 𝐼)) ∧ 𝑘 ∈ 𝐼) → (((𝑓‘𝑘) − (𝑔‘𝑘))↑2) ∈ V) |
54 | 46, 51, 52, 53 | fvmptd 6814 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑓 ∈ (ℝ ↑m 𝐼) ∧ 𝑔 ∈ (ℝ ↑m 𝐼)) ∧ 𝑘 ∈ 𝐼) → ((𝑥 ∈ 𝐼 ↦ (((𝑓‘𝑥) − (𝑔‘𝑥))↑2))‘𝑘) = (((𝑓‘𝑘) − (𝑔‘𝑘))↑2)) |
55 | 54 | sumeq2dv 15250 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑓 ∈ (ℝ ↑m 𝐼) ∧ 𝑔 ∈ (ℝ ↑m 𝐼)) → Σ𝑘 ∈ 𝐼 ((𝑥 ∈ 𝐼 ↦ (((𝑓‘𝑥) − (𝑔‘𝑥))↑2))‘𝑘) = Σ𝑘 ∈ 𝐼 (((𝑓‘𝑘) − (𝑔‘𝑘))↑2)) |
56 | 32, 45, 55 | 3eqtrd 2778 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑓 ∈ (ℝ ↑m 𝐼) ∧ 𝑔 ∈ (ℝ ↑m 𝐼)) → (ℝfld
Σg (𝑥 ∈ 𝐼 ↦ (((𝑓‘𝑥) − (𝑔‘𝑥))↑2))) = Σ𝑘 ∈ 𝐼 (((𝑓‘𝑘) − (𝑔‘𝑘))↑2)) |
57 | 56 | fveq2d 6710 |
. . . . 5
⊢ ((𝜑 ∧ 𝑓 ∈ (ℝ ↑m 𝐼) ∧ 𝑔 ∈ (ℝ ↑m 𝐼)) →
(√‘(ℝfld Σg (𝑥 ∈ 𝐼 ↦ (((𝑓‘𝑥) − (𝑔‘𝑥))↑2)))) = (√‘Σ𝑘 ∈ 𝐼 (((𝑓‘𝑘) − (𝑔‘𝑘))↑2))) |
58 | 7, 11, 16, 57 | syl3anc 1373 |
. . . 4
⊢ ((𝜑 ∧ (𝑓 ∈ (Base‘(ℝ^‘𝐼)) ∧ 𝑔 ∈ (Base‘(ℝ^‘𝐼)))) →
(√‘(ℝfld Σg (𝑥 ∈ 𝐼 ↦ (((𝑓‘𝑥) − (𝑔‘𝑥))↑2)))) = (√‘Σ𝑘 ∈ 𝐼 (((𝑓‘𝑘) − (𝑔‘𝑘))↑2))) |
59 | 5, 6, 58 | mpoeq123dva 7274 |
. . 3
⊢ (𝜑 → (𝑓 ∈ (Base‘(ℝ^‘𝐼)), 𝑔 ∈ (Base‘(ℝ^‘𝐼)) ↦
(√‘(ℝfld Σg (𝑥 ∈ 𝐼 ↦ (((𝑓‘𝑥) − (𝑔‘𝑥))↑2))))) = (𝑓 ∈ (ℝ ↑m 𝐼), 𝑔 ∈ (ℝ ↑m 𝐼) ↦
(√‘Σ𝑘
∈ 𝐼 (((𝑓‘𝑘) − (𝑔‘𝑘))↑2)))) |
60 | 59 | fveq2d 6710 |
. 2
⊢ (𝜑 → (MetOpen‘(𝑓 ∈
(Base‘(ℝ^‘𝐼)), 𝑔 ∈ (Base‘(ℝ^‘𝐼)) ↦
(√‘(ℝfld Σg (𝑥 ∈ 𝐼 ↦ (((𝑓‘𝑥) − (𝑔‘𝑥))↑2)))))) = (MetOpen‘(𝑓 ∈ (ℝ
↑m 𝐼),
𝑔 ∈ (ℝ
↑m 𝐼)
↦ (√‘Σ𝑘 ∈ 𝐼 (((𝑓‘𝑘) − (𝑔‘𝑘))↑2))))) |
61 | 2, 60 | eqtrd 2774 |
1
⊢ (𝜑 →
(TopOpen‘(ℝ^‘𝐼)) = (MetOpen‘(𝑓 ∈ (ℝ ↑m 𝐼), 𝑔 ∈ (ℝ ↑m 𝐼) ↦
(√‘Σ𝑘
∈ 𝐼 (((𝑓‘𝑘) − (𝑔‘𝑘))↑2))))) |