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	$⊢ H = msup$
	rrxbase.b	$⊢ B = {Base}_{H}$
Assertion	rrxds	$⊢ I \in V \to (f \in B, g \in B ⟼ \sqrt{\underset{x \in I}{\sum_{ℝ_{fld}}} {(f (x) - g (x))}^{2}}) = dist (H)$

Proof

Step	Hyp	Ref	Expression
1		rrxval.r	$⊢ H = msup$
2		rrxbase.b	$⊢ B = {Base}_{H}$
3	1	rrxval	$⊢ I \in V \to H = toCPreHil (ℝ_{fld} freeLMod I)$
4	3	fveq2d	$⊢ I \in V \to dist (H) = dist (toCPreHil (ℝ_{fld} freeLMod I))$
5		resrng	$⊢ ℝ_{fld} \in *-Ring$
6		srngring	$⊢ ℝ_{fld} \in *-Ring \to ℝ_{fld} \in Ring$
7	5 6	ax-mp	$⊢ ℝ_{fld} \in Ring$
8		eqid	$⊢ ℝ_{fld} freeLMod I = ℝ_{fld} freeLMod I$
9	8	frlmlmod	$⊢ (ℝ_{fld} \in Ring \land I \in V) \to ℝ_{fld} freeLMod I \in LMod$
10	7 9	mpan	$⊢ I \in V \to ℝ_{fld} freeLMod I \in LMod$
11		lmodgrp	$⊢ ℝ_{fld} freeLMod I \in LMod \to ℝ_{fld} freeLMod I \in Grp$
12		eqid	$⊢ toCPreHil (ℝ_{fld} freeLMod I) = toCPreHil (ℝ_{fld} freeLMod I)$
13		eqid	$⊢ norm (toCPreHil (ℝ_{fld} freeLMod I)) = norm (toCPreHil (ℝ_{fld} freeLMod I))$
14		eqid	$⊢ -_{(ℝ_{fld} freeLMod I)} = -_{(ℝ_{fld} freeLMod I)}$
15	12 13 14	tcphds	$⊢ ℝ_{fld} freeLMod I \in Grp \to norm (toCPreHil (ℝ_{fld} freeLMod I)) \circ -_{(ℝ_{fld} freeLMod I)} = dist (toCPreHil (ℝ_{fld} freeLMod I))$
16	10 11 15	3syl	$⊢ I \in V \to norm (toCPreHil (ℝ_{fld} freeLMod I)) \circ -_{(ℝ_{fld} freeLMod I)} = dist (toCPreHil (ℝ_{fld} freeLMod I))$
17		eqid	$⊢ {Base}_{(ℝ_{fld} freeLMod I)} = {Base}_{(ℝ_{fld} freeLMod I)}$
18	17 14	grpsubf	$⊢ ℝ_{fld} freeLMod I \in Grp \to -_{(ℝ_{fld} freeLMod I)} : {Base}_{(ℝ_{fld} freeLMod I)} \times {Base}_{(ℝ_{fld} freeLMod I)} ⟶ {Base}_{(ℝ_{fld} freeLMod I)}$
19	10 11 18	3syl	$⊢ I \in V \to -_{(ℝ_{fld} freeLMod I)} : {Base}_{(ℝ_{fld} freeLMod I)} \times {Base}_{(ℝ_{fld} freeLMod I)} ⟶ {Base}_{(ℝ_{fld} freeLMod I)}$
20	1 2	rrxbase	$⊢ I \in V \to B = \{h \in (ℝ^{I}) \| {finSupp}_{0} (h)\}$
21		rebase	$⊢ ℝ = {Base}_{ℝ_{fld}}$
22		re0g	$⊢ 0 = 0_{ℝ_{fld}}$
23		eqid	$⊢ \{h \in (ℝ^{I}) \| {finSupp}_{0} (h)\} = \{h \in (ℝ^{I}) \| {finSupp}_{0} (h)\}$
24	8 21 22 23	frlmbas	$⊢ (ℝ_{fld} \in Ring \land I \in V) \to \{h \in (ℝ^{I}) \| {finSupp}_{0} (h)\} = {Base}_{(ℝ_{fld} freeLMod I)}$
25	7 24	mpan	$⊢ I \in V \to \{h \in (ℝ^{I}) \| {finSupp}_{0} (h)\} = {Base}_{(ℝ_{fld} freeLMod I)}$
26	20 25	eqtrd	$⊢ I \in V \to B = {Base}_{(ℝ_{fld} freeLMod I)}$
27	26	sqxpeqd	$⊢ I \in V \to B \times B = {Base}_{(ℝ_{fld} freeLMod I)} \times {Base}_{(ℝ_{fld} freeLMod I)}$
28	27 26	feq23d	$⊢ I \in V \to (-_{(ℝ_{fld} freeLMod I)} : B \times B ⟶ B \leftrightarrow -_{(ℝ_{fld} freeLMod I)} : {Base}_{(ℝ_{fld} freeLMod I)} \times {Base}_{(ℝ_{fld} freeLMod I)} ⟶ {Base}_{(ℝ_{fld} freeLMod I)})$
29	19 28	mpbird	$⊢ I \in V \to -_{(ℝ_{fld} freeLMod I)} : B \times B ⟶ B$
30	29	fovcdmda	$⊢ (I \in V \land (f \in B \land g \in B)) \to f -_{(ℝ_{fld} freeLMod I)} g \in B$
31	29	ffnd	$⊢ I \in V \to -_{(ℝ_{fld} freeLMod I)} Fn (B \times B)$
32		fnov	$⊢ -_{(ℝ_{fld} freeLMod I)} Fn (B \times B) \leftrightarrow -_{(ℝ_{fld} freeLMod I)} = (f \in B, g \in B ⟼ f -_{(ℝ_{fld} freeLMod I)} g)$
33	31 32	sylib	$⊢ I \in V \to -_{(ℝ_{fld} freeLMod I)} = (f \in B, g \in B ⟼ f -_{(ℝ_{fld} freeLMod I)} g)$
34	1 2	rrxnm	$⊢ I \in V \to (h \in B ⟼ \sqrt{\underset{x \in I}{\sum_{ℝ_{fld}}} {h (x)}^{2}}) = norm (H)$
35	3	fveq2d	$⊢ I \in V \to norm (H) = norm (toCPreHil (ℝ_{fld} freeLMod I))$
36	34 35	eqtr2d	$⊢ I \in V \to norm (toCPreHil (ℝ_{fld} freeLMod I)) = (h \in B ⟼ \sqrt{\underset{x \in I}{\sum_{ℝ_{fld}}} {h (x)}^{2}})$
37		fveq1	$⊢ h = f -_{(ℝ_{fld} freeLMod I)} g \to h (x) = (f -_{(ℝ_{fld} freeLMod I)} g) (x)$
38	37	oveq1d	$⊢ h = f -_{(ℝ_{fld} freeLMod I)} g \to {h (x)}^{2} = {(f -_{(ℝ_{fld} freeLMod I)} g) (x)}^{2}$
39	38	mpteq2dv	$⊢ h = f -_{(ℝ_{fld} freeLMod I)} g \to (x \in I ⟼ {h (x)}^{2}) = (x \in I ⟼ {(f -_{(ℝ_{fld} freeLMod I)} g) (x)}^{2})$
40	39	oveq2d	$⊢ h = f -_{(ℝ_{fld} freeLMod I)} g \to \underset{x \in I}{\sum_{ℝ_{fld}}} {h (x)}^{2} = \underset{x \in I}{\sum_{ℝ_{fld}}} {(f -_{(ℝ_{fld} freeLMod I)} g) (x)}^{2}$
41	40	fveq2d	$⊢ h = f -_{(ℝ_{fld} freeLMod I)} g \to \sqrt{\underset{x \in I}{\sum_{ℝ_{fld}}} {h (x)}^{2}} = \sqrt{\underset{x \in I}{\sum_{ℝ_{fld}}} {(f -_{(ℝ_{fld} freeLMod I)} g) (x)}^{2}}$
42	30 33 36 41	fmpoco	$⊢ I \in V \to norm (toCPreHil (ℝ_{fld} freeLMod I)) \circ -_{(ℝ_{fld} freeLMod I)} = (f \in B, g \in B ⟼ \sqrt{\underset{x \in I}{\sum_{ℝ_{fld}}} {(f -_{(ℝ_{fld} freeLMod I)} g) (x)}^{2}})$
43		simp1	$⊢ (I \in V \land f \in B \land g \in B) \to I \in V$
44		simprl	$⊢ (I \in V \land (f \in B \land g \in B)) \to f \in B$
45	26	adantr	$⊢ (I \in V \land (f \in B \land g \in B)) \to B = {Base}_{(ℝ_{fld} freeLMod I)}$
46	44 45	eleqtrd	$⊢ (I \in V \land (f \in B \land g \in B)) \to f \in {Base}_{(ℝ_{fld} freeLMod I)}$
47	46	3impb	$⊢ (I \in V \land f \in B \land g \in B) \to f \in {Base}_{(ℝ_{fld} freeLMod I)}$
48	8 21 17	frlmbasmap	$⊢ (I \in V \land f \in {Base}_{(ℝ_{fld} freeLMod I)}) \to f \in (ℝ^{I})$
49	43 47 48	syl2anc	$⊢ (I \in V \land f \in B \land g \in B) \to f \in (ℝ^{I})$
50		elmapi	$⊢ f \in (ℝ^{I}) \to f : I ⟶ ℝ$
51	49 50	syl	$⊢ (I \in V \land f \in B \land g \in B) \to f : I ⟶ ℝ$
52	51	ffnd	$⊢ (I \in V \land f \in B \land g \in B) \to f Fn I$
53		simprr	$⊢ (I \in V \land (f \in B \land g \in B)) \to g \in B$
54	53 45	eleqtrd	$⊢ (I \in V \land (f \in B \land g \in B)) \to g \in {Base}_{(ℝ_{fld} freeLMod I)}$
55	54	3impb	$⊢ (I \in V \land f \in B \land g \in B) \to g \in {Base}_{(ℝ_{fld} freeLMod I)}$
56	8 21 17	frlmbasmap	$⊢ (I \in V \land g \in {Base}_{(ℝ_{fld} freeLMod I)}) \to g \in (ℝ^{I})$
57	43 55 56	syl2anc	$⊢ (I \in V \land f \in B \land g \in B) \to g \in (ℝ^{I})$
58		elmapi	$⊢ g \in (ℝ^{I}) \to g : I ⟶ ℝ$
59	57 58	syl	$⊢ (I \in V \land f \in B \land g \in B) \to g : I ⟶ ℝ$
60	59	ffnd	$⊢ (I \in V \land f \in B \land g \in B) \to g Fn I$
61		inidm	$⊢ I \cap I = I$
62		eqidd	$⊢ ((I \in V \land f \in B \land g \in B) \land x \in I) \to f (x) = f (x)$
63		eqidd	$⊢ ((I \in V \land f \in B \land g \in B) \land x \in I) \to g (x) = g (x)$
64	52 60 43 43 61 62 63	offval	$⊢ (I \in V \land f \in B \land g \in B) \to f {-_{ℝ_{fld}}}_{f} g = (x \in I ⟼ f (x) -_{ℝ_{fld}} g (x))$
65	7	a1i	$⊢ (I \in V \land (f \in B \land g \in B)) \to ℝ_{fld} \in Ring$
66		simpl	$⊢ (I \in V \land (f \in B \land g \in B)) \to I \in V$
67		eqid	$⊢ -_{ℝ_{fld}} = -_{ℝ_{fld}}$
68	8 17 65 66 46 54 67 14	frlmsubgval	$⊢ (I \in V \land (f \in B \land g \in B)) \to f -_{(ℝ_{fld} freeLMod I)} g = f {-_{ℝ_{fld}}}_{f} g$
69	68	3impb	$⊢ (I \in V \land f \in B \land g \in B) \to f -_{(ℝ_{fld} freeLMod I)} g = f {-_{ℝ_{fld}}}_{f} g$
70	51	ffvelcdmda	$⊢ ((I \in V \land f \in B \land g \in B) \land x \in I) \to f (x) \in ℝ$
71	59	ffvelcdmda	$⊢ ((I \in V \land f \in B \land g \in B) \land x \in I) \to g (x) \in ℝ$
72	67	resubgval	$⊢ (f (x) \in ℝ \land g (x) \in ℝ) \to f (x) - g (x) = f (x) -_{ℝ_{fld}} g (x)$
73	70 71 72	syl2anc	$⊢ ((I \in V \land f \in B \land g \in B) \land x \in I) \to f (x) - g (x) = f (x) -_{ℝ_{fld}} g (x)$
74	73	mpteq2dva	$⊢ (I \in V \land f \in B \land g \in B) \to (x \in I ⟼ f (x) - g (x)) = (x \in I ⟼ f (x) -_{ℝ_{fld}} g (x))$
75	64 69 74	3eqtr4d	$⊢ (I \in V \land f \in B \land g \in B) \to f -_{(ℝ_{fld} freeLMod I)} g = (x \in I ⟼ f (x) - g (x))$
76	70 71	resubcld	$⊢ ((I \in V \land f \in B \land g \in B) \land x \in I) \to f (x) - g (x) \in ℝ$
77	75 76	fvmpt2d	$⊢ ((I \in V \land f \in B \land g \in B) \land x \in I) \to (f -_{(ℝ_{fld} freeLMod I)} g) (x) = f (x) - g (x)$
78	77	oveq1d	$⊢ ((I \in V \land f \in B \land g \in B) \land x \in I) \to {(f -_{(ℝ_{fld} freeLMod I)} g) (x)}^{2} = {(f (x) - g (x))}^{2}$
79	78	mpteq2dva	$⊢ (I \in V \land f \in B \land g \in B) \to (x \in I ⟼ {(f -_{(ℝ_{fld} freeLMod I)} g) (x)}^{2}) = (x \in I ⟼ {(f (x) - g (x))}^{2})$
80	79	oveq2d	$⊢ (I \in V \land f \in B \land g \in B) \to \underset{x \in I}{\sum_{ℝ_{fld}}} {(f -_{(ℝ_{fld} freeLMod I)} g) (x)}^{2} = \underset{x \in I}{\sum_{ℝ_{fld}}} {(f (x) - g (x))}^{2}$
81	80	fveq2d	$⊢ (I \in V \land f \in B \land g \in B) \to \sqrt{\underset{x \in I}{\sum_{ℝ_{fld}}} {(f -_{(ℝ_{fld} freeLMod I)} g) (x)}^{2}} = \sqrt{\underset{x \in I}{\sum_{ℝ_{fld}}} {(f (x) - g (x))}^{2}}$
82	81	mpoeq3dva	$⊢ I \in V \to (f \in B, g \in B ⟼ \sqrt{\underset{x \in I}{\sum_{ℝ_{fld}}} {(f -_{(ℝ_{fld} freeLMod I)} g) (x)}^{2}}) = (f \in B, g \in B ⟼ \sqrt{\underset{x \in I}{\sum_{ℝ_{fld}}} {(f (x) - g (x))}^{2}})$
83	42 82	eqtrd	$⊢ I \in V \to norm (toCPreHil (ℝ_{fld} freeLMod I)) \circ -_{(ℝ_{fld} freeLMod I)} = (f \in B, g \in B ⟼ \sqrt{\underset{x \in I}{\sum_{ℝ_{fld}}} {(f (x) - g (x))}^{2}})$
84	4 16 83	3eqtr2rd	$⊢ I \in V \to (f \in B, g \in B ⟼ \sqrt{\underset{x \in I}{\sum_{ℝ_{fld}}} {(f (x) - g (x))}^{2}}) = dist (H)$

Metamath Proof Explorer

Theorem rrxds

Proof