Theorem qabsabv

Description: The regular absolute value function on the rationals is in fact an absolute value under our definition. (Contributed by Mario Carneiro, 9-Sep-2014)

	Ref	Expression
Hypotheses	qrng.q	$$⊢Q={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}$$
	qabsabv.a	$$⊢A=\mathrm{AbsVal}\left(Q\right)$$
Assertion	qabsabv	$$⊢{\mathrm{abs}\upharpoonright }_{\mathbb{Q}}\in A$$

Proof

Step	Hyp	Ref	Expression
1		qrng.q	$$⊢Q={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}$$
2		qabsabv.a	$$⊢A=\mathrm{AbsVal}\left(Q\right)$$
3		absabv	$$⊢\mathrm{abs}\in \mathrm{AbsVal}\left({ℂ}_{\mathrm{fld}}\right)$$
4		qsubdrg	$$⊢\left(\mathbb{Q}\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)\wedge {ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\in \mathrm{DivRing}\right)$$
5	4	simpli	$$⊢\mathbb{Q}\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)$$
6		eqid	$$⊢\mathrm{AbsVal}\left({ℂ}_{\mathrm{fld}}\right)=\mathrm{AbsVal}\left({ℂ}_{\mathrm{fld}}\right)$$
7	6 1 2	abvres	$$⊢\left(\mathrm{abs}\in \mathrm{AbsVal}\left({ℂ}_{\mathrm{fld}}\right)\wedge \mathbb{Q}\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)\right)\to {\mathrm{abs}\upharpoonright }_{\mathbb{Q}}\in A$$
8	3 5 7	mp2an	$$⊢{\mathrm{abs}\upharpoonright }_{\mathbb{Q}}\in A$$