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 = ( Base ` G )
	nmf.n	|- N = ( norm ` G )
	nmeq0.z	|- .0. = ( 0g ` G )
Assertion	nmrpcl	|- ( ( G e. NrmGrp /\ A e. X /\ A =/= .0. ) -> ( N ` A ) e. RR+ )

Proof

Step	Hyp	Ref	Expression
1		nmf.x	|- X = ( Base ` G )
2		nmf.n	|- N = ( norm ` G )
3		nmeq0.z	|- .0. = ( 0g ` G )
4	1 2	nmcl	|- ( ( G e. NrmGrp /\ A e. X ) -> ( N ` A ) e. RR )
5	4	3adant3	|- ( ( G e. NrmGrp /\ A e. X /\ A =/= .0. ) -> ( N ` A ) e. RR )
6	1 2	nmge0	|- ( ( G e. NrmGrp /\ A e. X ) -> 0 <_ ( N ` A ) )
7	6	3adant3	|- ( ( G e. NrmGrp /\ A e. X /\ A =/= .0. ) -> 0 <_ ( N ` A ) )
8	1 2 3	nmne0	|- ( ( G e. NrmGrp /\ A e. X /\ A =/= .0. ) -> ( N ` A ) =/= 0 )
9	5 7 8	ne0gt0d	|- ( ( G e. NrmGrp /\ A e. X /\ A =/= .0. ) -> 0 < ( N ` A ) )
10	5 9	elrpd	|- ( ( G e. NrmGrp /\ A e. X /\ A =/= .0. ) -> ( N ` A ) e. RR+ )