Theorem nmtri

Description: The triangle inequality for the norm of a sum. (Contributed by NM, 11-Nov-2006) (Revised by Mario Carneiro, 4-Oct-2015)

	Ref	Expression
Hypotheses	nmf.x	⊢ 𝑋 = ( Base ‘ 𝐺 )
	nmf.n	⊢ 𝑁 = ( norm ‘ 𝐺 )
	nmtri.p	⊢ + = ( +g ‘ 𝐺 )
Assertion	nmtri	⊢ ( ( 𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝑁 ‘ ( 𝐴 + 𝐵 ) ) ≤ ( ( 𝑁 ‘ 𝐴 ) + ( 𝑁 ‘ 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		nmf.x	⊢ 𝑋 = ( Base ‘ 𝐺 )
2		nmf.n	⊢ 𝑁 = ( norm ‘ 𝐺 )
3		nmtri.p	⊢ + = ( +g ‘ 𝐺 )
4		ngpgrp	⊢ ( 𝐺 ∈ NrmGrp → 𝐺 ∈ Grp )
5	4	3ad2ant1	⊢ ( ( 𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → 𝐺 ∈ Grp )
6		simp3	⊢ ( ( 𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → 𝐵 ∈ 𝑋 )
7		eqid	⊢ ( invg ‘ 𝐺 ) = ( invg ‘ 𝐺 )
8	1 7	grpinvcl	⊢ ( ( 𝐺 ∈ Grp ∧ 𝐵 ∈ 𝑋 ) → ( ( invg ‘ 𝐺 ) ‘ 𝐵 ) ∈ 𝑋 )
9	5 6 8	syl2anc	⊢ ( ( 𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( invg ‘ 𝐺 ) ‘ 𝐵 ) ∈ 𝑋 )
10		eqid	⊢ ( -g ‘ 𝐺 ) = ( -g ‘ 𝐺 )
11	1 2 10	nmmtri	⊢ ( ( 𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ ( ( invg ‘ 𝐺 ) ‘ 𝐵 ) ∈ 𝑋 ) → ( 𝑁 ‘ ( 𝐴 ( -g ‘ 𝐺 ) ( ( invg ‘ 𝐺 ) ‘ 𝐵 ) ) ) ≤ ( ( 𝑁 ‘ 𝐴 ) + ( 𝑁 ‘ ( ( invg ‘ 𝐺 ) ‘ 𝐵 ) ) ) )
12	9 11	syld3an3	⊢ ( ( 𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝑁 ‘ ( 𝐴 ( -g ‘ 𝐺 ) ( ( invg ‘ 𝐺 ) ‘ 𝐵 ) ) ) ≤ ( ( 𝑁 ‘ 𝐴 ) + ( 𝑁 ‘ ( ( invg ‘ 𝐺 ) ‘ 𝐵 ) ) ) )
13		simp2	⊢ ( ( 𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → 𝐴 ∈ 𝑋 )
14	1 3 10 7 5 13 6	grpsubinv	⊢ ( ( 𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 ( -g ‘ 𝐺 ) ( ( invg ‘ 𝐺 ) ‘ 𝐵 ) ) = ( 𝐴 + 𝐵 ) )
15	14	fveq2d	⊢ ( ( 𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝑁 ‘ ( 𝐴 ( -g ‘ 𝐺 ) ( ( invg ‘ 𝐺 ) ‘ 𝐵 ) ) ) = ( 𝑁 ‘ ( 𝐴 + 𝐵 ) ) )
16	1 2 7	nminv	⊢ ( ( 𝐺 ∈ NrmGrp ∧ 𝐵 ∈ 𝑋 ) → ( 𝑁 ‘ ( ( invg ‘ 𝐺 ) ‘ 𝐵 ) ) = ( 𝑁 ‘ 𝐵 ) )
17	16	3adant2	⊢ ( ( 𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝑁 ‘ ( ( invg ‘ 𝐺 ) ‘ 𝐵 ) ) = ( 𝑁 ‘ 𝐵 ) )
18	17	oveq2d	⊢ ( ( 𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝑁 ‘ 𝐴 ) + ( 𝑁 ‘ ( ( invg ‘ 𝐺 ) ‘ 𝐵 ) ) ) = ( ( 𝑁 ‘ 𝐴 ) + ( 𝑁 ‘ 𝐵 ) ) )
19	12 15 18	3brtr3d	⊢ ( ( 𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝑁 ‘ ( 𝐴 + 𝐵 ) ) ≤ ( ( 𝑁 ‘ 𝐴 ) + ( 𝑁 ‘ 𝐵 ) ) )