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 |`s U ) |
|
| sgrim.d | |- D = ( dist ` T ) |
||
| sgrim.e | |- E = ( dist ` X ) |
||
| Assertion | sgrim | |- ( U e. S -> E = D ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | sgrim.x | |- X = ( T |`s U ) |
|
| 2 | sgrim.d | |- D = ( dist ` T ) |
|
| 3 | sgrim.e | |- E = ( dist ` X ) |
|
| 4 | 1 2 | ressds | |- ( U e. S -> D = ( dist ` X ) ) |
| 5 | 3 4 | eqtr4id | |- ( U e. S -> E = D ) |