Metamath Proof Explorer

Theorem nmge0

Description: The norm of a normed group is nonnegative. Second part of Problem 2 of Kreyszig p. 64. (Contributed by NM, 28-Nov-2006) (Revised by Mario Carneiro, 4-Oct-2015)

		Ref	Expression
	Hypotheses	nmf.x	$⊢ X = {Base}_{G}$
		nmf.n	$⊢ N = norm (G)$
	Assertion	nmge0	$⊢ (G \in NrmGrp \land A \in X) \to 0 \leq N (A)$

Proof

Step	Hyp	Ref	Expression
1		nmf.x	$⊢ X = {Base}_{G}$
2		nmf.n	$⊢ N = norm (G)$
3		ngpgrp	$⊢ G \in NrmGrp \to G \in Grp$
4		eqid	$⊢ 0_{G} = 0_{G}$
5	1 4	grpidcl	$⊢ G \in Grp \to 0_{G} \in X$
6	3 5	syl	$⊢ G \in NrmGrp \to 0_{G} \in X$
7	6	adantr	$⊢ (G \in NrmGrp \land A \in X) \to 0_{G} \in X$
8		ngpxms	$⊢ G \in NrmGrp \to G \in ∞MetSp$
9		eqid	$⊢ dist (G) = dist (G)$
10	1 9	xmsge0	$⊢ (G \in ∞MetSp \land A \in X \land 0_{G} \in X) \to 0 \leq A dist (G) 0_{G}$
11	8 10	syl3an1	$⊢ (G \in NrmGrp \land A \in X \land 0_{G} \in X) \to 0 \leq A dist (G) 0_{G}$
12	7 11	mpd3an3	$⊢ (G \in NrmGrp \land A \in X) \to 0 \leq A dist (G) 0_{G}$
13	2 1 4 9	nmval	$⊢ A \in X \to N (A) = A dist (G) 0_{G}$
14	13	adantl	$⊢ (G \in NrmGrp \land A \in X) \to N (A) = A dist (G) 0_{G}$
15	12 14	breqtrrd	$⊢ (G \in NrmGrp \land A \in X) \to 0 \leq N (A)$