This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem rrxds

Description: The distance over generalized Euclidean spaces. Compare with df-rrn . (Contributed by Thierry Arnoux, 20-Jun-2019) (Proof shortened by AV, 20-Jul-2019)

Ref Expression
Hypotheses rrxval.r ⊢ 𝐻 = ( ℝ^ ‘ 𝐼 )
rrxbase.b ⊢ 𝐵 = ( Base ‘ 𝐻 )
Assertion rrxds ( 𝐼 ∈ 𝑉 → ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( √ ‘ ( ℝfld Σg ( 𝑥 ∈ 𝐼 ↦ ( ( ( 𝑓 ‘ 𝑥 ) − ( 𝑔 ‘ 𝑥 ) ) ↑ 2 ) ) ) ) ) = ( dist ‘ 𝐻 ) )

Proof

Step Hyp Ref Expression
1 rrxval.r ⊢ 𝐻 = ( ℝ^ ‘ 𝐼 )
2 rrxbase.b ⊢ 𝐵 = ( Base ‘ 𝐻 )
3 1 rrxval ⊢ ( 𝐼 ∈ 𝑉 → 𝐻 = ( toℂPreHil ‘ ( ℝfld freeLMod 𝐼 ) ) )
4 3 fveq2d ⊢ ( 𝐼 ∈ 𝑉 → ( dist ‘ 𝐻 ) = ( dist ‘ ( toℂPreHil ‘ ( ℝfld freeLMod 𝐼 ) ) ) )
5 resrng ⊢ ℝfld ∈ *-Ring
6 srngring ⊢ ( ℝfld ∈ *-Ring → ℝfld ∈ Ring )
7 5 6 ax-mp ⊢ ℝfld ∈ Ring
8 eqid ⊢ ( ℝfld freeLMod 𝐼 ) = ( ℝfld freeLMod 𝐼 )
9 8 frlmlmod ⊢ ( ( ℝfld ∈ Ring ∧ 𝐼 ∈ 𝑉 ) → ( ℝfld freeLMod 𝐼 ) ∈ LMod )
10 7 9 mpan ⊢ ( 𝐼 ∈ 𝑉 → ( ℝfld freeLMod 𝐼 ) ∈ LMod )
11 lmodgrp ⊢ ( ( ℝfld freeLMod 𝐼 ) ∈ LMod → ( ℝfld freeLMod 𝐼 ) ∈ Grp )
12 eqid ⊢ ( toℂPreHil ‘ ( ℝfld freeLMod 𝐼 ) ) = ( toℂPreHil ‘ ( ℝfld freeLMod 𝐼 ) )
13 eqid ⊢ ( norm ‘ ( toℂPreHil ‘ ( ℝfld freeLMod 𝐼 ) ) ) = ( norm ‘ ( toℂPreHil ‘ ( ℝfld freeLMod 𝐼 ) ) )
14 eqid ⊢ ( -g ‘ ( ℝfld freeLMod 𝐼 ) ) = ( -g ‘ ( ℝfld freeLMod 𝐼 ) )
15 12 13 14 tcphds ⊢ ( ( ℝfld freeLMod 𝐼 ) ∈ Grp → ( ( norm ‘ ( toℂPreHil ‘ ( ℝfld freeLMod 𝐼 ) ) ) ∘ ( -g ‘ ( ℝfld freeLMod 𝐼 ) ) ) = ( dist ‘ ( toℂPreHil ‘ ( ℝfld freeLMod 𝐼 ) ) ) )
16 10 11 15 3syl ⊢ ( 𝐼 ∈ 𝑉 → ( ( norm ‘ ( toℂPreHil ‘ ( ℝfld freeLMod 𝐼 ) ) ) ∘ ( -g ‘ ( ℝfld freeLMod 𝐼 ) ) ) = ( dist ‘ ( toℂPreHil ‘ ( ℝfld freeLMod 𝐼 ) ) ) )
17 eqid ⊢ ( Base ‘ ( ℝfld freeLMod 𝐼 ) ) = ( Base ‘ ( ℝfld freeLMod 𝐼 ) )
18 17 14 grpsubf ⊢ ( ( ℝfld freeLMod 𝐼 ) ∈ Grp → ( -g ‘ ( ℝfld freeLMod 𝐼 ) ) : ( ( Base ‘ ( ℝfld freeLMod 𝐼 ) ) × ( Base ‘ ( ℝfld freeLMod 𝐼 ) ) ) ⟶ ( Base ‘ ( ℝfld freeLMod 𝐼 ) ) )
19 10 11 18 3syl ⊢ ( 𝐼 ∈ 𝑉 → ( -g ‘ ( ℝfld freeLMod 𝐼 ) ) : ( ( Base ‘ ( ℝfld freeLMod 𝐼 ) ) × ( Base ‘ ( ℝfld freeLMod 𝐼 ) ) ) ⟶ ( Base ‘ ( ℝfld freeLMod 𝐼 ) ) )
20 1 2 rrxbase ⊢ ( 𝐼 ∈ 𝑉 → 𝐵 = { ℎ ∈ ( ℝ ↑m 𝐼 ) ∣ ℎ finSupp 0 } )
21 rebase ⊢ ℝ = ( Base ‘ ℝfld )
22 re0g ⊢ 0 = ( 0g ‘ ℝfld )
23 eqid ⊢ { ℎ ∈ ( ℝ ↑m 𝐼 ) ∣ ℎ finSupp 0 } = { ℎ ∈ ( ℝ ↑m 𝐼 ) ∣ ℎ finSupp 0 }
24 8 21 22 23 frlmbas ⊢ ( ( ℝfld ∈ Ring ∧ 𝐼 ∈ 𝑉 ) → { ℎ ∈ ( ℝ ↑m 𝐼 ) ∣ ℎ finSupp 0 } = ( Base ‘ ( ℝfld freeLMod 𝐼 ) ) )
25 7 24 mpan ⊢ ( 𝐼 ∈ 𝑉 → { ℎ ∈ ( ℝ ↑m 𝐼 ) ∣ ℎ finSupp 0 } = ( Base ‘ ( ℝfld freeLMod 𝐼 ) ) )
26 20 25 eqtrd ⊢ ( 𝐼 ∈ 𝑉 → 𝐵 = ( Base ‘ ( ℝfld freeLMod 𝐼 ) ) )
27 26 sqxpeqd ⊢ ( 𝐼 ∈ 𝑉 → ( 𝐵 × 𝐵 ) = ( ( Base ‘ ( ℝfld freeLMod 𝐼 ) ) × ( Base ‘ ( ℝfld freeLMod 𝐼 ) ) ) )
28 27 26 feq23d ⊢ ( 𝐼 ∈ 𝑉 → ( ( -g ‘ ( ℝfld freeLMod 𝐼 ) ) : ( 𝐵 × 𝐵 ) ⟶ 𝐵 ↔ ( -g ‘ ( ℝfld freeLMod 𝐼 ) ) : ( ( Base ‘ ( ℝfld freeLMod 𝐼 ) ) × ( Base ‘ ( ℝfld freeLMod 𝐼 ) ) ) ⟶ ( Base ‘ ( ℝfld freeLMod 𝐼 ) ) ) )
29 19 28 mpbird ⊢ ( 𝐼 ∈ 𝑉 → ( -g ‘ ( ℝfld freeLMod 𝐼 ) ) : ( 𝐵 × 𝐵 ) ⟶ 𝐵 )
30 29 fovcdmda ⊢ ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) → ( 𝑓 ( -g ‘ ( ℝfld freeLMod 𝐼 ) ) 𝑔 ) ∈ 𝐵 )
31 29 ffnd ⊢ ( 𝐼 ∈ 𝑉 → ( -g ‘ ( ℝfld freeLMod 𝐼 ) ) Fn ( 𝐵 × 𝐵 ) )
32 fnov ⊢ ( ( -g ‘ ( ℝfld freeLMod 𝐼 ) ) Fn ( 𝐵 × 𝐵 ) ↔ ( -g ‘ ( ℝfld freeLMod 𝐼 ) ) = ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( 𝑓 ( -g ‘ ( ℝfld freeLMod 𝐼 ) ) 𝑔 ) ) )
33 31 32 sylib ⊢ ( 𝐼 ∈ 𝑉 → ( -g ‘ ( ℝfld freeLMod 𝐼 ) ) = ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( 𝑓 ( -g ‘ ( ℝfld freeLMod 𝐼 ) ) 𝑔 ) ) )
34 1 2 rrxnm ⊢ ( 𝐼 ∈ 𝑉 → ( ℎ ∈ 𝐵 ↦ ( √ ‘ ( ℝfld Σg ( 𝑥 ∈ 𝐼 ↦ ( ( ℎ ‘ 𝑥 ) ↑ 2 ) ) ) ) ) = ( norm ‘ 𝐻 ) )
35 3 fveq2d ⊢ ( 𝐼 ∈ 𝑉 → ( norm ‘ 𝐻 ) = ( norm ‘ ( toℂPreHil ‘ ( ℝfld freeLMod 𝐼 ) ) ) )
36 34 35 eqtr2d ⊢ ( 𝐼 ∈ 𝑉 → ( norm ‘ ( toℂPreHil ‘ ( ℝfld freeLMod 𝐼 ) ) ) = ( ℎ ∈ 𝐵 ↦ ( √ ‘ ( ℝfld Σg ( 𝑥 ∈ 𝐼 ↦ ( ( ℎ ‘ 𝑥 ) ↑ 2 ) ) ) ) ) )
37 fveq1 ⊢ ( ℎ = ( 𝑓 ( -g ‘ ( ℝfld freeLMod 𝐼 ) ) 𝑔 ) → ( ℎ ‘ 𝑥 ) = ( ( 𝑓 ( -g ‘ ( ℝfld freeLMod 𝐼 ) ) 𝑔 ) ‘ 𝑥 ) )
38 37 oveq1d ⊢ ( ℎ = ( 𝑓 ( -g ‘ ( ℝfld freeLMod 𝐼 ) ) 𝑔 ) → ( ( ℎ ‘ 𝑥 ) ↑ 2 ) = ( ( ( 𝑓 ( -g ‘ ( ℝfld freeLMod 𝐼 ) ) 𝑔 ) ‘ 𝑥 ) ↑ 2 ) )
39 38 mpteq2dv ⊢ ( ℎ = ( 𝑓 ( -g ‘ ( ℝfld freeLMod 𝐼 ) ) 𝑔 ) → ( 𝑥 ∈ 𝐼 ↦ ( ( ℎ ‘ 𝑥 ) ↑ 2 ) ) = ( 𝑥 ∈ 𝐼 ↦ ( ( ( 𝑓 ( -g ‘ ( ℝfld freeLMod 𝐼 ) ) 𝑔 ) ‘ 𝑥 ) ↑ 2 ) ) )
40 39 oveq2d ⊢ ( ℎ = ( 𝑓 ( -g ‘ ( ℝfld freeLMod 𝐼 ) ) 𝑔 ) → ( ℝfld Σg ( 𝑥 ∈ 𝐼 ↦ ( ( ℎ ‘ 𝑥 ) ↑ 2 ) ) ) = ( ℝfld Σg ( 𝑥 ∈ 𝐼 ↦ ( ( ( 𝑓 ( -g ‘ ( ℝfld freeLMod 𝐼 ) ) 𝑔 ) ‘ 𝑥 ) ↑ 2 ) ) ) )
41 40 fveq2d ⊢ ( ℎ = ( 𝑓 ( -g ‘ ( ℝfld freeLMod 𝐼 ) ) 𝑔 ) → ( √ ‘ ( ℝfld Σg ( 𝑥 ∈ 𝐼 ↦ ( ( ℎ ‘ 𝑥 ) ↑ 2 ) ) ) ) = ( √ ‘ ( ℝfld Σg ( 𝑥 ∈ 𝐼 ↦ ( ( ( 𝑓 ( -g ‘ ( ℝfld freeLMod 𝐼 ) ) 𝑔 ) ‘ 𝑥 ) ↑ 2 ) ) ) ) )
42 30 33 36 41 fmpoco ⊢ ( 𝐼 ∈ 𝑉 → ( ( norm ‘ ( toℂPreHil ‘ ( ℝfld freeLMod 𝐼 ) ) ) ∘ ( -g ‘ ( ℝfld freeLMod 𝐼 ) ) ) = ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( √ ‘ ( ℝfld Σg ( 𝑥 ∈ 𝐼 ↦ ( ( ( 𝑓 ( -g ‘ ( ℝfld freeLMod 𝐼 ) ) 𝑔 ) ‘ 𝑥 ) ↑ 2 ) ) ) ) ) )
43 simp1 ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) → 𝐼 ∈ 𝑉 )
44 simprl ⊢ ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) → 𝑓 ∈ 𝐵 )
45 26 adantr ⊢ ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) → 𝐵 = ( Base ‘ ( ℝfld freeLMod 𝐼 ) ) )
46 44 45 eleqtrd ⊢ ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) → 𝑓 ∈ ( Base ‘ ( ℝfld freeLMod 𝐼 ) ) )
47 46 3impb ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) → 𝑓 ∈ ( Base ‘ ( ℝfld freeLMod 𝐼 ) ) )
48 8 21 17 frlmbasmap ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑓 ∈ ( Base ‘ ( ℝfld freeLMod 𝐼 ) ) ) → 𝑓 ∈ ( ℝ ↑m 𝐼 ) )
49 43 47 48 syl2anc ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) → 𝑓 ∈ ( ℝ ↑m 𝐼 ) )
50 elmapi ⊢ ( 𝑓 ∈ ( ℝ ↑m 𝐼 ) → 𝑓 : 𝐼 ⟶ ℝ )
51 49 50 syl ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) → 𝑓 : 𝐼 ⟶ ℝ )
52 51 ffnd ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) → 𝑓 Fn 𝐼 )
53 simprr ⊢ ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) → 𝑔 ∈ 𝐵 )
54 53 45 eleqtrd ⊢ ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) → 𝑔 ∈ ( Base ‘ ( ℝfld freeLMod 𝐼 ) ) )
55 54 3impb ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) → 𝑔 ∈ ( Base ‘ ( ℝfld freeLMod 𝐼 ) ) )
56 8 21 17 frlmbasmap ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑔 ∈ ( Base ‘ ( ℝfld freeLMod 𝐼 ) ) ) → 𝑔 ∈ ( ℝ ↑m 𝐼 ) )
57 43 55 56 syl2anc ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) → 𝑔 ∈ ( ℝ ↑m 𝐼 ) )
58 elmapi ⊢ ( 𝑔 ∈ ( ℝ ↑m 𝐼 ) → 𝑔 : 𝐼 ⟶ ℝ )
59 57 58 syl ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) → 𝑔 : 𝐼 ⟶ ℝ )
60 59 ffnd ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) → 𝑔 Fn 𝐼 )
61 inidm ⊢ ( 𝐼 ∩ 𝐼 ) = 𝐼
62 eqidd ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝑓 ‘ 𝑥 ) = ( 𝑓 ‘ 𝑥 ) )
63 eqidd ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝑔 ‘ 𝑥 ) = ( 𝑔 ‘ 𝑥 ) )
64 52 60 43 43 61 62 63 offval ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) → ( 𝑓 ∘f ( -g ‘ ℝfld ) 𝑔 ) = ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( -g ‘ ℝfld ) ( 𝑔 ‘ 𝑥 ) ) ) )
65 7 a1i ⊢ ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) → ℝfld ∈ Ring )
66 simpl ⊢ ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) → 𝐼 ∈ 𝑉 )
67 eqid ⊢ ( -g ‘ ℝfld ) = ( -g ‘ ℝfld )
68 8 17 65 66 46 54 67 14 frlmsubgval ⊢ ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) → ( 𝑓 ( -g ‘ ( ℝfld freeLMod 𝐼 ) ) 𝑔 ) = ( 𝑓 ∘f ( -g ‘ ℝfld ) 𝑔 ) )
69 68 3impb ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) → ( 𝑓 ( -g ‘ ( ℝfld freeLMod 𝐼 ) ) 𝑔 ) = ( 𝑓 ∘f ( -g ‘ ℝfld ) 𝑔 ) )
70 51 ffvelcdmda ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝑓 ‘ 𝑥 ) ∈ ℝ )
71 59 ffvelcdmda ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝑔 ‘ 𝑥 ) ∈ ℝ )
72 67 resubgval ⊢ ( ( ( 𝑓 ‘ 𝑥 ) ∈ ℝ ∧ ( 𝑔 ‘ 𝑥 ) ∈ ℝ ) → ( ( 𝑓 ‘ 𝑥 ) − ( 𝑔 ‘ 𝑥 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( -g ‘ ℝfld ) ( 𝑔 ‘ 𝑥 ) ) )
73 70 71 72 syl2anc ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐼 ) → ( ( 𝑓 ‘ 𝑥 ) − ( 𝑔 ‘ 𝑥 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( -g ‘ ℝfld ) ( 𝑔 ‘ 𝑥 ) ) )
74 73 mpteq2dva ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) → ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) − ( 𝑔 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( -g ‘ ℝfld ) ( 𝑔 ‘ 𝑥 ) ) ) )
75 64 69 74 3eqtr4d ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) → ( 𝑓 ( -g ‘ ( ℝfld freeLMod 𝐼 ) ) 𝑔 ) = ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) − ( 𝑔 ‘ 𝑥 ) ) ) )
76 70 71 resubcld ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐼 ) → ( ( 𝑓 ‘ 𝑥 ) − ( 𝑔 ‘ 𝑥 ) ) ∈ ℝ )
77 75 76 fvmpt2d ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐼 ) → ( ( 𝑓 ( -g ‘ ( ℝfld freeLMod 𝐼 ) ) 𝑔 ) ‘ 𝑥 ) = ( ( 𝑓 ‘ 𝑥 ) − ( 𝑔 ‘ 𝑥 ) ) )
78 77 oveq1d ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐼 ) → ( ( ( 𝑓 ( -g ‘ ( ℝfld freeLMod 𝐼 ) ) 𝑔 ) ‘ 𝑥 ) ↑ 2 ) = ( ( ( 𝑓 ‘ 𝑥 ) − ( 𝑔 ‘ 𝑥 ) ) ↑ 2 ) )
79 78 mpteq2dva ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) → ( 𝑥 ∈ 𝐼 ↦ ( ( ( 𝑓 ( -g ‘ ( ℝfld freeLMod 𝐼 ) ) 𝑔 ) ‘ 𝑥 ) ↑ 2 ) ) = ( 𝑥 ∈ 𝐼 ↦ ( ( ( 𝑓 ‘ 𝑥 ) − ( 𝑔 ‘ 𝑥 ) ) ↑ 2 ) ) )
80 79 oveq2d ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) → ( ℝfld Σg ( 𝑥 ∈ 𝐼 ↦ ( ( ( 𝑓 ( -g ‘ ( ℝfld freeLMod 𝐼 ) ) 𝑔 ) ‘ 𝑥 ) ↑ 2 ) ) ) = ( ℝfld Σg ( 𝑥 ∈ 𝐼 ↦ ( ( ( 𝑓 ‘ 𝑥 ) − ( 𝑔 ‘ 𝑥 ) ) ↑ 2 ) ) ) )
81 80 fveq2d ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) → ( √ ‘ ( ℝfld Σg ( 𝑥 ∈ 𝐼 ↦ ( ( ( 𝑓 ( -g ‘ ( ℝfld freeLMod 𝐼 ) ) 𝑔 ) ‘ 𝑥 ) ↑ 2 ) ) ) ) = ( √ ‘ ( ℝfld Σg ( 𝑥 ∈ 𝐼 ↦ ( ( ( 𝑓 ‘ 𝑥 ) − ( 𝑔 ‘ 𝑥 ) ) ↑ 2 ) ) ) ) )
82 81 mpoeq3dva ⊢ ( 𝐼 ∈ 𝑉 → ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( √ ‘ ( ℝfld Σg ( 𝑥 ∈ 𝐼 ↦ ( ( ( 𝑓 ( -g ‘ ( ℝfld freeLMod 𝐼 ) ) 𝑔 ) ‘ 𝑥 ) ↑ 2 ) ) ) ) ) = ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( √ ‘ ( ℝfld Σg ( 𝑥 ∈ 𝐼 ↦ ( ( ( 𝑓 ‘ 𝑥 ) − ( 𝑔 ‘ 𝑥 ) ) ↑ 2 ) ) ) ) ) )
83 42 82 eqtrd ⊢ ( 𝐼 ∈ 𝑉 → ( ( norm ‘ ( toℂPreHil ‘ ( ℝfld freeLMod 𝐼 ) ) ) ∘ ( -g ‘ ( ℝfld freeLMod 𝐼 ) ) ) = ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( √ ‘ ( ℝfld Σg ( 𝑥 ∈ 𝐼 ↦ ( ( ( 𝑓 ‘ 𝑥 ) − ( 𝑔 ‘ 𝑥 ) ) ↑ 2 ) ) ) ) ) )
84 4 16 83 3eqtr2rd ⊢ ( 𝐼 ∈ 𝑉 → ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( √ ‘ ( ℝfld Σg ( 𝑥 ∈ 𝐼 ↦ ( ( ( 𝑓 ‘ 𝑥 ) − ( 𝑔 ‘ 𝑥 ) ) ↑ 2 ) ) ) ) ) = ( dist ‘ 𝐻 ) )