Theorem nm2dif

Description: Inequality for the difference of norms. (Contributed by Mario Carneiro, 6-Oct-2015)

	Ref	Expression
Hypotheses	nmf.x	⊢ 𝑋 = ( Base ‘ 𝐺 )
	nmf.n	⊢ 𝑁 = ( norm ‘ 𝐺 )
	nmmtri.m	⊢ − = ( -g ‘ 𝐺 )
Assertion	nm2dif	⊢ ( ( 𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝑁 ‘ 𝐴 ) − ( 𝑁 ‘ 𝐵 ) ) ≤ ( 𝑁 ‘ ( 𝐴 − 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		nmf.x	⊢ 𝑋 = ( Base ‘ 𝐺 )
2		nmf.n	⊢ 𝑁 = ( norm ‘ 𝐺 )
3		nmmtri.m	⊢ − = ( -g ‘ 𝐺 )
4	1 2	nmcl	⊢ ( ( 𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ) → ( 𝑁 ‘ 𝐴 ) ∈ ℝ )
5	4	3adant3	⊢ ( ( 𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝑁 ‘ 𝐴 ) ∈ ℝ )
6	1 2	nmcl	⊢ ( ( 𝐺 ∈ NrmGrp ∧ 𝐵 ∈ 𝑋 ) → ( 𝑁 ‘ 𝐵 ) ∈ ℝ )
7	6	3adant2	⊢ ( ( 𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝑁 ‘ 𝐵 ) ∈ ℝ )
8	5 7	resubcld	⊢ ( ( 𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝑁 ‘ 𝐴 ) − ( 𝑁 ‘ 𝐵 ) ) ∈ ℝ )
9	8	recnd	⊢ ( ( 𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝑁 ‘ 𝐴 ) − ( 𝑁 ‘ 𝐵 ) ) ∈ ℂ )
10	9	abscld	⊢ ( ( 𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( abs ‘ ( ( 𝑁 ‘ 𝐴 ) − ( 𝑁 ‘ 𝐵 ) ) ) ∈ ℝ )
11		simp1	⊢ ( ( 𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → 𝐺 ∈ NrmGrp )
12		ngpgrp	⊢ ( 𝐺 ∈ NrmGrp → 𝐺 ∈ Grp )
13	1 3	grpsubcl	⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 − 𝐵 ) ∈ 𝑋 )
14	12 13	syl3an1	⊢ ( ( 𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 − 𝐵 ) ∈ 𝑋 )
15	1 2	nmcl	⊢ ( ( 𝐺 ∈ NrmGrp ∧ ( 𝐴 − 𝐵 ) ∈ 𝑋 ) → ( 𝑁 ‘ ( 𝐴 − 𝐵 ) ) ∈ ℝ )
16	11 14 15	syl2anc	⊢ ( ( 𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝑁 ‘ ( 𝐴 − 𝐵 ) ) ∈ ℝ )
17	8	leabsd	⊢ ( ( 𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝑁 ‘ 𝐴 ) − ( 𝑁 ‘ 𝐵 ) ) ≤ ( abs ‘ ( ( 𝑁 ‘ 𝐴 ) − ( 𝑁 ‘ 𝐵 ) ) ) )
18	1 2 3	nmrtri	⊢ ( ( 𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( abs ‘ ( ( 𝑁 ‘ 𝐴 ) − ( 𝑁 ‘ 𝐵 ) ) ) ≤ ( 𝑁 ‘ ( 𝐴 − 𝐵 ) ) )
19	8 10 16 17 18	letrd	⊢ ( ( 𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝑁 ‘ 𝐴 ) − ( 𝑁 ‘ 𝐵 ) ) ≤ ( 𝑁 ‘ ( 𝐴 − 𝐵 ) ) )