Definition df-rrn 33625

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.)

Assertion

Ref	Expression
df-rrn	|- Rn = ( i e. Fin |-> ( x e. ( RR ^m i ) , y e. ( RR ^m i ) |-> ( sqr ` sum_ k e. i ( ( ( x ` k ) - ( y ` k ) ) ^ 2 ) ) ) )

Distinct variable group:   x, i, y, k

Detailed syntax breakdown of Definition df-rrn

Step	Hyp	Ref	Expression
1		crrn 33624	. 2 class Rn
2		vi	. . 3 setvar i
3		cfn 7955	. . 3 class Fin
4		vx	. . . 4 setvar x
5		vy	. . . 4 setvar y
6		cr 9935	. . . . 5 class RR
7	2	cv 1482	. . . . 5 class i
8		cmap 7857	. . . . 5 class ^m
9	6, 7, 8	co 6650	. . . 4 class ( RR ^m i )
10		vk	. . . . . . . . . 10 setvar k
11	10	cv 1482	. . . . . . . . 9 class k
12	4	cv 1482	. . . . . . . . 9 class x
13	11, 12	cfv 5888	. . . . . . . 8 class ( x ` k )
14	5	cv 1482	. . . . . . . . 9 class y
15	11, 14	cfv 5888	. . . . . . . 8 class ( y ` k )
16		cmin 10266	. . . . . . . 8 class -
17	13, 15, 16	co 6650	. . . . . . 7 class ( ( x ` k ) - ( y ` k ) )
18		c2 11070	. . . . . . 7 class 2
19		cexp 12860	. . . . . . 7 class ^
20	17, 18, 19	co 6650	. . . . . 6 class ( ( ( x ` k ) - ( y ` k ) ) ^ 2 )
21	7, 20, 10	csu 14416	. . . . 5 class sum_ k e. i ( ( ( x ` k ) - ( y ` k ) ) ^ 2 )
22		csqrt 13973	. . . . 5 class sqr
23	21, 22	cfv 5888	. . . 4 class ( sqr ` sum_ k e. i ( ( ( x ` k ) - ( y ` k ) ) ^ 2 ) )
24	4, 5, 9, 9, 23	cmpt2 6652	. . 3 class ( x e. ( RR ^m i ) , y e. ( RR ^m i ) |-> ( sqr ` sum_ k e. i ( ( ( x ` k ) - ( y ` k ) ) ^ 2 ) ) )
25	2, 3, 24	cmpt 4729	. 2 class ( i e. Fin |-> ( x e. ( RR ^m i ) , y e. ( RR ^m i ) |-> ( sqr ` sum_ k e. i ( ( ( x ` k ) - ( y ` k ) ) ^ 2 ) ) ) )
26	1, 25	wceq 1483	1 wff Rn = ( i e. Fin |-> ( x e. ( RR ^m i ) , y e. ( RR ^m i ) |-> ( sqr ` sum_ k e. i ( ( ( x ` k ) - ( y ` k ) ) ^ 2 ) ) ) )

This definition is referenced by:  rrnval  33626