nvtri

Description: Triangle inequality for the norm of a normed complex vector space. (Contributed by NM, 11-Nov-2006) (Revised by Mario Carneiro, 21-Dec-2013) (New usage is discouraged.)

	Ref	Expression
Hypotheses	nvtri.1	$⊢ X = BaseSet (U)$
	nvtri.2	$⊢ G = +_{v} (U)$
	nvtri.6	$⊢ N = {norm}_{CV} (U)$
Assertion	nvtri	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to N (A G B) \leq N (A) + N (B)$

Proof

Step	Hyp	Ref	Expression
1		nvtri.1	$⊢ X = BaseSet (U)$
2		nvtri.2	$⊢ G = +_{v} (U)$
3		nvtri.6	$⊢ N = {norm}_{CV} (U)$
4		eqid	$⊢ \cdot_{𝑠OLD} (U) = \cdot_{𝑠OLD} (U)$
5	4	smfval	$⊢ \cdot_{𝑠OLD} (U) = 2^{nd} (1^{st} (U))$
6	5	eqcomi	$⊢ 2^{nd} (1^{st} (U)) = \cdot_{𝑠OLD} (U)$
7		eqid	$⊢ 0_{vec} (U) = 0_{vec} (U)$
8	1 2 6 7 3	nvi	$⊢ U \in NrmCVec \to (⟨G, 2^{nd} (1^{st} (U))⟩ \in {CVec}_{OLD} \land N : X ⟶ ℝ \land \forall x \in X ((N (x) = 0 \to x = 0_{vec} (U)) \land \forall y \in ℂ N (y 2^{nd} (1^{st} (U)) x) = \|y\| N (x) \land \forall y \in X N (x G y) \leq N (x) + N (y)))$
9	8	simp3d	$⊢ U \in NrmCVec \to \forall x \in X ((N (x) = 0 \to x = 0_{vec} (U)) \land \forall y \in ℂ N (y 2^{nd} (1^{st} (U)) x) = \|y\| N (x) \land \forall y \in X N (x G y) \leq N (x) + N (y))$
10		simp3	$⊢ ((N (x) = 0 \to x = 0_{vec} (U)) \land \forall y \in ℂ N (y 2^{nd} (1^{st} (U)) x) = \|y\| N (x) \land \forall y \in X N (x G y) \leq N (x) + N (y)) \to \forall y \in X N (x G y) \leq N (x) + N (y)$
11	10	ralimi	$⊢ \forall x \in X ((N (x) = 0 \to x = 0_{vec} (U)) \land \forall y \in ℂ N (y 2^{nd} (1^{st} (U)) x) = \|y\| N (x) \land \forall y \in X N (x G y) \leq N (x) + N (y)) \to \forall x \in X \forall y \in X N (x G y) \leq N (x) + N (y)$
12	9 11	syl	$⊢ U \in NrmCVec \to \forall x \in X \forall y \in X N (x G y) \leq N (x) + N (y)$
13		fvoveq1	$⊢ x = A \to N (x G y) = N (A G y)$
14		fveq2	$⊢ x = A \to N (x) = N (A)$
15	14	oveq1d	$⊢ x = A \to N (x) + N (y) = N (A) + N (y)$
16	13 15	breq12d	$⊢ x = A \to (N (x G y) \leq N (x) + N (y) \leftrightarrow N (A G y) \leq N (A) + N (y))$
17		oveq2	$⊢ y = B \to A G y = A G B$
18	17	fveq2d	$⊢ y = B \to N (A G y) = N (A G B)$
19		fveq2	$⊢ y = B \to N (y) = N (B)$
20	19	oveq2d	$⊢ y = B \to N (A) + N (y) = N (A) + N (B)$
21	18 20	breq12d	$⊢ y = B \to (N (A G y) \leq N (A) + N (y) \leftrightarrow N (A G B) \leq N (A) + N (B))$
22	16 21	rspc2v	$⊢ (A \in X \land B \in X) \to (\forall x \in X \forall y \in X N (x G y) \leq N (x) + N (y) \to N (A G B) \leq N (A) + N (B))$
23	12 22	syl5	$⊢ (A \in X \land B \in X) \to (U \in NrmCVec \to N (A G B) \leq N (A) + N (B))$
24	23	3impia	$⊢ (A \in X \land B \in X \land U \in NrmCVec) \to N (A G B) \leq N (A) + N (B)$
25	24	3comr	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to N (A G B) \leq N (A) + N (B)$

Metamath Proof Explorer

Theorem nvtri

Proof