rrxdsfi

Description: The distance over generalized Euclidean spaces. Finite dimensional case. (Contributed by Glauco Siliprandi, 24-Dec-2020)

	Ref	Expression
Hypotheses	rrxdsfi.h	$⊢ H = msup$
	rrxdsfi.b	$⊢ B = ℝ^{I}$
Assertion	rrxdsfi	$⊢ I \in Fin \to dist (H) = (f \in B, g \in B ⟼ \sqrt{\sum_{k \in I} {(f (k) - g (k))}^{2}})$

Proof

Step	Hyp	Ref	Expression
1		rrxdsfi.h	$⊢ H = msup$
2		rrxdsfi.b	$⊢ B = ℝ^{I}$
3		id	$⊢ I \in Fin \to I \in Fin$
4		eqid	$⊢ {Base}_{H} = {Base}_{H}$
5	3 1 4	rrxbasefi	$⊢ I \in Fin \to {Base}_{H} = ℝ^{I}$
6	2 5	eqtr4id	$⊢ I \in Fin \to B = {Base}_{H}$
7	6	adantr	$⊢ (I \in Fin \land f \in B) \to B = {Base}_{H}$
8		df-refld	$⊢ ℝ_{fld} = ℂ_{fld} ↾_{𝑠} ℝ$
9	8	oveq1i	$⊢ \underset{k \in I}{\sum_{ℝ_{fld}}} {(f (k) - g (k))}^{2} = \underset{k \in I}{\sum_{ℂ_{fld} ↾_{𝑠} ℝ}} {(f (k) - g (k))}^{2}$
10		simp1	$⊢ (I \in Fin \land f \in B \land g \in B) \to I \in Fin$
11		simpr	$⊢ (I \in Fin \land f \in B) \to f \in B$
12	11 2	eleqtrdi	$⊢ (I \in Fin \land f \in B) \to f \in (ℝ^{I})$
13	12	3adant3	$⊢ (I \in Fin \land f \in B \land g \in B) \to f \in (ℝ^{I})$
14		elmapi	$⊢ f \in (ℝ^{I}) \to f : I ⟶ ℝ$
15	13 14	syl	$⊢ (I \in Fin \land f \in B \land g \in B) \to f : I ⟶ ℝ$
16	15	ffvelcdmda	$⊢ ((I \in Fin \land f \in B \land g \in B) \land k \in I) \to f (k) \in ℝ$
17		simpr	$⊢ (I \in Fin \land g \in B) \to g \in B$
18	17 2	eleqtrdi	$⊢ (I \in Fin \land g \in B) \to g \in (ℝ^{I})$
19	18	3adant2	$⊢ (I \in Fin \land f \in B \land g \in B) \to g \in (ℝ^{I})$
20		elmapi	$⊢ g \in (ℝ^{I}) \to g : I ⟶ ℝ$
21	19 20	syl	$⊢ (I \in Fin \land f \in B \land g \in B) \to g : I ⟶ ℝ$
22	21	ffvelcdmda	$⊢ ((I \in Fin \land f \in B \land g \in B) \land k \in I) \to g (k) \in ℝ$
23	16 22	resubcld	$⊢ ((I \in Fin \land f \in B \land g \in B) \land k \in I) \to f (k) - g (k) \in ℝ$
24	23	resqcld	$⊢ ((I \in Fin \land f \in B \land g \in B) \land k \in I) \to {(f (k) - g (k))}^{2} \in ℝ$
25	10 24	regsumfsum	$⊢ (I \in Fin \land f \in B \land g \in B) \to \underset{k \in I}{\sum_{ℂ_{fld} ↾_{𝑠} ℝ}} {(f (k) - g (k))}^{2} = \sum_{k \in I} {(f (k) - g (k))}^{2}$
26	9 25	eqtr2id	$⊢ (I \in Fin \land f \in B \land g \in B) \to \sum_{k \in I} {(f (k) - g (k))}^{2} = \underset{k \in I}{\sum_{ℝ_{fld}}} {(f (k) - g (k))}^{2}$
27	26	fveq2d	$⊢ (I \in Fin \land f \in B \land g \in B) \to \sqrt{\sum_{k \in I} {(f (k) - g (k))}^{2}} = \sqrt{\underset{k \in I}{\sum_{ℝ_{fld}}} {(f (k) - g (k))}^{2}}$
28	27	3expb	$⊢ (I \in Fin \land (f \in B \land g \in B)) \to \sqrt{\sum_{k \in I} {(f (k) - g (k))}^{2}} = \sqrt{\underset{k \in I}{\sum_{ℝ_{fld}}} {(f (k) - g (k))}^{2}}$
29	6 7 28	mpoeq123dva	$⊢ I \in Fin \to (f \in B, g \in B ⟼ \sqrt{\sum_{k \in I} {(f (k) - g (k))}^{2}}) = (f \in {Base}_{H}, g \in {Base}_{H} ⟼ \sqrt{\underset{k \in I}{\sum_{ℝ_{fld}}} {(f (k) - g (k))}^{2}})$
30	1 4	rrxds	$⊢ I \in Fin \to (f \in {Base}_{H}, g \in {Base}_{H} ⟼ \sqrt{\underset{k \in I}{\sum_{ℝ_{fld}}} {(f (k) - g (k))}^{2}}) = dist (H)$
31	29 30	eqtr2d	$⊢ I \in Fin \to dist (H) = (f \in B, g \in B ⟼ \sqrt{\sum_{k \in I} {(f (k) - g (k))}^{2}})$

Metamath Proof Explorer

Theorem rrxdsfi

Proof