This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 = {Base}_{G}$
	nmf.n	$⊢ N = norm (G)$
	nmeq0.z	$⊢ \underset{˙}{0} = 0_{G}$
Assertion	nmne0	$⊢ (G \in NrmGrp \land A \in X \land A \neq \underset{˙}{0}) \to N (A) \neq 0$

Step	Hyp	Ref	Expression
1		nmf.x	$⊢ X = {Base}_{G}$
2		nmf.n	$⊢ N = norm (G)$
3		nmeq0.z	$⊢ \underset{˙}{0} = 0_{G}$
4	1 2 3	nmeq0	$⊢ (G \in NrmGrp \land A \in X) \to (N (A) = 0 \leftrightarrow A = \underset{˙}{0})$
5	4	necon3bid	$⊢ (G \in NrmGrp \land A \in X) \to (N (A) \neq 0 \leftrightarrow A \neq \underset{˙}{0})$
6	5	biimp3ar	$⊢ (G \in NrmGrp \land A \in X \land A \neq \underset{˙}{0}) \to N (A) \neq 0$