qrngdiv

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

		Ref	Expression
	Hypothesis	qrng.q	$⊢ Q = ℂ_{fld} ↾_{𝑠} ℚ$
	Assertion	qrngdiv	$⊢ (X \in ℚ \land Y \in ℚ \land Y \neq 0) \to X /_{r} (Q) Y = \frac{X}{Y}$

Step	Hyp	Ref	Expression
1		qrng.q	$⊢ Q = ℂ_{fld} ↾_{𝑠} ℚ$
2		qsubdrg	$⊢ (ℚ \in SubRing (ℂ_{fld}) \land ℂ_{fld} ↾_{𝑠} ℚ \in DivRing)$
3	2	simpli	$⊢ ℚ \in SubRing (ℂ_{fld})$
4		simp1	$⊢ (X \in ℚ \land Y \in ℚ \land Y \neq 0) \to X \in ℚ$
5		3simpc	$⊢ (X \in ℚ \land Y \in ℚ \land Y \neq 0) \to (Y \in ℚ \land Y \neq 0)$
6		eldifsn	$⊢ Y \in (ℚ ∖ \{0\}) \leftrightarrow (Y \in ℚ \land Y \neq 0)$
7	5 6	sylibr	$⊢ (X \in ℚ \land Y \in ℚ \land Y \neq 0) \to Y \in (ℚ ∖ \{0\})$
8		cnflddiv	$⊢ \div = /_{r} (ℂ_{fld})$
9	1	qrngbas	$⊢ ℚ = {Base}_{Q}$
10	1	qrng0	$⊢ 0 = 0_{Q}$
11	1	qdrng	$⊢ Q \in DivRing$
12	9 10 11	drngui	$⊢ ℚ ∖ \{0\} = Unit (Q)$
13		eqid	$⊢ /_{r} (Q) = /_{r} (Q)$
14	1 8 12 13	subrgdv	$⊢ (ℚ \in SubRing (ℂ_{fld}) \land X \in ℚ \land Y \in (ℚ ∖ \{0\})) \to \frac{X}{Y} = X /_{r} (Q) Y$
15	3 4 7 14	mp3an2i	$⊢ (X \in ℚ \land Y \in ℚ \land Y \neq 0) \to \frac{X}{Y} = X /_{r} (Q) Y$
16	15	eqcomd	$⊢ (X \in ℚ \land Y \in ℚ \land Y \neq 0) \to X /_{r} (Q) Y = \frac{X}{Y}$

Metamath Proof Explorer