Theorem nmcl

Description: The norm of a normed group is closed in 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	nmcl	$$⊢\left(G\in \mathrm{NrmGrp}\wedge A\in X\right)\to N\left(A\right)\in ℝ$$

Proof

Step	Hyp	Ref	Expression
1		nmf.x	$$⊢X={\mathrm{Base}}_G$$
2		nmf.n	$$⊢N=\mathrm{norm}\left(G\right)$$
3	1 2	nmf	$$⊢G\in \mathrm{NrmGrp}\to N:X⟶ℝ$$
4	3	ffvelcdmda	$$⊢\left(G\in \mathrm{NrmGrp}\wedge A\in X\right)\to N\left(A\right)\in ℝ$$