nmtri2

Description: Triangle inequality for the norm of two subtractions. (Contributed by NM, 24-Feb-2008) (Revised by AV, 8-Oct-2021)

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

Proof

Step	Hyp	Ref	Expression
1		nmtri2.x	$⊢ X = {Base}_{G}$
2		nmtri2.n	$⊢ N = norm (G)$
3		nmtri2.m	$⊢ \underset{˙}{-} = -_{G}$
4		ngpgrp	$⊢ G \in NrmGrp \to G \in Grp$
5		eqid	$⊢ +_{G} = +_{G}$
6	1 5 3	grpnpncan	$⊢ (G \in Grp \land (A \in X \land B \in X \land C \in X)) \to (A \underset{˙}{-} B) +_{G} (B \underset{˙}{-} C) = A \underset{˙}{-} C$
7	6	eqcomd	$⊢ (G \in Grp \land (A \in X \land B \in X \land C \in X)) \to A \underset{˙}{-} C = (A \underset{˙}{-} B) +_{G} (B \underset{˙}{-} C)$
8	4 7	sylan	$⊢ (G \in NrmGrp \land (A \in X \land B \in X \land C \in X)) \to A \underset{˙}{-} C = (A \underset{˙}{-} B) +_{G} (B \underset{˙}{-} C)$
9	8	fveq2d	$⊢ (G \in NrmGrp \land (A \in X \land B \in X \land C \in X)) \to N (A \underset{˙}{-} C) = N ((A \underset{˙}{-} B) +_{G} (B \underset{˙}{-} C))$
10		simpl	$⊢ (G \in NrmGrp \land (A \in X \land B \in X \land C \in X)) \to G \in NrmGrp$
11	4	adantr	$⊢ (G \in NrmGrp \land (A \in X \land B \in X \land C \in X)) \to G \in Grp$
12		simpr1	$⊢ (G \in NrmGrp \land (A \in X \land B \in X \land C \in X)) \to A \in X$
13		simpr2	$⊢ (G \in NrmGrp \land (A \in X \land B \in X \land C \in X)) \to B \in X$
14	1 3	grpsubcl	$⊢ (G \in Grp \land A \in X \land B \in X) \to A \underset{˙}{-} B \in X$
15	11 12 13 14	syl3anc	$⊢ (G \in NrmGrp \land (A \in X \land B \in X \land C \in X)) \to A \underset{˙}{-} B \in X$
16		simpr3	$⊢ (G \in NrmGrp \land (A \in X \land B \in X \land C \in X)) \to C \in X$
17	1 3	grpsubcl	$⊢ (G \in Grp \land B \in X \land C \in X) \to B \underset{˙}{-} C \in X$
18	11 13 16 17	syl3anc	$⊢ (G \in NrmGrp \land (A \in X \land B \in X \land C \in X)) \to B \underset{˙}{-} C \in X$
19	1 2 5	nmtri	$⊢ (G \in NrmGrp \land A \underset{˙}{-} B \in X \land B \underset{˙}{-} C \in X) \to N ((A \underset{˙}{-} B) +_{G} (B \underset{˙}{-} C)) \leq N (A \underset{˙}{-} B) + N (B \underset{˙}{-} C)$
20	10 15 18 19	syl3anc	$⊢ (G \in NrmGrp \land (A \in X \land B \in X \land C \in X)) \to N ((A \underset{˙}{-} B) +_{G} (B \underset{˙}{-} C)) \leq N (A \underset{˙}{-} B) + N (B \underset{˙}{-} C)$
21	9 20	eqbrtrd	$⊢ (G \in NrmGrp \land (A \in X \land B \in X \land C \in X)) \to N (A \underset{˙}{-} C) \leq N (A \underset{˙}{-} B) + N (B \underset{˙}{-} C)$

Metamath Proof Explorer

Theorem nmtri2

Proof