Metamath Proof Explorer

Theorem 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 ( ( 𝑅 ∈ ( SubRing ‘ ℂfld ) ∧ ( ℂfld ↾s 𝑅 ) ∈ DivRing ) → ℚ ⊆ 𝑅 )

Proof

Step Hyp Ref Expression
1 elq ⊢ ( 𝑧 ∈ ℚ ↔ ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℕ 𝑧 = ( 𝑥 / 𝑦 ) )
2 drngring ⊢ ( ( ℂfld ↾s 𝑅 ) ∈ DivRing → ( ℂfld ↾s 𝑅 ) ∈ Ring )
3 2 ad2antlr ⊢ ( ( ( 𝑅 ∈ ( SubRing ‘ ℂfld ) ∧ ( ℂfld ↾s 𝑅 ) ∈ DivRing ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ ) ) → ( ℂfld ↾s 𝑅 ) ∈ Ring )
4 zsssubrg ⊢ ( 𝑅 ∈ ( SubRing ‘ ℂfld ) → ℤ ⊆ 𝑅 )
5 4 ad2antrr ⊢ ( ( ( 𝑅 ∈ ( SubRing ‘ ℂfld ) ∧ ( ℂfld ↾s 𝑅 ) ∈ DivRing ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ ) ) → ℤ ⊆ 𝑅 )
6 eqid ⊢ ( ℂfld ↾s 𝑅 ) = ( ℂfld ↾s 𝑅 )
7 6 subrgbas ⊢ ( 𝑅 ∈ ( SubRing ‘ ℂfld ) → 𝑅 = ( Base ‘ ( ℂfld ↾s 𝑅 ) ) )
8 7 ad2antrr ⊢ ( ( ( 𝑅 ∈ ( SubRing ‘ ℂfld ) ∧ ( ℂfld ↾s 𝑅 ) ∈ DivRing ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ ) ) → 𝑅 = ( Base ‘ ( ℂfld ↾s 𝑅 ) ) )
9 5 8 sseqtrd ⊢ ( ( ( 𝑅 ∈ ( SubRing ‘ ℂfld ) ∧ ( ℂfld ↾s 𝑅 ) ∈ DivRing ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ ) ) → ℤ ⊆ ( Base ‘ ( ℂfld ↾s 𝑅 ) ) )
10 simprl ⊢ ( ( ( 𝑅 ∈ ( SubRing ‘ ℂfld ) ∧ ( ℂfld ↾s 𝑅 ) ∈ DivRing ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ ) ) → 𝑥 ∈ ℤ )
11 9 10 sseldd ⊢ ( ( ( 𝑅 ∈ ( SubRing ‘ ℂfld ) ∧ ( ℂfld ↾s 𝑅 ) ∈ DivRing ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ ) ) → 𝑥 ∈ ( Base ‘ ( ℂfld ↾s 𝑅 ) ) )
12 nnz ⊢ ( 𝑦 ∈ ℕ → 𝑦 ∈ ℤ )
13 12 ad2antll ⊢ ( ( ( 𝑅 ∈ ( SubRing ‘ ℂfld ) ∧ ( ℂfld ↾s 𝑅 ) ∈ DivRing ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ ) ) → 𝑦 ∈ ℤ )
14 9 13 sseldd ⊢ ( ( ( 𝑅 ∈ ( SubRing ‘ ℂfld ) ∧ ( ℂfld ↾s 𝑅 ) ∈ DivRing ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ ) ) → 𝑦 ∈ ( Base ‘ ( ℂfld ↾s 𝑅 ) ) )
15 nnne0 ⊢ ( 𝑦 ∈ ℕ → 𝑦 ≠ 0 )
16 15 ad2antll ⊢ ( ( ( 𝑅 ∈ ( SubRing ‘ ℂfld ) ∧ ( ℂfld ↾s 𝑅 ) ∈ DivRing ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ ) ) → 𝑦 ≠ 0 )
17 cnfld0 ⊢ 0 = ( 0g ‘ ℂfld )
18 6 17 subrg0 ⊢ ( 𝑅 ∈ ( SubRing ‘ ℂfld ) → 0 = ( 0g ‘ ( ℂfld ↾s 𝑅 ) ) )
19 18 ad2antrr ⊢ ( ( ( 𝑅 ∈ ( SubRing ‘ ℂfld ) ∧ ( ℂfld ↾s 𝑅 ) ∈ DivRing ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ ) ) → 0 = ( 0g ‘ ( ℂfld ↾s 𝑅 ) ) )
20 16 19 neeqtrd ⊢ ( ( ( 𝑅 ∈ ( SubRing ‘ ℂfld ) ∧ ( ℂfld ↾s 𝑅 ) ∈ DivRing ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ ) ) → 𝑦 ≠ ( 0g ‘ ( ℂfld ↾s 𝑅 ) ) )
21 eqid ⊢ ( Base ‘ ( ℂfld ↾s 𝑅 ) ) = ( Base ‘ ( ℂfld ↾s 𝑅 ) )
22 eqid ⊢ ( Unit ‘ ( ℂfld ↾s 𝑅 ) ) = ( Unit ‘ ( ℂfld ↾s 𝑅 ) )
23 eqid ⊢ ( 0g ‘ ( ℂfld ↾s 𝑅 ) ) = ( 0g ‘ ( ℂfld ↾s 𝑅 ) )
24 21 22 23 drngunit ⊢ ( ( ℂfld ↾s 𝑅 ) ∈ DivRing → ( 𝑦 ∈ ( Unit ‘ ( ℂfld ↾s 𝑅 ) ) ↔ ( 𝑦 ∈ ( Base ‘ ( ℂfld ↾s 𝑅 ) ) ∧ 𝑦 ≠ ( 0g ‘ ( ℂfld ↾s 𝑅 ) ) ) ) )
25 24 ad2antlr ⊢ ( ( ( 𝑅 ∈ ( SubRing ‘ ℂfld ) ∧ ( ℂfld ↾s 𝑅 ) ∈ DivRing ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ ) ) → ( 𝑦 ∈ ( Unit ‘ ( ℂfld ↾s 𝑅 ) ) ↔ ( 𝑦 ∈ ( Base ‘ ( ℂfld ↾s 𝑅 ) ) ∧ 𝑦 ≠ ( 0g ‘ ( ℂfld ↾s 𝑅 ) ) ) ) )
26 14 20 25 mpbir2and ⊢ ( ( ( 𝑅 ∈ ( SubRing ‘ ℂfld ) ∧ ( ℂfld ↾s 𝑅 ) ∈ DivRing ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ ) ) → 𝑦 ∈ ( Unit ‘ ( ℂfld ↾s 𝑅 ) ) )
27 eqid ⊢ ( /r ‘ ( ℂfld ↾s 𝑅 ) ) = ( /r ‘ ( ℂfld ↾s 𝑅 ) )
28 21 22 27 dvrcl ⊢ ( ( ( ℂfld ↾s 𝑅 ) ∈ Ring ∧ 𝑥 ∈ ( Base ‘ ( ℂfld ↾s 𝑅 ) ) ∧ 𝑦 ∈ ( Unit ‘ ( ℂfld ↾s 𝑅 ) ) ) → ( 𝑥 ( /r ‘ ( ℂfld ↾s 𝑅 ) ) 𝑦 ) ∈ ( Base ‘ ( ℂfld ↾s 𝑅 ) ) )
29 3 11 26 28 syl3anc ⊢ ( ( ( 𝑅 ∈ ( SubRing ‘ ℂfld ) ∧ ( ℂfld ↾s 𝑅 ) ∈ DivRing ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ ) ) → ( 𝑥 ( /r ‘ ( ℂfld ↾s 𝑅 ) ) 𝑦 ) ∈ ( Base ‘ ( ℂfld ↾s 𝑅 ) ) )
30 simpll ⊢ ( ( ( 𝑅 ∈ ( SubRing ‘ ℂfld ) ∧ ( ℂfld ↾s 𝑅 ) ∈ DivRing ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ ) ) → 𝑅 ∈ ( SubRing ‘ ℂfld ) )
31 5 10 sseldd ⊢ ( ( ( 𝑅 ∈ ( SubRing ‘ ℂfld ) ∧ ( ℂfld ↾s 𝑅 ) ∈ DivRing ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ ) ) → 𝑥 ∈ 𝑅 )
32 cnflddiv ⊢ / = ( /r ‘ ℂfld )
33 6 32 22 27 subrgdv ⊢ ( ( 𝑅 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ ( Unit ‘ ( ℂfld ↾s 𝑅 ) ) ) → ( 𝑥 / 𝑦 ) = ( 𝑥 ( /r ‘ ( ℂfld ↾s 𝑅 ) ) 𝑦 ) )
34 30 31 26 33 syl3anc ⊢ ( ( ( 𝑅 ∈ ( SubRing ‘ ℂfld ) ∧ ( ℂfld ↾s 𝑅 ) ∈ DivRing ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ ) ) → ( 𝑥 / 𝑦 ) = ( 𝑥 ( /r ‘ ( ℂfld ↾s 𝑅 ) ) 𝑦 ) )
35 29 34 8 3eltr4d ⊢ ( ( ( 𝑅 ∈ ( SubRing ‘ ℂfld ) ∧ ( ℂfld ↾s 𝑅 ) ∈ DivRing ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ ) ) → ( 𝑥 / 𝑦 ) ∈ 𝑅 )
36 eleq1 ⊢ ( 𝑧 = ( 𝑥 / 𝑦 ) → ( 𝑧 ∈ 𝑅 ↔ ( 𝑥 / 𝑦 ) ∈ 𝑅 ) )
37 35 36 syl5ibrcom ⊢ ( ( ( 𝑅 ∈ ( SubRing ‘ ℂfld ) ∧ ( ℂfld ↾s 𝑅 ) ∈ DivRing ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ ) ) → ( 𝑧 = ( 𝑥 / 𝑦 ) → 𝑧 ∈ 𝑅 ) )
38 37 rexlimdvva ⊢ ( ( 𝑅 ∈ ( SubRing ‘ ℂfld ) ∧ ( ℂfld ↾s 𝑅 ) ∈ DivRing ) → ( ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℕ 𝑧 = ( 𝑥 / 𝑦 ) → 𝑧 ∈ 𝑅 ) )
39 1 38 syl5bi ⊢ ( ( 𝑅 ∈ ( SubRing ‘ ℂfld ) ∧ ( ℂfld ↾s 𝑅 ) ∈ DivRing ) → ( 𝑧 ∈ ℚ → 𝑧 ∈ 𝑅 ) )
40 39 ssrdv ⊢ ( ( 𝑅 ∈ ( SubRing ‘ ℂfld ) ∧ ( ℂfld ↾s 𝑅 ) ∈ DivRing ) → ℚ ⊆ 𝑅 )