This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 \in S \to 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 \in S \to D = dist (X)$
5	3 4	eqtr4id	$⊢ U \in S \to E = D$