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	$⊢ \underset{˙}{0} = 0_{G}$
Assertion	nmgt0	$⊢ (G \in NrmGrp \land A \in X) \to (A \neq \underset{˙}{0} \leftrightarrow 0 < N (A))$

Step	Hyp	Ref	Expression
1		nmgt0.x	$⊢ X = {Base}_{G}$
2		nmgt0.n	$⊢ N = norm (G)$
3		nmgt0.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	1 2	nmcl	$⊢ (G \in NrmGrp \land A \in X) \to N (A) \in ℝ$
7	1 2	nmge0	$⊢ (G \in NrmGrp \land A \in X) \to 0 \leq N (A)$
8		ne0gt0	$⊢ (N (A) \in ℝ \land 0 \leq N (A)) \to (N (A) \neq 0 \leftrightarrow 0 < N (A))$
9	6 7 8	syl2anc	$⊢ (G \in NrmGrp \land A \in X) \to (N (A) \neq 0 \leftrightarrow 0 < N (A))$
10	5 9	bitr3d	$⊢ (G \in NrmGrp \land A \in X) \to (A \neq \underset{˙}{0} \leftrightarrow 0 < N (A))$

Metamath Proof Explorer