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