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