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 | |
|
sgrim.d | |
||
sgrim.e | |
||
Assertion | sgrim | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sgrim.x | |
|
2 | sgrim.d | |
|
3 | sgrim.e | |
|
4 | 1 2 | ressds | |
5 | 3 4 | eqtr4id | |