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 ) ) )