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 = ( 0_g ‘ ℝ_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 ‘ 𝐻 ) )

Metamath Proof Explorer

Theorem rrxds

Proof