Theorem qrngdiv

Description: The division operation in the field of rationals. (Contributed by Mario Carneiro, 8-Sep-2014)

	Ref	Expression
Hypothesis	qrng.q	$$⊢Q={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}$$
Assertion	qrngdiv	$$⊢\left(X\in \mathbb{Q}\wedge Y\in \mathbb{Q}\wedge Y\ne 0\right)\to X{/}_r\left(Q\right)Y=\frac{X}{Y}$$

Proof

Step	Hyp	Ref	Expression
1		qrng.q	$$⊢Q={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}$$
2		qsubdrg	$$⊢\left(\mathbb{Q}\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)\wedge {ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\in \mathrm{DivRing}\right)$$
3	2	simpli	$$⊢\mathbb{Q}\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)$$
4		simp1	$$⊢\left(X\in \mathbb{Q}\wedge Y\in \mathbb{Q}\wedge Y\ne 0\right)\to X\in \mathbb{Q}$$
5		3simpc	$$⊢\left(X\in \mathbb{Q}\wedge Y\in \mathbb{Q}\wedge Y\ne 0\right)\to \left(Y\in \mathbb{Q}\wedge Y\ne 0\right)$$
6		eldifsn	$$⊢Y\in \left(\mathbb{Q}\setminus \left\{0\right\}\right)\leftrightarrow \left(Y\in \mathbb{Q}\wedge Y\ne 0\right)$$
7	5 6	sylibr	$$⊢\left(X\in \mathbb{Q}\wedge Y\in \mathbb{Q}\wedge Y\ne 0\right)\to Y\in \left(\mathbb{Q}\setminus \left\{0\right\}\right)$$
8		cnflddiv	$$⊢÷={/}_r\left({ℂ}_{\mathrm{fld}}\right)$$
9	1	qrngbas	$$⊢\mathbb{Q}={\mathrm{Base}}_Q$$
10	1	qrng0	$$⊢0=0_Q$$
11	1	qdrng	$$⊢Q\in \mathrm{DivRing}$$
12	9 10 11	drngui	$$⊢\mathbb{Q}\setminus \left\{0\right\}=\mathrm{Unit}\left(Q\right)$$
13		eqid	$$⊢{/}_r\left(Q\right)={/}_r\left(Q\right)$$
14	1 8 12 13	subrgdv	$$⊢\left(\mathbb{Q}\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)\wedge X\in \mathbb{Q}\wedge Y\in \left(\mathbb{Q}\setminus \left\{0\right\}\right)\right)\to \frac{X}{Y}=X{/}_r\left(Q\right)Y$$
15	3 4 7 14	mp3an2i	$$⊢\left(X\in \mathbb{Q}\wedge Y\in \mathbb{Q}\wedge Y\ne 0\right)\to \frac{X}{Y}=X{/}_r\left(Q\right)Y$$
16	15	eqcomd	$$⊢\left(X\in \mathbb{Q}\wedge Y\in \mathbb{Q}\wedge Y\ne 0\right)\to X{/}_r\left(Q\right)Y=\frac{X}{Y}$$