Metamath Proof Explorer


Theorem rrnval

Description: The n-dimensional Euclidean space. (Contributed by Jeff Madsen, 2-Sep-2009) (Revised by Mario Carneiro, 13-Sep-2015)

Ref Expression
Hypothesis rrnval.1 X = I
Assertion rrnval I Fin n I = x X , y X k I x k y k 2

Proof

Step Hyp Ref Expression
1 rrnval.1 X = I
2 oveq2 i = I i = I
3 2 1 eqtr4di i = I i = X
4 sumeq1 i = I k i x k y k 2 = k I x k y k 2
5 4 fveq2d i = I k i x k y k 2 = k I x k y k 2
6 3 3 5 mpoeq123dv i = I x i , y i k i x k y k 2 = x X , y X k I x k y k 2
7 df-rrn n = i Fin x i , y i k i x k y k 2
8 fvrn0 k I x k y k 2 ran
9 8 rgen2w x X y X k I x k y k 2 ran
10 eqid x X , y X k I x k y k 2 = x X , y X k I x k y k 2
11 10 fmpo x X y X k I x k y k 2 ran x X , y X k I x k y k 2 : X × X ran
12 9 11 mpbi x X , y X k I x k y k 2 : X × X ran
13 ovex I V
14 1 13 eqeltri X V
15 14 14 xpex X × X V
16 cnex V
17 sqrtf :
18 frn : ran
19 17 18 ax-mp ran
20 16 19 ssexi ran V
21 p0ex V
22 20 21 unex ran V
23 fex2 x X , y X k I x k y k 2 : X × X ran X × X V ran V x X , y X k I x k y k 2 V
24 12 15 22 23 mp3an x X , y X k I x k y k 2 V
25 6 7 24 fvmpt I Fin n I = x X , y X k I x k y k 2