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	$⊢ \underset{˙}{+} = +_{G}$
Assertion	nmtri	$⊢ (G \in NrmGrp \land A \in X \land B \in X) \to N (A \underset{˙}{+} B) \leq N (A) + N (B)$

Step	Hyp	Ref	Expression
1		nmf.x	$⊢ X = {Base}_{G}$
2		nmf.n	$⊢ N = norm (G)$
3		nmtri.p	$⊢ \underset{˙}{+} = +_{G}$
4		ngpgrp	$⊢ G \in NrmGrp \to G \in Grp$
5	4	3ad2ant1	$⊢ (G \in NrmGrp \land A \in X \land B \in X) \to G \in Grp$
6		simp3	$⊢ (G \in NrmGrp \land A \in X \land B \in X) \to B \in X$
7		eqid	$⊢ {inv}_{g} (G) = {inv}_{g} (G)$
8	1 7	grpinvcl	$⊢ (G \in Grp \land B \in X) \to {inv}_{g} (G) (B) \in X$
9	5 6 8	syl2anc	$⊢ (G \in NrmGrp \land A \in X \land B \in X) \to {inv}_{g} (G) (B) \in X$
10		eqid	$⊢ -_{G} = -_{G}$
11	1 2 10	nmmtri	$⊢ (G \in NrmGrp \land A \in X \land {inv}_{g} (G) (B) \in X) \to N (A -_{G} {inv}_{g} (G) (B)) \leq N (A) + N ({inv}_{g} (G) (B))$
12	9 11	syld3an3	$⊢ (G \in NrmGrp \land A \in X \land B \in X) \to N (A -_{G} {inv}_{g} (G) (B)) \leq N (A) + N ({inv}_{g} (G) (B))$
13		simp2	$⊢ (G \in NrmGrp \land A \in X \land B \in X) \to A \in X$
14	1 3 10 7 5 13 6	grpsubinv	$⊢ (G \in NrmGrp \land A \in X \land B \in X) \to A -_{G} {inv}_{g} (G) (B) = A \underset{˙}{+} B$
15	14	fveq2d	$⊢ (G \in NrmGrp \land A \in X \land B \in X) \to N (A -_{G} {inv}_{g} (G) (B)) = N (A \underset{˙}{+} B)$
16	1 2 7	nminv	$⊢ (G \in NrmGrp \land B \in X) \to N ({inv}_{g} (G) (B)) = N (B)$
17	16	3adant2	$⊢ (G \in NrmGrp \land A \in X \land B \in X) \to N ({inv}_{g} (G) (B)) = N (B)$
18	17	oveq2d	$⊢ (G \in NrmGrp \land A \in X \land B \in X) \to N (A) + N ({inv}_{g} (G) (B)) = N (A) + N (B)$
19	12 15 18	3brtr3d	$⊢ (G \in NrmGrp \land A \in X \land B \in X) \to N (A \underset{˙}{+} B) \leq N (A) + N (B)$

Metamath Proof Explorer