Metamath Proof Explorer


Theorem nmtri2

Description: Triangle inequality for the norm of two subtractions. (Contributed by NM, 24-Feb-2008) (Revised by AV, 8-Oct-2021)

Ref Expression
Hypotheses nmtri2.x 𝑋 = ( Base ‘ 𝐺 )
nmtri2.n 𝑁 = ( norm ‘ 𝐺 )
nmtri2.m = ( -g𝐺 )
Assertion nmtri2 ( ( 𝐺 ∈ NrmGrp ∧ ( 𝐴𝑋𝐵𝑋𝐶𝑋 ) ) → ( 𝑁 ‘ ( 𝐴 𝐶 ) ) ≤ ( ( 𝑁 ‘ ( 𝐴 𝐵 ) ) + ( 𝑁 ‘ ( 𝐵 𝐶 ) ) ) )

Proof

Step Hyp Ref Expression
1 nmtri2.x 𝑋 = ( Base ‘ 𝐺 )
2 nmtri2.n 𝑁 = ( norm ‘ 𝐺 )
3 nmtri2.m = ( -g𝐺 )
4 ngpgrp ( 𝐺 ∈ NrmGrp → 𝐺 ∈ Grp )
5 eqid ( +g𝐺 ) = ( +g𝐺 )
6 1 5 3 grpnpncan ( ( 𝐺 ∈ Grp ∧ ( 𝐴𝑋𝐵𝑋𝐶𝑋 ) ) → ( ( 𝐴 𝐵 ) ( +g𝐺 ) ( 𝐵 𝐶 ) ) = ( 𝐴 𝐶 ) )
7 6 eqcomd ( ( 𝐺 ∈ Grp ∧ ( 𝐴𝑋𝐵𝑋𝐶𝑋 ) ) → ( 𝐴 𝐶 ) = ( ( 𝐴 𝐵 ) ( +g𝐺 ) ( 𝐵 𝐶 ) ) )
8 4 7 sylan ( ( 𝐺 ∈ NrmGrp ∧ ( 𝐴𝑋𝐵𝑋𝐶𝑋 ) ) → ( 𝐴 𝐶 ) = ( ( 𝐴 𝐵 ) ( +g𝐺 ) ( 𝐵 𝐶 ) ) )
9 8 fveq2d ( ( 𝐺 ∈ NrmGrp ∧ ( 𝐴𝑋𝐵𝑋𝐶𝑋 ) ) → ( 𝑁 ‘ ( 𝐴 𝐶 ) ) = ( 𝑁 ‘ ( ( 𝐴 𝐵 ) ( +g𝐺 ) ( 𝐵 𝐶 ) ) ) )
10 simpl ( ( 𝐺 ∈ NrmGrp ∧ ( 𝐴𝑋𝐵𝑋𝐶𝑋 ) ) → 𝐺 ∈ NrmGrp )
11 4 adantr ( ( 𝐺 ∈ NrmGrp ∧ ( 𝐴𝑋𝐵𝑋𝐶𝑋 ) ) → 𝐺 ∈ Grp )
12 simpr1 ( ( 𝐺 ∈ NrmGrp ∧ ( 𝐴𝑋𝐵𝑋𝐶𝑋 ) ) → 𝐴𝑋 )
13 simpr2 ( ( 𝐺 ∈ NrmGrp ∧ ( 𝐴𝑋𝐵𝑋𝐶𝑋 ) ) → 𝐵𝑋 )
14 1 3 grpsubcl ( ( 𝐺 ∈ Grp ∧ 𝐴𝑋𝐵𝑋 ) → ( 𝐴 𝐵 ) ∈ 𝑋 )
15 11 12 13 14 syl3anc ( ( 𝐺 ∈ NrmGrp ∧ ( 𝐴𝑋𝐵𝑋𝐶𝑋 ) ) → ( 𝐴 𝐵 ) ∈ 𝑋 )
16 simpr3 ( ( 𝐺 ∈ NrmGrp ∧ ( 𝐴𝑋𝐵𝑋𝐶𝑋 ) ) → 𝐶𝑋 )
17 1 3 grpsubcl ( ( 𝐺 ∈ Grp ∧ 𝐵𝑋𝐶𝑋 ) → ( 𝐵 𝐶 ) ∈ 𝑋 )
18 11 13 16 17 syl3anc ( ( 𝐺 ∈ NrmGrp ∧ ( 𝐴𝑋𝐵𝑋𝐶𝑋 ) ) → ( 𝐵 𝐶 ) ∈ 𝑋 )
19 1 2 5 nmtri ( ( 𝐺 ∈ NrmGrp ∧ ( 𝐴 𝐵 ) ∈ 𝑋 ∧ ( 𝐵 𝐶 ) ∈ 𝑋 ) → ( 𝑁 ‘ ( ( 𝐴 𝐵 ) ( +g𝐺 ) ( 𝐵 𝐶 ) ) ) ≤ ( ( 𝑁 ‘ ( 𝐴 𝐵 ) ) + ( 𝑁 ‘ ( 𝐵 𝐶 ) ) ) )
20 10 15 18 19 syl3anc ( ( 𝐺 ∈ NrmGrp ∧ ( 𝐴𝑋𝐵𝑋𝐶𝑋 ) ) → ( 𝑁 ‘ ( ( 𝐴 𝐵 ) ( +g𝐺 ) ( 𝐵 𝐶 ) ) ) ≤ ( ( 𝑁 ‘ ( 𝐴 𝐵 ) ) + ( 𝑁 ‘ ( 𝐵 𝐶 ) ) ) )
21 9 20 eqbrtrd ( ( 𝐺 ∈ NrmGrp ∧ ( 𝐴𝑋𝐵𝑋𝐶𝑋 ) ) → ( 𝑁 ‘ ( 𝐴 𝐶 ) ) ≤ ( ( 𝑁 ‘ ( 𝐴 𝐵 ) ) + ( 𝑁 ‘ ( 𝐵 𝐶 ) ) ) )