tngngpd

Description: Derive the axioms for a normed group from the axioms for a metric space. (Contributed by Mario Carneiro, 4-Oct-2015)

	Ref	Expression
Hypotheses	tngngp.t	$⊢ T = G toNrmGrp N$
	tngngp.x	$⊢ X = {Base}_{G}$
	tngngp.m	$⊢ \underset{˙}{-} = -_{G}$
	tngngp.z	$⊢ \underset{˙}{0} = 0_{G}$
	tngngpd.1	$⊢ φ \to G \in Grp$
	tngngpd.2	$⊢ φ \to N : X ⟶ ℝ$
	tngngpd.3	$⊢ (φ \land x \in X) \to (N (x) = 0 \leftrightarrow x = \underset{˙}{0})$
	tngngpd.4	$⊢ (φ \land (x \in X \land y \in X)) \to N (x \underset{˙}{-} y) \leq N (x) + N (y)$
Assertion	tngngpd	$⊢ φ \to T \in NrmGrp$

Step	Hyp	Ref	Expression
1		tngngp.t	$⊢ T = G toNrmGrp N$
2		tngngp.x	$⊢ X = {Base}_{G}$
3		tngngp.m	$⊢ \underset{˙}{-} = -_{G}$
4		tngngp.z	$⊢ \underset{˙}{0} = 0_{G}$
5		tngngpd.1	$⊢ φ \to G \in Grp$
6		tngngpd.2	$⊢ φ \to N : X ⟶ ℝ$
7		tngngpd.3	$⊢ (φ \land x \in X) \to (N (x) = 0 \leftrightarrow x = \underset{˙}{0})$
8		tngngpd.4	$⊢ (φ \land (x \in X \land y \in X)) \to N (x \underset{˙}{-} y) \leq N (x) + N (y)$
9	2	fvexi	$⊢ X \in V$
10		reex	$⊢ ℝ \in V$
11		fex2	$⊢ (N : X ⟶ ℝ \land X \in V \land ℝ \in V) \to N \in V$
12	9 10 11	mp3an23	$⊢ N : X ⟶ ℝ \to N \in V$
13	1 3	tngds	$⊢ N \in V \to N \circ \underset{˙}{-} = dist (T)$
14	6 12 13	3syl	$⊢ φ \to N \circ \underset{˙}{-} = dist (T)$
15	2 3 4 5 6 7 8	nrmmetd	$⊢ φ \to N \circ \underset{˙}{-} \in Met (X)$
16	14 15	eqeltrrd	$⊢ φ \to dist (T) \in Met (X)$
17		eqid	$⊢ dist (T) = dist (T)$
18	1 2 17	tngngp2	$⊢ N : X ⟶ ℝ \to (T \in NrmGrp \leftrightarrow (G \in Grp \land dist (T) \in Met (X)))$
19	6 18	syl	$⊢ φ \to (T \in NrmGrp \leftrightarrow (G \in Grp \land dist (T) \in Met (X)))$
20	5 16 19	mpbir2and	$⊢ φ \to T \in NrmGrp$

Metamath Proof Explorer