Theorem qdrng

Description: The rationals form a division ring. (Contributed by Mario Carneiro, 8-Sep-2014)

	Ref	Expression
Hypothesis	qrng.q	⊢ 𝑄 = ( ℂfld ↾s ℚ )
Assertion	qdrng	⊢ 𝑄 ∈ DivRing

Proof

Step	Hyp	Ref	Expression
1		qrng.q	⊢ 𝑄 = ( ℂfld ↾s ℚ )
2		qsubdrg	⊢ ( ℚ ∈ ( SubRing ‘ ℂfld ) ∧ ( ℂfld ↾s ℚ ) ∈ DivRing )
3	2	simpri	⊢ ( ℂfld ↾s ℚ ) ∈ DivRing
4	1 3	eqeltri	⊢ 𝑄 ∈ DivRing