Step | Hyp | Ref
| Expression |
1 | | rrxval.r |
. . . 4
⊢ 𝐻 = (ℝ^‘𝐼) |
2 | 1 | rrxval 23175 |
. . 3
⊢ (𝐼 ∈ 𝑉 → 𝐻 =
(toℂHil‘(ℝfld freeLMod 𝐼))) |
3 | 2 | fveq2d 6195 |
. 2
⊢ (𝐼 ∈ 𝑉 → (dist‘𝐻) =
(dist‘(toℂHil‘(ℝfld freeLMod 𝐼)))) |
4 | | recrng 19967 |
. . . . 5
⊢
ℝfld ∈ *-Ring |
5 | | srngring 18852 |
. . . . 5
⊢
(ℝfld ∈ *-Ring → ℝfld ∈
Ring) |
6 | 4, 5 | ax-mp 5 |
. . . 4
⊢
ℝfld ∈ Ring |
7 | | eqid 2622 |
. . . . 5
⊢
(ℝfld freeLMod 𝐼) = (ℝfld freeLMod 𝐼) |
8 | 7 | frlmlmod 20093 |
. . . 4
⊢
((ℝfld ∈ Ring ∧ 𝐼 ∈ 𝑉) → (ℝfld freeLMod
𝐼) ∈
LMod) |
9 | 6, 8 | mpan 706 |
. . 3
⊢ (𝐼 ∈ 𝑉 → (ℝfld freeLMod
𝐼) ∈
LMod) |
10 | | lmodgrp 18870 |
. . 3
⊢
((ℝfld freeLMod 𝐼) ∈ LMod → (ℝfld
freeLMod 𝐼) ∈
Grp) |
11 | | eqid 2622 |
. . . 4
⊢
(toℂHil‘(ℝfld freeLMod 𝐼)) =
(toℂHil‘(ℝfld freeLMod 𝐼)) |
12 | | eqid 2622 |
. . . 4
⊢
(norm‘(toℂHil‘(ℝfld freeLMod 𝐼))) =
(norm‘(toℂHil‘(ℝfld freeLMod 𝐼))) |
13 | | eqid 2622 |
. . . 4
⊢
(-g‘(ℝfld freeLMod 𝐼)) =
(-g‘(ℝfld freeLMod 𝐼)) |
14 | 11, 12, 13 | tchds 23030 |
. . 3
⊢
((ℝfld freeLMod 𝐼) ∈ Grp →
((norm‘(toℂHil‘(ℝfld freeLMod 𝐼))) ∘
(-g‘(ℝfld freeLMod 𝐼))) =
(dist‘(toℂHil‘(ℝfld freeLMod 𝐼)))) |
15 | 9, 10, 14 | 3syl 18 |
. 2
⊢ (𝐼 ∈ 𝑉 →
((norm‘(toℂHil‘(ℝfld freeLMod 𝐼))) ∘
(-g‘(ℝfld freeLMod 𝐼))) =
(dist‘(toℂHil‘(ℝfld freeLMod 𝐼)))) |
16 | | eqid 2622 |
. . . . . . . 8
⊢
(Base‘(ℝfld freeLMod 𝐼)) = (Base‘(ℝfld
freeLMod 𝐼)) |
17 | 16, 13 | grpsubf 17494 |
. . . . . . 7
⊢
((ℝfld freeLMod 𝐼) ∈ Grp →
(-g‘(ℝfld freeLMod 𝐼)):((Base‘(ℝfld
freeLMod 𝐼)) ×
(Base‘(ℝfld freeLMod 𝐼)))⟶(Base‘(ℝfld
freeLMod 𝐼))) |
18 | 9, 10, 17 | 3syl 18 |
. . . . . 6
⊢ (𝐼 ∈ 𝑉 →
(-g‘(ℝfld freeLMod 𝐼)):((Base‘(ℝfld
freeLMod 𝐼)) ×
(Base‘(ℝfld freeLMod 𝐼)))⟶(Base‘(ℝfld
freeLMod 𝐼))) |
19 | | rrxbase.b |
. . . . . . . . . 10
⊢ 𝐵 = (Base‘𝐻) |
20 | 1, 19 | rrxbase 23176 |
. . . . . . . . 9
⊢ (𝐼 ∈ 𝑉 → 𝐵 = {ℎ ∈ (ℝ ↑𝑚
𝐼) ∣ ℎ finSupp 0}) |
21 | | rebase 19952 |
. . . . . . . . . . 11
⊢ ℝ =
(Base‘ℝfld) |
22 | | re0g 19958 |
. . . . . . . . . . 11
⊢ 0 =
(0g‘ℝfld) |
23 | | eqid 2622 |
. . . . . . . . . . 11
⊢ {ℎ ∈ (ℝ
↑𝑚 𝐼) ∣ ℎ finSupp 0} = {ℎ ∈ (ℝ ↑𝑚
𝐼) ∣ ℎ finSupp 0} |
24 | 7, 21, 22, 23 | frlmbas 20099 |
. . . . . . . . . 10
⊢
((ℝfld ∈ Ring ∧ 𝐼 ∈ 𝑉) → {ℎ ∈ (ℝ ↑𝑚
𝐼) ∣ ℎ finSupp 0} =
(Base‘(ℝfld freeLMod 𝐼))) |
25 | 6, 24 | mpan 706 |
. . . . . . . . 9
⊢ (𝐼 ∈ 𝑉 → {ℎ ∈ (ℝ ↑𝑚
𝐼) ∣ ℎ finSupp 0} =
(Base‘(ℝfld freeLMod 𝐼))) |
26 | 20, 25 | eqtrd 2656 |
. . . . . . . 8
⊢ (𝐼 ∈ 𝑉 → 𝐵 = (Base‘(ℝfld
freeLMod 𝐼))) |
27 | 26 | sqxpeqd 5141 |
. . . . . . 7
⊢ (𝐼 ∈ 𝑉 → (𝐵 × 𝐵) = ((Base‘(ℝfld
freeLMod 𝐼)) ×
(Base‘(ℝfld freeLMod 𝐼)))) |
28 | 27, 26 | feq23d 6040 |
. . . . . 6
⊢ (𝐼 ∈ 𝑉 →
((-g‘(ℝfld freeLMod 𝐼)):(𝐵 × 𝐵)⟶𝐵 ↔
(-g‘(ℝfld freeLMod 𝐼)):((Base‘(ℝfld
freeLMod 𝐼)) ×
(Base‘(ℝfld freeLMod 𝐼)))⟶(Base‘(ℝfld
freeLMod 𝐼)))) |
29 | 18, 28 | mpbird 247 |
. . . . 5
⊢ (𝐼 ∈ 𝑉 →
(-g‘(ℝfld freeLMod 𝐼)):(𝐵 × 𝐵)⟶𝐵) |
30 | 29 | fovrnda 6805 |
. . . 4
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → (𝑓(-g‘(ℝfld
freeLMod 𝐼))𝑔) ∈ 𝐵) |
31 | | ffn 6045 |
. . . . . 6
⊢
((-g‘(ℝfld freeLMod 𝐼)):(𝐵 × 𝐵)⟶𝐵 →
(-g‘(ℝfld freeLMod 𝐼)) Fn (𝐵 × 𝐵)) |
32 | 29, 31 | syl 17 |
. . . . 5
⊢ (𝐼 ∈ 𝑉 →
(-g‘(ℝfld freeLMod 𝐼)) Fn (𝐵 × 𝐵)) |
33 | | fnov 6768 |
. . . . 5
⊢
((-g‘(ℝfld freeLMod 𝐼)) Fn (𝐵 × 𝐵) ↔
(-g‘(ℝfld freeLMod 𝐼)) = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑓(-g‘(ℝfld
freeLMod 𝐼))𝑔))) |
34 | 32, 33 | sylib 208 |
. . . 4
⊢ (𝐼 ∈ 𝑉 →
(-g‘(ℝfld freeLMod 𝐼)) = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑓(-g‘(ℝfld
freeLMod 𝐼))𝑔))) |
35 | 1, 19 | rrxnm 23179 |
. . . . 5
⊢ (𝐼 ∈ 𝑉 → (ℎ ∈ 𝐵 ↦
(√‘(ℝfld Σg (𝑥 ∈ 𝐼 ↦ ((ℎ‘𝑥)↑2))))) = (norm‘𝐻)) |
36 | 2 | fveq2d 6195 |
. . . . 5
⊢ (𝐼 ∈ 𝑉 → (norm‘𝐻) =
(norm‘(toℂHil‘(ℝfld freeLMod 𝐼)))) |
37 | 35, 36 | eqtr2d 2657 |
. . . 4
⊢ (𝐼 ∈ 𝑉 →
(norm‘(toℂHil‘(ℝfld freeLMod 𝐼))) = (ℎ ∈ 𝐵 ↦
(√‘(ℝfld Σg (𝑥 ∈ 𝐼 ↦ ((ℎ‘𝑥)↑2)))))) |
38 | | fveq1 6190 |
. . . . . . . 8
⊢ (ℎ = (𝑓(-g‘(ℝfld
freeLMod 𝐼))𝑔) → (ℎ‘𝑥) = ((𝑓(-g‘(ℝfld
freeLMod 𝐼))𝑔)‘𝑥)) |
39 | 38 | oveq1d 6665 |
. . . . . . 7
⊢ (ℎ = (𝑓(-g‘(ℝfld
freeLMod 𝐼))𝑔) → ((ℎ‘𝑥)↑2) = (((𝑓(-g‘(ℝfld
freeLMod 𝐼))𝑔)‘𝑥)↑2)) |
40 | 39 | mpteq2dv 4745 |
. . . . . 6
⊢ (ℎ = (𝑓(-g‘(ℝfld
freeLMod 𝐼))𝑔) → (𝑥 ∈ 𝐼 ↦ ((ℎ‘𝑥)↑2)) = (𝑥 ∈ 𝐼 ↦ (((𝑓(-g‘(ℝfld
freeLMod 𝐼))𝑔)‘𝑥)↑2))) |
41 | 40 | oveq2d 6666 |
. . . . 5
⊢ (ℎ = (𝑓(-g‘(ℝfld
freeLMod 𝐼))𝑔) → (ℝfld
Σg (𝑥 ∈ 𝐼 ↦ ((ℎ‘𝑥)↑2))) = (ℝfld
Σg (𝑥 ∈ 𝐼 ↦ (((𝑓(-g‘(ℝfld
freeLMod 𝐼))𝑔)‘𝑥)↑2)))) |
42 | 41 | fveq2d 6195 |
. . . 4
⊢ (ℎ = (𝑓(-g‘(ℝfld
freeLMod 𝐼))𝑔) →
(√‘(ℝfld Σg (𝑥 ∈ 𝐼 ↦ ((ℎ‘𝑥)↑2)))) =
(√‘(ℝfld Σg (𝑥 ∈ 𝐼 ↦ (((𝑓(-g‘(ℝfld
freeLMod 𝐼))𝑔)‘𝑥)↑2))))) |
43 | 30, 34, 37, 42 | fmpt2co 7260 |
. . 3
⊢ (𝐼 ∈ 𝑉 →
((norm‘(toℂHil‘(ℝfld freeLMod 𝐼))) ∘
(-g‘(ℝfld freeLMod 𝐼))) = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦
(√‘(ℝfld Σg (𝑥 ∈ 𝐼 ↦ (((𝑓(-g‘(ℝfld
freeLMod 𝐼))𝑔)‘𝑥)↑2)))))) |
44 | | simp1 1061 |
. . . . . . . . . . . . . 14
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵) → 𝐼 ∈ 𝑉) |
45 | | simprl 794 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → 𝑓 ∈ 𝐵) |
46 | 26 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → 𝐵 = (Base‘(ℝfld
freeLMod 𝐼))) |
47 | 45, 46 | eleqtrd 2703 |
. . . . . . . . . . . . . . 15
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) |
48 | 47 | 3impb 1260 |
. . . . . . . . . . . . . 14
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵) → 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) |
49 | 7, 21, 16 | frlmbasmap 20103 |
. . . . . . . . . . . . . 14
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) → 𝑓 ∈ (ℝ
↑𝑚 𝐼)) |
50 | 44, 48, 49 | syl2anc 693 |
. . . . . . . . . . . . 13
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵) → 𝑓 ∈ (ℝ ↑𝑚
𝐼)) |
51 | | elmapi 7879 |
. . . . . . . . . . . . 13
⊢ (𝑓 ∈ (ℝ
↑𝑚 𝐼) → 𝑓:𝐼⟶ℝ) |
52 | 50, 51 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵) → 𝑓:𝐼⟶ℝ) |
53 | | ffn 6045 |
. . . . . . . . . . . 12
⊢ (𝑓:𝐼⟶ℝ → 𝑓 Fn 𝐼) |
54 | 52, 53 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵) → 𝑓 Fn 𝐼) |
55 | | simprr 796 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → 𝑔 ∈ 𝐵) |
56 | 55, 46 | eleqtrd 2703 |
. . . . . . . . . . . . . . 15
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → 𝑔 ∈ (Base‘(ℝfld
freeLMod 𝐼))) |
57 | 56 | 3impb 1260 |
. . . . . . . . . . . . . 14
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵) → 𝑔 ∈ (Base‘(ℝfld
freeLMod 𝐼))) |
58 | 7, 21, 16 | frlmbasmap 20103 |
. . . . . . . . . . . . . 14
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑔 ∈ (Base‘(ℝfld
freeLMod 𝐼))) → 𝑔 ∈ (ℝ
↑𝑚 𝐼)) |
59 | 44, 57, 58 | syl2anc 693 |
. . . . . . . . . . . . 13
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵) → 𝑔 ∈ (ℝ ↑𝑚
𝐼)) |
60 | | elmapi 7879 |
. . . . . . . . . . . . 13
⊢ (𝑔 ∈ (ℝ
↑𝑚 𝐼) → 𝑔:𝐼⟶ℝ) |
61 | 59, 60 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵) → 𝑔:𝐼⟶ℝ) |
62 | | ffn 6045 |
. . . . . . . . . . . 12
⊢ (𝑔:𝐼⟶ℝ → 𝑔 Fn 𝐼) |
63 | 61, 62 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵) → 𝑔 Fn 𝐼) |
64 | | inidm 3822 |
. . . . . . . . . . 11
⊢ (𝐼 ∩ 𝐼) = 𝐼 |
65 | | eqidd 2623 |
. . . . . . . . . . 11
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵) ∧ 𝑥 ∈ 𝐼) → (𝑓‘𝑥) = (𝑓‘𝑥)) |
66 | | eqidd 2623 |
. . . . . . . . . . 11
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵) ∧ 𝑥 ∈ 𝐼) → (𝑔‘𝑥) = (𝑔‘𝑥)) |
67 | 54, 63, 44, 44, 64, 65, 66 | offval 6904 |
. . . . . . . . . 10
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵) → (𝑓 ∘𝑓
(-g‘ℝfld)𝑔) = (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(-g‘ℝfld)(𝑔‘𝑥)))) |
68 | 6 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → ℝfld ∈
Ring) |
69 | | simpl 473 |
. . . . . . . . . . . 12
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → 𝐼 ∈ 𝑉) |
70 | | eqid 2622 |
. . . . . . . . . . . 12
⊢
(-g‘ℝfld) =
(-g‘ℝfld) |
71 | 7, 16, 68, 69, 47, 56, 70, 13 | frlmsubgval 20108 |
. . . . . . . . . . 11
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → (𝑓(-g‘(ℝfld
freeLMod 𝐼))𝑔) = (𝑓 ∘𝑓
(-g‘ℝfld)𝑔)) |
72 | 71 | 3impb 1260 |
. . . . . . . . . 10
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵) → (𝑓(-g‘(ℝfld
freeLMod 𝐼))𝑔) = (𝑓 ∘𝑓
(-g‘ℝfld)𝑔)) |
73 | 52 | ffvelrnda 6359 |
. . . . . . . . . . . 12
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵) ∧ 𝑥 ∈ 𝐼) → (𝑓‘𝑥) ∈ ℝ) |
74 | 61 | ffvelrnda 6359 |
. . . . . . . . . . . 12
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵) ∧ 𝑥 ∈ 𝐼) → (𝑔‘𝑥) ∈ ℝ) |
75 | 70 | resubgval 19955 |
. . . . . . . . . . . 12
⊢ (((𝑓‘𝑥) ∈ ℝ ∧ (𝑔‘𝑥) ∈ ℝ) → ((𝑓‘𝑥) − (𝑔‘𝑥)) = ((𝑓‘𝑥)(-g‘ℝfld)(𝑔‘𝑥))) |
76 | 73, 74, 75 | syl2anc 693 |
. . . . . . . . . . 11
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵) ∧ 𝑥 ∈ 𝐼) → ((𝑓‘𝑥) − (𝑔‘𝑥)) = ((𝑓‘𝑥)(-g‘ℝfld)(𝑔‘𝑥))) |
77 | 76 | mpteq2dva 4744 |
. . . . . . . . . 10
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵) → (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥) − (𝑔‘𝑥))) = (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(-g‘ℝfld)(𝑔‘𝑥)))) |
78 | 67, 72, 77 | 3eqtr4d 2666 |
. . . . . . . . 9
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵) → (𝑓(-g‘(ℝfld
freeLMod 𝐼))𝑔) = (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥) − (𝑔‘𝑥)))) |
79 | 73, 74 | resubcld 10458 |
. . . . . . . . 9
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵) ∧ 𝑥 ∈ 𝐼) → ((𝑓‘𝑥) − (𝑔‘𝑥)) ∈ ℝ) |
80 | 78, 79 | fvmpt2d 6293 |
. . . . . . . 8
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵) ∧ 𝑥 ∈ 𝐼) → ((𝑓(-g‘(ℝfld
freeLMod 𝐼))𝑔)‘𝑥) = ((𝑓‘𝑥) − (𝑔‘𝑥))) |
81 | 80 | oveq1d 6665 |
. . . . . . 7
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵) ∧ 𝑥 ∈ 𝐼) → (((𝑓(-g‘(ℝfld
freeLMod 𝐼))𝑔)‘𝑥)↑2) = (((𝑓‘𝑥) − (𝑔‘𝑥))↑2)) |
82 | 81 | mpteq2dva 4744 |
. . . . . 6
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵) → (𝑥 ∈ 𝐼 ↦ (((𝑓(-g‘(ℝfld
freeLMod 𝐼))𝑔)‘𝑥)↑2)) = (𝑥 ∈ 𝐼 ↦ (((𝑓‘𝑥) − (𝑔‘𝑥))↑2))) |
83 | 82 | oveq2d 6666 |
. . . . 5
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵) → (ℝfld
Σg (𝑥 ∈ 𝐼 ↦ (((𝑓(-g‘(ℝfld
freeLMod 𝐼))𝑔)‘𝑥)↑2))) = (ℝfld
Σg (𝑥 ∈ 𝐼 ↦ (((𝑓‘𝑥) − (𝑔‘𝑥))↑2)))) |
84 | 83 | fveq2d 6195 |
. . . 4
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵) →
(√‘(ℝfld Σg (𝑥 ∈ 𝐼 ↦ (((𝑓(-g‘(ℝfld
freeLMod 𝐼))𝑔)‘𝑥)↑2)))) =
(√‘(ℝfld Σg (𝑥 ∈ 𝐼 ↦ (((𝑓‘𝑥) − (𝑔‘𝑥))↑2))))) |
85 | 84 | mpt2eq3dva 6719 |
. . 3
⊢ (𝐼 ∈ 𝑉 → (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦
(√‘(ℝfld Σg (𝑥 ∈ 𝐼 ↦ (((𝑓(-g‘(ℝfld
freeLMod 𝐼))𝑔)‘𝑥)↑2))))) = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦
(√‘(ℝfld Σg (𝑥 ∈ 𝐼 ↦ (((𝑓‘𝑥) − (𝑔‘𝑥))↑2)))))) |
86 | 43, 85 | eqtrd 2656 |
. 2
⊢ (𝐼 ∈ 𝑉 →
((norm‘(toℂHil‘(ℝfld freeLMod 𝐼))) ∘
(-g‘(ℝfld freeLMod 𝐼))) = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦
(√‘(ℝfld Σg (𝑥 ∈ 𝐼 ↦ (((𝑓‘𝑥) − (𝑔‘𝑥))↑2)))))) |
87 | 3, 15, 86 | 3eqtr2rd 2663 |
1
⊢ (𝐼 ∈ 𝑉 → (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦
(√‘(ℝfld Σg (𝑥 ∈ 𝐼 ↦ (((𝑓‘𝑥) − (𝑔‘𝑥))↑2))))) = (dist‘𝐻)) |