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	⊢ 𝑋 = ( 𝑇 ↾s 𝑈 )
	sgrim.d	⊢ 𝐷 = ( dist ‘ 𝑇 )
	sgrim.e	⊢ 𝐸 = ( dist ‘ 𝑋 )
Assertion	sgrim	⊢ ( 𝑈 ∈ 𝑆 → 𝐸 = 𝐷 )

Proof

Step	Hyp	Ref	Expression
1		sgrim.x	⊢ 𝑋 = ( 𝑇 ↾s 𝑈 )
2		sgrim.d	⊢ 𝐷 = ( dist ‘ 𝑇 )
3		sgrim.e	⊢ 𝐸 = ( dist ‘ 𝑋 )
4	1 2	ressds	⊢ ( 𝑈 ∈ 𝑆 → 𝐷 = ( dist ‘ 𝑋 ) )
5	3 4	eqtr4id	⊢ ( 𝑈 ∈ 𝑆 → 𝐸 = 𝐷 )