Theorem tngngpim

Description: The induced metric of a normed group is a function. (Contributed by AV, 19-Oct-2021)

	Ref	Expression
Hypotheses	tngngpim.t	⊢ 𝑇 = ( 𝐺 toNrmGrp 𝑁 )
	tngngpim.n	⊢ 𝑁 = ( norm ‘ 𝐺 )
	tngngpim.x	⊢ 𝑋 = ( Base ‘ 𝐺 )
	tngngpim.d	⊢ 𝐷 = ( dist ‘ 𝑇 )
Assertion	tngngpim	⊢ ( 𝐺 ∈ NrmGrp → 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ )

Proof

Step	Hyp	Ref	Expression
1		tngngpim.t	⊢ 𝑇 = ( 𝐺 toNrmGrp 𝑁 )
2		tngngpim.n	⊢ 𝑁 = ( norm ‘ 𝐺 )
3		tngngpim.x	⊢ 𝑋 = ( Base ‘ 𝐺 )
4		tngngpim.d	⊢ 𝐷 = ( dist ‘ 𝑇 )
5	3 2	nmf	⊢ ( 𝐺 ∈ NrmGrp → 𝑁 : 𝑋 ⟶ ℝ )
6	2	oveq2i	⊢ ( 𝐺 toNrmGrp 𝑁 ) = ( 𝐺 toNrmGrp ( norm ‘ 𝐺 ) )
7	1 6	eqtri	⊢ 𝑇 = ( 𝐺 toNrmGrp ( norm ‘ 𝐺 ) )
8	7	nrmtngnrm	⊢ ( 𝐺 ∈ NrmGrp → ( 𝑇 ∈ NrmGrp ∧ ( norm ‘ 𝑇 ) = ( norm ‘ 𝐺 ) ) )
9	1 3 4	tngngp2	⊢ ( 𝑁 : 𝑋 ⟶ ℝ → ( 𝑇 ∈ NrmGrp ↔ ( 𝐺 ∈ Grp ∧ 𝐷 ∈ ( Met ‘ 𝑋 ) ) ) )
10		simpr	⊢ ( ( 𝐺 ∈ Grp ∧ 𝐷 ∈ ( Met ‘ 𝑋 ) ) → 𝐷 ∈ ( Met ‘ 𝑋 ) )
11	9 10	syl6bi	⊢ ( 𝑁 : 𝑋 ⟶ ℝ → ( 𝑇 ∈ NrmGrp → 𝐷 ∈ ( Met ‘ 𝑋 ) ) )
12	11	com12	⊢ ( 𝑇 ∈ NrmGrp → ( 𝑁 : 𝑋 ⟶ ℝ → 𝐷 ∈ ( Met ‘ 𝑋 ) ) )
13	12	adantr	⊢ ( ( 𝑇 ∈ NrmGrp ∧ ( norm ‘ 𝑇 ) = ( norm ‘ 𝐺 ) ) → ( 𝑁 : 𝑋 ⟶ ℝ → 𝐷 ∈ ( Met ‘ 𝑋 ) ) )
14	8 13	syl	⊢ ( 𝐺 ∈ NrmGrp → ( 𝑁 : 𝑋 ⟶ ℝ → 𝐷 ∈ ( Met ‘ 𝑋 ) ) )
15		metf	⊢ ( 𝐷 ∈ ( Met ‘ 𝑋 ) → 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ )
16	14 15	syl6	⊢ ( 𝐺 ∈ NrmGrp → ( 𝑁 : 𝑋 ⟶ ℝ → 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ ) )
17	5 16	mpd	⊢ ( 𝐺 ∈ NrmGrp → 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ )