nmmtri

Description: The triangle inequality for the norm of a subtraction. (Contributed by NM, 27-Dec-2007) (Revised by Mario Carneiro, 4-Oct-2015)

	Ref	Expression
Hypotheses	nmf.x	$⊢ X = {Base}_{G}$
	nmf.n	$⊢ N = norm (G)$
	nmmtri.m	$⊢ \underset{˙}{-} = -_{G}$
Assertion	nmmtri	$⊢ (G \in NrmGrp \land A \in X \land B \in X) \to N (A \underset{˙}{-} B) \leq N (A) + N (B)$

Proof

Step	Hyp	Ref	Expression
1		nmf.x	$⊢ X = {Base}_{G}$
2		nmf.n	$⊢ N = norm (G)$
3		nmmtri.m	$⊢ \underset{˙}{-} = -_{G}$
4		eqid	$⊢ dist (G) = dist (G)$
5	2 1 3 4	ngpds	$⊢ (G \in NrmGrp \land A \in X \land B \in X) \to A dist (G) B = N (A \underset{˙}{-} B)$
6		ngpms	$⊢ G \in NrmGrp \to G \in MetSp$
7	6	3ad2ant1	$⊢ (G \in NrmGrp \land A \in X \land B \in X) \to G \in MetSp$
8		simp2	$⊢ (G \in NrmGrp \land A \in X \land B \in X) \to A \in X$
9		simp3	$⊢ (G \in NrmGrp \land A \in X \land B \in X) \to B \in X$
10		ngpgrp	$⊢ G \in NrmGrp \to G \in Grp$
11		eqid	$⊢ 0_{G} = 0_{G}$
12	1 11	grpidcl	$⊢ G \in Grp \to 0_{G} \in X$
13	10 12	syl	$⊢ G \in NrmGrp \to 0_{G} \in X$
14	13	3ad2ant1	$⊢ (G \in NrmGrp \land A \in X \land B \in X) \to 0_{G} \in X$
15	1 4	mstri3	$⊢ (G \in MetSp \land (A \in X \land B \in X \land 0_{G} \in X)) \to A dist (G) B \leq (A dist (G) 0_{G}) + (B dist (G) 0_{G})$
16	7 8 9 14 15	syl13anc	$⊢ (G \in NrmGrp \land A \in X \land B \in X) \to A dist (G) B \leq (A dist (G) 0_{G}) + (B dist (G) 0_{G})$
17	2 1 11 4	nmval	$⊢ A \in X \to N (A) = A dist (G) 0_{G}$
18	17	3ad2ant2	$⊢ (G \in NrmGrp \land A \in X \land B \in X) \to N (A) = A dist (G) 0_{G}$
19	2 1 11 4	nmval	$⊢ B \in X \to N (B) = B dist (G) 0_{G}$
20	19	3ad2ant3	$⊢ (G \in NrmGrp \land A \in X \land B \in X) \to N (B) = B dist (G) 0_{G}$
21	18 20	oveq12d	$⊢ (G \in NrmGrp \land A \in X \land B \in X) \to N (A) + N (B) = (A dist (G) 0_{G}) + (B dist (G) 0_{G})$
22	16 21	breqtrrd	$⊢ (G \in NrmGrp \land A \in X \land B \in X) \to A dist (G) B \leq N (A) + N (B)$
23	5 22	eqbrtrrd	$⊢ (G \in NrmGrp \land A \in X \land B \in X) \to N (A \underset{˙}{-} B) \leq N (A) + N (B)$

Metamath Proof Explorer

Theorem nmmtri

Proof