absabv

Description: The regular absolute value function on the complex numbers is in fact an absolute value under our definition. (Contributed by Mario Carneiro, 4-Dec-2014)

		Ref	Expression
	Assertion	absabv	$⊢ abs \in AbsVal (ℂ_{fld})$

Proof

Step	Hyp	Ref	Expression
1		eqidd	$⊢ ⊤ \to AbsVal (ℂ_{fld}) = AbsVal (ℂ_{fld})$
2		cnfldbas	$⊢ ℂ = {Base}_{ℂ_{fld}}$
3	2	a1i	$⊢ ⊤ \to ℂ = {Base}_{ℂ_{fld}}$
4		cnfldadd	$⊢ + = +_{ℂ_{fld}}$
5	4	a1i	$⊢ ⊤ \to + = +_{ℂ_{fld}}$
6		cnfldmul	$⊢ \times = \cdot_{ℂ_{fld}}$
7	6	a1i	$⊢ ⊤ \to \times = \cdot_{ℂ_{fld}}$
8		cnfld0	$⊢ 0 = 0_{ℂ_{fld}}$
9	8	a1i	$⊢ ⊤ \to 0 = 0_{ℂ_{fld}}$
10		cnring	$⊢ ℂ_{fld} \in Ring$
11	10	a1i	$⊢ ⊤ \to ℂ_{fld} \in Ring$
12		absf	$⊢ abs : ℂ ⟶ ℝ$
13	12	a1i	$⊢ ⊤ \to abs : ℂ ⟶ ℝ$
14		abs0	$⊢ \|0\| = 0$
15	14	a1i	$⊢ ⊤ \to \|0\| = 0$
16		absgt0	$⊢ x \in ℂ \to (x \neq 0 \leftrightarrow 0 < \|x\|)$
17	16	biimpa	$⊢ (x \in ℂ \land x \neq 0) \to 0 < \|x\|$
18	17	3adant1	$⊢ (⊤ \land x \in ℂ \land x \neq 0) \to 0 < \|x\|$
19		absmul	$⊢ (x \in ℂ \land y \in ℂ) \to \|x y\| = \|x\| \|y\|$
20	19	ad2ant2r	$⊢ ((x \in ℂ \land x \neq 0) \land (y \in ℂ \land y \neq 0)) \to \|x y\| = \|x\| \|y\|$
21	20	3adant1	$⊢ (⊤ \land (x \in ℂ \land x \neq 0) \land (y \in ℂ \land y \neq 0)) \to \|x y\| = \|x\| \|y\|$
22		abstri	$⊢ (x \in ℂ \land y \in ℂ) \to \|x + y\| \leq \|x\| + \|y\|$
23	22	ad2ant2r	$⊢ ((x \in ℂ \land x \neq 0) \land (y \in ℂ \land y \neq 0)) \to \|x + y\| \leq \|x\| + \|y\|$
24	23	3adant1	$⊢ (⊤ \land (x \in ℂ \land x \neq 0) \land (y \in ℂ \land y \neq 0)) \to \|x + y\| \leq \|x\| + \|y\|$
25	1 3 5 7 9 11 13 15 18 21 24	isabvd	$⊢ ⊤ \to abs \in AbsVal (ℂ_{fld})$
26	25	mptru	$⊢ abs \in AbsVal (ℂ_{fld})$

Metamath Proof Explorer

Theorem absabv

Proof