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	⊢ 𝑄 = ( ℂfld ↾s ℚ )
	qabsabv.a	⊢ 𝐴 = ( AbsVal ‘ 𝑄 )
Assertion	qabsabv	⊢ ( abs ↾ ℚ ) ∈ 𝐴

Proof

Step	Hyp	Ref	Expression
1		qrng.q	⊢ 𝑄 = ( ℂfld ↾s ℚ )
2		qabsabv.a	⊢ 𝐴 = ( AbsVal ‘ 𝑄 )
3		absabv	⊢ abs ∈ ( AbsVal ‘ ℂfld )
4		qsubdrg	⊢ ( ℚ ∈ ( SubRing ‘ ℂfld ) ∧ ( ℂfld ↾s ℚ ) ∈ DivRing )
5	4	simpli	⊢ ℚ ∈ ( SubRing ‘ ℂfld )
6		eqid	⊢ ( AbsVal ‘ ℂfld ) = ( AbsVal ‘ ℂfld )
7	6 1 2	abvres	⊢ ( ( abs ∈ ( AbsVal ‘ ℂfld ) ∧ ℚ ∈ ( SubRing ‘ ℂfld ) ) → ( abs ↾ ℚ ) ∈ 𝐴 )
8	3 5 7	mp2an	⊢ ( abs ↾ ℚ ) ∈ 𝐴