Metamath Proof Explorer

Theorem rrnmet

Description: Euclidean space is a metric space. (Contributed by Jeff Madsen, 2-Sep-2009) (Proof shortened by Mario Carneiro, 5-Jun-2014)

Ref Expression
Hypothesis rrnval.1 ⊢ 𝑋 = ( ℝ ↑m 𝐼 )
Assertion rrnmet ( 𝐼 ∈ Fin → ( ℝn ‘ 𝐼 ) ∈ ( Met ‘ 𝑋 ) )

Proof

Step Hyp Ref Expression
1 rrnval.1 ⊢ 𝑋 = ( ℝ ↑m 𝐼 )
2 simpl ⊢ ( ( 𝐼 ∈ Fin ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → 𝐼 ∈ Fin )
3 simprl ⊢ ( ( 𝐼 ∈ Fin ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → 𝑥 ∈ 𝑋 )
4 3 1 eleqtrdi ⊢ ( ( 𝐼 ∈ Fin ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → 𝑥 ∈ ( ℝ ↑m 𝐼 ) )
5 elmapi ⊢ ( 𝑥 ∈ ( ℝ ↑m 𝐼 ) → 𝑥 : 𝐼 ⟶ ℝ )
6 4 5 syl ⊢ ( ( 𝐼 ∈ Fin ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → 𝑥 : 𝐼 ⟶ ℝ )
7 6 ffvelcdmda ⊢ ( ( ( 𝐼 ∈ Fin ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ 𝑘 ∈ 𝐼 ) → ( 𝑥 ‘ 𝑘 ) ∈ ℝ )
8 simprr ⊢ ( ( 𝐼 ∈ Fin ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → 𝑦 ∈ 𝑋 )
9 8 1 eleqtrdi ⊢ ( ( 𝐼 ∈ Fin ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → 𝑦 ∈ ( ℝ ↑m 𝐼 ) )
10 elmapi ⊢ ( 𝑦 ∈ ( ℝ ↑m 𝐼 ) → 𝑦 : 𝐼 ⟶ ℝ )
11 9 10 syl ⊢ ( ( 𝐼 ∈ Fin ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → 𝑦 : 𝐼 ⟶ ℝ )
12 11 ffvelcdmda ⊢ ( ( ( 𝐼 ∈ Fin ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ 𝑘 ∈ 𝐼 ) → ( 𝑦 ‘ 𝑘 ) ∈ ℝ )
13 7 12 resubcld ⊢ ( ( ( 𝐼 ∈ Fin ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ 𝑘 ∈ 𝐼 ) → ( ( 𝑥 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ∈ ℝ )
14 13 resqcld ⊢ ( ( ( 𝐼 ∈ Fin ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ 𝑘 ∈ 𝐼 ) → ( ( ( 𝑥 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ↑ 2 ) ∈ ℝ )
15 2 14 fsumrecl ⊢ ( ( 𝐼 ∈ Fin ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → Σ 𝑘 ∈ 𝐼 ( ( ( 𝑥 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ↑ 2 ) ∈ ℝ )
16 13 sqge0d ⊢ ( ( ( 𝐼 ∈ Fin ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ 𝑘 ∈ 𝐼 ) → 0 ≤ ( ( ( 𝑥 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ↑ 2 ) )
17 2 14 16 fsumge0 ⊢ ( ( 𝐼 ∈ Fin ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → 0 ≤ Σ 𝑘 ∈ 𝐼 ( ( ( 𝑥 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ↑ 2 ) )
18 15 17 resqrtcld ⊢ ( ( 𝐼 ∈ Fin ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( √ ‘ Σ 𝑘 ∈ 𝐼 ( ( ( 𝑥 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ↑ 2 ) ) ∈ ℝ )
19 18 ralrimivva ⊢ ( 𝐼 ∈ Fin → ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( √ ‘ Σ 𝑘 ∈ 𝐼 ( ( ( 𝑥 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ↑ 2 ) ) ∈ ℝ )
20 eqid ⊢ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ( √ ‘ Σ 𝑘 ∈ 𝐼 ( ( ( 𝑥 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ↑ 2 ) ) ) = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ( √ ‘ Σ 𝑘 ∈ 𝐼 ( ( ( 𝑥 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ↑ 2 ) ) )
21 20 fmpo ⊢ ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( √ ‘ Σ 𝑘 ∈ 𝐼 ( ( ( 𝑥 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ↑ 2 ) ) ∈ ℝ ↔ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ( √ ‘ Σ 𝑘 ∈ 𝐼 ( ( ( 𝑥 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ↑ 2 ) ) ) : ( 𝑋 × 𝑋 ) ⟶ ℝ )
22 19 21 sylib ⊢ ( 𝐼 ∈ Fin → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ( √ ‘ Σ 𝑘 ∈ 𝐼 ( ( ( 𝑥 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ↑ 2 ) ) ) : ( 𝑋 × 𝑋 ) ⟶ ℝ )
23 1 rrnval ⊢ ( 𝐼 ∈ Fin → ( ℝn ‘ 𝐼 ) = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ( √ ‘ Σ 𝑘 ∈ 𝐼 ( ( ( 𝑥 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ↑ 2 ) ) ) )
24 23 feq1d ⊢ ( 𝐼 ∈ Fin → ( ( ℝn ‘ 𝐼 ) : ( 𝑋 × 𝑋 ) ⟶ ℝ ↔ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ( √ ‘ Σ 𝑘 ∈ 𝐼 ( ( ( 𝑥 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ↑ 2 ) ) ) : ( 𝑋 × 𝑋 ) ⟶ ℝ ) )
25 22 24 mpbird ⊢ ( 𝐼 ∈ Fin → ( ℝn ‘ 𝐼 ) : ( 𝑋 × 𝑋 ) ⟶ ℝ )
26 sqrt00 ⊢ ( ( Σ 𝑘 ∈ 𝐼 ( ( ( 𝑥 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ↑ 2 ) ∈ ℝ ∧ 0 ≤ Σ 𝑘 ∈ 𝐼 ( ( ( 𝑥 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ↑ 2 ) ) → ( ( √ ‘ Σ 𝑘 ∈ 𝐼 ( ( ( 𝑥 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ↑ 2 ) ) = 0 ↔ Σ 𝑘 ∈ 𝐼 ( ( ( 𝑥 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ↑ 2 ) = 0 ) )
27 15 17 26 syl2anc ⊢ ( ( 𝐼 ∈ Fin ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( ( √ ‘ Σ 𝑘 ∈ 𝐼 ( ( ( 𝑥 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ↑ 2 ) ) = 0 ↔ Σ 𝑘 ∈ 𝐼 ( ( ( 𝑥 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ↑ 2 ) = 0 ) )
28 2 14 16 fsum00 ⊢ ( ( 𝐼 ∈ Fin ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( Σ 𝑘 ∈ 𝐼 ( ( ( 𝑥 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ↑ 2 ) = 0 ↔ ∀ 𝑘 ∈ 𝐼 ( ( ( 𝑥 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ↑ 2 ) = 0 ) )
29 27 28 bitrd ⊢ ( ( 𝐼 ∈ Fin ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( ( √ ‘ Σ 𝑘 ∈ 𝐼 ( ( ( 𝑥 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ↑ 2 ) ) = 0 ↔ ∀ 𝑘 ∈ 𝐼 ( ( ( 𝑥 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ↑ 2 ) = 0 ) )
30 13 recnd ⊢ ( ( ( 𝐼 ∈ Fin ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ 𝑘 ∈ 𝐼 ) → ( ( 𝑥 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ∈ ℂ )
31 sqeq0 ⊢ ( ( ( 𝑥 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ∈ ℂ → ( ( ( ( 𝑥 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ↑ 2 ) = 0 ↔ ( ( 𝑥 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) = 0 ) )
32 30 31 syl ⊢ ( ( ( 𝐼 ∈ Fin ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ 𝑘 ∈ 𝐼 ) → ( ( ( ( 𝑥 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ↑ 2 ) = 0 ↔ ( ( 𝑥 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) = 0 ) )
33 7 recnd ⊢ ( ( ( 𝐼 ∈ Fin ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ 𝑘 ∈ 𝐼 ) → ( 𝑥 ‘ 𝑘 ) ∈ ℂ )
34 12 recnd ⊢ ( ( ( 𝐼 ∈ Fin ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ 𝑘 ∈ 𝐼 ) → ( 𝑦 ‘ 𝑘 ) ∈ ℂ )
35 33 34 subeq0ad ⊢ ( ( ( 𝐼 ∈ Fin ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ 𝑘 ∈ 𝐼 ) → ( ( ( 𝑥 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) = 0 ↔ ( 𝑥 ‘ 𝑘 ) = ( 𝑦 ‘ 𝑘 ) ) )
36 32 35 bitrd ⊢ ( ( ( 𝐼 ∈ Fin ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ 𝑘 ∈ 𝐼 ) → ( ( ( ( 𝑥 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ↑ 2 ) = 0 ↔ ( 𝑥 ‘ 𝑘 ) = ( 𝑦 ‘ 𝑘 ) ) )
37 36 ralbidva ⊢ ( ( 𝐼 ∈ Fin ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( ∀ 𝑘 ∈ 𝐼 ( ( ( 𝑥 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ↑ 2 ) = 0 ↔ ∀ 𝑘 ∈ 𝐼 ( 𝑥 ‘ 𝑘 ) = ( 𝑦 ‘ 𝑘 ) ) )
38 29 37 bitrd ⊢ ( ( 𝐼 ∈ Fin ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( ( √ ‘ Σ 𝑘 ∈ 𝐼 ( ( ( 𝑥 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ↑ 2 ) ) = 0 ↔ ∀ 𝑘 ∈ 𝐼 ( 𝑥 ‘ 𝑘 ) = ( 𝑦 ‘ 𝑘 ) ) )
39 1 rrnmval ⊢ ( ( 𝐼 ∈ Fin ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( 𝑥 ( ℝn ‘ 𝐼 ) 𝑦 ) = ( √ ‘ Σ 𝑘 ∈ 𝐼 ( ( ( 𝑥 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ↑ 2 ) ) )
40 39 3expb ⊢ ( ( 𝐼 ∈ Fin ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝑥 ( ℝn ‘ 𝐼 ) 𝑦 ) = ( √ ‘ Σ 𝑘 ∈ 𝐼 ( ( ( 𝑥 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ↑ 2 ) ) )
41 40 eqeq1d ⊢ ( ( 𝐼 ∈ Fin ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( ( 𝑥 ( ℝn ‘ 𝐼 ) 𝑦 ) = 0 ↔ ( √ ‘ Σ 𝑘 ∈ 𝐼 ( ( ( 𝑥 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ↑ 2 ) ) = 0 ) )
42 6 ffnd ⊢ ( ( 𝐼 ∈ Fin ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → 𝑥 Fn 𝐼 )
43 11 ffnd ⊢ ( ( 𝐼 ∈ Fin ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → 𝑦 Fn 𝐼 )
44 eqfnfv ⊢ ( ( 𝑥 Fn 𝐼 ∧ 𝑦 Fn 𝐼 ) → ( 𝑥 = 𝑦 ↔ ∀ 𝑘 ∈ 𝐼 ( 𝑥 ‘ 𝑘 ) = ( 𝑦 ‘ 𝑘 ) ) )
45 42 43 44 syl2anc ⊢ ( ( 𝐼 ∈ Fin ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝑥 = 𝑦 ↔ ∀ 𝑘 ∈ 𝐼 ( 𝑥 ‘ 𝑘 ) = ( 𝑦 ‘ 𝑘 ) ) )
46 38 41 45 3bitr4d ⊢ ( ( 𝐼 ∈ Fin ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( ( 𝑥 ( ℝn ‘ 𝐼 ) 𝑦 ) = 0 ↔ 𝑥 = 𝑦 ) )
47 simpll ⊢ ( ( ( 𝐼 ∈ Fin ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ 𝑧 ∈ 𝑋 ) → 𝐼 ∈ Fin )
48 7 adantlr ⊢ ( ( ( ( 𝐼 ∈ Fin ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ 𝑧 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝐼 ) → ( 𝑥 ‘ 𝑘 ) ∈ ℝ )
49 simpr ⊢ ( ( ( 𝐼 ∈ Fin ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ 𝑧 ∈ 𝑋 ) → 𝑧 ∈ 𝑋 )
50 49 1 eleqtrdi ⊢ ( ( ( 𝐼 ∈ Fin ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ 𝑧 ∈ 𝑋 ) → 𝑧 ∈ ( ℝ ↑m 𝐼 ) )
51 elmapi ⊢ ( 𝑧 ∈ ( ℝ ↑m 𝐼 ) → 𝑧 : 𝐼 ⟶ ℝ )
52 50 51 syl ⊢ ( ( ( 𝐼 ∈ Fin ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ 𝑧 ∈ 𝑋 ) → 𝑧 : 𝐼 ⟶ ℝ )
53 52 ffvelcdmda ⊢ ( ( ( ( 𝐼 ∈ Fin ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ 𝑧 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝐼 ) → ( 𝑧 ‘ 𝑘 ) ∈ ℝ )
54 48 53 resubcld ⊢ ( ( ( ( 𝐼 ∈ Fin ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ 𝑧 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝐼 ) → ( ( 𝑥 ‘ 𝑘 ) − ( 𝑧 ‘ 𝑘 ) ) ∈ ℝ )
55 12 adantlr ⊢ ( ( ( ( 𝐼 ∈ Fin ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ 𝑧 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝐼 ) → ( 𝑦 ‘ 𝑘 ) ∈ ℝ )
56 53 55 resubcld ⊢ ( ( ( ( 𝐼 ∈ Fin ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ 𝑧 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝐼 ) → ( ( 𝑧 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ∈ ℝ )
57 47 54 56 trirn ⊢ ( ( ( 𝐼 ∈ Fin ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ 𝑧 ∈ 𝑋 ) → ( √ ‘ Σ 𝑘 ∈ 𝐼 ( ( ( ( 𝑥 ‘ 𝑘 ) − ( 𝑧 ‘ 𝑘 ) ) + ( ( 𝑧 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ) ↑ 2 ) ) ≤ ( ( √ ‘ Σ 𝑘 ∈ 𝐼 ( ( ( 𝑥 ‘ 𝑘 ) − ( 𝑧 ‘ 𝑘 ) ) ↑ 2 ) ) + ( √ ‘ Σ 𝑘 ∈ 𝐼 ( ( ( 𝑧 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ↑ 2 ) ) ) )
58 33 adantlr ⊢ ( ( ( ( 𝐼 ∈ Fin ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ 𝑧 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝐼 ) → ( 𝑥 ‘ 𝑘 ) ∈ ℂ )
59 53 recnd ⊢ ( ( ( ( 𝐼 ∈ Fin ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ 𝑧 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝐼 ) → ( 𝑧 ‘ 𝑘 ) ∈ ℂ )
60 34 adantlr ⊢ ( ( ( ( 𝐼 ∈ Fin ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ 𝑧 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝐼 ) → ( 𝑦 ‘ 𝑘 ) ∈ ℂ )
61 58 59 60 npncand ⊢ ( ( ( ( 𝐼 ∈ Fin ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ 𝑧 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝐼 ) → ( ( ( 𝑥 ‘ 𝑘 ) − ( 𝑧 ‘ 𝑘 ) ) + ( ( 𝑧 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ) = ( ( 𝑥 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) )
62 61 oveq1d ⊢ ( ( ( ( 𝐼 ∈ Fin ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ 𝑧 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝐼 ) → ( ( ( ( 𝑥 ‘ 𝑘 ) − ( 𝑧 ‘ 𝑘 ) ) + ( ( 𝑧 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ) ↑ 2 ) = ( ( ( 𝑥 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ↑ 2 ) )
63 62 sumeq2dv ⊢ ( ( ( 𝐼 ∈ Fin ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ 𝑧 ∈ 𝑋 ) → Σ 𝑘 ∈ 𝐼 ( ( ( ( 𝑥 ‘ 𝑘 ) − ( 𝑧 ‘ 𝑘 ) ) + ( ( 𝑧 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ) ↑ 2 ) = Σ 𝑘 ∈ 𝐼 ( ( ( 𝑥 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ↑ 2 ) )
64 63 fveq2d ⊢ ( ( ( 𝐼 ∈ Fin ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ 𝑧 ∈ 𝑋 ) → ( √ ‘ Σ 𝑘 ∈ 𝐼 ( ( ( ( 𝑥 ‘ 𝑘 ) − ( 𝑧 ‘ 𝑘 ) ) + ( ( 𝑧 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ) ↑ 2 ) ) = ( √ ‘ Σ 𝑘 ∈ 𝐼 ( ( ( 𝑥 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ↑ 2 ) ) )
65 sqsubswap ⊢ ( ( ( 𝑥 ‘ 𝑘 ) ∈ ℂ ∧ ( 𝑧 ‘ 𝑘 ) ∈ ℂ ) → ( ( ( 𝑥 ‘ 𝑘 ) − ( 𝑧 ‘ 𝑘 ) ) ↑ 2 ) = ( ( ( 𝑧 ‘ 𝑘 ) − ( 𝑥 ‘ 𝑘 ) ) ↑ 2 ) )
66 58 59 65 syl2anc ⊢ ( ( ( ( 𝐼 ∈ Fin ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ 𝑧 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝐼 ) → ( ( ( 𝑥 ‘ 𝑘 ) − ( 𝑧 ‘ 𝑘 ) ) ↑ 2 ) = ( ( ( 𝑧 ‘ 𝑘 ) − ( 𝑥 ‘ 𝑘 ) ) ↑ 2 ) )
67 66 sumeq2dv ⊢ ( ( ( 𝐼 ∈ Fin ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ 𝑧 ∈ 𝑋 ) → Σ 𝑘 ∈ 𝐼 ( ( ( 𝑥 ‘ 𝑘 ) − ( 𝑧 ‘ 𝑘 ) ) ↑ 2 ) = Σ 𝑘 ∈ 𝐼 ( ( ( 𝑧 ‘ 𝑘 ) − ( 𝑥 ‘ 𝑘 ) ) ↑ 2 ) )
68 67 fveq2d ⊢ ( ( ( 𝐼 ∈ Fin ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ 𝑧 ∈ 𝑋 ) → ( √ ‘ Σ 𝑘 ∈ 𝐼 ( ( ( 𝑥 ‘ 𝑘 ) − ( 𝑧 ‘ 𝑘 ) ) ↑ 2 ) ) = ( √ ‘ Σ 𝑘 ∈ 𝐼 ( ( ( 𝑧 ‘ 𝑘 ) − ( 𝑥 ‘ 𝑘 ) ) ↑ 2 ) ) )
69 68 oveq1d ⊢ ( ( ( 𝐼 ∈ Fin ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ 𝑧 ∈ 𝑋 ) → ( ( √ ‘ Σ 𝑘 ∈ 𝐼 ( ( ( 𝑥 ‘ 𝑘 ) − ( 𝑧 ‘ 𝑘 ) ) ↑ 2 ) ) + ( √ ‘ Σ 𝑘 ∈ 𝐼 ( ( ( 𝑧 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ↑ 2 ) ) ) = ( ( √ ‘ Σ 𝑘 ∈ 𝐼 ( ( ( 𝑧 ‘ 𝑘 ) − ( 𝑥 ‘ 𝑘 ) ) ↑ 2 ) ) + ( √ ‘ Σ 𝑘 ∈ 𝐼 ( ( ( 𝑧 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ↑ 2 ) ) ) )
70 57 64 69 3brtr3d ⊢ ( ( ( 𝐼 ∈ Fin ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ 𝑧 ∈ 𝑋 ) → ( √ ‘ Σ 𝑘 ∈ 𝐼 ( ( ( 𝑥 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ↑ 2 ) ) ≤ ( ( √ ‘ Σ 𝑘 ∈ 𝐼 ( ( ( 𝑧 ‘ 𝑘 ) − ( 𝑥 ‘ 𝑘 ) ) ↑ 2 ) ) + ( √ ‘ Σ 𝑘 ∈ 𝐼 ( ( ( 𝑧 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ↑ 2 ) ) ) )
71 40 adantr ⊢ ( ( ( 𝐼 ∈ Fin ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ 𝑧 ∈ 𝑋 ) → ( 𝑥 ( ℝn ‘ 𝐼 ) 𝑦 ) = ( √ ‘ Σ 𝑘 ∈ 𝐼 ( ( ( 𝑥 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ↑ 2 ) ) )
72 1 rrnmval ⊢ ( ( 𝐼 ∈ Fin ∧ 𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ) → ( 𝑧 ( ℝn ‘ 𝐼 ) 𝑥 ) = ( √ ‘ Σ 𝑘 ∈ 𝐼 ( ( ( 𝑧 ‘ 𝑘 ) − ( 𝑥 ‘ 𝑘 ) ) ↑ 2 ) ) )
73 72 3adant3r ⊢ ( ( 𝐼 ∈ Fin ∧ 𝑧 ∈ 𝑋 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝑧 ( ℝn ‘ 𝐼 ) 𝑥 ) = ( √ ‘ Σ 𝑘 ∈ 𝐼 ( ( ( 𝑧 ‘ 𝑘 ) − ( 𝑥 ‘ 𝑘 ) ) ↑ 2 ) ) )
74 1 rrnmval ⊢ ( ( 𝐼 ∈ Fin ∧ 𝑧 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( 𝑧 ( ℝn ‘ 𝐼 ) 𝑦 ) = ( √ ‘ Σ 𝑘 ∈ 𝐼 ( ( ( 𝑧 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ↑ 2 ) ) )
75 74 3adant3l ⊢ ( ( 𝐼 ∈ Fin ∧ 𝑧 ∈ 𝑋 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝑧 ( ℝn ‘ 𝐼 ) 𝑦 ) = ( √ ‘ Σ 𝑘 ∈ 𝐼 ( ( ( 𝑧 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ↑ 2 ) ) )
76 73 75 oveq12d ⊢ ( ( 𝐼 ∈ Fin ∧ 𝑧 ∈ 𝑋 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( ( 𝑧 ( ℝn ‘ 𝐼 ) 𝑥 ) + ( 𝑧 ( ℝn ‘ 𝐼 ) 𝑦 ) ) = ( ( √ ‘ Σ 𝑘 ∈ 𝐼 ( ( ( 𝑧 ‘ 𝑘 ) − ( 𝑥 ‘ 𝑘 ) ) ↑ 2 ) ) + ( √ ‘ Σ 𝑘 ∈ 𝐼 ( ( ( 𝑧 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ↑ 2 ) ) ) )
77 76 3expa ⊢ ( ( ( 𝐼 ∈ Fin ∧ 𝑧 ∈ 𝑋 ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( ( 𝑧 ( ℝn ‘ 𝐼 ) 𝑥 ) + ( 𝑧 ( ℝn ‘ 𝐼 ) 𝑦 ) ) = ( ( √ ‘ Σ 𝑘 ∈ 𝐼 ( ( ( 𝑧 ‘ 𝑘 ) − ( 𝑥 ‘ 𝑘 ) ) ↑ 2 ) ) + ( √ ‘ Σ 𝑘 ∈ 𝐼 ( ( ( 𝑧 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ↑ 2 ) ) ) )
78 77 an32s ⊢ ( ( ( 𝐼 ∈ Fin ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ 𝑧 ∈ 𝑋 ) → ( ( 𝑧 ( ℝn ‘ 𝐼 ) 𝑥 ) + ( 𝑧 ( ℝn ‘ 𝐼 ) 𝑦 ) ) = ( ( √ ‘ Σ 𝑘 ∈ 𝐼 ( ( ( 𝑧 ‘ 𝑘 ) − ( 𝑥 ‘ 𝑘 ) ) ↑ 2 ) ) + ( √ ‘ Σ 𝑘 ∈ 𝐼 ( ( ( 𝑧 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ↑ 2 ) ) ) )
79 70 71 78 3brtr4d ⊢ ( ( ( 𝐼 ∈ Fin ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ 𝑧 ∈ 𝑋 ) → ( 𝑥 ( ℝn ‘ 𝐼 ) 𝑦 ) ≤ ( ( 𝑧 ( ℝn ‘ 𝐼 ) 𝑥 ) + ( 𝑧 ( ℝn ‘ 𝐼 ) 𝑦 ) ) )
80 79 ralrimiva ⊢ ( ( 𝐼 ∈ Fin ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ∀ 𝑧 ∈ 𝑋 ( 𝑥 ( ℝn ‘ 𝐼 ) 𝑦 ) ≤ ( ( 𝑧 ( ℝn ‘ 𝐼 ) 𝑥 ) + ( 𝑧 ( ℝn ‘ 𝐼 ) 𝑦 ) ) )
81 46 80 jca ⊢ ( ( 𝐼 ∈ Fin ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( ( ( 𝑥 ( ℝn ‘ 𝐼 ) 𝑦 ) = 0 ↔ 𝑥 = 𝑦 ) ∧ ∀ 𝑧 ∈ 𝑋 ( 𝑥 ( ℝn ‘ 𝐼 ) 𝑦 ) ≤ ( ( 𝑧 ( ℝn ‘ 𝐼 ) 𝑥 ) + ( 𝑧 ( ℝn ‘ 𝐼 ) 𝑦 ) ) ) )
82 81 ralrimivva ⊢ ( 𝐼 ∈ Fin → ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( ( 𝑥 ( ℝn ‘ 𝐼 ) 𝑦 ) = 0 ↔ 𝑥 = 𝑦 ) ∧ ∀ 𝑧 ∈ 𝑋 ( 𝑥 ( ℝn ‘ 𝐼 ) 𝑦 ) ≤ ( ( 𝑧 ( ℝn ‘ 𝐼 ) 𝑥 ) + ( 𝑧 ( ℝn ‘ 𝐼 ) 𝑦 ) ) ) )
83 ovex ⊢ ( ℝ ↑m 𝐼 ) ∈ V
84 1 83 eqeltri ⊢ 𝑋 ∈ V
85 ismet ⊢ ( 𝑋 ∈ V → ( ( ℝn ‘ 𝐼 ) ∈ ( Met ‘ 𝑋 ) ↔ ( ( ℝn ‘ 𝐼 ) : ( 𝑋 × 𝑋 ) ⟶ ℝ ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( ( 𝑥 ( ℝn ‘ 𝐼 ) 𝑦 ) = 0 ↔ 𝑥 = 𝑦 ) ∧ ∀ 𝑧 ∈ 𝑋 ( 𝑥 ( ℝn ‘ 𝐼 ) 𝑦 ) ≤ ( ( 𝑧 ( ℝn ‘ 𝐼 ) 𝑥 ) + ( 𝑧 ( ℝn ‘ 𝐼 ) 𝑦 ) ) ) ) ) )
86 84 85 ax-mp ⊢ ( ( ℝn ‘ 𝐼 ) ∈ ( Met ‘ 𝑋 ) ↔ ( ( ℝn ‘ 𝐼 ) : ( 𝑋 × 𝑋 ) ⟶ ℝ ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( ( 𝑥 ( ℝn ‘ 𝐼 ) 𝑦 ) = 0 ↔ 𝑥 = 𝑦 ) ∧ ∀ 𝑧 ∈ 𝑋 ( 𝑥 ( ℝn ‘ 𝐼 ) 𝑦 ) ≤ ( ( 𝑧 ( ℝn ‘ 𝐼 ) 𝑥 ) + ( 𝑧 ( ℝn ‘ 𝐼 ) 𝑦 ) ) ) ) )
87 25 82 86 sylanbrc ⊢ ( 𝐼 ∈ Fin → ( ℝn ‘ 𝐼 ) ∈ ( Met ‘ 𝑋 ) )