Theorem nmne0

Description: The norm of a nonzero element is nonzero. (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	nmne0	|- ( ( G e. NrmGrp /\ A e. X /\ A =/= .0. ) -> ( N ` A ) =/= 0 )

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 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	5	biimp3ar	|- ( ( G e. NrmGrp /\ A e. X /\ A =/= .0. ) -> ( N ` A ) =/= 0 )