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

Metamath Proof Explorer

Theorem nmgt0

Description: The norm of a nonzero element is a positive real. (Contributed by NM, 20-Nov-2007) (Revised by AV, 8-Oct-2021)

Ref Expression
Hypotheses nmgt0.x 
|- X = ( Base ` G )
nmgt0.n 
|- N = ( norm ` G )
nmgt0.z 
|- .0. = ( 0g ` G )
Assertion nmgt0 
|- ( ( G e. NrmGrp /\ A e. X ) -> ( A =/= .0. <-> 0 < ( N ` A ) ) )

Proof

Step Hyp Ref Expression
1 nmgt0.x 
 |-  X = ( Base ` G )
2 nmgt0.n 
 |-  N = ( norm ` G )
3 nmgt0.z 
 |-  .0. = ( 0g ` G )
4 1 2 3 nmeq0 
 |-  ( ( G e. NrmGrp /\ A e. X ) -> ( ( N ` A ) = 0 <-> A = .0. ) )
5 4 necon3bid 
 |-  ( ( G e. NrmGrp /\ A e. X ) -> ( ( N ` A ) =/= 0 <-> A =/= .0. ) )
6 1 2 nmcl 
 |-  ( ( G e. NrmGrp /\ A e. X ) -> ( N ` A ) e. RR )
7 1 2 nmge0 
 |-  ( ( G e. NrmGrp /\ A e. X ) -> 0 <_ ( N ` A ) )
8 ne0gt0 
 |-  ( ( ( N ` A ) e. RR /\ 0 <_ ( N ` A ) ) -> ( ( N ` A ) =/= 0 <-> 0 < ( N ` A ) ) )
9 6 7 8 syl2anc 
 |-  ( ( G e. NrmGrp /\ A e. X ) -> ( ( N ` A ) =/= 0 <-> 0 < ( N ` A ) ) )
10 5 9 bitr3d 
 |-  ( ( G e. NrmGrp /\ A e. X ) -> ( A =/= .0. <-> 0 < ( N ` A ) ) )