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=distT
sgrim.e E=distX
Assertion sgrim USE=D

Proof

Step Hyp Ref Expression
1 sgrim.x X=T𝑠U
2 sgrim.d D=distT
3 sgrim.e E=distX
4 1 2 ressds USD=distX
5 3 4 eqtr4id USE=D