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	⊢ 𝑋 = ( 𝑇 ↾_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	⊢ ( 𝑈 ∈ 𝑆 → 𝐸 = 𝐷 )