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 ) )