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

Metamath Proof Explorer

Theorem nm2dif

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

Ref Expression
Hypotheses nmf.x 
|- X = ( Base ` G )
nmf.n 
|- N = ( norm ` G )
nmmtri.m 
|- .- = ( -g ` G )
Assertion nm2dif 
|- ( ( G e. NrmGrp /\ A e. X /\ B e. X ) -> ( ( N ` A ) - ( N ` B ) ) <_ ( N ` ( A .- B ) ) )

Proof

Step Hyp Ref Expression
1 nmf.x 
 |-  X = ( Base ` G )
2 nmf.n 
 |-  N = ( norm ` G )
3 nmmtri.m 
 |-  .- = ( -g ` G )
4 1 2 nmcl 
 |-  ( ( G e. NrmGrp /\ A e. X ) -> ( N ` A ) e. RR )
5 4 3adant3 
 |-  ( ( G e. NrmGrp /\ A e. X /\ B e. X ) -> ( N ` A ) e. RR )
6 1 2 nmcl 
 |-  ( ( G e. NrmGrp /\ B e. X ) -> ( N ` B ) e. RR )
7 6 3adant2 
 |-  ( ( G e. NrmGrp /\ A e. X /\ B e. X ) -> ( N ` B ) e. RR )
8 5 7 resubcld 
 |-  ( ( G e. NrmGrp /\ A e. X /\ B e. X ) -> ( ( N ` A ) - ( N ` B ) ) e. RR )
9 8 recnd 
 |-  ( ( G e. NrmGrp /\ A e. X /\ B e. X ) -> ( ( N ` A ) - ( N ` B ) ) e. CC )
10 9 abscld 
 |-  ( ( G e. NrmGrp /\ A e. X /\ B e. X ) -> ( abs ` ( ( N ` A ) - ( N ` B ) ) ) e. RR )
11 simp1 
 |-  ( ( G e. NrmGrp /\ A e. X /\ B e. X ) -> G e. NrmGrp )
12 ngpgrp 
 |-  ( G e. NrmGrp -> G e. Grp )
13 1 3 grpsubcl 
 |-  ( ( G e. Grp /\ A e. X /\ B e. X ) -> ( A .- B ) e. X )
14 12 13 syl3an1 
 |-  ( ( G e. NrmGrp /\ A e. X /\ B e. X ) -> ( A .- B ) e. X )
15 1 2 nmcl 
 |-  ( ( G e. NrmGrp /\ ( A .- B ) e. X ) -> ( N ` ( A .- B ) ) e. RR )
16 11 14 15 syl2anc 
 |-  ( ( G e. NrmGrp /\ A e. X /\ B e. X ) -> ( N ` ( A .- B ) ) e. RR )
17 8 leabsd 
 |-  ( ( G e. NrmGrp /\ A e. X /\ B e. X ) -> ( ( N ` A ) - ( N ` B ) ) <_ ( abs ` ( ( N ` A ) - ( N ` B ) ) ) )
18 1 2 3 nmrtri 
 |-  ( ( G e. NrmGrp /\ A e. X /\ B e. X ) -> ( abs ` ( ( N ` A ) - ( N ` B ) ) ) <_ ( N ` ( A .- B ) ) )
19 8 10 16 17 18 letrd 
 |-  ( ( G e. NrmGrp /\ A e. X /\ B e. X ) -> ( ( N ` A ) - ( N ` B ) ) <_ ( N ` ( A .- B ) ) )