nmrpcl

Description: The norm of a nonzero element is a positive real. (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	nmrpcl	$⊢ (G \in NrmGrp \land A \in X \land A \neq \underset{˙}{0}) \to N (A) \in ℝ^{+}$

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	nmcl	$⊢ (G \in NrmGrp \land A \in X) \to N (A) \in ℝ$
5	4	3adant3	$⊢ (G \in NrmGrp \land A \in X \land A \neq \underset{˙}{0}) \to N (A) \in ℝ$
6	1 2	nmge0	$⊢ (G \in NrmGrp \land A \in X) \to 0 \leq N (A)$
7	6	3adant3	$⊢ (G \in NrmGrp \land A \in X \land A \neq \underset{˙}{0}) \to 0 \leq N (A)$
8	1 2 3	nmne0	$⊢ (G \in NrmGrp \land A \in X \land A \neq \underset{˙}{0}) \to N (A) \neq 0$
9	5 7 8	ne0gt0d	$⊢ (G \in NrmGrp \land A \in X \land A \neq \underset{˙}{0}) \to 0 < N (A)$
10	5 9	elrpd	$⊢ (G \in NrmGrp \land A \in X \land A \neq \underset{˙}{0}) \to N (A) \in ℝ^{+}$

Metamath Proof Explorer