Database
BASIC TOPOLOGY
Metric spaces
Normed algebraic structures
sgrim
Metamath Proof Explorer
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 ∈ S → 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 ∈ S → D = dist ⁡ X
5
3 4
eqtr4id
⊢ U ∈ S → E = D