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 ∧ 𝑈 ∈ 𝑆 ) ∧ ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑈 ) ) → ( 𝐴 𝐸 𝐵 ) = ( 𝐴 𝐷 𝐵 ) )