Metamath Proof Explorer

Theorem rrxmet

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

Ref Expression
Hypotheses rrxmval.1 ⊢ 𝑋 = { ℎ ∈ ( ℝ ↑m 𝐼 ) ∣ ℎ finSupp 0 }
rrxmval.d ⊢ 𝐷 = ( dist ‘ ( ℝ^ ‘ 𝐼 ) )
Assertion rrxmet ( 𝐼 ∈ 𝑉 → 𝐷 ∈ ( Met ‘ 𝑋 ) )

Proof

Step Hyp Ref Expression
1 rrxmval.1 ⊢ 𝑋 = { ℎ ∈ ( ℝ ↑m 𝐼 ) ∣ ℎ finSupp 0 }
2 rrxmval.d ⊢ 𝐷 = ( dist ‘ ( ℝ^ ‘ 𝐼 ) )
3 simprl ⊢ ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → 𝑥 ∈ 𝑋 )
4 1 3 rrxfsupp ⊢ ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝑥 supp 0 ) ∈ Fin )
5 simprr ⊢ ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → 𝑦 ∈ 𝑋 )
6 1 5 rrxfsupp ⊢ ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝑦 supp 0 ) ∈ Fin )
7 unfi ⊢ ( ( ( 𝑥 supp 0 ) ∈ Fin ∧ ( 𝑦 supp 0 ) ∈ Fin ) → ( ( 𝑥 supp 0 ) ∪ ( 𝑦 supp 0 ) ) ∈ Fin )
8 4 6 7 syl2anc ⊢ ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( ( 𝑥 supp 0 ) ∪ ( 𝑦 supp 0 ) ) ∈ Fin )
9 1 3 rrxsuppss ⊢ ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝑥 supp 0 ) ⊆ 𝐼 )
10 1 5 rrxsuppss ⊢ ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝑦 supp 0 ) ⊆ 𝐼 )
11 9 10 unssd ⊢ ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( ( 𝑥 supp 0 ) ∪ ( 𝑦 supp 0 ) ) ⊆ 𝐼 )
12 11 sselda ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ 𝑘 ∈ ( ( 𝑥 supp 0 ) ∪ ( 𝑦 supp 0 ) ) ) → 𝑘 ∈ 𝐼 )
13 1 3 rrxf ⊢ ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → 𝑥 : 𝐼 ⟶ ℝ )
14 13 ffvelrnda ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ 𝑘 ∈ 𝐼 ) → ( 𝑥 ‘ 𝑘 ) ∈ ℝ )
15 1 5 rrxf ⊢ ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → 𝑦 : 𝐼 ⟶ ℝ )
16 15 ffvelrnda ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ 𝑘 ∈ 𝐼 ) → ( 𝑦 ‘ 𝑘 ) ∈ ℝ )
17 14 16 resubcld ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ 𝑘 ∈ 𝐼 ) → ( ( 𝑥 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ∈ ℝ )
18 17 resqcld ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ 𝑘 ∈ 𝐼 ) → ( ( ( 𝑥 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ↑ 2 ) ∈ ℝ )
19 12 18 syldan ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ 𝑘 ∈ ( ( 𝑥 supp 0 ) ∪ ( 𝑦 supp 0 ) ) ) → ( ( ( 𝑥 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ↑ 2 ) ∈ ℝ )
20 8 19 fsumrecl ⊢ ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → Σ 𝑘 ∈ ( ( 𝑥 supp 0 ) ∪ ( 𝑦 supp 0 ) ) ( ( ( 𝑥 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ↑ 2 ) ∈ ℝ )
21 17 sqge0d ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ 𝑘 ∈ 𝐼 ) → 0 ≤ ( ( ( 𝑥 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ↑ 2 ) )
22 12 21 syldan ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ 𝑘 ∈ ( ( 𝑥 supp 0 ) ∪ ( 𝑦 supp 0 ) ) ) → 0 ≤ ( ( ( 𝑥 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ↑ 2 ) )
23 8 19 22 fsumge0 ⊢ ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → 0 ≤ Σ 𝑘 ∈ ( ( 𝑥 supp 0 ) ∪ ( 𝑦 supp 0 ) ) ( ( ( 𝑥 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ↑ 2 ) )
24 20 23 resqrtcld ⊢ ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( √ ‘ Σ 𝑘 ∈ ( ( 𝑥 supp 0 ) ∪ ( 𝑦 supp 0 ) ) ( ( ( 𝑥 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ↑ 2 ) ) ∈ ℝ )
25 24 ralrimivva ⊢ ( 𝐼 ∈ 𝑉 → ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( √ ‘ Σ 𝑘 ∈ ( ( 𝑥 supp 0 ) ∪ ( 𝑦 supp 0 ) ) ( ( ( 𝑥 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ↑ 2 ) ) ∈ ℝ )
26 eqid ⊢ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ( √ ‘ Σ 𝑘 ∈ ( ( 𝑥 supp 0 ) ∪ ( 𝑦 supp 0 ) ) ( ( ( 𝑥 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ↑ 2 ) ) ) = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ( √ ‘ Σ 𝑘 ∈ ( ( 𝑥 supp 0 ) ∪ ( 𝑦 supp 0 ) ) ( ( ( 𝑥 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ↑ 2 ) ) )
27 26 fmpo ⊢ ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( √ ‘ Σ 𝑘 ∈ ( ( 𝑥 supp 0 ) ∪ ( 𝑦 supp 0 ) ) ( ( ( 𝑥 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ↑ 2 ) ) ∈ ℝ ↔ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ( √ ‘ Σ 𝑘 ∈ ( ( 𝑥 supp 0 ) ∪ ( 𝑦 supp 0 ) ) ( ( ( 𝑥 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ↑ 2 ) ) ) : ( 𝑋 × 𝑋 ) ⟶ ℝ )
28 25 27 sylib ⊢ ( 𝐼 ∈ 𝑉 → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ( √ ‘ Σ 𝑘 ∈ ( ( 𝑥 supp 0 ) ∪ ( 𝑦 supp 0 ) ) ( ( ( 𝑥 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ↑ 2 ) ) ) : ( 𝑋 × 𝑋 ) ⟶ ℝ )
29 1 2 rrxmfval ⊢ ( 𝐼 ∈ 𝑉 → 𝐷 = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ( √ ‘ Σ 𝑘 ∈ ( ( 𝑥 supp 0 ) ∪ ( 𝑦 supp 0 ) ) ( ( ( 𝑥 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ↑ 2 ) ) ) )
30 29 feq1d ⊢ ( 𝐼 ∈ 𝑉 → ( 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ ↔ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ( √ ‘ Σ 𝑘 ∈ ( ( 𝑥 supp 0 ) ∪ ( 𝑦 supp 0 ) ) ( ( ( 𝑥 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ↑ 2 ) ) ) : ( 𝑋 × 𝑋 ) ⟶ ℝ ) )
31 28 30 mpbird ⊢ ( 𝐼 ∈ 𝑉 → 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ )
32 sqrt00 ⊢ ( ( Σ 𝑘 ∈ ( ( 𝑥 supp 0 ) ∪ ( 𝑦 supp 0 ) ) ( ( ( 𝑥 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ↑ 2 ) ∈ ℝ ∧ 0 ≤ Σ 𝑘 ∈ ( ( 𝑥 supp 0 ) ∪ ( 𝑦 supp 0 ) ) ( ( ( 𝑥 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ↑ 2 ) ) → ( ( √ ‘ Σ 𝑘 ∈ ( ( 𝑥 supp 0 ) ∪ ( 𝑦 supp 0 ) ) ( ( ( 𝑥 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ↑ 2 ) ) = 0 ↔ Σ 𝑘 ∈ ( ( 𝑥 supp 0 ) ∪ ( 𝑦 supp 0 ) ) ( ( ( 𝑥 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ↑ 2 ) = 0 ) )
33 20 23 32 syl2anc ⊢ ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( ( √ ‘ Σ 𝑘 ∈ ( ( 𝑥 supp 0 ) ∪ ( 𝑦 supp 0 ) ) ( ( ( 𝑥 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ↑ 2 ) ) = 0 ↔ Σ 𝑘 ∈ ( ( 𝑥 supp 0 ) ∪ ( 𝑦 supp 0 ) ) ( ( ( 𝑥 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ↑ 2 ) = 0 ) )
34 8 19 22 fsum00 ⊢ ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( Σ 𝑘 ∈ ( ( 𝑥 supp 0 ) ∪ ( 𝑦 supp 0 ) ) ( ( ( 𝑥 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ↑ 2 ) = 0 ↔ ∀ 𝑘 ∈ ( ( 𝑥 supp 0 ) ∪ ( 𝑦 supp 0 ) ) ( ( ( 𝑥 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ↑ 2 ) = 0 ) )
35 17 recnd ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ 𝑘 ∈ 𝐼 ) → ( ( 𝑥 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ∈ ℂ )
36 sqeq0 ⊢ ( ( ( 𝑥 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ∈ ℂ → ( ( ( ( 𝑥 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ↑ 2 ) = 0 ↔ ( ( 𝑥 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) = 0 ) )
37 35 36 syl ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ 𝑘 ∈ 𝐼 ) → ( ( ( ( 𝑥 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ↑ 2 ) = 0 ↔ ( ( 𝑥 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) = 0 ) )
38 14 recnd ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ 𝑘 ∈ 𝐼 ) → ( 𝑥 ‘ 𝑘 ) ∈ ℂ )
39 16 recnd ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ 𝑘 ∈ 𝐼 ) → ( 𝑦 ‘ 𝑘 ) ∈ ℂ )
40 38 39 subeq0ad ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ 𝑘 ∈ 𝐼 ) → ( ( ( 𝑥 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) = 0 ↔ ( 𝑥 ‘ 𝑘 ) = ( 𝑦 ‘ 𝑘 ) ) )
41 37 40 bitrd ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ 𝑘 ∈ 𝐼 ) → ( ( ( ( 𝑥 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ↑ 2 ) = 0 ↔ ( 𝑥 ‘ 𝑘 ) = ( 𝑦 ‘ 𝑘 ) ) )
42 12 41 syldan ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ 𝑘 ∈ ( ( 𝑥 supp 0 ) ∪ ( 𝑦 supp 0 ) ) ) → ( ( ( ( 𝑥 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ↑ 2 ) = 0 ↔ ( 𝑥 ‘ 𝑘 ) = ( 𝑦 ‘ 𝑘 ) ) )
43 42 ralbidva ⊢ ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( ∀ 𝑘 ∈ ( ( 𝑥 supp 0 ) ∪ ( 𝑦 supp 0 ) ) ( ( ( 𝑥 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ↑ 2 ) = 0 ↔ ∀ 𝑘 ∈ ( ( 𝑥 supp 0 ) ∪ ( 𝑦 supp 0 ) ) ( 𝑥 ‘ 𝑘 ) = ( 𝑦 ‘ 𝑘 ) ) )
44 33 34 43 3bitrd ⊢ ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( ( √ ‘ Σ 𝑘 ∈ ( ( 𝑥 supp 0 ) ∪ ( 𝑦 supp 0 ) ) ( ( ( 𝑥 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ↑ 2 ) ) = 0 ↔ ∀ 𝑘 ∈ ( ( 𝑥 supp 0 ) ∪ ( 𝑦 supp 0 ) ) ( 𝑥 ‘ 𝑘 ) = ( 𝑦 ‘ 𝑘 ) ) )
45 1 2 rrxmval ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( 𝑥 𝐷 𝑦 ) = ( √ ‘ Σ 𝑘 ∈ ( ( 𝑥 supp 0 ) ∪ ( 𝑦 supp 0 ) ) ( ( ( 𝑥 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ↑ 2 ) ) )
46 45 3expb ⊢ ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝑥 𝐷 𝑦 ) = ( √ ‘ Σ 𝑘 ∈ ( ( 𝑥 supp 0 ) ∪ ( 𝑦 supp 0 ) ) ( ( ( 𝑥 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ↑ 2 ) ) )
47 46 eqeq1d ⊢ ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( ( 𝑥 𝐷 𝑦 ) = 0 ↔ ( √ ‘ Σ 𝑘 ∈ ( ( 𝑥 supp 0 ) ∪ ( 𝑦 supp 0 ) ) ( ( ( 𝑥 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ↑ 2 ) ) = 0 ) )
48 13 ffnd ⊢ ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → 𝑥 Fn 𝐼 )
49 15 ffnd ⊢ ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → 𝑦 Fn 𝐼 )
50 eqfnfv ⊢ ( ( 𝑥 Fn 𝐼 ∧ 𝑦 Fn 𝐼 ) → ( 𝑥 = 𝑦 ↔ ∀ 𝑘 ∈ 𝐼 ( 𝑥 ‘ 𝑘 ) = ( 𝑦 ‘ 𝑘 ) ) )
51 48 49 50 syl2anc ⊢ ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝑥 = 𝑦 ↔ ∀ 𝑘 ∈ 𝐼 ( 𝑥 ‘ 𝑘 ) = ( 𝑦 ‘ 𝑘 ) ) )
52 ssun1 ⊢ ( 𝑥 supp 0 ) ⊆ ( ( 𝑥 supp 0 ) ∪ ( 𝑦 supp 0 ) )
53 52 a1i ⊢ ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝑥 supp 0 ) ⊆ ( ( 𝑥 supp 0 ) ∪ ( 𝑦 supp 0 ) ) )
54 simpl ⊢ ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → 𝐼 ∈ 𝑉 )
55 0red ⊢ ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → 0 ∈ ℝ )
56 13 53 54 55 suppssr ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ 𝑘 ∈ ( 𝐼 ∖ ( ( 𝑥 supp 0 ) ∪ ( 𝑦 supp 0 ) ) ) ) → ( 𝑥 ‘ 𝑘 ) = 0 )
57 ssun2 ⊢ ( 𝑦 supp 0 ) ⊆ ( ( 𝑥 supp 0 ) ∪ ( 𝑦 supp 0 ) )
58 57 a1i ⊢ ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝑦 supp 0 ) ⊆ ( ( 𝑥 supp 0 ) ∪ ( 𝑦 supp 0 ) ) )
59 15 58 54 55 suppssr ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ 𝑘 ∈ ( 𝐼 ∖ ( ( 𝑥 supp 0 ) ∪ ( 𝑦 supp 0 ) ) ) ) → ( 𝑦 ‘ 𝑘 ) = 0 )
60 56 59 eqtr4d ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ 𝑘 ∈ ( 𝐼 ∖ ( ( 𝑥 supp 0 ) ∪ ( 𝑦 supp 0 ) ) ) ) → ( 𝑥 ‘ 𝑘 ) = ( 𝑦 ‘ 𝑘 ) )
61 60 ralrimiva ⊢ ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ∀ 𝑘 ∈ ( 𝐼 ∖ ( ( 𝑥 supp 0 ) ∪ ( 𝑦 supp 0 ) ) ) ( 𝑥 ‘ 𝑘 ) = ( 𝑦 ‘ 𝑘 ) )
62 11 61 raldifeq ⊢ ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( ∀ 𝑘 ∈ ( ( 𝑥 supp 0 ) ∪ ( 𝑦 supp 0 ) ) ( 𝑥 ‘ 𝑘 ) = ( 𝑦 ‘ 𝑘 ) ↔ ∀ 𝑘 ∈ 𝐼 ( 𝑥 ‘ 𝑘 ) = ( 𝑦 ‘ 𝑘 ) ) )
63 51 62 bitr4d ⊢ ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝑥 = 𝑦 ↔ ∀ 𝑘 ∈ ( ( 𝑥 supp 0 ) ∪ ( 𝑦 supp 0 ) ) ( 𝑥 ‘ 𝑘 ) = ( 𝑦 ‘ 𝑘 ) ) )
64 44 47 63 3bitr4d ⊢ ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( ( 𝑥 𝐷 𝑦 ) = 0 ↔ 𝑥 = 𝑦 ) )
65 8 3adant2 ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( ( 𝑥 supp 0 ) ∪ ( 𝑦 supp 0 ) ) ∈ Fin )
66 simp2 ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → 𝑧 ∈ 𝑋 )
67 1 66 rrxfsupp ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝑧 supp 0 ) ∈ Fin )
68 unfi ⊢ ( ( ( ( 𝑥 supp 0 ) ∪ ( 𝑦 supp 0 ) ) ∈ Fin ∧ ( 𝑧 supp 0 ) ∈ Fin ) → ( ( ( 𝑥 supp 0 ) ∪ ( 𝑦 supp 0 ) ) ∪ ( 𝑧 supp 0 ) ) ∈ Fin )
69 65 67 68 syl2anc ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( ( ( 𝑥 supp 0 ) ∪ ( 𝑦 supp 0 ) ) ∪ ( 𝑧 supp 0 ) ) ∈ Fin )
70 69 3expa ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋 ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( ( ( 𝑥 supp 0 ) ∪ ( 𝑦 supp 0 ) ) ∪ ( 𝑧 supp 0 ) ) ∈ Fin )
71 70 an32s ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ 𝑧 ∈ 𝑋 ) → ( ( ( 𝑥 supp 0 ) ∪ ( 𝑦 supp 0 ) ) ∪ ( 𝑧 supp 0 ) ) ∈ Fin )
72 11 adantr ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ 𝑧 ∈ 𝑋 ) → ( ( 𝑥 supp 0 ) ∪ ( 𝑦 supp 0 ) ) ⊆ 𝐼 )
73 simpr ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ 𝑧 ∈ 𝑋 ) → 𝑧 ∈ 𝑋 )
74 1 73 rrxsuppss ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ 𝑧 ∈ 𝑋 ) → ( 𝑧 supp 0 ) ⊆ 𝐼 )
75 72 74 unssd ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ 𝑧 ∈ 𝑋 ) → ( ( ( 𝑥 supp 0 ) ∪ ( 𝑦 supp 0 ) ) ∪ ( 𝑧 supp 0 ) ) ⊆ 𝐼 )
76 75 sselda ⊢ ( ( ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ 𝑧 ∈ 𝑋 ) ∧ 𝑘 ∈ ( ( ( 𝑥 supp 0 ) ∪ ( 𝑦 supp 0 ) ) ∪ ( 𝑧 supp 0 ) ) ) → 𝑘 ∈ 𝐼 )
77 14 adantlr ⊢ ( ( ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ 𝑧 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝐼 ) → ( 𝑥 ‘ 𝑘 ) ∈ ℝ )
78 1 73 rrxf ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ 𝑧 ∈ 𝑋 ) → 𝑧 : 𝐼 ⟶ ℝ )
79 78 ffvelrnda ⊢ ( ( ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ 𝑧 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝐼 ) → ( 𝑧 ‘ 𝑘 ) ∈ ℝ )
80 77 79 resubcld ⊢ ( ( ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ 𝑧 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝐼 ) → ( ( 𝑥 ‘ 𝑘 ) − ( 𝑧 ‘ 𝑘 ) ) ∈ ℝ )
81 76 80 syldan ⊢ ( ( ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ 𝑧 ∈ 𝑋 ) ∧ 𝑘 ∈ ( ( ( 𝑥 supp 0 ) ∪ ( 𝑦 supp 0 ) ) ∪ ( 𝑧 supp 0 ) ) ) → ( ( 𝑥 ‘ 𝑘 ) − ( 𝑧 ‘ 𝑘 ) ) ∈ ℝ )
82 16 adantlr ⊢ ( ( ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ 𝑧 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝐼 ) → ( 𝑦 ‘ 𝑘 ) ∈ ℝ )
83 79 82 resubcld ⊢ ( ( ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ 𝑧 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝐼 ) → ( ( 𝑧 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ∈ ℝ )
84 76 83 syldan ⊢ ( ( ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ 𝑧 ∈ 𝑋 ) ∧ 𝑘 ∈ ( ( ( 𝑥 supp 0 ) ∪ ( 𝑦 supp 0 ) ) ∪ ( 𝑧 supp 0 ) ) ) → ( ( 𝑧 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ∈ ℝ )
85 71 81 84 trirn ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ 𝑧 ∈ 𝑋 ) → ( √ ‘ Σ 𝑘 ∈ ( ( ( 𝑥 supp 0 ) ∪ ( 𝑦 supp 0 ) ) ∪ ( 𝑧 supp 0 ) ) ( ( ( ( 𝑥 ‘ 𝑘 ) − ( 𝑧 ‘ 𝑘 ) ) + ( ( 𝑧 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ) ↑ 2 ) ) ≤ ( ( √ ‘ Σ 𝑘 ∈ ( ( ( 𝑥 supp 0 ) ∪ ( 𝑦 supp 0 ) ) ∪ ( 𝑧 supp 0 ) ) ( ( ( 𝑥 ‘ 𝑘 ) − ( 𝑧 ‘ 𝑘 ) ) ↑ 2 ) ) + ( √ ‘ Σ 𝑘 ∈ ( ( ( 𝑥 supp 0 ) ∪ ( 𝑦 supp 0 ) ) ∪ ( 𝑧 supp 0 ) ) ( ( ( 𝑧 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ↑ 2 ) ) ) )
86 38 adantlr ⊢ ( ( ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ 𝑧 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝐼 ) → ( 𝑥 ‘ 𝑘 ) ∈ ℂ )
87 79 recnd ⊢ ( ( ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ 𝑧 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝐼 ) → ( 𝑧 ‘ 𝑘 ) ∈ ℂ )
88 39 adantlr ⊢ ( ( ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ 𝑧 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝐼 ) → ( 𝑦 ‘ 𝑘 ) ∈ ℂ )
89 86 87 88 npncand ⊢ ( ( ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ 𝑧 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝐼 ) → ( ( ( 𝑥 ‘ 𝑘 ) − ( 𝑧 ‘ 𝑘 ) ) + ( ( 𝑧 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ) = ( ( 𝑥 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) )
90 89 oveq1d ⊢ ( ( ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ 𝑧 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝐼 ) → ( ( ( ( 𝑥 ‘ 𝑘 ) − ( 𝑧 ‘ 𝑘 ) ) + ( ( 𝑧 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ) ↑ 2 ) = ( ( ( 𝑥 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ↑ 2 ) )
91 76 90 syldan ⊢ ( ( ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ 𝑧 ∈ 𝑋 ) ∧ 𝑘 ∈ ( ( ( 𝑥 supp 0 ) ∪ ( 𝑦 supp 0 ) ) ∪ ( 𝑧 supp 0 ) ) ) → ( ( ( ( 𝑥 ‘ 𝑘 ) − ( 𝑧 ‘ 𝑘 ) ) + ( ( 𝑧 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ) ↑ 2 ) = ( ( ( 𝑥 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ↑ 2 ) )
92 91 sumeq2dv ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ 𝑧 ∈ 𝑋 ) → Σ 𝑘 ∈ ( ( ( 𝑥 supp 0 ) ∪ ( 𝑦 supp 0 ) ) ∪ ( 𝑧 supp 0 ) ) ( ( ( ( 𝑥 ‘ 𝑘 ) − ( 𝑧 ‘ 𝑘 ) ) + ( ( 𝑧 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ) ↑ 2 ) = Σ 𝑘 ∈ ( ( ( 𝑥 supp 0 ) ∪ ( 𝑦 supp 0 ) ) ∪ ( 𝑧 supp 0 ) ) ( ( ( 𝑥 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ↑ 2 ) )
93 92 fveq2d ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ 𝑧 ∈ 𝑋 ) → ( √ ‘ Σ 𝑘 ∈ ( ( ( 𝑥 supp 0 ) ∪ ( 𝑦 supp 0 ) ) ∪ ( 𝑧 supp 0 ) ) ( ( ( ( 𝑥 ‘ 𝑘 ) − ( 𝑧 ‘ 𝑘 ) ) + ( ( 𝑧 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ) ↑ 2 ) ) = ( √ ‘ Σ 𝑘 ∈ ( ( ( 𝑥 supp 0 ) ∪ ( 𝑦 supp 0 ) ) ∪ ( 𝑧 supp 0 ) ) ( ( ( 𝑥 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ↑ 2 ) ) )
94 sqsubswap ⊢ ( ( ( 𝑥 ‘ 𝑘 ) ∈ ℂ ∧ ( 𝑧 ‘ 𝑘 ) ∈ ℂ ) → ( ( ( 𝑥 ‘ 𝑘 ) − ( 𝑧 ‘ 𝑘 ) ) ↑ 2 ) = ( ( ( 𝑧 ‘ 𝑘 ) − ( 𝑥 ‘ 𝑘 ) ) ↑ 2 ) )
95 86 87 94 syl2anc ⊢ ( ( ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ 𝑧 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝐼 ) → ( ( ( 𝑥 ‘ 𝑘 ) − ( 𝑧 ‘ 𝑘 ) ) ↑ 2 ) = ( ( ( 𝑧 ‘ 𝑘 ) − ( 𝑥 ‘ 𝑘 ) ) ↑ 2 ) )
96 76 95 syldan ⊢ ( ( ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ 𝑧 ∈ 𝑋 ) ∧ 𝑘 ∈ ( ( ( 𝑥 supp 0 ) ∪ ( 𝑦 supp 0 ) ) ∪ ( 𝑧 supp 0 ) ) ) → ( ( ( 𝑥 ‘ 𝑘 ) − ( 𝑧 ‘ 𝑘 ) ) ↑ 2 ) = ( ( ( 𝑧 ‘ 𝑘 ) − ( 𝑥 ‘ 𝑘 ) ) ↑ 2 ) )
97 96 sumeq2dv ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ 𝑧 ∈ 𝑋 ) → Σ 𝑘 ∈ ( ( ( 𝑥 supp 0 ) ∪ ( 𝑦 supp 0 ) ) ∪ ( 𝑧 supp 0 ) ) ( ( ( 𝑥 ‘ 𝑘 ) − ( 𝑧 ‘ 𝑘 ) ) ↑ 2 ) = Σ 𝑘 ∈ ( ( ( 𝑥 supp 0 ) ∪ ( 𝑦 supp 0 ) ) ∪ ( 𝑧 supp 0 ) ) ( ( ( 𝑧 ‘ 𝑘 ) − ( 𝑥 ‘ 𝑘 ) ) ↑ 2 ) )
98 97 fveq2d ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ 𝑧 ∈ 𝑋 ) → ( √ ‘ Σ 𝑘 ∈ ( ( ( 𝑥 supp 0 ) ∪ ( 𝑦 supp 0 ) ) ∪ ( 𝑧 supp 0 ) ) ( ( ( 𝑥 ‘ 𝑘 ) − ( 𝑧 ‘ 𝑘 ) ) ↑ 2 ) ) = ( √ ‘ Σ 𝑘 ∈ ( ( ( 𝑥 supp 0 ) ∪ ( 𝑦 supp 0 ) ) ∪ ( 𝑧 supp 0 ) ) ( ( ( 𝑧 ‘ 𝑘 ) − ( 𝑥 ‘ 𝑘 ) ) ↑ 2 ) ) )
99 98 oveq1d ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ 𝑧 ∈ 𝑋 ) → ( ( √ ‘ Σ 𝑘 ∈ ( ( ( 𝑥 supp 0 ) ∪ ( 𝑦 supp 0 ) ) ∪ ( 𝑧 supp 0 ) ) ( ( ( 𝑥 ‘ 𝑘 ) − ( 𝑧 ‘ 𝑘 ) ) ↑ 2 ) ) + ( √ ‘ Σ 𝑘 ∈ ( ( ( 𝑥 supp 0 ) ∪ ( 𝑦 supp 0 ) ) ∪ ( 𝑧 supp 0 ) ) ( ( ( 𝑧 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ↑ 2 ) ) ) = ( ( √ ‘ Σ 𝑘 ∈ ( ( ( 𝑥 supp 0 ) ∪ ( 𝑦 supp 0 ) ) ∪ ( 𝑧 supp 0 ) ) ( ( ( 𝑧 ‘ 𝑘 ) − ( 𝑥 ‘ 𝑘 ) ) ↑ 2 ) ) + ( √ ‘ Σ 𝑘 ∈ ( ( ( 𝑥 supp 0 ) ∪ ( 𝑦 supp 0 ) ) ∪ ( 𝑧 supp 0 ) ) ( ( ( 𝑧 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ↑ 2 ) ) ) )
100 85 93 99 3brtr3d ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ 𝑧 ∈ 𝑋 ) → ( √ ‘ Σ 𝑘 ∈ ( ( ( 𝑥 supp 0 ) ∪ ( 𝑦 supp 0 ) ) ∪ ( 𝑧 supp 0 ) ) ( ( ( 𝑥 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ↑ 2 ) ) ≤ ( ( √ ‘ Σ 𝑘 ∈ ( ( ( 𝑥 supp 0 ) ∪ ( 𝑦 supp 0 ) ) ∪ ( 𝑧 supp 0 ) ) ( ( ( 𝑧 ‘ 𝑘 ) − ( 𝑥 ‘ 𝑘 ) ) ↑ 2 ) ) + ( √ ‘ Σ 𝑘 ∈ ( ( ( 𝑥 supp 0 ) ∪ ( 𝑦 supp 0 ) ) ∪ ( 𝑧 supp 0 ) ) ( ( ( 𝑧 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ↑ 2 ) ) ) )
101 46 adantr ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ 𝑧 ∈ 𝑋 ) → ( 𝑥 𝐷 𝑦 ) = ( √ ‘ Σ 𝑘 ∈ ( ( 𝑥 supp 0 ) ∪ ( 𝑦 supp 0 ) ) ( ( ( 𝑥 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ↑ 2 ) ) )
102 simp1 ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → 𝐼 ∈ 𝑉 )
103 3 3adant2 ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → 𝑥 ∈ 𝑋 )
104 5 3adant2 ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → 𝑦 ∈ 𝑋 )
105 1 103 rrxsuppss ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝑥 supp 0 ) ⊆ 𝐼 )
106 1 104 rrxsuppss ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝑦 supp 0 ) ⊆ 𝐼 )
107 105 106 unssd ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( ( 𝑥 supp 0 ) ∪ ( 𝑦 supp 0 ) ) ⊆ 𝐼 )
108 1 66 rrxsuppss ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝑧 supp 0 ) ⊆ 𝐼 )
109 107 108 unssd ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( ( ( 𝑥 supp 0 ) ∪ ( 𝑦 supp 0 ) ) ∪ ( 𝑧 supp 0 ) ) ⊆ 𝐼 )
110 ssun1 ⊢ ( ( 𝑥 supp 0 ) ∪ ( 𝑦 supp 0 ) ) ⊆ ( ( ( 𝑥 supp 0 ) ∪ ( 𝑦 supp 0 ) ) ∪ ( 𝑧 supp 0 ) )
111 110 a1i ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( ( 𝑥 supp 0 ) ∪ ( 𝑦 supp 0 ) ) ⊆ ( ( ( 𝑥 supp 0 ) ∪ ( 𝑦 supp 0 ) ) ∪ ( 𝑧 supp 0 ) ) )
112 1 2 102 103 104 109 69 111 rrxmetlem ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → Σ 𝑘 ∈ ( ( 𝑥 supp 0 ) ∪ ( 𝑦 supp 0 ) ) ( ( ( 𝑥 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ↑ 2 ) = Σ 𝑘 ∈ ( ( ( 𝑥 supp 0 ) ∪ ( 𝑦 supp 0 ) ) ∪ ( 𝑧 supp 0 ) ) ( ( ( 𝑥 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ↑ 2 ) )
113 112 fveq2d ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( √ ‘ Σ 𝑘 ∈ ( ( 𝑥 supp 0 ) ∪ ( 𝑦 supp 0 ) ) ( ( ( 𝑥 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ↑ 2 ) ) = ( √ ‘ Σ 𝑘 ∈ ( ( ( 𝑥 supp 0 ) ∪ ( 𝑦 supp 0 ) ) ∪ ( 𝑧 supp 0 ) ) ( ( ( 𝑥 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ↑ 2 ) ) )
114 113 3expa ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋 ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( √ ‘ Σ 𝑘 ∈ ( ( 𝑥 supp 0 ) ∪ ( 𝑦 supp 0 ) ) ( ( ( 𝑥 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ↑ 2 ) ) = ( √ ‘ Σ 𝑘 ∈ ( ( ( 𝑥 supp 0 ) ∪ ( 𝑦 supp 0 ) ) ∪ ( 𝑧 supp 0 ) ) ( ( ( 𝑥 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ↑ 2 ) ) )
115 114 an32s ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ 𝑧 ∈ 𝑋 ) → ( √ ‘ Σ 𝑘 ∈ ( ( 𝑥 supp 0 ) ∪ ( 𝑦 supp 0 ) ) ( ( ( 𝑥 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ↑ 2 ) ) = ( √ ‘ Σ 𝑘 ∈ ( ( ( 𝑥 supp 0 ) ∪ ( 𝑦 supp 0 ) ) ∪ ( 𝑧 supp 0 ) ) ( ( ( 𝑥 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ↑ 2 ) ) )
116 101 115 eqtrd ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ 𝑧 ∈ 𝑋 ) → ( 𝑥 𝐷 𝑦 ) = ( √ ‘ Σ 𝑘 ∈ ( ( ( 𝑥 supp 0 ) ∪ ( 𝑦 supp 0 ) ) ∪ ( 𝑧 supp 0 ) ) ( ( ( 𝑥 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ↑ 2 ) ) )
117 1 2 rrxmval ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ) → ( 𝑧 𝐷 𝑥 ) = ( √ ‘ Σ 𝑘 ∈ ( ( 𝑧 supp 0 ) ∪ ( 𝑥 supp 0 ) ) ( ( ( 𝑧 ‘ 𝑘 ) − ( 𝑥 ‘ 𝑘 ) ) ↑ 2 ) ) )
118 117 3adant3r ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝑧 𝐷 𝑥 ) = ( √ ‘ Σ 𝑘 ∈ ( ( 𝑧 supp 0 ) ∪ ( 𝑥 supp 0 ) ) ( ( ( 𝑧 ‘ 𝑘 ) − ( 𝑥 ‘ 𝑘 ) ) ↑ 2 ) ) )
119 1 2 rrxmval ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( 𝑧 𝐷 𝑦 ) = ( √ ‘ Σ 𝑘 ∈ ( ( 𝑧 supp 0 ) ∪ ( 𝑦 supp 0 ) ) ( ( ( 𝑧 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ↑ 2 ) ) )
120 119 3adant3l ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝑧 𝐷 𝑦 ) = ( √ ‘ Σ 𝑘 ∈ ( ( 𝑧 supp 0 ) ∪ ( 𝑦 supp 0 ) ) ( ( ( 𝑧 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ↑ 2 ) ) )
121 118 120 oveq12d ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( ( 𝑧 𝐷 𝑥 ) + ( 𝑧 𝐷 𝑦 ) ) = ( ( √ ‘ Σ 𝑘 ∈ ( ( 𝑧 supp 0 ) ∪ ( 𝑥 supp 0 ) ) ( ( ( 𝑧 ‘ 𝑘 ) − ( 𝑥 ‘ 𝑘 ) ) ↑ 2 ) ) + ( √ ‘ Σ 𝑘 ∈ ( ( 𝑧 supp 0 ) ∪ ( 𝑦 supp 0 ) ) ( ( ( 𝑧 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ↑ 2 ) ) ) )
122 ssun2 ⊢ ( 𝑧 supp 0 ) ⊆ ( ( ( 𝑥 supp 0 ) ∪ ( 𝑦 supp 0 ) ) ∪ ( 𝑧 supp 0 ) )
123 122 a1i ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝑧 supp 0 ) ⊆ ( ( ( 𝑥 supp 0 ) ∪ ( 𝑦 supp 0 ) ) ∪ ( 𝑧 supp 0 ) ) )
124 52 110 sstri ⊢ ( 𝑥 supp 0 ) ⊆ ( ( ( 𝑥 supp 0 ) ∪ ( 𝑦 supp 0 ) ) ∪ ( 𝑧 supp 0 ) )
125 124 a1i ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝑥 supp 0 ) ⊆ ( ( ( 𝑥 supp 0 ) ∪ ( 𝑦 supp 0 ) ) ∪ ( 𝑧 supp 0 ) ) )
126 123 125 unssd ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( ( 𝑧 supp 0 ) ∪ ( 𝑥 supp 0 ) ) ⊆ ( ( ( 𝑥 supp 0 ) ∪ ( 𝑦 supp 0 ) ) ∪ ( 𝑧 supp 0 ) ) )
127 1 2 102 66 103 109 69 126 rrxmetlem ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → Σ 𝑘 ∈ ( ( 𝑧 supp 0 ) ∪ ( 𝑥 supp 0 ) ) ( ( ( 𝑧 ‘ 𝑘 ) − ( 𝑥 ‘ 𝑘 ) ) ↑ 2 ) = Σ 𝑘 ∈ ( ( ( 𝑥 supp 0 ) ∪ ( 𝑦 supp 0 ) ) ∪ ( 𝑧 supp 0 ) ) ( ( ( 𝑧 ‘ 𝑘 ) − ( 𝑥 ‘ 𝑘 ) ) ↑ 2 ) )
128 127 fveq2d ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( √ ‘ Σ 𝑘 ∈ ( ( 𝑧 supp 0 ) ∪ ( 𝑥 supp 0 ) ) ( ( ( 𝑧 ‘ 𝑘 ) − ( 𝑥 ‘ 𝑘 ) ) ↑ 2 ) ) = ( √ ‘ Σ 𝑘 ∈ ( ( ( 𝑥 supp 0 ) ∪ ( 𝑦 supp 0 ) ) ∪ ( 𝑧 supp 0 ) ) ( ( ( 𝑧 ‘ 𝑘 ) − ( 𝑥 ‘ 𝑘 ) ) ↑ 2 ) ) )
129 57 110 sstri ⊢ ( 𝑦 supp 0 ) ⊆ ( ( ( 𝑥 supp 0 ) ∪ ( 𝑦 supp 0 ) ) ∪ ( 𝑧 supp 0 ) )
130 129 a1i ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝑦 supp 0 ) ⊆ ( ( ( 𝑥 supp 0 ) ∪ ( 𝑦 supp 0 ) ) ∪ ( 𝑧 supp 0 ) ) )
131 123 130 unssd ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( ( 𝑧 supp 0 ) ∪ ( 𝑦 supp 0 ) ) ⊆ ( ( ( 𝑥 supp 0 ) ∪ ( 𝑦 supp 0 ) ) ∪ ( 𝑧 supp 0 ) ) )
132 1 2 102 66 104 109 69 131 rrxmetlem ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → Σ 𝑘 ∈ ( ( 𝑧 supp 0 ) ∪ ( 𝑦 supp 0 ) ) ( ( ( 𝑧 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ↑ 2 ) = Σ 𝑘 ∈ ( ( ( 𝑥 supp 0 ) ∪ ( 𝑦 supp 0 ) ) ∪ ( 𝑧 supp 0 ) ) ( ( ( 𝑧 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ↑ 2 ) )
133 132 fveq2d ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( √ ‘ Σ 𝑘 ∈ ( ( 𝑧 supp 0 ) ∪ ( 𝑦 supp 0 ) ) ( ( ( 𝑧 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ↑ 2 ) ) = ( √ ‘ Σ 𝑘 ∈ ( ( ( 𝑥 supp 0 ) ∪ ( 𝑦 supp 0 ) ) ∪ ( 𝑧 supp 0 ) ) ( ( ( 𝑧 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ↑ 2 ) ) )
134 128 133 oveq12d ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( ( √ ‘ Σ 𝑘 ∈ ( ( 𝑧 supp 0 ) ∪ ( 𝑥 supp 0 ) ) ( ( ( 𝑧 ‘ 𝑘 ) − ( 𝑥 ‘ 𝑘 ) ) ↑ 2 ) ) + ( √ ‘ Σ 𝑘 ∈ ( ( 𝑧 supp 0 ) ∪ ( 𝑦 supp 0 ) ) ( ( ( 𝑧 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ↑ 2 ) ) ) = ( ( √ ‘ Σ 𝑘 ∈ ( ( ( 𝑥 supp 0 ) ∪ ( 𝑦 supp 0 ) ) ∪ ( 𝑧 supp 0 ) ) ( ( ( 𝑧 ‘ 𝑘 ) − ( 𝑥 ‘ 𝑘 ) ) ↑ 2 ) ) + ( √ ‘ Σ 𝑘 ∈ ( ( ( 𝑥 supp 0 ) ∪ ( 𝑦 supp 0 ) ) ∪ ( 𝑧 supp 0 ) ) ( ( ( 𝑧 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ↑ 2 ) ) ) )
135 121 134 eqtrd ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( ( 𝑧 𝐷 𝑥 ) + ( 𝑧 𝐷 𝑦 ) ) = ( ( √ ‘ Σ 𝑘 ∈ ( ( ( 𝑥 supp 0 ) ∪ ( 𝑦 supp 0 ) ) ∪ ( 𝑧 supp 0 ) ) ( ( ( 𝑧 ‘ 𝑘 ) − ( 𝑥 ‘ 𝑘 ) ) ↑ 2 ) ) + ( √ ‘ Σ 𝑘 ∈ ( ( ( 𝑥 supp 0 ) ∪ ( 𝑦 supp 0 ) ) ∪ ( 𝑧 supp 0 ) ) ( ( ( 𝑧 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ↑ 2 ) ) ) )
136 135 3expa ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋 ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( ( 𝑧 𝐷 𝑥 ) + ( 𝑧 𝐷 𝑦 ) ) = ( ( √ ‘ Σ 𝑘 ∈ ( ( ( 𝑥 supp 0 ) ∪ ( 𝑦 supp 0 ) ) ∪ ( 𝑧 supp 0 ) ) ( ( ( 𝑧 ‘ 𝑘 ) − ( 𝑥 ‘ 𝑘 ) ) ↑ 2 ) ) + ( √ ‘ Σ 𝑘 ∈ ( ( ( 𝑥 supp 0 ) ∪ ( 𝑦 supp 0 ) ) ∪ ( 𝑧 supp 0 ) ) ( ( ( 𝑧 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ↑ 2 ) ) ) )
137 136 an32s ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ 𝑧 ∈ 𝑋 ) → ( ( 𝑧 𝐷 𝑥 ) + ( 𝑧 𝐷 𝑦 ) ) = ( ( √ ‘ Σ 𝑘 ∈ ( ( ( 𝑥 supp 0 ) ∪ ( 𝑦 supp 0 ) ) ∪ ( 𝑧 supp 0 ) ) ( ( ( 𝑧 ‘ 𝑘 ) − ( 𝑥 ‘ 𝑘 ) ) ↑ 2 ) ) + ( √ ‘ Σ 𝑘 ∈ ( ( ( 𝑥 supp 0 ) ∪ ( 𝑦 supp 0 ) ) ∪ ( 𝑧 supp 0 ) ) ( ( ( 𝑧 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ↑ 2 ) ) ) )
138 100 116 137 3brtr4d ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ 𝑧 ∈ 𝑋 ) → ( 𝑥 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 𝑥 ) + ( 𝑧 𝐷 𝑦 ) ) )
139 138 ralrimiva ⊢ ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ∀ 𝑧 ∈ 𝑋 ( 𝑥 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 𝑥 ) + ( 𝑧 𝐷 𝑦 ) ) )
140 64 139 jca ⊢ ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( ( ( 𝑥 𝐷 𝑦 ) = 0 ↔ 𝑥 = 𝑦 ) ∧ ∀ 𝑧 ∈ 𝑋 ( 𝑥 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 𝑥 ) + ( 𝑧 𝐷 𝑦 ) ) ) )
141 140 ralrimivva ⊢ ( 𝐼 ∈ 𝑉 → ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( ( 𝑥 𝐷 𝑦 ) = 0 ↔ 𝑥 = 𝑦 ) ∧ ∀ 𝑧 ∈ 𝑋 ( 𝑥 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 𝑥 ) + ( 𝑧 𝐷 𝑦 ) ) ) )
142 ovex ⊢ ( ℝ ↑m 𝐼 ) ∈ V
143 1 142 rabex2 ⊢ 𝑋 ∈ V
144 ismet ⊢ ( 𝑋 ∈ V → ( 𝐷 ∈ ( Met ‘ 𝑋 ) ↔ ( 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( ( 𝑥 𝐷 𝑦 ) = 0 ↔ 𝑥 = 𝑦 ) ∧ ∀ 𝑧 ∈ 𝑋 ( 𝑥 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 𝑥 ) + ( 𝑧 𝐷 𝑦 ) ) ) ) ) )
145 143 144 ax-mp ⊢ ( 𝐷 ∈ ( Met ‘ 𝑋 ) ↔ ( 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( ( 𝑥 𝐷 𝑦 ) = 0 ↔ 𝑥 = 𝑦 ) ∧ ∀ 𝑧 ∈ 𝑋 ( 𝑥 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 𝑥 ) + ( 𝑧 𝐷 𝑦 ) ) ) ) )
146 31 141 145 sylanbrc ⊢ ( 𝐼 ∈ 𝑉 → 𝐷 ∈ ( Met ‘ 𝑋 ) )