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 | ⊢ 𝑁 = ( norm ‘ 𝑊 ) | |
| nmfval0.x | ⊢ 𝑋 = ( Base ‘ 𝑊 ) | ||
| nmfval0.z | ⊢ 0 = ( 0g ‘ 𝑊 ) | ||
| nmfval0.d | ⊢ 𝐷 = ( dist ‘ 𝑊 ) | ||
| nmfval0.e | ⊢ 𝐸 = ( 𝐷 ↾ ( 𝑋 × 𝑋 ) ) | ||
| Assertion | nmfval0 | ⊢ ( 0 ∈ 𝑋 → 𝑁 = ( 𝑥 ∈ 𝑋 ↦ ( 𝑥 𝐸 0 ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | nmfval0.n | ⊢ 𝑁 = ( norm ‘ 𝑊 ) | |
| 2 | nmfval0.x | ⊢ 𝑋 = ( Base ‘ 𝑊 ) | |
| 3 | nmfval0.z | ⊢ 0 = ( 0g ‘ 𝑊 ) | |
| 4 | nmfval0.d | ⊢ 𝐷 = ( dist ‘ 𝑊 ) | |
| 5 | nmfval0.e | ⊢ 𝐸 = ( 𝐷 ↾ ( 𝑋 × 𝑋 ) ) | |
| 6 | 1 2 3 4 | nmfval | ⊢ 𝑁 = ( 𝑥 ∈ 𝑋 ↦ ( 𝑥 𝐷 0 ) ) |
| 7 | 5 | oveqi | ⊢ ( 𝑥 𝐸 0 ) = ( 𝑥 ( 𝐷 ↾ ( 𝑋 × 𝑋 ) ) 0 ) |
| 8 | ovres | ⊢ ( ( 𝑥 ∈ 𝑋 ∧ 0 ∈ 𝑋 ) → ( 𝑥 ( 𝐷 ↾ ( 𝑋 × 𝑋 ) ) 0 ) = ( 𝑥 𝐷 0 ) ) | |
| 9 | 8 | ancoms | ⊢ ( ( 0 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ) → ( 𝑥 ( 𝐷 ↾ ( 𝑋 × 𝑋 ) ) 0 ) = ( 𝑥 𝐷 0 ) ) |
| 10 | 7 9 | eqtr2id | ⊢ ( ( 0 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ) → ( 𝑥 𝐷 0 ) = ( 𝑥 𝐸 0 ) ) |
| 11 | 10 | mpteq2dva | ⊢ ( 0 ∈ 𝑋 → ( 𝑥 ∈ 𝑋 ↦ ( 𝑥 𝐷 0 ) ) = ( 𝑥 ∈ 𝑋 ↦ ( 𝑥 𝐸 0 ) ) ) |
| 12 | 6 11 | syl5eq | ⊢ ( 0 ∈ 𝑋 → 𝑁 = ( 𝑥 ∈ 𝑋 ↦ ( 𝑥 𝐸 0 ) ) ) |