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

Step	Hyp	Ref	Expression
1		nmf.x	$⊢ X = {Base}_{G}$
2		nmf.n	$⊢ N = norm (G)$
3		nmmtri.m	$⊢ \underset{˙}{-} = -_{G}$
4	1 2	nmcl	$⊢ (G \in NrmGrp \land A \in X) \to N (A) \in ℝ$
5	4	3adant3	$⊢ (G \in NrmGrp \land A \in X \land B \in X) \to N (A) \in ℝ$
6	1 2	nmcl	$⊢ (G \in NrmGrp \land B \in X) \to N (B) \in ℝ$
7	6	3adant2	$⊢ (G \in NrmGrp \land A \in X \land B \in X) \to N (B) \in ℝ$
8	5 7	resubcld	$⊢ (G \in NrmGrp \land A \in X \land B \in X) \to N (A) - N (B) \in ℝ$
9	8	recnd	$⊢ (G \in NrmGrp \land A \in X \land B \in X) \to N (A) - N (B) \in ℂ$
10	9	abscld	$⊢ (G \in NrmGrp \land A \in X \land B \in X) \to \|N (A) - N (B)\| \in ℝ$
11		simp1	$⊢ (G \in NrmGrp \land A \in X \land B \in X) \to G \in NrmGrp$
12		ngpgrp	$⊢ G \in NrmGrp \to G \in Grp$
13	1 3	grpsubcl	$⊢ (G \in Grp \land A \in X \land B \in X) \to A \underset{˙}{-} B \in X$
14	12 13	syl3an1	$⊢ (G \in NrmGrp \land A \in X \land B \in X) \to A \underset{˙}{-} B \in X$
15	1 2	nmcl	$⊢ (G \in NrmGrp \land A \underset{˙}{-} B \in X) \to N (A \underset{˙}{-} B) \in ℝ$
16	11 14 15	syl2anc	$⊢ (G \in NrmGrp \land A \in X \land B \in X) \to N (A \underset{˙}{-} B) \in ℝ$
17	8	leabsd	$⊢ (G \in NrmGrp \land A \in X \land B \in X) \to N (A) - N (B) \leq \|N (A) - N (B)\|$
18	1 2 3	nmrtri	$⊢ (G \in NrmGrp \land A \in X \land B \in X) \to \|N (A) - N (B)\| \leq N (A \underset{˙}{-} B)$
19	8 10 16 17 18	letrd	$⊢ (G \in NrmGrp \land A \in X \land B \in X) \to N (A) - N (B) \leq N (A \underset{˙}{-} B)$

Metamath Proof Explorer