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	|- X = ( Base ` G )
	nmf.n	|- N = ( norm ` G )
	nmtri.p	|- .+ = ( +g ` G )
Assertion	nmtri	|- ( ( G e. NrmGrp /\ A e. X /\ B e. X ) -> ( N ` ( A .+ B ) ) <_ ( ( N ` A ) + ( N ` B ) ) )

Proof

Step	Hyp	Ref	Expression
1		nmf.x	|- X = ( Base ` G )
2		nmf.n	|- N = ( norm ` G )
3		nmtri.p	|- .+ = ( +g ` G )
4		ngpgrp	|- ( G e. NrmGrp -> G e. Grp )
5	4	3ad2ant1	|- ( ( G e. NrmGrp /\ A e. X /\ B e. X ) -> G e. Grp )
6		simp3	|- ( ( G e. NrmGrp /\ A e. X /\ B e. X ) -> B e. X )
7		eqid	|- ( invg ` G ) = ( invg ` G )
8	1 7	grpinvcl	|- ( ( G e. Grp /\ B e. X ) -> ( ( invg ` G ) ` B ) e. X )
9	5 6 8	syl2anc	|- ( ( G e. NrmGrp /\ A e. X /\ B e. X ) -> ( ( invg ` G ) ` B ) e. X )
10		eqid	|- ( -g ` G ) = ( -g ` G )
11	1 2 10	nmmtri	|- ( ( G e. NrmGrp /\ A e. X /\ ( ( invg ` G ) ` B ) e. X ) -> ( N ` ( A ( -g ` G ) ( ( invg ` G ) ` B ) ) ) <_ ( ( N ` A ) + ( N ` ( ( invg ` G ) ` B ) ) ) )
12	9 11	syld3an3	|- ( ( G e. NrmGrp /\ A e. X /\ B e. X ) -> ( N ` ( A ( -g ` G ) ( ( invg ` G ) ` B ) ) ) <_ ( ( N ` A ) + ( N ` ( ( invg ` G ) ` B ) ) ) )
13		simp2	|- ( ( G e. NrmGrp /\ A e. X /\ B e. X ) -> A e. X )
14	1 3 10 7 5 13 6	grpsubinv	|- ( ( G e. NrmGrp /\ A e. X /\ B e. X ) -> ( A ( -g ` G ) ( ( invg ` G ) ` B ) ) = ( A .+ B ) )
15	14	fveq2d	|- ( ( G e. NrmGrp /\ A e. X /\ B e. X ) -> ( N ` ( A ( -g ` G ) ( ( invg ` G ) ` B ) ) ) = ( N ` ( A .+ B ) ) )
16	1 2 7	nminv	|- ( ( G e. NrmGrp /\ B e. X ) -> ( N ` ( ( invg ` G ) ` B ) ) = ( N ` B ) )
17	16	3adant2	|- ( ( G e. NrmGrp /\ A e. X /\ B e. X ) -> ( N ` ( ( invg ` G ) ` B ) ) = ( N ` B ) )
18	17	oveq2d	|- ( ( G e. NrmGrp /\ A e. X /\ B e. X ) -> ( ( N ` A ) + ( N ` ( ( invg ` G ) ` B ) ) ) = ( ( N ` A ) + ( N ` B ) ) )
19	12 15 18	3brtr3d	|- ( ( G e. NrmGrp /\ A e. X /\ B e. X ) -> ( N ` ( A .+ B ) ) <_ ( ( N ` A ) + ( N ` B ) ) )