This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem nmval2

Description: The value of the norm on a group as the distance restricted to the elements of the base set to zero. (Contributed by Mario Carneiro, 2-Oct-2015)

Ref Expression
Hypotheses nmfval2.n ⊢ 𝑁 = ( norm ‘ 𝑊 )
nmfval2.x ⊢ 𝑋 = ( Base ‘ 𝑊 )
nmfval2.z ⊢ 0 = ( 0g ‘ 𝑊 )
nmfval2.d ⊢ 𝐷 = ( dist ‘ 𝑊 )
nmfval2.e ⊢ 𝐸 = ( 𝐷 ↾ ( 𝑋 × 𝑋 ) )
Assertion nmval2 ( ( 𝑊 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) → ( 𝑁 ‘ 𝐴 ) = ( 𝐴 𝐸 0 ) )

Proof

Step Hyp Ref Expression
1 nmfval2.n ⊢ 𝑁 = ( norm ‘ 𝑊 )
2 nmfval2.x ⊢ 𝑋 = ( Base ‘ 𝑊 )
3 nmfval2.z ⊢ 0 = ( 0g ‘ 𝑊 )
4 nmfval2.d ⊢ 𝐷 = ( dist ‘ 𝑊 )
5 nmfval2.e ⊢ 𝐸 = ( 𝐷 ↾ ( 𝑋 × 𝑋 ) )
6 1 2 3 4 nmval ⊢ ( 𝐴 ∈ 𝑋 → ( 𝑁 ‘ 𝐴 ) = ( 𝐴 𝐷 0 ) )
7 6 adantl ⊢ ( ( 𝑊 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) → ( 𝑁 ‘ 𝐴 ) = ( 𝐴 𝐷 0 ) )
8 5 oveqi ⊢ ( 𝐴 𝐸 0 ) = ( 𝐴 ( 𝐷 ↾ ( 𝑋 × 𝑋 ) ) 0 )
9 id ⊢ ( 𝐴 ∈ 𝑋 → 𝐴 ∈ 𝑋 )
10 2 3 grpidcl ⊢ ( 𝑊 ∈ Grp → 0 ∈ 𝑋 )
11 ovres ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 0 ∈ 𝑋 ) → ( 𝐴 ( 𝐷 ↾ ( 𝑋 × 𝑋 ) ) 0 ) = ( 𝐴 𝐷 0 ) )
12 9 10 11 syl2anr ⊢ ( ( 𝑊 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) → ( 𝐴 ( 𝐷 ↾ ( 𝑋 × 𝑋 ) ) 0 ) = ( 𝐴 𝐷 0 ) )
13 8 12 eqtr2id ⊢ ( ( 𝑊 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) → ( 𝐴 𝐷 0 ) = ( 𝐴 𝐸 0 ) )
14 7 13 eqtrd ⊢ ( ( 𝑊 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) → ( 𝑁 ‘ 𝐴 ) = ( 𝐴 𝐸 0 ) )