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

Metamath Proof Explorer

Theorem ngpds

Description: Value of the distance function in terms of the norm of a normed group. Equation 1 of Kreyszig p. 59. (Contributed by NM, 28-Nov-2006) (Revised by Mario Carneiro, 2-Oct-2015)

Ref Expression
Hypotheses ngpds.n ⊢ 𝑁 = ( norm ‘ 𝐺 )
ngpds.x ⊢ 𝑋 = ( Base ‘ 𝐺 )
ngpds.m ⊢ − = ( -g ‘ 𝐺 )
ngpds.d ⊢ 𝐷 = ( dist ‘ 𝐺 )
Assertion ngpds ( ( 𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝐷 𝐵 ) = ( 𝑁 ‘ ( 𝐴 − 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 ngpds.n ⊢ 𝑁 = ( norm ‘ 𝐺 )
2 ngpds.x ⊢ 𝑋 = ( Base ‘ 𝐺 )
3 ngpds.m ⊢ − = ( -g ‘ 𝐺 )
4 ngpds.d ⊢ 𝐷 = ( dist ‘ 𝐺 )
5 eqid ⊢ ( 𝐷 ↾ ( 𝑋 × 𝑋 ) ) = ( 𝐷 ↾ ( 𝑋 × 𝑋 ) )
6 1 3 4 2 5 isngp2 ⊢ ( 𝐺 ∈ NrmGrp ↔ ( 𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp ∧ ( 𝑁 ∘ − ) = ( 𝐷 ↾ ( 𝑋 × 𝑋 ) ) ) )
7 6 simp3bi ⊢ ( 𝐺 ∈ NrmGrp → ( 𝑁 ∘ − ) = ( 𝐷 ↾ ( 𝑋 × 𝑋 ) ) )
8 7 3ad2ant1 ⊢ ( ( 𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝑁 ∘ − ) = ( 𝐷 ↾ ( 𝑋 × 𝑋 ) ) )
9 8 oveqd ⊢ ( ( 𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 ( 𝑁 ∘ − ) 𝐵 ) = ( 𝐴 ( 𝐷 ↾ ( 𝑋 × 𝑋 ) ) 𝐵 ) )
10 ngpgrp ⊢ ( 𝐺 ∈ NrmGrp → 𝐺 ∈ Grp )
11 2 3 grpsubf ⊢ ( 𝐺 ∈ Grp → − : ( 𝑋 × 𝑋 ) ⟶ 𝑋 )
12 10 11 syl ⊢ ( 𝐺 ∈ NrmGrp → − : ( 𝑋 × 𝑋 ) ⟶ 𝑋 )
13 12 3ad2ant1 ⊢ ( ( 𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → − : ( 𝑋 × 𝑋 ) ⟶ 𝑋 )
14 opelxpi ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ⟨ 𝐴 , 𝐵 ⟩ ∈ ( 𝑋 × 𝑋 ) )
15 14 3adant1 ⊢ ( ( 𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ⟨ 𝐴 , 𝐵 ⟩ ∈ ( 𝑋 × 𝑋 ) )
16 fvco3 ⊢ ( ( − : ( 𝑋 × 𝑋 ) ⟶ 𝑋 ∧ ⟨ 𝐴 , 𝐵 ⟩ ∈ ( 𝑋 × 𝑋 ) ) → ( ( 𝑁 ∘ − ) ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = ( 𝑁 ‘ ( − ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) )
17 13 15 16 syl2anc ⊢ ( ( 𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝑁 ∘ − ) ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = ( 𝑁 ‘ ( − ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) )
18 df-ov ⊢ ( 𝐴 ( 𝑁 ∘ − ) 𝐵 ) = ( ( 𝑁 ∘ − ) ‘ ⟨ 𝐴 , 𝐵 ⟩ )
19 df-ov ⊢ ( 𝐴 − 𝐵 ) = ( − ‘ ⟨ 𝐴 , 𝐵 ⟩ )
20 19 fveq2i ⊢ ( 𝑁 ‘ ( 𝐴 − 𝐵 ) ) = ( 𝑁 ‘ ( − ‘ ⟨ 𝐴 , 𝐵 ⟩ ) )
21 17 18 20 3eqtr4g ⊢ ( ( 𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 ( 𝑁 ∘ − ) 𝐵 ) = ( 𝑁 ‘ ( 𝐴 − 𝐵 ) ) )
22 ovres ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 ( 𝐷 ↾ ( 𝑋 × 𝑋 ) ) 𝐵 ) = ( 𝐴 𝐷 𝐵 ) )
23 22 3adant1 ⊢ ( ( 𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 ( 𝐷 ↾ ( 𝑋 × 𝑋 ) ) 𝐵 ) = ( 𝐴 𝐷 𝐵 ) )
24 9 21 23 3eqtr3rd ⊢ ( ( 𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝐷 𝐵 ) = ( 𝑁 ‘ ( 𝐴 − 𝐵 ) ) )