tngngpim

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

Step	Hyp	Ref	Expression
1		tngngpim.t	$⊢ T = G toNrmGrp N$
2		tngngpim.n	$⊢ N = norm (G)$
3		tngngpim.x	$⊢ X = {Base}_{G}$
4		tngngpim.d	$⊢ D = dist (T)$
5	3 2	nmf	$⊢ G \in NrmGrp \to N : X ⟶ ℝ$
6	2	oveq2i	$⊢ G toNrmGrp N = G toNrmGrp norm (G)$
7	1 6	eqtri	$⊢ T = G toNrmGrp norm (G)$
8	7	nrmtngnrm	$⊢ G \in NrmGrp \to (T \in NrmGrp \land norm (T) = norm (G))$
9	1 3 4	tngngp2	$⊢ N : X ⟶ ℝ \to (T \in NrmGrp \leftrightarrow (G \in Grp \land D \in Met (X)))$
10		simpr	$⊢ (G \in Grp \land D \in Met (X)) \to D \in Met (X)$
11	9 10	syl6bi	$⊢ N : X ⟶ ℝ \to (T \in NrmGrp \to D \in Met (X))$
12	11	com12	$⊢ T \in NrmGrp \to (N : X ⟶ ℝ \to D \in Met (X))$
13	12	adantr	$⊢ (T \in NrmGrp \land norm (T) = norm (G)) \to (N : X ⟶ ℝ \to D \in Met (X))$
14	8 13	syl	$⊢ G \in NrmGrp \to (N : X ⟶ ℝ \to D \in Met (X))$
15		metf	$⊢ D \in Met (X) \to D : X \times X ⟶ ℝ$
16	14 15	syl6	$⊢ G \in NrmGrp \to (N : X ⟶ ℝ \to D : X \times X ⟶ ℝ)$
17	5 16	mpd	$⊢ G \in NrmGrp \to D : X \times X ⟶ ℝ$

Metamath Proof Explorer