Theorem nmrpcl

Description: The norm of a nonzero element is a positive real. (Contributed by Mario Carneiro, 4-Oct-2015)

	Ref	Expression
Hypotheses	nmf.x	$$⊢X={\mathrm{Base}}_G$$
	nmf.n	$$⊢N=\mathrm{norm}\left(G\right)$$
	nmeq0.z	$$⊢\underset{\dot{}}{0}=0_G$$
Assertion	nmrpcl	$$⊢\left(G\in \mathrm{NrmGrp}\wedge A\in X\wedge A\ne \underset{\dot{}}{0}\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		nmeq0.z	$$⊢\underset{\dot{}}{0}=0_G$$
4	1 2	nmcl	$$⊢\left(G\in \mathrm{NrmGrp}\wedge A\in X\right)\to N\left(A\right)\in ℝ$$
5	4	3adant3	$$⊢\left(G\in \mathrm{NrmGrp}\wedge A\in X\wedge A\ne \underset{\dot{}}{0}\right)\to N\left(A\right)\in ℝ$$
6	1 2	nmge0	$$⊢\left(G\in \mathrm{NrmGrp}\wedge A\in X\right)\to 0\le N\left(A\right)$$
7	6	3adant3	$$⊢\left(G\in \mathrm{NrmGrp}\wedge A\in X\wedge A\ne \underset{\dot{}}{0}\right)\to 0\le N\left(A\right)$$
8	1 2 3	nmne0	$$⊢\left(G\in \mathrm{NrmGrp}\wedge A\in X\wedge A\ne \underset{\dot{}}{0}\right)\to N\left(A\right)\ne 0$$
9	5 7 8	ne0gt0d	$$⊢\left(G\in \mathrm{NrmGrp}\wedge A\in X\wedge A\ne \underset{\dot{}}{0}\right)\to 0<N\left(A\right)$$
10	5 9	elrpd	$$⊢\left(G\in \mathrm{NrmGrp}\wedge A\in X\wedge A\ne \underset{\dot{}}{0}\right)\to N\left(A\right)\in {ℝ}^{+}$$