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 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝐷 𝐵 ) = ( 𝑁 ‘ ( 𝐴 − 𝐵 ) ) )