Metamath Proof Explorer


Theorem sgrim

Description: The induced metric on a subgroup is the induced metric on the parent group equipped with a norm. (Contributed by NM, 1-Feb-2008) (Revised by AV, 19-Oct-2021)

Ref Expression
Hypotheses sgrim.x X = T 𝑠 U
sgrim.d D = dist T
sgrim.e E = dist X
Assertion sgrim U S E = D

Proof

Step Hyp Ref Expression
1 sgrim.x X = T 𝑠 U
2 sgrim.d D = dist T
3 sgrim.e E = dist X
4 1 2 ressds U S D = dist X
5 3 4 eqtr4id U S E = D