Metamath Proof Explorer


Theorem rrndsxmet

Description: D is an extended metric for the n-dimensional real Euclidean space. (Contributed by Glauco Siliprandi, 8-Apr-2021)

Ref Expression
Hypotheses rrndsxmet.1 φ X Fin
rrndsxmet.2 D = f X , g X k X f k g k 2
Assertion rrndsxmet φ D ∞Met X

Proof

Step Hyp Ref Expression
1 rrndsxmet.1 φ X Fin
2 rrndsxmet.2 D = f X , g X k X f k g k 2
3 1 2 rrndsmet φ D Met X
4 metxmet D Met X D ∞Met X
5 3 4 syl φ D ∞Met X