MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  rrxmet Structured version   Visualization version   GIF version

Theorem rrxmet 23714
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.)
Hypotheses
Ref Expression
rrxmval.1 𝑋 = { ∈ (ℝ ↑𝑚 𝐼) ∣ finSupp 0}
rrxmval.d 𝐷 = (dist‘(ℝ^‘𝐼))
Assertion
Ref Expression
rrxmet (𝐼𝑉𝐷 ∈ (Met‘𝑋))
Distinct variable groups:   ,𝐼   ,𝑉
Allowed substitution hints:   𝐷()   𝑋()

Proof of Theorem rrxmet
Dummy variables 𝑘 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 rrxmval.1 . . . . . . . . 9 𝑋 = { ∈ (ℝ ↑𝑚 𝐼) ∣ finSupp 0}
2 simprl 758 . . . . . . . . 9 ((𝐼𝑉 ∧ (𝑥𝑋𝑦𝑋)) → 𝑥𝑋)
31, 2rrxfsupp 23708 . . . . . . . 8 ((𝐼𝑉 ∧ (𝑥𝑋𝑦𝑋)) → (𝑥 supp 0) ∈ Fin)
4 simprr 760 . . . . . . . . 9 ((𝐼𝑉 ∧ (𝑥𝑋𝑦𝑋)) → 𝑦𝑋)
51, 4rrxfsupp 23708 . . . . . . . 8 ((𝐼𝑉 ∧ (𝑥𝑋𝑦𝑋)) → (𝑦 supp 0) ∈ Fin)
6 unfi 8580 . . . . . . . 8 (((𝑥 supp 0) ∈ Fin ∧ (𝑦 supp 0) ∈ Fin) → ((𝑥 supp 0) ∪ (𝑦 supp 0)) ∈ Fin)
73, 5, 6syl2anc 576 . . . . . . 7 ((𝐼𝑉 ∧ (𝑥𝑋𝑦𝑋)) → ((𝑥 supp 0) ∪ (𝑦 supp 0)) ∈ Fin)
81, 2rrxsuppss 23709 . . . . . . . . . 10 ((𝐼𝑉 ∧ (𝑥𝑋𝑦𝑋)) → (𝑥 supp 0) ⊆ 𝐼)
91, 4rrxsuppss 23709 . . . . . . . . . 10 ((𝐼𝑉 ∧ (𝑥𝑋𝑦𝑋)) → (𝑦 supp 0) ⊆ 𝐼)
108, 9unssd 4051 . . . . . . . . 9 ((𝐼𝑉 ∧ (𝑥𝑋𝑦𝑋)) → ((𝑥 supp 0) ∪ (𝑦 supp 0)) ⊆ 𝐼)
1110sselda 3859 . . . . . . . 8 (((𝐼𝑉 ∧ (𝑥𝑋𝑦𝑋)) ∧ 𝑘 ∈ ((𝑥 supp 0) ∪ (𝑦 supp 0))) → 𝑘𝐼)
121, 2rrxf 23707 . . . . . . . . . . 11 ((𝐼𝑉 ∧ (𝑥𝑋𝑦𝑋)) → 𝑥:𝐼⟶ℝ)
1312ffvelrnda 6676 . . . . . . . . . 10 (((𝐼𝑉 ∧ (𝑥𝑋𝑦𝑋)) ∧ 𝑘𝐼) → (𝑥𝑘) ∈ ℝ)
141, 4rrxf 23707 . . . . . . . . . . 11 ((𝐼𝑉 ∧ (𝑥𝑋𝑦𝑋)) → 𝑦:𝐼⟶ℝ)
1514ffvelrnda 6676 . . . . . . . . . 10 (((𝐼𝑉 ∧ (𝑥𝑋𝑦𝑋)) ∧ 𝑘𝐼) → (𝑦𝑘) ∈ ℝ)
1613, 15resubcld 10869 . . . . . . . . 9 (((𝐼𝑉 ∧ (𝑥𝑋𝑦𝑋)) ∧ 𝑘𝐼) → ((𝑥𝑘) − (𝑦𝑘)) ∈ ℝ)
1716resqcld 13426 . . . . . . . 8 (((𝐼𝑉 ∧ (𝑥𝑋𝑦𝑋)) ∧ 𝑘𝐼) → (((𝑥𝑘) − (𝑦𝑘))↑2) ∈ ℝ)
1811, 17syldan 582 . . . . . . 7 (((𝐼𝑉 ∧ (𝑥𝑋𝑦𝑋)) ∧ 𝑘 ∈ ((𝑥 supp 0) ∪ (𝑦 supp 0))) → (((𝑥𝑘) − (𝑦𝑘))↑2) ∈ ℝ)
197, 18fsumrecl 14951 . . . . . 6 ((𝐼𝑉 ∧ (𝑥𝑋𝑦𝑋)) → Σ𝑘 ∈ ((𝑥 supp 0) ∪ (𝑦 supp 0))(((𝑥𝑘) − (𝑦𝑘))↑2) ∈ ℝ)
2016sqge0d 13427 . . . . . . . 8 (((𝐼𝑉 ∧ (𝑥𝑋𝑦𝑋)) ∧ 𝑘𝐼) → 0 ≤ (((𝑥𝑘) − (𝑦𝑘))↑2))
2111, 20syldan 582 . . . . . . 7 (((𝐼𝑉 ∧ (𝑥𝑋𝑦𝑋)) ∧ 𝑘 ∈ ((𝑥 supp 0) ∪ (𝑦 supp 0))) → 0 ≤ (((𝑥𝑘) − (𝑦𝑘))↑2))
227, 18, 21fsumge0 15010 . . . . . 6 ((𝐼𝑉 ∧ (𝑥𝑋𝑦𝑋)) → 0 ≤ Σ𝑘 ∈ ((𝑥 supp 0) ∪ (𝑦 supp 0))(((𝑥𝑘) − (𝑦𝑘))↑2))
2319, 22resqrtcld 14638 . . . . 5 ((𝐼𝑉 ∧ (𝑥𝑋𝑦𝑋)) → (√‘Σ𝑘 ∈ ((𝑥 supp 0) ∪ (𝑦 supp 0))(((𝑥𝑘) − (𝑦𝑘))↑2)) ∈ ℝ)
2423ralrimivva 3142 . . . 4 (𝐼𝑉 → ∀𝑥𝑋𝑦𝑋 (√‘Σ𝑘 ∈ ((𝑥 supp 0) ∪ (𝑦 supp 0))(((𝑥𝑘) − (𝑦𝑘))↑2)) ∈ ℝ)
25 eqid 2779 . . . . 5 (𝑥𝑋, 𝑦𝑋 ↦ (√‘Σ𝑘 ∈ ((𝑥 supp 0) ∪ (𝑦 supp 0))(((𝑥𝑘) − (𝑦𝑘))↑2))) = (𝑥𝑋, 𝑦𝑋 ↦ (√‘Σ𝑘 ∈ ((𝑥 supp 0) ∪ (𝑦 supp 0))(((𝑥𝑘) − (𝑦𝑘))↑2)))
2625fmpo 7574 . . . 4 (∀𝑥𝑋𝑦𝑋 (√‘Σ𝑘 ∈ ((𝑥 supp 0) ∪ (𝑦 supp 0))(((𝑥𝑘) − (𝑦𝑘))↑2)) ∈ ℝ ↔ (𝑥𝑋, 𝑦𝑋 ↦ (√‘Σ𝑘 ∈ ((𝑥 supp 0) ∪ (𝑦 supp 0))(((𝑥𝑘) − (𝑦𝑘))↑2))):(𝑋 × 𝑋)⟶ℝ)
2724, 26sylib 210 . . 3 (𝐼𝑉 → (𝑥𝑋, 𝑦𝑋 ↦ (√‘Σ𝑘 ∈ ((𝑥 supp 0) ∪ (𝑦 supp 0))(((𝑥𝑘) − (𝑦𝑘))↑2))):(𝑋 × 𝑋)⟶ℝ)
28 rrxmval.d . . . . 5 𝐷 = (dist‘(ℝ^‘𝐼))
291, 28rrxmfval 23712 . . . 4 (𝐼𝑉𝐷 = (𝑥𝑋, 𝑦𝑋 ↦ (√‘Σ𝑘 ∈ ((𝑥 supp 0) ∪ (𝑦 supp 0))(((𝑥𝑘) − (𝑦𝑘))↑2))))
3029feq1d 6329 . . 3 (𝐼𝑉 → (𝐷:(𝑋 × 𝑋)⟶ℝ ↔ (𝑥𝑋, 𝑦𝑋 ↦ (√‘Σ𝑘 ∈ ((𝑥 supp 0) ∪ (𝑦 supp 0))(((𝑥𝑘) − (𝑦𝑘))↑2))):(𝑋 × 𝑋)⟶ℝ))
3127, 30mpbird 249 . 2 (𝐼𝑉𝐷:(𝑋 × 𝑋)⟶ℝ)
32 sqrt00 14484 . . . . . . 7 ((Σ𝑘 ∈ ((𝑥 supp 0) ∪ (𝑦 supp 0))(((𝑥𝑘) − (𝑦𝑘))↑2) ∈ ℝ ∧ 0 ≤ Σ𝑘 ∈ ((𝑥 supp 0) ∪ (𝑦 supp 0))(((𝑥𝑘) − (𝑦𝑘))↑2)) → ((√‘Σ𝑘 ∈ ((𝑥 supp 0) ∪ (𝑦 supp 0))(((𝑥𝑘) − (𝑦𝑘))↑2)) = 0 ↔ Σ𝑘 ∈ ((𝑥 supp 0) ∪ (𝑦 supp 0))(((𝑥𝑘) − (𝑦𝑘))↑2) = 0))
3319, 22, 32syl2anc 576 . . . . . 6 ((𝐼𝑉 ∧ (𝑥𝑋𝑦𝑋)) → ((√‘Σ𝑘 ∈ ((𝑥 supp 0) ∪ (𝑦 supp 0))(((𝑥𝑘) − (𝑦𝑘))↑2)) = 0 ↔ Σ𝑘 ∈ ((𝑥 supp 0) ∪ (𝑦 supp 0))(((𝑥𝑘) − (𝑦𝑘))↑2) = 0))
347, 18, 21fsum00 15013 . . . . . 6 ((𝐼𝑉 ∧ (𝑥𝑋𝑦𝑋)) → (Σ𝑘 ∈ ((𝑥 supp 0) ∪ (𝑦 supp 0))(((𝑥𝑘) − (𝑦𝑘))↑2) = 0 ↔ ∀𝑘 ∈ ((𝑥 supp 0) ∪ (𝑦 supp 0))(((𝑥𝑘) − (𝑦𝑘))↑2) = 0))
3516recnd 10468 . . . . . . . . . 10 (((𝐼𝑉 ∧ (𝑥𝑋𝑦𝑋)) ∧ 𝑘𝐼) → ((𝑥𝑘) − (𝑦𝑘)) ∈ ℂ)
36 sqeq0 13301 . . . . . . . . . 10 (((𝑥𝑘) − (𝑦𝑘)) ∈ ℂ → ((((𝑥𝑘) − (𝑦𝑘))↑2) = 0 ↔ ((𝑥𝑘) − (𝑦𝑘)) = 0))
3735, 36syl 17 . . . . . . . . 9 (((𝐼𝑉 ∧ (𝑥𝑋𝑦𝑋)) ∧ 𝑘𝐼) → ((((𝑥𝑘) − (𝑦𝑘))↑2) = 0 ↔ ((𝑥𝑘) − (𝑦𝑘)) = 0))
3813recnd 10468 . . . . . . . . . 10 (((𝐼𝑉 ∧ (𝑥𝑋𝑦𝑋)) ∧ 𝑘𝐼) → (𝑥𝑘) ∈ ℂ)
3915recnd 10468 . . . . . . . . . 10 (((𝐼𝑉 ∧ (𝑥𝑋𝑦𝑋)) ∧ 𝑘𝐼) → (𝑦𝑘) ∈ ℂ)
4038, 39subeq0ad 10808 . . . . . . . . 9 (((𝐼𝑉 ∧ (𝑥𝑋𝑦𝑋)) ∧ 𝑘𝐼) → (((𝑥𝑘) − (𝑦𝑘)) = 0 ↔ (𝑥𝑘) = (𝑦𝑘)))
4137, 40bitrd 271 . . . . . . . 8 (((𝐼𝑉 ∧ (𝑥𝑋𝑦𝑋)) ∧ 𝑘𝐼) → ((((𝑥𝑘) − (𝑦𝑘))↑2) = 0 ↔ (𝑥𝑘) = (𝑦𝑘)))
4211, 41syldan 582 . . . . . . 7 (((𝐼𝑉 ∧ (𝑥𝑋𝑦𝑋)) ∧ 𝑘 ∈ ((𝑥 supp 0) ∪ (𝑦 supp 0))) → ((((𝑥𝑘) − (𝑦𝑘))↑2) = 0 ↔ (𝑥𝑘) = (𝑦𝑘)))
4342ralbidva 3147 . . . . . 6 ((𝐼𝑉 ∧ (𝑥𝑋𝑦𝑋)) → (∀𝑘 ∈ ((𝑥 supp 0) ∪ (𝑦 supp 0))(((𝑥𝑘) − (𝑦𝑘))↑2) = 0 ↔ ∀𝑘 ∈ ((𝑥 supp 0) ∪ (𝑦 supp 0))(𝑥𝑘) = (𝑦𝑘)))
4433, 34, 433bitrd 297 . . . . 5 ((𝐼𝑉 ∧ (𝑥𝑋𝑦𝑋)) → ((√‘Σ𝑘 ∈ ((𝑥 supp 0) ∪ (𝑦 supp 0))(((𝑥𝑘) − (𝑦𝑘))↑2)) = 0 ↔ ∀𝑘 ∈ ((𝑥 supp 0) ∪ (𝑦 supp 0))(𝑥𝑘) = (𝑦𝑘)))
451, 28rrxmval 23711 . . . . . . 7 ((𝐼𝑉𝑥𝑋𝑦𝑋) → (𝑥𝐷𝑦) = (√‘Σ𝑘 ∈ ((𝑥 supp 0) ∪ (𝑦 supp 0))(((𝑥𝑘) − (𝑦𝑘))↑2)))
46453expb 1100 . . . . . 6 ((𝐼𝑉 ∧ (𝑥𝑋𝑦𝑋)) → (𝑥𝐷𝑦) = (√‘Σ𝑘 ∈ ((𝑥 supp 0) ∪ (𝑦 supp 0))(((𝑥𝑘) − (𝑦𝑘))↑2)))
4746eqeq1d 2781 . . . . 5 ((𝐼𝑉 ∧ (𝑥𝑋𝑦𝑋)) → ((𝑥𝐷𝑦) = 0 ↔ (√‘Σ𝑘 ∈ ((𝑥 supp 0) ∪ (𝑦 supp 0))(((𝑥𝑘) − (𝑦𝑘))↑2)) = 0))
4812ffnd 6345 . . . . . . 7 ((𝐼𝑉 ∧ (𝑥𝑋𝑦𝑋)) → 𝑥 Fn 𝐼)
4914ffnd 6345 . . . . . . 7 ((𝐼𝑉 ∧ (𝑥𝑋𝑦𝑋)) → 𝑦 Fn 𝐼)
50 eqfnfv 6627 . . . . . . 7 ((𝑥 Fn 𝐼𝑦 Fn 𝐼) → (𝑥 = 𝑦 ↔ ∀𝑘𝐼 (𝑥𝑘) = (𝑦𝑘)))
5148, 49, 50syl2anc 576 . . . . . 6 ((𝐼𝑉 ∧ (𝑥𝑋𝑦𝑋)) → (𝑥 = 𝑦 ↔ ∀𝑘𝐼 (𝑥𝑘) = (𝑦𝑘)))
52 ssun1 4038 . . . . . . . . . . 11 (𝑥 supp 0) ⊆ ((𝑥 supp 0) ∪ (𝑦 supp 0))
5352a1i 11 . . . . . . . . . 10 ((𝐼𝑉 ∧ (𝑥𝑋𝑦𝑋)) → (𝑥 supp 0) ⊆ ((𝑥 supp 0) ∪ (𝑦 supp 0)))
54 simpl 475 . . . . . . . . . 10 ((𝐼𝑉 ∧ (𝑥𝑋𝑦𝑋)) → 𝐼𝑉)
55 0red 10443 . . . . . . . . . 10 ((𝐼𝑉 ∧ (𝑥𝑋𝑦𝑋)) → 0 ∈ ℝ)
5612, 53, 54, 55suppssr 7664 . . . . . . . . 9 (((𝐼𝑉 ∧ (𝑥𝑋𝑦𝑋)) ∧ 𝑘 ∈ (𝐼 ∖ ((𝑥 supp 0) ∪ (𝑦 supp 0)))) → (𝑥𝑘) = 0)
57 ssun2 4039 . . . . . . . . . . 11 (𝑦 supp 0) ⊆ ((𝑥 supp 0) ∪ (𝑦 supp 0))
5857a1i 11 . . . . . . . . . 10 ((𝐼𝑉 ∧ (𝑥𝑋𝑦𝑋)) → (𝑦 supp 0) ⊆ ((𝑥 supp 0) ∪ (𝑦 supp 0)))
5914, 58, 54, 55suppssr 7664 . . . . . . . . 9 (((𝐼𝑉 ∧ (𝑥𝑋𝑦𝑋)) ∧ 𝑘 ∈ (𝐼 ∖ ((𝑥 supp 0) ∪ (𝑦 supp 0)))) → (𝑦𝑘) = 0)
6056, 59eqtr4d 2818 . . . . . . . 8 (((𝐼𝑉 ∧ (𝑥𝑋𝑦𝑋)) ∧ 𝑘 ∈ (𝐼 ∖ ((𝑥 supp 0) ∪ (𝑦 supp 0)))) → (𝑥𝑘) = (𝑦𝑘))
6160ralrimiva 3133 . . . . . . 7 ((𝐼𝑉 ∧ (𝑥𝑋𝑦𝑋)) → ∀𝑘 ∈ (𝐼 ∖ ((𝑥 supp 0) ∪ (𝑦 supp 0)))(𝑥𝑘) = (𝑦𝑘))
6210, 61raldifeq 4322 . . . . . 6 ((𝐼𝑉 ∧ (𝑥𝑋𝑦𝑋)) → (∀𝑘 ∈ ((𝑥 supp 0) ∪ (𝑦 supp 0))(𝑥𝑘) = (𝑦𝑘) ↔ ∀𝑘𝐼 (𝑥𝑘) = (𝑦𝑘)))
6351, 62bitr4d 274 . . . . 5 ((𝐼𝑉 ∧ (𝑥𝑋𝑦𝑋)) → (𝑥 = 𝑦 ↔ ∀𝑘 ∈ ((𝑥 supp 0) ∪ (𝑦 supp 0))(𝑥𝑘) = (𝑦𝑘)))
6444, 47, 633bitr4d 303 . . . 4 ((𝐼𝑉 ∧ (𝑥𝑋𝑦𝑋)) → ((𝑥𝐷𝑦) = 0 ↔ 𝑥 = 𝑦))
6573adant2 1111 . . . . . . . . . . 11 ((𝐼𝑉𝑧𝑋 ∧ (𝑥𝑋𝑦𝑋)) → ((𝑥 supp 0) ∪ (𝑦 supp 0)) ∈ Fin)
66 simp2 1117 . . . . . . . . . . . 12 ((𝐼𝑉𝑧𝑋 ∧ (𝑥𝑋𝑦𝑋)) → 𝑧𝑋)
671, 66rrxfsupp 23708 . . . . . . . . . . 11 ((𝐼𝑉𝑧𝑋 ∧ (𝑥𝑋𝑦𝑋)) → (𝑧 supp 0) ∈ Fin)
68 unfi 8580 . . . . . . . . . . 11 ((((𝑥 supp 0) ∪ (𝑦 supp 0)) ∈ Fin ∧ (𝑧 supp 0) ∈ Fin) → (((𝑥 supp 0) ∪ (𝑦 supp 0)) ∪ (𝑧 supp 0)) ∈ Fin)
6965, 67, 68syl2anc 576 . . . . . . . . . 10 ((𝐼𝑉𝑧𝑋 ∧ (𝑥𝑋𝑦𝑋)) → (((𝑥 supp 0) ∪ (𝑦 supp 0)) ∪ (𝑧 supp 0)) ∈ Fin)
70693expa 1098 . . . . . . . . 9 (((𝐼𝑉𝑧𝑋) ∧ (𝑥𝑋𝑦𝑋)) → (((𝑥 supp 0) ∪ (𝑦 supp 0)) ∪ (𝑧 supp 0)) ∈ Fin)
7170an32s 639 . . . . . . . 8 (((𝐼𝑉 ∧ (𝑥𝑋𝑦𝑋)) ∧ 𝑧𝑋) → (((𝑥 supp 0) ∪ (𝑦 supp 0)) ∪ (𝑧 supp 0)) ∈ Fin)
7210adantr 473 . . . . . . . . . . 11 (((𝐼𝑉 ∧ (𝑥𝑋𝑦𝑋)) ∧ 𝑧𝑋) → ((𝑥 supp 0) ∪ (𝑦 supp 0)) ⊆ 𝐼)
73 simpr 477 . . . . . . . . . . . 12 (((𝐼𝑉 ∧ (𝑥𝑋𝑦𝑋)) ∧ 𝑧𝑋) → 𝑧𝑋)
741, 73rrxsuppss 23709 . . . . . . . . . . 11 (((𝐼𝑉 ∧ (𝑥𝑋𝑦𝑋)) ∧ 𝑧𝑋) → (𝑧 supp 0) ⊆ 𝐼)
7572, 74unssd 4051 . . . . . . . . . 10 (((𝐼𝑉 ∧ (𝑥𝑋𝑦𝑋)) ∧ 𝑧𝑋) → (((𝑥 supp 0) ∪ (𝑦 supp 0)) ∪ (𝑧 supp 0)) ⊆ 𝐼)
7675sselda 3859 . . . . . . . . 9 ((((𝐼𝑉 ∧ (𝑥𝑋𝑦𝑋)) ∧ 𝑧𝑋) ∧ 𝑘 ∈ (((𝑥 supp 0) ∪ (𝑦 supp 0)) ∪ (𝑧 supp 0))) → 𝑘𝐼)
7713adantlr 702 . . . . . . . . . 10 ((((𝐼𝑉 ∧ (𝑥𝑋𝑦𝑋)) ∧ 𝑧𝑋) ∧ 𝑘𝐼) → (𝑥𝑘) ∈ ℝ)
781, 73rrxf 23707 . . . . . . . . . . 11 (((𝐼𝑉 ∧ (𝑥𝑋𝑦𝑋)) ∧ 𝑧𝑋) → 𝑧:𝐼⟶ℝ)
7978ffvelrnda 6676 . . . . . . . . . 10 ((((𝐼𝑉 ∧ (𝑥𝑋𝑦𝑋)) ∧ 𝑧𝑋) ∧ 𝑘𝐼) → (𝑧𝑘) ∈ ℝ)
8077, 79resubcld 10869 . . . . . . . . 9 ((((𝐼𝑉 ∧ (𝑥𝑋𝑦𝑋)) ∧ 𝑧𝑋) ∧ 𝑘𝐼) → ((𝑥𝑘) − (𝑧𝑘)) ∈ ℝ)
8176, 80syldan 582 . . . . . . . 8 ((((𝐼𝑉 ∧ (𝑥𝑋𝑦𝑋)) ∧ 𝑧𝑋) ∧ 𝑘 ∈ (((𝑥 supp 0) ∪ (𝑦 supp 0)) ∪ (𝑧 supp 0))) → ((𝑥𝑘) − (𝑧𝑘)) ∈ ℝ)
8215adantlr 702 . . . . . . . . . 10 ((((𝐼𝑉 ∧ (𝑥𝑋𝑦𝑋)) ∧ 𝑧𝑋) ∧ 𝑘𝐼) → (𝑦𝑘) ∈ ℝ)
8379, 82resubcld 10869 . . . . . . . . 9 ((((𝐼𝑉 ∧ (𝑥𝑋𝑦𝑋)) ∧ 𝑧𝑋) ∧ 𝑘𝐼) → ((𝑧𝑘) − (𝑦𝑘)) ∈ ℝ)
8476, 83syldan 582 . . . . . . . 8 ((((𝐼𝑉 ∧ (𝑥𝑋𝑦𝑋)) ∧ 𝑧𝑋) ∧ 𝑘 ∈ (((𝑥 supp 0) ∪ (𝑦 supp 0)) ∪ (𝑧 supp 0))) → ((𝑧𝑘) − (𝑦𝑘)) ∈ ℝ)
8571, 81, 84trirn 23706 . . . . . . 7 (((𝐼𝑉 ∧ (𝑥𝑋𝑦𝑋)) ∧ 𝑧𝑋) → (√‘Σ𝑘 ∈ (((𝑥 supp 0) ∪ (𝑦 supp 0)) ∪ (𝑧 supp 0))((((𝑥𝑘) − (𝑧𝑘)) + ((𝑧𝑘) − (𝑦𝑘)))↑2)) ≤ ((√‘Σ𝑘 ∈ (((𝑥 supp 0) ∪ (𝑦 supp 0)) ∪ (𝑧 supp 0))(((𝑥𝑘) − (𝑧𝑘))↑2)) + (√‘Σ𝑘 ∈ (((𝑥 supp 0) ∪ (𝑦 supp 0)) ∪ (𝑧 supp 0))(((𝑧𝑘) − (𝑦𝑘))↑2))))
8638adantlr 702 . . . . . . . . . . . 12 ((((𝐼𝑉 ∧ (𝑥𝑋𝑦𝑋)) ∧ 𝑧𝑋) ∧ 𝑘𝐼) → (𝑥𝑘) ∈ ℂ)
8779recnd 10468 . . . . . . . . . . . 12 ((((𝐼𝑉 ∧ (𝑥𝑋𝑦𝑋)) ∧ 𝑧𝑋) ∧ 𝑘𝐼) → (𝑧𝑘) ∈ ℂ)
8839adantlr 702 . . . . . . . . . . . 12 ((((𝐼𝑉 ∧ (𝑥𝑋𝑦𝑋)) ∧ 𝑧𝑋) ∧ 𝑘𝐼) → (𝑦𝑘) ∈ ℂ)
8986, 87, 88npncand 10822 . . . . . . . . . . 11 ((((𝐼𝑉 ∧ (𝑥𝑋𝑦𝑋)) ∧ 𝑧𝑋) ∧ 𝑘𝐼) → (((𝑥𝑘) − (𝑧𝑘)) + ((𝑧𝑘) − (𝑦𝑘))) = ((𝑥𝑘) − (𝑦𝑘)))
9089oveq1d 6991 . . . . . . . . . 10 ((((𝐼𝑉 ∧ (𝑥𝑋𝑦𝑋)) ∧ 𝑧𝑋) ∧ 𝑘𝐼) → ((((𝑥𝑘) − (𝑧𝑘)) + ((𝑧𝑘) − (𝑦𝑘)))↑2) = (((𝑥𝑘) − (𝑦𝑘))↑2))
9176, 90syldan 582 . . . . . . . . 9 ((((𝐼𝑉 ∧ (𝑥𝑋𝑦𝑋)) ∧ 𝑧𝑋) ∧ 𝑘 ∈ (((𝑥 supp 0) ∪ (𝑦 supp 0)) ∪ (𝑧 supp 0))) → ((((𝑥𝑘) − (𝑧𝑘)) + ((𝑧𝑘) − (𝑦𝑘)))↑2) = (((𝑥𝑘) − (𝑦𝑘))↑2))
9291sumeq2dv 14920 . . . . . . . 8 (((𝐼𝑉 ∧ (𝑥𝑋𝑦𝑋)) ∧ 𝑧𝑋) → Σ𝑘 ∈ (((𝑥 supp 0) ∪ (𝑦 supp 0)) ∪ (𝑧 supp 0))((((𝑥𝑘) − (𝑧𝑘)) + ((𝑧𝑘) − (𝑦𝑘)))↑2) = Σ𝑘 ∈ (((𝑥 supp 0) ∪ (𝑦 supp 0)) ∪ (𝑧 supp 0))(((𝑥𝑘) − (𝑦𝑘))↑2))
9392fveq2d 6503 . . . . . . 7 (((𝐼𝑉 ∧ (𝑥𝑋𝑦𝑋)) ∧ 𝑧𝑋) → (√‘Σ𝑘 ∈ (((𝑥 supp 0) ∪ (𝑦 supp 0)) ∪ (𝑧 supp 0))((((𝑥𝑘) − (𝑧𝑘)) + ((𝑧𝑘) − (𝑦𝑘)))↑2)) = (√‘Σ𝑘 ∈ (((𝑥 supp 0) ∪ (𝑦 supp 0)) ∪ (𝑧 supp 0))(((𝑥𝑘) − (𝑦𝑘))↑2)))
94 sqsubswap 13298 . . . . . . . . . . . 12 (((𝑥𝑘) ∈ ℂ ∧ (𝑧𝑘) ∈ ℂ) → (((𝑥𝑘) − (𝑧𝑘))↑2) = (((𝑧𝑘) − (𝑥𝑘))↑2))
9586, 87, 94syl2anc 576 . . . . . . . . . . 11 ((((𝐼𝑉 ∧ (𝑥𝑋𝑦𝑋)) ∧ 𝑧𝑋) ∧ 𝑘𝐼) → (((𝑥𝑘) − (𝑧𝑘))↑2) = (((𝑧𝑘) − (𝑥𝑘))↑2))
9676, 95syldan 582 . . . . . . . . . 10 ((((𝐼𝑉 ∧ (𝑥𝑋𝑦𝑋)) ∧ 𝑧𝑋) ∧ 𝑘 ∈ (((𝑥 supp 0) ∪ (𝑦 supp 0)) ∪ (𝑧 supp 0))) → (((𝑥𝑘) − (𝑧𝑘))↑2) = (((𝑧𝑘) − (𝑥𝑘))↑2))
9796sumeq2dv 14920 . . . . . . . . 9 (((𝐼𝑉 ∧ (𝑥𝑋𝑦𝑋)) ∧ 𝑧𝑋) → Σ𝑘 ∈ (((𝑥 supp 0) ∪ (𝑦 supp 0)) ∪ (𝑧 supp 0))(((𝑥𝑘) − (𝑧𝑘))↑2) = Σ𝑘 ∈ (((𝑥 supp 0) ∪ (𝑦 supp 0)) ∪ (𝑧 supp 0))(((𝑧𝑘) − (𝑥𝑘))↑2))
9897fveq2d 6503 . . . . . . . 8 (((𝐼𝑉 ∧ (𝑥𝑋𝑦𝑋)) ∧ 𝑧𝑋) → (√‘Σ𝑘 ∈ (((𝑥 supp 0) ∪ (𝑦 supp 0)) ∪ (𝑧 supp 0))(((𝑥𝑘) − (𝑧𝑘))↑2)) = (√‘Σ𝑘 ∈ (((𝑥 supp 0) ∪ (𝑦 supp 0)) ∪ (𝑧 supp 0))(((𝑧𝑘) − (𝑥𝑘))↑2)))
9998oveq1d 6991 . . . . . . 7 (((𝐼𝑉 ∧ (𝑥𝑋𝑦𝑋)) ∧ 𝑧𝑋) → ((√‘Σ𝑘 ∈ (((𝑥 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))))
10085, 93, 993brtr3d 4960 . . . . . 6 (((𝐼𝑉 ∧ (𝑥𝑋𝑦𝑋)) ∧ 𝑧𝑋) → (√‘Σ𝑘 ∈ (((𝑥 supp 0) ∪ (𝑦 supp 0)) ∪ (𝑧 supp 0))(((𝑥𝑘) − (𝑦𝑘))↑2)) ≤ ((√‘Σ𝑘 ∈ (((𝑥 supp 0) ∪ (𝑦 supp 0)) ∪ (𝑧 supp 0))(((𝑧𝑘) − (𝑥𝑘))↑2)) + (√‘Σ𝑘 ∈ (((𝑥 supp 0) ∪ (𝑦 supp 0)) ∪ (𝑧 supp 0))(((𝑧𝑘) − (𝑦𝑘))↑2))))
10146adantr 473 . . . . . . 7 (((𝐼𝑉 ∧ (𝑥𝑋𝑦𝑋)) ∧ 𝑧𝑋) → (𝑥𝐷𝑦) = (√‘Σ𝑘 ∈ ((𝑥 supp 0) ∪ (𝑦 supp 0))(((𝑥𝑘) − (𝑦𝑘))↑2)))
102 simp1 1116 . . . . . . . . . . 11 ((𝐼𝑉𝑧𝑋 ∧ (𝑥𝑋𝑦𝑋)) → 𝐼𝑉)
10323adant2 1111 . . . . . . . . . . 11 ((𝐼𝑉𝑧𝑋 ∧ (𝑥𝑋𝑦𝑋)) → 𝑥𝑋)
10443adant2 1111 . . . . . . . . . . 11 ((𝐼𝑉𝑧𝑋 ∧ (𝑥𝑋𝑦𝑋)) → 𝑦𝑋)
1051, 103rrxsuppss 23709 . . . . . . . . . . . . 13 ((𝐼𝑉𝑧𝑋 ∧ (𝑥𝑋𝑦𝑋)) → (𝑥 supp 0) ⊆ 𝐼)
1061, 104rrxsuppss 23709 . . . . . . . . . . . . 13 ((𝐼𝑉𝑧𝑋 ∧ (𝑥𝑋𝑦𝑋)) → (𝑦 supp 0) ⊆ 𝐼)
107105, 106unssd 4051 . . . . . . . . . . . 12 ((𝐼𝑉𝑧𝑋 ∧ (𝑥𝑋𝑦𝑋)) → ((𝑥 supp 0) ∪ (𝑦 supp 0)) ⊆ 𝐼)
1081, 66rrxsuppss 23709 . . . . . . . . . . . 12 ((𝐼𝑉𝑧𝑋 ∧ (𝑥𝑋𝑦𝑋)) → (𝑧 supp 0) ⊆ 𝐼)
109107, 108unssd 4051 . . . . . . . . . . 11 ((𝐼𝑉𝑧𝑋 ∧ (𝑥𝑋𝑦𝑋)) → (((𝑥 supp 0) ∪ (𝑦 supp 0)) ∪ (𝑧 supp 0)) ⊆ 𝐼)
110 ssun1 4038 . . . . . . . . . . . 12 ((𝑥 supp 0) ∪ (𝑦 supp 0)) ⊆ (((𝑥 supp 0) ∪ (𝑦 supp 0)) ∪ (𝑧 supp 0))
111110a1i 11 . . . . . . . . . . 11 ((𝐼𝑉𝑧𝑋 ∧ (𝑥𝑋𝑦𝑋)) → ((𝑥 supp 0) ∪ (𝑦 supp 0)) ⊆ (((𝑥 supp 0) ∪ (𝑦 supp 0)) ∪ (𝑧 supp 0)))
1121, 28, 102, 103, 104, 109, 69, 111rrxmetlem 23713 . . . . . . . . . 10 ((𝐼𝑉𝑧𝑋 ∧ (𝑥𝑋𝑦𝑋)) → Σ𝑘 ∈ ((𝑥 supp 0) ∪ (𝑦 supp 0))(((𝑥𝑘) − (𝑦𝑘))↑2) = Σ𝑘 ∈ (((𝑥 supp 0) ∪ (𝑦 supp 0)) ∪ (𝑧 supp 0))(((𝑥𝑘) − (𝑦𝑘))↑2))
113112fveq2d 6503 . . . . . . . . 9 ((𝐼𝑉𝑧𝑋 ∧ (𝑥𝑋𝑦𝑋)) → (√‘Σ𝑘 ∈ ((𝑥 supp 0) ∪ (𝑦 supp 0))(((𝑥𝑘) − (𝑦𝑘))↑2)) = (√‘Σ𝑘 ∈ (((𝑥 supp 0) ∪ (𝑦 supp 0)) ∪ (𝑧 supp 0))(((𝑥𝑘) − (𝑦𝑘))↑2)))
1141133expa 1098 . . . . . . . 8 (((𝐼𝑉𝑧𝑋) ∧ (𝑥𝑋𝑦𝑋)) → (√‘Σ𝑘 ∈ ((𝑥 supp 0) ∪ (𝑦 supp 0))(((𝑥𝑘) − (𝑦𝑘))↑2)) = (√‘Σ𝑘 ∈ (((𝑥 supp 0) ∪ (𝑦 supp 0)) ∪ (𝑧 supp 0))(((𝑥𝑘) − (𝑦𝑘))↑2)))
115114an32s 639 . . . . . . 7 (((𝐼𝑉 ∧ (𝑥𝑋𝑦𝑋)) ∧ 𝑧𝑋) → (√‘Σ𝑘 ∈ ((𝑥 supp 0) ∪ (𝑦 supp 0))(((𝑥𝑘) − (𝑦𝑘))↑2)) = (√‘Σ𝑘 ∈ (((𝑥 supp 0) ∪ (𝑦 supp 0)) ∪ (𝑧 supp 0))(((𝑥𝑘) − (𝑦𝑘))↑2)))
116101, 115eqtrd 2815 . . . . . 6 (((𝐼𝑉 ∧ (𝑥𝑋𝑦𝑋)) ∧ 𝑧𝑋) → (𝑥𝐷𝑦) = (√‘Σ𝑘 ∈ (((𝑥 supp 0) ∪ (𝑦 supp 0)) ∪ (𝑧 supp 0))(((𝑥𝑘) − (𝑦𝑘))↑2)))
1171, 28rrxmval 23711 . . . . . . . . . . 11 ((𝐼𝑉𝑧𝑋𝑥𝑋) → (𝑧𝐷𝑥) = (√‘Σ𝑘 ∈ ((𝑧 supp 0) ∪ (𝑥 supp 0))(((𝑧𝑘) − (𝑥𝑘))↑2)))
1181173adant3r 1161 . . . . . . . . . 10 ((𝐼𝑉𝑧𝑋 ∧ (𝑥𝑋𝑦𝑋)) → (𝑧𝐷𝑥) = (√‘Σ𝑘 ∈ ((𝑧 supp 0) ∪ (𝑥 supp 0))(((𝑧𝑘) − (𝑥𝑘))↑2)))
1191, 28rrxmval 23711 . . . . . . . . . . 11 ((𝐼𝑉𝑧𝑋𝑦𝑋) → (𝑧𝐷𝑦) = (√‘Σ𝑘 ∈ ((𝑧 supp 0) ∪ (𝑦 supp 0))(((𝑧𝑘) − (𝑦𝑘))↑2)))
1201193adant3l 1160 . . . . . . . . . 10 ((𝐼𝑉𝑧𝑋 ∧ (𝑥𝑋𝑦𝑋)) → (𝑧𝐷𝑦) = (√‘Σ𝑘 ∈ ((𝑧 supp 0) ∪ (𝑦 supp 0))(((𝑧𝑘) − (𝑦𝑘))↑2)))
121118, 120oveq12d 6994 . . . . . . . . 9 ((𝐼𝑉𝑧𝑋 ∧ (𝑥𝑋𝑦𝑋)) → ((𝑧𝐷𝑥) + (𝑧𝐷𝑦)) = ((√‘Σ𝑘 ∈ ((𝑧 supp 0) ∪ (𝑥 supp 0))(((𝑧𝑘) − (𝑥𝑘))↑2)) + (√‘Σ𝑘 ∈ ((𝑧 supp 0) ∪ (𝑦 supp 0))(((𝑧𝑘) − (𝑦𝑘))↑2))))
122 ssun2 4039 . . . . . . . . . . . . . 14 (𝑧 supp 0) ⊆ (((𝑥 supp 0) ∪ (𝑦 supp 0)) ∪ (𝑧 supp 0))
123122a1i 11 . . . . . . . . . . . . 13 ((𝐼𝑉𝑧𝑋 ∧ (𝑥𝑋𝑦𝑋)) → (𝑧 supp 0) ⊆ (((𝑥 supp 0) ∪ (𝑦 supp 0)) ∪ (𝑧 supp 0)))
12452, 110sstri 3868 . . . . . . . . . . . . . 14 (𝑥 supp 0) ⊆ (((𝑥 supp 0) ∪ (𝑦 supp 0)) ∪ (𝑧 supp 0))
125124a1i 11 . . . . . . . . . . . . 13 ((𝐼𝑉𝑧𝑋 ∧ (𝑥𝑋𝑦𝑋)) → (𝑥 supp 0) ⊆ (((𝑥 supp 0) ∪ (𝑦 supp 0)) ∪ (𝑧 supp 0)))
126123, 125unssd 4051 . . . . . . . . . . . 12 ((𝐼𝑉𝑧𝑋 ∧ (𝑥𝑋𝑦𝑋)) → ((𝑧 supp 0) ∪ (𝑥 supp 0)) ⊆ (((𝑥 supp 0) ∪ (𝑦 supp 0)) ∪ (𝑧 supp 0)))
1271, 28, 102, 66, 103, 109, 69, 126rrxmetlem 23713 . . . . . . . . . . 11 ((𝐼𝑉𝑧𝑋 ∧ (𝑥𝑋𝑦𝑋)) → Σ𝑘 ∈ ((𝑧 supp 0) ∪ (𝑥 supp 0))(((𝑧𝑘) − (𝑥𝑘))↑2) = Σ𝑘 ∈ (((𝑥 supp 0) ∪ (𝑦 supp 0)) ∪ (𝑧 supp 0))(((𝑧𝑘) − (𝑥𝑘))↑2))
128127fveq2d 6503 . . . . . . . . . 10 ((𝐼𝑉𝑧𝑋 ∧ (𝑥𝑋𝑦𝑋)) → (√‘Σ𝑘 ∈ ((𝑧 supp 0) ∪ (𝑥 supp 0))(((𝑧𝑘) − (𝑥𝑘))↑2)) = (√‘Σ𝑘 ∈ (((𝑥 supp 0) ∪ (𝑦 supp 0)) ∪ (𝑧 supp 0))(((𝑧𝑘) − (𝑥𝑘))↑2)))
12957, 110sstri 3868 . . . . . . . . . . . . . 14 (𝑦 supp 0) ⊆ (((𝑥 supp 0) ∪ (𝑦 supp 0)) ∪ (𝑧 supp 0))
130129a1i 11 . . . . . . . . . . . . 13 ((𝐼𝑉𝑧𝑋 ∧ (𝑥𝑋𝑦𝑋)) → (𝑦 supp 0) ⊆ (((𝑥 supp 0) ∪ (𝑦 supp 0)) ∪ (𝑧 supp 0)))
131123, 130unssd 4051 . . . . . . . . . . . 12 ((𝐼𝑉𝑧𝑋 ∧ (𝑥𝑋𝑦𝑋)) → ((𝑧 supp 0) ∪ (𝑦 supp 0)) ⊆ (((𝑥 supp 0) ∪ (𝑦 supp 0)) ∪ (𝑧 supp 0)))
1321, 28, 102, 66, 104, 109, 69, 131rrxmetlem 23713 . . . . . . . . . . 11 ((𝐼𝑉𝑧𝑋 ∧ (𝑥𝑋𝑦𝑋)) → Σ𝑘 ∈ ((𝑧 supp 0) ∪ (𝑦 supp 0))(((𝑧𝑘) − (𝑦𝑘))↑2) = Σ𝑘 ∈ (((𝑥 supp 0) ∪ (𝑦 supp 0)) ∪ (𝑧 supp 0))(((𝑧𝑘) − (𝑦𝑘))↑2))
133132fveq2d 6503 . . . . . . . . . 10 ((𝐼𝑉𝑧𝑋 ∧ (𝑥𝑋𝑦𝑋)) → (√‘Σ𝑘 ∈ ((𝑧 supp 0) ∪ (𝑦 supp 0))(((𝑧𝑘) − (𝑦𝑘))↑2)) = (√‘Σ𝑘 ∈ (((𝑥 supp 0) ∪ (𝑦 supp 0)) ∪ (𝑧 supp 0))(((𝑧𝑘) − (𝑦𝑘))↑2)))
134128, 133oveq12d 6994 . . . . . . . . 9 ((𝐼𝑉𝑧𝑋 ∧ (𝑥𝑋𝑦𝑋)) → ((√‘Σ𝑘 ∈ ((𝑧 supp 0) ∪ (𝑥 supp 0))(((𝑧𝑘) − (𝑥𝑘))↑2)) + (√‘Σ𝑘 ∈ ((𝑧 supp 0) ∪ (𝑦 supp 0))(((𝑧𝑘) − (𝑦𝑘))↑2))) = ((√‘Σ𝑘 ∈ (((𝑥 supp 0) ∪ (𝑦 supp 0)) ∪ (𝑧 supp 0))(((𝑧𝑘) − (𝑥𝑘))↑2)) + (√‘Σ𝑘 ∈ (((𝑥 supp 0) ∪ (𝑦 supp 0)) ∪ (𝑧 supp 0))(((𝑧𝑘) − (𝑦𝑘))↑2))))
135121, 134eqtrd 2815 . . . . . . . 8 ((𝐼𝑉𝑧𝑋 ∧ (𝑥𝑋𝑦𝑋)) → ((𝑧𝐷𝑥) + (𝑧𝐷𝑦)) = ((√‘Σ𝑘 ∈ (((𝑥 supp 0) ∪ (𝑦 supp 0)) ∪ (𝑧 supp 0))(((𝑧𝑘) − (𝑥𝑘))↑2)) + (√‘Σ𝑘 ∈ (((𝑥 supp 0) ∪ (𝑦 supp 0)) ∪ (𝑧 supp 0))(((𝑧𝑘) − (𝑦𝑘))↑2))))
1361353expa 1098 . . . . . . 7 (((𝐼𝑉𝑧𝑋) ∧ (𝑥𝑋𝑦𝑋)) → ((𝑧𝐷𝑥) + (𝑧𝐷𝑦)) = ((√‘Σ𝑘 ∈ (((𝑥 supp 0) ∪ (𝑦 supp 0)) ∪ (𝑧 supp 0))(((𝑧𝑘) − (𝑥𝑘))↑2)) + (√‘Σ𝑘 ∈ (((𝑥 supp 0) ∪ (𝑦 supp 0)) ∪ (𝑧 supp 0))(((𝑧𝑘) − (𝑦𝑘))↑2))))
137136an32s 639 . . . . . 6 (((𝐼𝑉 ∧ (𝑥𝑋𝑦𝑋)) ∧ 𝑧𝑋) → ((𝑧𝐷𝑥) + (𝑧𝐷𝑦)) = ((√‘Σ𝑘 ∈ (((𝑥 supp 0) ∪ (𝑦 supp 0)) ∪ (𝑧 supp 0))(((𝑧𝑘) − (𝑥𝑘))↑2)) + (√‘Σ𝑘 ∈ (((𝑥 supp 0) ∪ (𝑦 supp 0)) ∪ (𝑧 supp 0))(((𝑧𝑘) − (𝑦𝑘))↑2))))
138100, 116, 1373brtr4d 4961 . . . . 5 (((𝐼𝑉 ∧ (𝑥𝑋𝑦𝑋)) ∧ 𝑧𝑋) → (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) + (𝑧𝐷𝑦)))
139138ralrimiva 3133 . . . 4 ((𝐼𝑉 ∧ (𝑥𝑋𝑦𝑋)) → ∀𝑧𝑋 (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) + (𝑧𝐷𝑦)))
14064, 139jca 504 . . 3 ((𝐼𝑉 ∧ (𝑥𝑋𝑦𝑋)) → (((𝑥𝐷𝑦) = 0 ↔ 𝑥 = 𝑦) ∧ ∀𝑧𝑋 (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) + (𝑧𝐷𝑦))))
141140ralrimivva 3142 . 2 (𝐼𝑉 → ∀𝑥𝑋𝑦𝑋 (((𝑥𝐷𝑦) = 0 ↔ 𝑥 = 𝑦) ∧ ∀𝑧𝑋 (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) + (𝑧𝐷𝑦))))
142 ovex 7008 . . . 4 (ℝ ↑𝑚 𝐼) ∈ V
1431, 142rabex2 5093 . . 3 𝑋 ∈ V
144 ismet 22636 . . 3 (𝑋 ∈ V → (𝐷 ∈ (Met‘𝑋) ↔ (𝐷:(𝑋 × 𝑋)⟶ℝ ∧ ∀𝑥𝑋𝑦𝑋 (((𝑥𝐷𝑦) = 0 ↔ 𝑥 = 𝑦) ∧ ∀𝑧𝑋 (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) + (𝑧𝐷𝑦))))))
145143, 144ax-mp 5 . 2 (𝐷 ∈ (Met‘𝑋) ↔ (𝐷:(𝑋 × 𝑋)⟶ℝ ∧ ∀𝑥𝑋𝑦𝑋 (((𝑥𝐷𝑦) = 0 ↔ 𝑥 = 𝑦) ∧ ∀𝑧𝑋 (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) + (𝑧𝐷𝑦)))))
14631, 141, 145sylanbrc 575 1 (𝐼𝑉𝐷 ∈ (Met‘𝑋))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198  wa 387  w3a 1068   = wceq 1507  wcel 2050  wral 3089  {crab 3093  Vcvv 3416  cdif 3827  cun 3828  wss 3830   class class class wbr 4929   × cxp 5405   Fn wfn 6183  wf 6184  cfv 6188  (class class class)co 6976  cmpo 6978   supp csupp 7633  𝑚 cmap 8206  Fincfn 8306   finSupp cfsupp 8628  cc 10333  cr 10334  0cc0 10335   + caddc 10338  cle 10475  cmin 10670  2c2 11495  cexp 13244  csqrt 14453  Σcsu 14903  distcds 16430  Metcmet 20233  ℝ^crrx 23689
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-13 2301  ax-ext 2751  ax-rep 5049  ax-sep 5060  ax-nul 5067  ax-pow 5119  ax-pr 5186  ax-un 7279  ax-inf2 8898  ax-cnex 10391  ax-resscn 10392  ax-1cn 10393  ax-icn 10394  ax-addcl 10395  ax-addrcl 10396  ax-mulcl 10397  ax-mulrcl 10398  ax-mulcom 10399  ax-addass 10400  ax-mulass 10401  ax-distr 10402  ax-i2m1 10403  ax-1ne0 10404  ax-1rid 10405  ax-rnegex 10406  ax-rrecex 10407  ax-cnre 10408  ax-pre-lttri 10409  ax-pre-lttrn 10410  ax-pre-ltadd 10411  ax-pre-mulgt0 10412  ax-pre-sup 10413  ax-addf 10414  ax-mulf 10415
This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3or 1069  df-3an 1070  df-tru 1510  df-fal 1520  df-ex 1743  df-nf 1747  df-sb 2016  df-mo 2547  df-eu 2584  df-clab 2760  df-cleq 2772  df-clel 2847  df-nfc 2919  df-ne 2969  df-nel 3075  df-ral 3094  df-rex 3095  df-reu 3096  df-rmo 3097  df-rab 3098  df-v 3418  df-sbc 3683  df-csb 3788  df-dif 3833  df-un 3835  df-in 3837  df-ss 3844  df-pss 3846  df-nul 4180  df-if 4351  df-pw 4424  df-sn 4442  df-pr 4444  df-tp 4446  df-op 4448  df-uni 4713  df-int 4750  df-iun 4794  df-br 4930  df-opab 4992  df-mpt 5009  df-tr 5031  df-id 5312  df-eprel 5317  df-po 5326  df-so 5327  df-fr 5366  df-se 5367  df-we 5368  df-xp 5413  df-rel 5414  df-cnv 5415  df-co 5416  df-dm 5417  df-rn 5418  df-res 5419  df-ima 5420  df-pred 5986  df-ord 6032  df-on 6033  df-lim 6034  df-suc 6035  df-iota 6152  df-fun 6190  df-fn 6191  df-f 6192  df-f1 6193  df-fo 6194  df-f1o 6195  df-fv 6196  df-isom 6197  df-riota 6937  df-ov 6979  df-oprab 6980  df-mpo 6981  df-of 7227  df-om 7397  df-1st 7501  df-2nd 7502  df-supp 7634  df-tpos 7695  df-wrecs 7750  df-recs 7812  df-rdg 7850  df-1o 7905  df-oadd 7909  df-er 8089  df-map 8208  df-ixp 8260  df-en 8307  df-dom 8308  df-sdom 8309  df-fin 8310  df-fsupp 8629  df-sup 8701  df-oi 8769  df-card 9162  df-pnf 10476  df-mnf 10477  df-xr 10478  df-ltxr 10479  df-le 10480  df-sub 10672  df-neg 10673  df-div 11099  df-nn 11440  df-2 11503  df-3 11504  df-4 11505  df-5 11506  df-6 11507  df-7 11508  df-8 11509  df-9 11510  df-n0 11708  df-z 11794  df-dec 11912  df-uz 12059  df-rp 12205  df-ico 12560  df-fz 12709  df-fzo 12850  df-seq 13185  df-exp 13245  df-hash 13506  df-cj 14319  df-re 14320  df-im 14321  df-sqrt 14455  df-abs 14456  df-clim 14706  df-sum 14904  df-struct 16341  df-ndx 16342  df-slot 16343  df-base 16345  df-sets 16346  df-ress 16347  df-plusg 16434  df-mulr 16435  df-starv 16436  df-sca 16437  df-vsca 16438  df-ip 16439  df-tset 16440  df-ple 16441  df-ds 16443  df-unif 16444  df-hom 16445  df-cco 16446  df-0g 16571  df-gsum 16572  df-prds 16577  df-pws 16579  df-mgm 17710  df-sgrp 17752  df-mnd 17763  df-mhm 17803  df-grp 17894  df-minusg 17895  df-sbg 17896  df-subg 18060  df-ghm 18127  df-cntz 18218  df-cmn 18668  df-abl 18669  df-mgp 18963  df-ur 18975  df-ring 19022  df-cring 19023  df-oppr 19096  df-dvdsr 19114  df-unit 19115  df-invr 19145  df-dvr 19156  df-rnghom 19190  df-drng 19227  df-field 19228  df-subrg 19256  df-staf 19338  df-srng 19339  df-lmod 19358  df-lss 19426  df-sra 19666  df-rgmod 19667  df-met 20241  df-cnfld 20248  df-refld 20451  df-dsmm 20578  df-frlm 20593  df-nm 22895  df-tng 22897  df-tcph 23476  df-rrx 23691
This theorem is referenced by:  rrxdstprj1  23715  rrxmetfi  23718
  Copyright terms: Public domain W3C validator