This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝑁 ‘ ( 𝐴 + 𝐵 ) ) ≤ ( ( 𝑁 ‘ 𝐴 ) + ( 𝑁 ‘ 𝐵 ) ) )