Theorem qrng1

Description: The unit element of the field of rationals. (Contributed by Mario Carneiro, 8-Sep-2014)

	Ref	Expression
Hypothesis	qrng.q	⊢ 𝑄 = ( ℂfld ↾s ℚ )
Assertion	qrng1	⊢ 1 = ( 1r ‘ 𝑄 )

Proof

Step	Hyp	Ref	Expression
1		qrng.q	⊢ 𝑄 = ( ℂfld ↾s ℚ )
2		qsubdrg	⊢ ( ℚ ∈ ( SubRing ‘ ℂfld ) ∧ ( ℂfld ↾s ℚ ) ∈ DivRing )
3	2	simpli	⊢ ℚ ∈ ( SubRing ‘ ℂfld )
4		cnfld1	⊢ 1 = ( 1r ‘ ℂfld )
5	1 4	subrg1	⊢ ( ℚ ∈ ( SubRing ‘ ℂfld ) → 1 = ( 1r ‘ 𝑄 ) )
6	3 5	ax-mp	⊢ 1 = ( 1r ‘ 𝑄 )