Description: The value of the norm function on a structure containing a zero as the distance restricted to the elements of the base set to zero. Examples of structures containing a "zero" are groups (see nmfval2 proved from this theorem and grpidcl ) or more generally monoids (see mndidcl ), or pointed sets). (Contributed by Mario Carneiro, 2-Oct-2015) Extract this result from the proof of nmfval2 . (Revised by BJ, 27-Aug-2024)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | nmfval0.n | |- N = ( norm ` W ) |
|
| nmfval0.x | |- X = ( Base ` W ) |
||
| nmfval0.z | |- .0. = ( 0g ` W ) |
||
| nmfval0.d | |- D = ( dist ` W ) |
||
| nmfval0.e | |- E = ( D |` ( X X. X ) ) |
||
| Assertion | nmfval0 | |- ( .0. e. X -> N = ( x e. X |-> ( x E .0. ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | nmfval0.n | |- N = ( norm ` W ) |
|
| 2 | nmfval0.x | |- X = ( Base ` W ) |
|
| 3 | nmfval0.z | |- .0. = ( 0g ` W ) |
|
| 4 | nmfval0.d | |- D = ( dist ` W ) |
|
| 5 | nmfval0.e | |- E = ( D |` ( X X. X ) ) |
|
| 6 | 1 2 3 4 | nmfval | |- N = ( x e. X |-> ( x D .0. ) ) |
| 7 | 5 | oveqi | |- ( x E .0. ) = ( x ( D |` ( X X. X ) ) .0. ) |
| 8 | ovres | |- ( ( x e. X /\ .0. e. X ) -> ( x ( D |` ( X X. X ) ) .0. ) = ( x D .0. ) ) |
|
| 9 | 8 | ancoms | |- ( ( .0. e. X /\ x e. X ) -> ( x ( D |` ( X X. X ) ) .0. ) = ( x D .0. ) ) |
| 10 | 7 9 | eqtr2id | |- ( ( .0. e. X /\ x e. X ) -> ( x D .0. ) = ( x E .0. ) ) |
| 11 | 10 | mpteq2dva | |- ( .0. e. X -> ( x e. X |-> ( x D .0. ) ) = ( x e. X |-> ( x E .0. ) ) ) |
| 12 | 6 11 | syl5eq | |- ( .0. e. X -> N = ( x e. X |-> ( x E .0. ) ) ) |