qsssubdrg

Description: The rational numbers are a subset of any subfield of the complex numbers. (Contributed by Mario Carneiro, 15-Oct-2015)

		Ref	Expression
	Assertion	qsssubdrg	$⊢ (R \in SubRing (ℂ_{fld}) \land ℂ_{fld} ↾_{𝑠} R \in DivRing) \to ℚ \subseteq R$

Proof

Step	Hyp	Ref	Expression
1		elq	$⊢ z \in ℚ \leftrightarrow \exists x \in ℤ \exists y \in ℕ z = \frac{x}{y}$
2		drngring	$⊢ ℂ_{fld} ↾_{𝑠} R \in DivRing \to ℂ_{fld} ↾_{𝑠} R \in Ring$
3	2	ad2antlr	$⊢ ((R \in SubRing (ℂ_{fld}) \land ℂ_{fld} ↾_{𝑠} R \in DivRing) \land (x \in ℤ \land y \in ℕ)) \to ℂ_{fld} ↾_{𝑠} R \in Ring$
4		zsssubrg	$⊢ R \in SubRing (ℂ_{fld}) \to ℤ \subseteq R$
5	4	ad2antrr	$⊢ ((R \in SubRing (ℂ_{fld}) \land ℂ_{fld} ↾_{𝑠} R \in DivRing) \land (x \in ℤ \land y \in ℕ)) \to ℤ \subseteq R$
6		eqid	$⊢ ℂ_{fld} ↾_{𝑠} R = ℂ_{fld} ↾_{𝑠} R$
7	6	subrgbas	$⊢ R \in SubRing (ℂ_{fld}) \to R = {Base}_{(ℂ_{fld} ↾_{𝑠} R)}$
8	7	ad2antrr	$⊢ ((R \in SubRing (ℂ_{fld}) \land ℂ_{fld} ↾_{𝑠} R \in DivRing) \land (x \in ℤ \land y \in ℕ)) \to R = {Base}_{(ℂ_{fld} ↾_{𝑠} R)}$
9	5 8	sseqtrd	$⊢ ((R \in SubRing (ℂ_{fld}) \land ℂ_{fld} ↾_{𝑠} R \in DivRing) \land (x \in ℤ \land y \in ℕ)) \to ℤ \subseteq {Base}_{(ℂ_{fld} ↾_{𝑠} R)}$
10		simprl	$⊢ ((R \in SubRing (ℂ_{fld}) \land ℂ_{fld} ↾_{𝑠} R \in DivRing) \land (x \in ℤ \land y \in ℕ)) \to x \in ℤ$
11	9 10	sseldd	$⊢ ((R \in SubRing (ℂ_{fld}) \land ℂ_{fld} ↾_{𝑠} R \in DivRing) \land (x \in ℤ \land y \in ℕ)) \to x \in {Base}_{(ℂ_{fld} ↾_{𝑠} R)}$
12		nnz	$⊢ y \in ℕ \to y \in ℤ$
13	12	ad2antll	$⊢ ((R \in SubRing (ℂ_{fld}) \land ℂ_{fld} ↾_{𝑠} R \in DivRing) \land (x \in ℤ \land y \in ℕ)) \to y \in ℤ$
14	9 13	sseldd	$⊢ ((R \in SubRing (ℂ_{fld}) \land ℂ_{fld} ↾_{𝑠} R \in DivRing) \land (x \in ℤ \land y \in ℕ)) \to y \in {Base}_{(ℂ_{fld} ↾_{𝑠} R)}$
15		nnne0	$⊢ y \in ℕ \to y \neq 0$
16	15	ad2antll	$⊢ ((R \in SubRing (ℂ_{fld}) \land ℂ_{fld} ↾_{𝑠} R \in DivRing) \land (x \in ℤ \land y \in ℕ)) \to y \neq 0$
17		cnfld0	$⊢ 0 = 0_{ℂ_{fld}}$
18	6 17	subrg0	$⊢ R \in SubRing (ℂ_{fld}) \to 0 = 0_{(ℂ_{fld} ↾_{𝑠} R)}$
19	18	ad2antrr	$⊢ ((R \in SubRing (ℂ_{fld}) \land ℂ_{fld} ↾_{𝑠} R \in DivRing) \land (x \in ℤ \land y \in ℕ)) \to 0 = 0_{(ℂ_{fld} ↾_{𝑠} R)}$
20	16 19	neeqtrd	$⊢ ((R \in SubRing (ℂ_{fld}) \land ℂ_{fld} ↾_{𝑠} R \in DivRing) \land (x \in ℤ \land y \in ℕ)) \to y \neq 0_{(ℂ_{fld} ↾_{𝑠} R)}$
21		eqid	$⊢ {Base}_{(ℂ_{fld} ↾_{𝑠} R)} = {Base}_{(ℂ_{fld} ↾_{𝑠} R)}$
22		eqid	$⊢ Unit (ℂ_{fld} ↾_{𝑠} R) = Unit (ℂ_{fld} ↾_{𝑠} R)$
23		eqid	$⊢ 0_{(ℂ_{fld} ↾_{𝑠} R)} = 0_{(ℂ_{fld} ↾_{𝑠} R)}$
24	21 22 23	drngunit	$⊢ ℂ_{fld} ↾_{𝑠} R \in DivRing \to (y \in Unit (ℂ_{fld} ↾_{𝑠} R) \leftrightarrow (y \in {Base}_{(ℂ_{fld} ↾_{𝑠} R)} \land y \neq 0_{(ℂ_{fld} ↾_{𝑠} R)}))$
25	24	ad2antlr	$⊢ ((R \in SubRing (ℂ_{fld}) \land ℂ_{fld} ↾_{𝑠} R \in DivRing) \land (x \in ℤ \land y \in ℕ)) \to (y \in Unit (ℂ_{fld} ↾_{𝑠} R) \leftrightarrow (y \in {Base}_{(ℂ_{fld} ↾_{𝑠} R)} \land y \neq 0_{(ℂ_{fld} ↾_{𝑠} R)}))$
26	14 20 25	mpbir2and	$⊢ ((R \in SubRing (ℂ_{fld}) \land ℂ_{fld} ↾_{𝑠} R \in DivRing) \land (x \in ℤ \land y \in ℕ)) \to y \in Unit (ℂ_{fld} ↾_{𝑠} R)$
27		eqid	$⊢ /_{r} (ℂ_{fld} ↾_{𝑠} R) = /_{r} (ℂ_{fld} ↾_{𝑠} R)$
28	21 22 27	dvrcl	$⊢ (ℂ_{fld} ↾_{𝑠} R \in Ring \land x \in {Base}_{(ℂ_{fld} ↾_{𝑠} R)} \land y \in Unit (ℂ_{fld} ↾_{𝑠} R)) \to x /_{r} (ℂ_{fld} ↾_{𝑠} R) y \in {Base}_{(ℂ_{fld} ↾_{𝑠} R)}$
29	3 11 26 28	syl3anc	$⊢ ((R \in SubRing (ℂ_{fld}) \land ℂ_{fld} ↾_{𝑠} R \in DivRing) \land (x \in ℤ \land y \in ℕ)) \to x /_{r} (ℂ_{fld} ↾_{𝑠} R) y \in {Base}_{(ℂ_{fld} ↾_{𝑠} R)}$
30		simpll	$⊢ ((R \in SubRing (ℂ_{fld}) \land ℂ_{fld} ↾_{𝑠} R \in DivRing) \land (x \in ℤ \land y \in ℕ)) \to R \in SubRing (ℂ_{fld})$
31	5 10	sseldd	$⊢ ((R \in SubRing (ℂ_{fld}) \land ℂ_{fld} ↾_{𝑠} R \in DivRing) \land (x \in ℤ \land y \in ℕ)) \to x \in R$
32		cnflddiv	$⊢ \div = /_{r} (ℂ_{fld})$
33	6 32 22 27	subrgdv	$⊢ (R \in SubRing (ℂ_{fld}) \land x \in R \land y \in Unit (ℂ_{fld} ↾_{𝑠} R)) \to \frac{x}{y} = x /_{r} (ℂ_{fld} ↾_{𝑠} R) y$
34	30 31 26 33	syl3anc	$⊢ ((R \in SubRing (ℂ_{fld}) \land ℂ_{fld} ↾_{𝑠} R \in DivRing) \land (x \in ℤ \land y \in ℕ)) \to \frac{x}{y} = x /_{r} (ℂ_{fld} ↾_{𝑠} R) y$
35	29 34 8	3eltr4d	$⊢ ((R \in SubRing (ℂ_{fld}) \land ℂ_{fld} ↾_{𝑠} R \in DivRing) \land (x \in ℤ \land y \in ℕ)) \to \frac{x}{y} \in R$
36		eleq1	$⊢ z = \frac{x}{y} \to (z \in R \leftrightarrow \frac{x}{y} \in R)$
37	35 36	syl5ibrcom	$⊢ ((R \in SubRing (ℂ_{fld}) \land ℂ_{fld} ↾_{𝑠} R \in DivRing) \land (x \in ℤ \land y \in ℕ)) \to (z = \frac{x}{y} \to z \in R)$
38	37	rexlimdvva	$⊢ (R \in SubRing (ℂ_{fld}) \land ℂ_{fld} ↾_{𝑠} R \in DivRing) \to (\exists x \in ℤ \exists y \in ℕ z = \frac{x}{y} \to z \in R)$
39	1 38	biimtrid	$⊢ (R \in SubRing (ℂ_{fld}) \land ℂ_{fld} ↾_{𝑠} R \in DivRing) \to (z \in ℚ \to z \in R)$
40	39	ssrdv	$⊢ (R \in SubRing (ℂ_{fld}) \land ℂ_{fld} ↾_{𝑠} R \in DivRing) \to ℚ \subseteq R$

Metamath Proof Explorer

Theorem qsssubdrg

Proof