Theorem nmf

Description: The norm on a normed group is a function into the reals. (Contributed by Mario Carneiro, 4-Oct-2015)

	Ref	Expression
Hypotheses	nmf.x	$$⊢X={\mathrm{Base}}_G$$
	nmf.n	$$⊢N=\mathrm{norm}\left(G\right)$$
Assertion	nmf	$$⊢G\in \mathrm{NrmGrp}\to N:X⟶ℝ$$

Proof

Step	Hyp	Ref	Expression
1		nmf.x	$$⊢X={\mathrm{Base}}_G$$
2		nmf.n	$$⊢N=\mathrm{norm}\left(G\right)$$
3		ngpgrp	$$⊢G\in \mathrm{NrmGrp}\to G\in \mathrm{Grp}$$
4		eqid	$$⊢{\mathrm{dist}\left(G\right)\upharpoonright }_{\left(X\times X\right)}={\mathrm{dist}\left(G\right)\upharpoonright }_{\left(X\times X\right)}$$
5	1 4	ngpmet	$$⊢G\in \mathrm{NrmGrp}\to {\mathrm{dist}\left(G\right)\upharpoonright }_{\left(X\times X\right)}\in \mathrm{Met}\left(X\right)$$
6		eqid	$$⊢\mathrm{dist}\left(G\right)=\mathrm{dist}\left(G\right)$$
7	2 1 6 4	nmf2	$$⊢\left(G\in \mathrm{Grp}\wedge {\mathrm{dist}\left(G\right)\upharpoonright }_{\left(X\times X\right)}\in \mathrm{Met}\left(X\right)\right)\to N:X⟶ℝ$$
8	3 5 7	syl2anc	$$⊢G\in \mathrm{NrmGrp}\to N:X⟶ℝ$$