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	⊢ 𝑋 = ( Base ‘ 𝐺 )
	nmf.n	⊢ 𝑁 = ( norm ‘ 𝐺 )
Assertion	nmge0	⊢ ( ( 𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ) → 0 ≤ ( 𝑁 ‘ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		nmf.x	⊢ 𝑋 = ( Base ‘ 𝐺 )
2		nmf.n	⊢ 𝑁 = ( norm ‘ 𝐺 )
3		ngpgrp	⊢ ( 𝐺 ∈ NrmGrp → 𝐺 ∈ Grp )
4		eqid	⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
5	1 4	grpidcl	⊢ ( 𝐺 ∈ Grp → ( 0g ‘ 𝐺 ) ∈ 𝑋 )
6	3 5	syl	⊢ ( 𝐺 ∈ NrmGrp → ( 0g ‘ 𝐺 ) ∈ 𝑋 )
7	6	adantr	⊢ ( ( 𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ) → ( 0g ‘ 𝐺 ) ∈ 𝑋 )
8		ngpxms	⊢ ( 𝐺 ∈ NrmGrp → 𝐺 ∈ ∞MetSp )
9		eqid	⊢ ( dist ‘ 𝐺 ) = ( dist ‘ 𝐺 )
10	1 9	xmsge0	⊢ ( ( 𝐺 ∈ ∞MetSp ∧ 𝐴 ∈ 𝑋 ∧ ( 0g ‘ 𝐺 ) ∈ 𝑋 ) → 0 ≤ ( 𝐴 ( dist ‘ 𝐺 ) ( 0g ‘ 𝐺 ) ) )
11	8 10	syl3an1	⊢ ( ( 𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ ( 0g ‘ 𝐺 ) ∈ 𝑋 ) → 0 ≤ ( 𝐴 ( dist ‘ 𝐺 ) ( 0g ‘ 𝐺 ) ) )
12	7 11	mpd3an3	⊢ ( ( 𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ) → 0 ≤ ( 𝐴 ( dist ‘ 𝐺 ) ( 0g ‘ 𝐺 ) ) )
13	2 1 4 9	nmval	⊢ ( 𝐴 ∈ 𝑋 → ( 𝑁 ‘ 𝐴 ) = ( 𝐴 ( dist ‘ 𝐺 ) ( 0g ‘ 𝐺 ) ) )
14	13	adantl	⊢ ( ( 𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ) → ( 𝑁 ‘ 𝐴 ) = ( 𝐴 ( dist ‘ 𝐺 ) ( 0g ‘ 𝐺 ) ) )
15	12 14	breqtrrd	⊢ ( ( 𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ) → 0 ≤ ( 𝑁 ‘ 𝐴 ) )