Definition df-rrn

Description: Define n-dimensional Euclidean space as a metric space with the standard Euclidean norm given by the quadratic mean. (Contributed by Jeff Madsen, 2-Sep-2009)

	Ref	Expression
Assertion	df-rrn	⊢ ℝn = ( 𝑖 ∈ Fin ↦ ( 𝑥 ∈ ( ℝ ↑m 𝑖 ) , 𝑦 ∈ ( ℝ ↑m 𝑖 ) ↦ ( √ ‘ Σ 𝑘 ∈ 𝑖 ( ( ( 𝑥 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ↑ 2 ) ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		crrn	⊢ ℝn
1		vi	⊢ 𝑖
2		cfn	⊢ Fin
3		vx	⊢ 𝑥
4		cr	⊢ ℝ
5		cmap	⊢ ↑m
6	1	cv	⊢ 𝑖
7	4 6 5	co	⊢ ( ℝ ↑m 𝑖 )
8		vy	⊢ 𝑦
9		csqrt	⊢ √
10		vk	⊢ 𝑘
11	3	cv	⊢ 𝑥
12	10	cv	⊢ 𝑘
13	12 11	cfv	⊢ ( 𝑥 ‘ 𝑘 )
14		cmin	⊢ −
15	8	cv	⊢ 𝑦
16	12 15	cfv	⊢ ( 𝑦 ‘ 𝑘 )
17	13 16 14	co	⊢ ( ( 𝑥 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) )
18		cexp	⊢ ↑
19		c2	⊢ 2
20	17 19 18	co	⊢ ( ( ( 𝑥 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ↑ 2 )
21	6 20 10	csu	⊢ Σ 𝑘 ∈ 𝑖 ( ( ( 𝑥 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ↑ 2 )
22	21 9	cfv	⊢ ( √ ‘ Σ 𝑘 ∈ 𝑖 ( ( ( 𝑥 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ↑ 2 ) )
23	3 8 7 7 22	cmpo	⊢ ( 𝑥 ∈ ( ℝ ↑m 𝑖 ) , 𝑦 ∈ ( ℝ ↑m 𝑖 ) ↦ ( √ ‘ Σ 𝑘 ∈ 𝑖 ( ( ( 𝑥 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ↑ 2 ) ) )
24	1 2 23	cmpt	⊢ ( 𝑖 ∈ Fin ↦ ( 𝑥 ∈ ( ℝ ↑m 𝑖 ) , 𝑦 ∈ ( ℝ ↑m 𝑖 ) ↦ ( √ ‘ Σ 𝑘 ∈ 𝑖 ( ( ( 𝑥 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ↑ 2 ) ) ) )
25	0 24	wceq	⊢ ℝn = ( 𝑖 ∈ Fin ↦ ( 𝑥 ∈ ( ℝ ↑m 𝑖 ) , 𝑦 ∈ ( ℝ ↑m 𝑖 ) ↦ ( √ ‘ Σ 𝑘 ∈ 𝑖 ( ( ( 𝑥 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ↑ 2 ) ) ) )