Theorem 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\mathrm{toNrmGrp}N$$
	tngngp.x	$$⊢X={\mathrm{Base}}_G$$
	tngngp.m	$$⊢\underset{\dot{}}{-}={-}_G$$
	tngngp.z	$$⊢\underset{\dot{}}{0}=0_G$$
	tngngpd.1	$$⊢\phi \to G\in \mathrm{Grp}$$
	tngngpd.2	$$⊢\phi \to N:X⟶ℝ$$
	tngngpd.3	$$⊢\left(\phi \wedge x\in X\right)\to \left(N\left(x\right)=0\leftrightarrow x=\underset{\dot{}}{0}\right)$$
	tngngpd.4	$$⊢\left(\phi \wedge \left(x\in X\wedge y\in X\right)\right)\to N\left(x\underset{\dot{}}{-}y\right)\le N\left(x\right)+N\left(y\right)$$
Assertion	tngngpd	$$⊢\phi \to T\in \mathrm{NrmGrp}$$

Proof

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