abvsubtri

Description: An absolute value satisfies the triangle inequality. (Contributed by Mario Carneiro, 4-Oct-2015)

	Ref	Expression
Hypotheses	abv0.a	$⊢ A = AbsVal (R)$
	abvneg.b	$⊢ B = {Base}_{R}$
	abvsubtri.p	$⊢ \underset{˙}{-} = -_{R}$
Assertion	abvsubtri	$⊢ (F \in A \land X \in B \land Y \in B) \to F (X \underset{˙}{-} Y) \leq F (X) + F (Y)$

Proof

Step	Hyp	Ref	Expression
1		abv0.a	$⊢ A = AbsVal (R)$
2		abvneg.b	$⊢ B = {Base}_{R}$
3		abvsubtri.p	$⊢ \underset{˙}{-} = -_{R}$
4		eqid	$⊢ +_{R} = +_{R}$
5		eqid	$⊢ {inv}_{g} (R) = {inv}_{g} (R)$
6	2 4 5 3	grpsubval	$⊢ (X \in B \land Y \in B) \to X \underset{˙}{-} Y = X +_{R} {inv}_{g} (R) (Y)$
7	6	3adant1	$⊢ (F \in A \land X \in B \land Y \in B) \to X \underset{˙}{-} Y = X +_{R} {inv}_{g} (R) (Y)$
8	7	fveq2d	$⊢ (F \in A \land X \in B \land Y \in B) \to F (X \underset{˙}{-} Y) = F (X +_{R} {inv}_{g} (R) (Y))$
9	1	abvrcl	$⊢ F \in A \to R \in Ring$
10	9	3ad2ant1	$⊢ (F \in A \land X \in B \land Y \in B) \to R \in Ring$
11		ringgrp	$⊢ R \in Ring \to R \in Grp$
12	10 11	syl	$⊢ (F \in A \land X \in B \land Y \in B) \to R \in Grp$
13		simp3	$⊢ (F \in A \land X \in B \land Y \in B) \to Y \in B$
14	2 5	grpinvcl	$⊢ (R \in Grp \land Y \in B) \to {inv}_{g} (R) (Y) \in B$
15	12 13 14	syl2anc	$⊢ (F \in A \land X \in B \land Y \in B) \to {inv}_{g} (R) (Y) \in B$
16	1 2 4	abvtri	$⊢ (F \in A \land X \in B \land {inv}_{g} (R) (Y) \in B) \to F (X +_{R} {inv}_{g} (R) (Y)) \leq F (X) + F ({inv}_{g} (R) (Y))$
17	15 16	syld3an3	$⊢ (F \in A \land X \in B \land Y \in B) \to F (X +_{R} {inv}_{g} (R) (Y)) \leq F (X) + F ({inv}_{g} (R) (Y))$
18	1 2 5	abvneg	$⊢ (F \in A \land Y \in B) \to F ({inv}_{g} (R) (Y)) = F (Y)$
19	18	3adant2	$⊢ (F \in A \land X \in B \land Y \in B) \to F ({inv}_{g} (R) (Y)) = F (Y)$
20	19	oveq2d	$⊢ (F \in A \land X \in B \land Y \in B) \to F (X) + F ({inv}_{g} (R) (Y)) = F (X) + F (Y)$
21	17 20	breqtrd	$⊢ (F \in A \land X \in B \land Y \in B) \to F (X +_{R} {inv}_{g} (R) (Y)) \leq F (X) + F (Y)$
22	8 21	eqbrtrd	$⊢ (F \in A \land X \in B \land Y \in B) \to F (X \underset{˙}{-} Y) \leq F (X) + F (Y)$

Metamath Proof Explorer

Theorem abvsubtri

Proof