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{\upharpoonright }_{𝑠}U$$
	sgrim.d	$$⊢D=\mathrm{dist}\left(T\right)$$
	sgrim.e	$$⊢E=\mathrm{dist}\left(X\right)$$
Assertion	sgrim	$$⊢U\in S\to E=D$$

Proof

Step	Hyp	Ref	Expression
1		sgrim.x	$$⊢X=T{\upharpoonright }_{𝑠}U$$
2		sgrim.d	$$⊢D=\mathrm{dist}\left(T\right)$$
3		sgrim.e	$$⊢E=\mathrm{dist}\left(X\right)$$
4	1 2	ressds	$$⊢U\in S\to D=\mathrm{dist}\left(X\right)$$
5	3 4	eqtr4id	$$⊢U\in S\to E=D$$