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