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

Metamath Proof Explorer

Theorem sgrimval

Description: The induced metric on a subgroup in terms of the induced metric on the parent normed group. (Contributed by NM, 1-Feb-2008) (Revised by AV, 19-Oct-2021)

		Ref	Expression
	Hypotheses	sgrim.x	⊢ 𝑋 = ( 𝑇 ↾_s 𝑈 )
		sgrim.d	⊢ 𝐷 = ( dist ‘ 𝑇 )
		sgrim.e	⊢ 𝐸 = ( dist ‘ 𝑋 )
		sgrimval.t	⊢ 𝑇 = ( 𝐺 toNrmGrp 𝑁 )
		sgrimval.n	⊢ 𝑁 = ( norm ‘ 𝐺 )
		sgrimval.s	⊢ 𝑆 = ( SubGrp ‘ 𝑇 )
	Assertion	sgrimval	⊢ ( ( ( 𝐺 ∈ NrmGrp ∧ 𝑈 ∈ 𝑆 ) ∧ ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑈 ) ) → ( 𝐴 𝐸 𝐵 ) = ( 𝐴 𝐷 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		sgrim.x	⊢ 𝑋 = ( 𝑇 ↾_s 𝑈 )
2		sgrim.d	⊢ 𝐷 = ( dist ‘ 𝑇 )
3		sgrim.e	⊢ 𝐸 = ( dist ‘ 𝑋 )
4		sgrimval.t	⊢ 𝑇 = ( 𝐺 toNrmGrp 𝑁 )
5		sgrimval.n	⊢ 𝑁 = ( norm ‘ 𝐺 )
6		sgrimval.s	⊢ 𝑆 = ( SubGrp ‘ 𝑇 )
7	1 2 3	sgrim	⊢ ( 𝑈 ∈ 𝑆 → 𝐸 = 𝐷 )
8	7	oveqd	⊢ ( 𝑈 ∈ 𝑆 → ( 𝐴 𝐸 𝐵 ) = ( 𝐴 𝐷 𝐵 ) )
9	8	ad2antlr	⊢ ( ( ( 𝐺 ∈ NrmGrp ∧ 𝑈 ∈ 𝑆 ) ∧ ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑈 ) ) → ( 𝐴 𝐸 𝐵 ) = ( 𝐴 𝐷 𝐵 ) )