Theorem nmne0

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

	Ref	Expression
Hypotheses	nmf.x	$$⊢X={\mathrm{Base}}_G$$
	nmf.n	$$⊢N=\mathrm{norm}\left(G\right)$$
	nmeq0.z	$$⊢\underset{\dot{}}{0}=0_G$$
Assertion	nmne0	$$⊢\left(G\in \mathrm{NrmGrp}\wedge A\in X\wedge A\ne \underset{\dot{}}{0}\right)\to N\left(A\right)\ne 0$$

Proof

Step	Hyp	Ref	Expression
1		nmf.x	$$⊢X={\mathrm{Base}}_G$$
2		nmf.n	$$⊢N=\mathrm{norm}\left(G\right)$$
3		nmeq0.z	$$⊢\underset{\dot{}}{0}=0_G$$
4	1 2 3	nmeq0	$$⊢\left(G\in \mathrm{NrmGrp}\wedge A\in X\right)\to \left(N\left(A\right)=0\leftrightarrow A=\underset{\dot{}}{0}\right)$$
5	4	necon3bid	$$⊢\left(G\in \mathrm{NrmGrp}\wedge A\in X\right)\to \left(N\left(A\right)\ne 0\leftrightarrow A\ne \underset{\dot{}}{0}\right)$$
6	5	biimp3ar	$$⊢\left(G\in \mathrm{NrmGrp}\wedge A\in X\wedge A\ne \underset{\dot{}}{0}\right)\to N\left(A\right)\ne 0$$