| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | rrxval.r | . . . 4
⊢ 𝐻 = (ℝ^‘𝐼) | 
| 2 | 1 | rrxval 25421 | . . 3
⊢ (𝐼 ∈ 𝑉 → 𝐻 =
(toℂPreHil‘(ℝfld freeLMod 𝐼))) | 
| 3 | 2 | fveq2d 6910 | . 2
⊢ (𝐼 ∈ 𝑉 → (dist‘𝐻) =
(dist‘(toℂPreHil‘(ℝfld freeLMod 𝐼)))) | 
| 4 |  | resrng 21639 | . . . . 5
⊢
ℝfld ∈ *-Ring | 
| 5 |  | srngring 20847 | . . . . 5
⊢
(ℝfld ∈ *-Ring → ℝfld ∈
Ring) | 
| 6 | 4, 5 | ax-mp 5 | . . . 4
⊢
ℝfld ∈ Ring | 
| 7 |  | eqid 2737 | . . . . 5
⊢
(ℝfld freeLMod 𝐼) = (ℝfld freeLMod 𝐼) | 
| 8 | 7 | frlmlmod 21769 | . . . 4
⊢
((ℝfld ∈ Ring ∧ 𝐼 ∈ 𝑉) → (ℝfld freeLMod
𝐼) ∈
LMod) | 
| 9 | 6, 8 | mpan 690 | . . 3
⊢ (𝐼 ∈ 𝑉 → (ℝfld freeLMod
𝐼) ∈
LMod) | 
| 10 |  | lmodgrp 20865 | . . 3
⊢
((ℝfld freeLMod 𝐼) ∈ LMod → (ℝfld
freeLMod 𝐼) ∈
Grp) | 
| 11 |  | eqid 2737 | . . . 4
⊢
(toℂPreHil‘(ℝfld freeLMod 𝐼)) =
(toℂPreHil‘(ℝfld freeLMod 𝐼)) | 
| 12 |  | eqid 2737 | . . . 4
⊢
(norm‘(toℂPreHil‘(ℝfld freeLMod 𝐼))) =
(norm‘(toℂPreHil‘(ℝfld freeLMod 𝐼))) | 
| 13 |  | eqid 2737 | . . . 4
⊢
(-g‘(ℝfld freeLMod 𝐼)) =
(-g‘(ℝfld freeLMod 𝐼)) | 
| 14 | 11, 12, 13 | tcphds 25265 | . . 3
⊢
((ℝfld freeLMod 𝐼) ∈ Grp →
((norm‘(toℂPreHil‘(ℝfld freeLMod 𝐼))) ∘
(-g‘(ℝfld freeLMod 𝐼))) =
(dist‘(toℂPreHil‘(ℝfld freeLMod 𝐼)))) | 
| 15 | 9, 10, 14 | 3syl 18 | . 2
⊢ (𝐼 ∈ 𝑉 →
((norm‘(toℂPreHil‘(ℝfld freeLMod 𝐼))) ∘
(-g‘(ℝfld freeLMod 𝐼))) =
(dist‘(toℂPreHil‘(ℝfld freeLMod 𝐼)))) | 
| 16 |  | eqid 2737 | . . . . . . . 8
⊢
(Base‘(ℝfld freeLMod 𝐼)) = (Base‘(ℝfld
freeLMod 𝐼)) | 
| 17 | 16, 13 | grpsubf 19037 | . . . . . . 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 25422 | . . . . . . . . 9
⊢ (𝐼 ∈ 𝑉 → 𝐵 = {ℎ ∈ (ℝ ↑m 𝐼) ∣ ℎ finSupp 0}) | 
| 21 |  | rebase 21624 | . . . . . . . . . . 11
⊢ ℝ =
(Base‘ℝfld) | 
| 22 |  | re0g 21630 | . . . . . . . . . . 11
⊢ 0 =
(0g‘ℝfld) | 
| 23 |  | eqid 2737 | . . . . . . . . . . 11
⊢ {ℎ ∈ (ℝ
↑m 𝐼)
∣ ℎ finSupp 0} =
{ℎ ∈ (ℝ
↑m 𝐼)
∣ ℎ finSupp
0} | 
| 24 | 7, 21, 22, 23 | frlmbas 21775 | . . . . . . . . . 10
⊢
((ℝfld ∈ Ring ∧ 𝐼 ∈ 𝑉) → {ℎ ∈ (ℝ ↑m 𝐼) ∣ ℎ finSupp 0} =
(Base‘(ℝfld freeLMod 𝐼))) | 
| 25 | 6, 24 | mpan 690 | . . . . . . . . 9
⊢ (𝐼 ∈ 𝑉 → {ℎ ∈ (ℝ ↑m 𝐼) ∣ ℎ finSupp 0} =
(Base‘(ℝfld freeLMod 𝐼))) | 
| 26 | 20, 25 | eqtrd 2777 | . . . . . . . 8
⊢ (𝐼 ∈ 𝑉 → 𝐵 = (Base‘(ℝfld
freeLMod 𝐼))) | 
| 27 | 26 | sqxpeqd 5717 | . . . . . . 7
⊢ (𝐼 ∈ 𝑉 → (𝐵 × 𝐵) = ((Base‘(ℝfld
freeLMod 𝐼)) ×
(Base‘(ℝfld freeLMod 𝐼)))) | 
| 28 | 27, 26 | feq23d 6731 | . . . . . 6
⊢ (𝐼 ∈ 𝑉 →
((-g‘(ℝfld freeLMod 𝐼)):(𝐵 × 𝐵)⟶𝐵 ↔
(-g‘(ℝfld freeLMod 𝐼)):((Base‘(ℝfld
freeLMod 𝐼)) ×
(Base‘(ℝfld freeLMod 𝐼)))⟶(Base‘(ℝfld
freeLMod 𝐼)))) | 
| 29 | 18, 28 | mpbird 257 | . . . . 5
⊢ (𝐼 ∈ 𝑉 →
(-g‘(ℝfld freeLMod 𝐼)):(𝐵 × 𝐵)⟶𝐵) | 
| 30 | 29 | fovcdmda 7604 | . . . 4
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → (𝑓(-g‘(ℝfld
freeLMod 𝐼))𝑔) ∈ 𝐵) | 
| 31 | 29 | ffnd 6737 | . . . . 5
⊢ (𝐼 ∈ 𝑉 →
(-g‘(ℝfld freeLMod 𝐼)) Fn (𝐵 × 𝐵)) | 
| 32 |  | fnov 7564 | . . . . 5
⊢
((-g‘(ℝfld freeLMod 𝐼)) Fn (𝐵 × 𝐵) ↔
(-g‘(ℝfld freeLMod 𝐼)) = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑓(-g‘(ℝfld
freeLMod 𝐼))𝑔))) | 
| 33 | 31, 32 | sylib 218 | . . . 4
⊢ (𝐼 ∈ 𝑉 →
(-g‘(ℝfld freeLMod 𝐼)) = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑓(-g‘(ℝfld
freeLMod 𝐼))𝑔))) | 
| 34 | 1, 19 | rrxnm 25425 | . . . . 5
⊢ (𝐼 ∈ 𝑉 → (ℎ ∈ 𝐵 ↦
(√‘(ℝfld Σg (𝑥 ∈ 𝐼 ↦ ((ℎ‘𝑥)↑2))))) = (norm‘𝐻)) | 
| 35 | 2 | fveq2d 6910 | . . . . 5
⊢ (𝐼 ∈ 𝑉 → (norm‘𝐻) =
(norm‘(toℂPreHil‘(ℝfld freeLMod 𝐼)))) | 
| 36 | 34, 35 | eqtr2d 2778 | . . . 4
⊢ (𝐼 ∈ 𝑉 →
(norm‘(toℂPreHil‘(ℝfld freeLMod 𝐼))) = (ℎ ∈ 𝐵 ↦
(√‘(ℝfld Σg (𝑥 ∈ 𝐼 ↦ ((ℎ‘𝑥)↑2)))))) | 
| 37 |  | fveq1 6905 | . . . . . . . 8
⊢ (ℎ = (𝑓(-g‘(ℝfld
freeLMod 𝐼))𝑔) → (ℎ‘𝑥) = ((𝑓(-g‘(ℝfld
freeLMod 𝐼))𝑔)‘𝑥)) | 
| 38 | 37 | oveq1d 7446 | . . . . . . 7
⊢ (ℎ = (𝑓(-g‘(ℝfld
freeLMod 𝐼))𝑔) → ((ℎ‘𝑥)↑2) = (((𝑓(-g‘(ℝfld
freeLMod 𝐼))𝑔)‘𝑥)↑2)) | 
| 39 | 38 | mpteq2dv 5244 | . . . . . 6
⊢ (ℎ = (𝑓(-g‘(ℝfld
freeLMod 𝐼))𝑔) → (𝑥 ∈ 𝐼 ↦ ((ℎ‘𝑥)↑2)) = (𝑥 ∈ 𝐼 ↦ (((𝑓(-g‘(ℝfld
freeLMod 𝐼))𝑔)‘𝑥)↑2))) | 
| 40 | 39 | oveq2d 7447 | . . . . 5
⊢ (ℎ = (𝑓(-g‘(ℝfld
freeLMod 𝐼))𝑔) → (ℝfld
Σg (𝑥 ∈ 𝐼 ↦ ((ℎ‘𝑥)↑2))) = (ℝfld
Σg (𝑥 ∈ 𝐼 ↦ (((𝑓(-g‘(ℝfld
freeLMod 𝐼))𝑔)‘𝑥)↑2)))) | 
| 41 | 40 | fveq2d 6910 | . . . 4
⊢ (ℎ = (𝑓(-g‘(ℝfld
freeLMod 𝐼))𝑔) →
(√‘(ℝfld Σg (𝑥 ∈ 𝐼 ↦ ((ℎ‘𝑥)↑2)))) =
(√‘(ℝfld Σg (𝑥 ∈ 𝐼 ↦ (((𝑓(-g‘(ℝfld
freeLMod 𝐼))𝑔)‘𝑥)↑2))))) | 
| 42 | 30, 33, 36, 41 | fmpoco 8120 | . . 3
⊢ (𝐼 ∈ 𝑉 →
((norm‘(toℂPreHil‘(ℝfld freeLMod 𝐼))) ∘
(-g‘(ℝfld freeLMod 𝐼))) = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦
(√‘(ℝfld Σg (𝑥 ∈ 𝐼 ↦ (((𝑓(-g‘(ℝfld
freeLMod 𝐼))𝑔)‘𝑥)↑2)))))) | 
| 43 |  | simp1 1137 | . . . . . . . . . . . . . 14
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵) → 𝐼 ∈ 𝑉) | 
| 44 |  | simprl 771 | . . . . . . . . . . . . . . . 16
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → 𝑓 ∈ 𝐵) | 
| 45 | 26 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → 𝐵 = (Base‘(ℝfld
freeLMod 𝐼))) | 
| 46 | 44, 45 | eleqtrd 2843 | . . . . . . . . . . . . . . 15
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) | 
| 47 | 46 | 3impb 1115 | . . . . . . . . . . . . . 14
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵) → 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) | 
| 48 | 7, 21, 16 | frlmbasmap 21779 | . . . . . . . . . . . . . 14
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) → 𝑓 ∈ (ℝ
↑m 𝐼)) | 
| 49 | 43, 47, 48 | syl2anc 584 | . . . . . . . . . . . . 13
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵) → 𝑓 ∈ (ℝ ↑m 𝐼)) | 
| 50 |  | elmapi 8889 | . . . . . . . . . . . . 13
⊢ (𝑓 ∈ (ℝ
↑m 𝐼)
→ 𝑓:𝐼⟶ℝ) | 
| 51 | 49, 50 | syl 17 | . . . . . . . . . . . 12
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵) → 𝑓:𝐼⟶ℝ) | 
| 52 | 51 | ffnd 6737 | . . . . . . . . . . 11
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵) → 𝑓 Fn 𝐼) | 
| 53 |  | simprr 773 | . . . . . . . . . . . . . . . 16
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → 𝑔 ∈ 𝐵) | 
| 54 | 53, 45 | eleqtrd 2843 | . . . . . . . . . . . . . . 15
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → 𝑔 ∈ (Base‘(ℝfld
freeLMod 𝐼))) | 
| 55 | 54 | 3impb 1115 | . . . . . . . . . . . . . 14
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵) → 𝑔 ∈ (Base‘(ℝfld
freeLMod 𝐼))) | 
| 56 | 7, 21, 16 | frlmbasmap 21779 | . . . . . . . . . . . . . 14
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑔 ∈ (Base‘(ℝfld
freeLMod 𝐼))) → 𝑔 ∈ (ℝ
↑m 𝐼)) | 
| 57 | 43, 55, 56 | syl2anc 584 | . . . . . . . . . . . . 13
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵) → 𝑔 ∈ (ℝ ↑m 𝐼)) | 
| 58 |  | elmapi 8889 | . . . . . . . . . . . . 13
⊢ (𝑔 ∈ (ℝ
↑m 𝐼)
→ 𝑔:𝐼⟶ℝ) | 
| 59 | 57, 58 | syl 17 | . . . . . . . . . . . 12
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵) → 𝑔:𝐼⟶ℝ) | 
| 60 | 59 | ffnd 6737 | . . . . . . . . . . 11
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵) → 𝑔 Fn 𝐼) | 
| 61 |  | inidm 4227 | . . . . . . . . . . 11
⊢ (𝐼 ∩ 𝐼) = 𝐼 | 
| 62 |  | eqidd 2738 | . . . . . . . . . . 11
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵) ∧ 𝑥 ∈ 𝐼) → (𝑓‘𝑥) = (𝑓‘𝑥)) | 
| 63 |  | eqidd 2738 | . . . . . . . . . . 11
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵) ∧ 𝑥 ∈ 𝐼) → (𝑔‘𝑥) = (𝑔‘𝑥)) | 
| 64 | 52, 60, 43, 43, 61, 62, 63 | offval 7706 | . . . . . . . . . 10
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵) → (𝑓 ∘f
(-g‘ℝfld)𝑔) = (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(-g‘ℝfld)(𝑔‘𝑥)))) | 
| 65 | 6 | a1i 11 | . . . . . . . . . . . 12
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → ℝfld ∈
Ring) | 
| 66 |  | simpl 482 | . . . . . . . . . . . 12
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → 𝐼 ∈ 𝑉) | 
| 67 |  | eqid 2737 | . . . . . . . . . . . 12
⊢
(-g‘ℝfld) =
(-g‘ℝfld) | 
| 68 | 7, 16, 65, 66, 46, 54, 67, 13 | frlmsubgval 21785 | . . . . . . . . . . 11
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → (𝑓(-g‘(ℝfld
freeLMod 𝐼))𝑔) = (𝑓 ∘f
(-g‘ℝfld)𝑔)) | 
| 69 | 68 | 3impb 1115 | . . . . . . . . . 10
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵) → (𝑓(-g‘(ℝfld
freeLMod 𝐼))𝑔) = (𝑓 ∘f
(-g‘ℝfld)𝑔)) | 
| 70 | 51 | ffvelcdmda 7104 | . . . . . . . . . . . 12
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵) ∧ 𝑥 ∈ 𝐼) → (𝑓‘𝑥) ∈ ℝ) | 
| 71 | 59 | ffvelcdmda 7104 | . . . . . . . . . . . 12
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵) ∧ 𝑥 ∈ 𝐼) → (𝑔‘𝑥) ∈ ℝ) | 
| 72 | 67 | resubgval 21627 | . . . . . . . . . . . 12
⊢ (((𝑓‘𝑥) ∈ ℝ ∧ (𝑔‘𝑥) ∈ ℝ) → ((𝑓‘𝑥) − (𝑔‘𝑥)) = ((𝑓‘𝑥)(-g‘ℝfld)(𝑔‘𝑥))) | 
| 73 | 70, 71, 72 | syl2anc 584 | . . . . . . . . . . 11
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵) ∧ 𝑥 ∈ 𝐼) → ((𝑓‘𝑥) − (𝑔‘𝑥)) = ((𝑓‘𝑥)(-g‘ℝfld)(𝑔‘𝑥))) | 
| 74 | 73 | mpteq2dva 5242 | . . . . . . . . . 10
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵) → (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥) − (𝑔‘𝑥))) = (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(-g‘ℝfld)(𝑔‘𝑥)))) | 
| 75 | 64, 69, 74 | 3eqtr4d 2787 | . . . . . . . . 9
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵) → (𝑓(-g‘(ℝfld
freeLMod 𝐼))𝑔) = (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥) − (𝑔‘𝑥)))) | 
| 76 | 70, 71 | resubcld 11691 | . . . . . . . . 9
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵) ∧ 𝑥 ∈ 𝐼) → ((𝑓‘𝑥) − (𝑔‘𝑥)) ∈ ℝ) | 
| 77 | 75, 76 | fvmpt2d 7029 | . . . . . . . 8
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵) ∧ 𝑥 ∈ 𝐼) → ((𝑓(-g‘(ℝfld
freeLMod 𝐼))𝑔)‘𝑥) = ((𝑓‘𝑥) − (𝑔‘𝑥))) | 
| 78 | 77 | oveq1d 7446 | . . . . . . 7
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵) ∧ 𝑥 ∈ 𝐼) → (((𝑓(-g‘(ℝfld
freeLMod 𝐼))𝑔)‘𝑥)↑2) = (((𝑓‘𝑥) − (𝑔‘𝑥))↑2)) | 
| 79 | 78 | mpteq2dva 5242 | . . . . . 6
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵) → (𝑥 ∈ 𝐼 ↦ (((𝑓(-g‘(ℝfld
freeLMod 𝐼))𝑔)‘𝑥)↑2)) = (𝑥 ∈ 𝐼 ↦ (((𝑓‘𝑥) − (𝑔‘𝑥))↑2))) | 
| 80 | 79 | oveq2d 7447 | . . . . 5
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵) → (ℝfld
Σg (𝑥 ∈ 𝐼 ↦ (((𝑓(-g‘(ℝfld
freeLMod 𝐼))𝑔)‘𝑥)↑2))) = (ℝfld
Σg (𝑥 ∈ 𝐼 ↦ (((𝑓‘𝑥) − (𝑔‘𝑥))↑2)))) | 
| 81 | 80 | fveq2d 6910 | . . . 4
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵) →
(√‘(ℝfld Σg (𝑥 ∈ 𝐼 ↦ (((𝑓(-g‘(ℝfld
freeLMod 𝐼))𝑔)‘𝑥)↑2)))) =
(√‘(ℝfld Σg (𝑥 ∈ 𝐼 ↦ (((𝑓‘𝑥) − (𝑔‘𝑥))↑2))))) | 
| 82 | 81 | mpoeq3dva 7510 | . . 3
⊢ (𝐼 ∈ 𝑉 → (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦
(√‘(ℝfld Σg (𝑥 ∈ 𝐼 ↦ (((𝑓(-g‘(ℝfld
freeLMod 𝐼))𝑔)‘𝑥)↑2))))) = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦
(√‘(ℝfld Σg (𝑥 ∈ 𝐼 ↦ (((𝑓‘𝑥) − (𝑔‘𝑥))↑2)))))) | 
| 83 | 42, 82 | eqtrd 2777 | . 2
⊢ (𝐼 ∈ 𝑉 →
((norm‘(toℂPreHil‘(ℝfld freeLMod 𝐼))) ∘
(-g‘(ℝfld freeLMod 𝐼))) = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦
(√‘(ℝfld Σg (𝑥 ∈ 𝐼 ↦ (((𝑓‘𝑥) − (𝑔‘𝑥))↑2)))))) | 
| 84 | 3, 15, 83 | 3eqtr2rd 2784 | 1
⊢ (𝐼 ∈ 𝑉 → (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦
(√‘(ℝfld Σg (𝑥 ∈ 𝐼 ↦ (((𝑓‘𝑥) − (𝑔‘𝑥))↑2))))) = (dist‘𝐻)) |