This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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+ )