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