Metamath Proof Explorer


Theorem nmne0

Description: The norm of a nonzero element is nonzero. (Contributed by Mario Carneiro, 4-Oct-2015)

Ref Expression
Hypotheses nmf.x X=BaseG
nmf.n N=normG
nmeq0.z 0˙=0G
Assertion nmne0 GNrmGrpAXA0˙NA0

Proof

Step Hyp Ref Expression
1 nmf.x X=BaseG
2 nmf.n N=normG
3 nmeq0.z 0˙=0G
4 1 2 3 nmeq0 GNrmGrpAXNA=0A=0˙
5 4 necon3bid GNrmGrpAXNA0A0˙
6 5 biimp3ar GNrmGrpAXA0˙NA0