Metamath Proof Explorer

Theorem 1fldgenq

Description: The field of rational numbers QQ is generated by 1 in CCfld , that is, QQ is the prime field of CCfld . (Contributed by Thierry Arnoux, 15-Jan-2025)

Ref Expression
Assertion 1fldgenq ( ℂfld fldGen { 1 } ) = ℚ

Proof

Step Hyp Ref Expression
1 cnfldbas ⊢ ℂ = ( Base ‘ ℂfld )
2 cndrng ⊢ ℂfld ∈ DivRing
3 2 a1i ⊢ ( ⊤ → ℂfld ∈ DivRing )
4 qsscn ⊢ ℚ ⊆ ℂ
5 4 a1i ⊢ ( ⊤ → ℚ ⊆ ℂ )
6 1z ⊢ 1 ∈ ℤ
7 snssi ⊢ ( 1 ∈ ℤ → { 1 } ⊆ ℤ )
8 6 7 ax-mp ⊢ { 1 } ⊆ ℤ
9 zssq ⊢ ℤ ⊆ ℚ
10 8 9 sstri ⊢ { 1 } ⊆ ℚ
11 10 a1i ⊢ ( ⊤ → { 1 } ⊆ ℚ )
12 1 3 5 11 fldgenss ⊢ ( ⊤ → ( ℂfld fldGen { 1 } ) ⊆ ( ℂfld fldGen ℚ ) )
13 qsubdrg ⊢ ( ℚ ∈ ( SubRing ‘ ℂfld ) ∧ ( ℂfld ↾s ℚ ) ∈ DivRing )
14 13 simpli ⊢ ℚ ∈ ( SubRing ‘ ℂfld )
15 13 simpri ⊢ ( ℂfld ↾s ℚ ) ∈ DivRing
16 issdrg ⊢ ( ℚ ∈ ( SubDRing ‘ ℂfld ) ↔ ( ℂfld ∈ DivRing ∧ ℚ ∈ ( SubRing ‘ ℂfld ) ∧ ( ℂfld ↾s ℚ ) ∈ DivRing ) )
17 2 14 15 16 mpbir3an ⊢ ℚ ∈ ( SubDRing ‘ ℂfld )
18 17 a1i ⊢ ( ⊤ → ℚ ∈ ( SubDRing ‘ ℂfld ) )
19 1 3 18 fldgenidfld ⊢ ( ⊤ → ( ℂfld fldGen ℚ ) = ℚ )
20 12 19 sseqtrd ⊢ ( ⊤ → ( ℂfld fldGen { 1 } ) ⊆ ℚ )
21 elq ⊢ ( 𝑧 ∈ ℚ ↔ ∃ 𝑝 ∈ ℤ ∃ 𝑞 ∈ ℕ 𝑧 = ( 𝑝 / 𝑞 ) )
22 cnflddiv ⊢ / = ( /r ‘ ℂfld )
23 cnfld0 ⊢ 0 = ( 0g ‘ ℂfld )
24 11 4 sstrdi ⊢ ( ⊤ → { 1 } ⊆ ℂ )
25 1 3 24 fldgensdrg ⊢ ( ⊤ → ( ℂfld fldGen { 1 } ) ∈ ( SubDRing ‘ ℂfld ) )
26 25 mptru ⊢ ( ℂfld fldGen { 1 } ) ∈ ( SubDRing ‘ ℂfld )
27 26 a1i ⊢ ( ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) → ( ℂfld fldGen { 1 } ) ∈ ( SubDRing ‘ ℂfld ) )
28 ax-1cn ⊢ 1 ∈ ℂ
29 cnfldmulg ⊢ ( ( 𝑝 ∈ ℤ ∧ 1 ∈ ℂ ) → ( 𝑝 ( .g ‘ ℂfld ) 1 ) = ( 𝑝 · 1 ) )
30 28 29 mpan2 ⊢ ( 𝑝 ∈ ℤ → ( 𝑝 ( .g ‘ ℂfld ) 1 ) = ( 𝑝 · 1 ) )
31 zre ⊢ ( 𝑝 ∈ ℤ → 𝑝 ∈ ℝ )
32 ax-1rid ⊢ ( 𝑝 ∈ ℝ → ( 𝑝 · 1 ) = 𝑝 )
33 31 32 syl ⊢ ( 𝑝 ∈ ℤ → ( 𝑝 · 1 ) = 𝑝 )
34 30 33 eqtrd ⊢ ( 𝑝 ∈ ℤ → ( 𝑝 ( .g ‘ ℂfld ) 1 ) = 𝑝 )
35 issdrg ⊢ ( ( ℂfld fldGen { 1 } ) ∈ ( SubDRing ‘ ℂfld ) ↔ ( ℂfld ∈ DivRing ∧ ( ℂfld fldGen { 1 } ) ∈ ( SubRing ‘ ℂfld ) ∧ ( ℂfld ↾s ( ℂfld fldGen { 1 } ) ) ∈ DivRing ) )
36 26 35 mpbi ⊢ ( ℂfld ∈ DivRing ∧ ( ℂfld fldGen { 1 } ) ∈ ( SubRing ‘ ℂfld ) ∧ ( ℂfld ↾s ( ℂfld fldGen { 1 } ) ) ∈ DivRing )
37 36 simp2i ⊢ ( ℂfld fldGen { 1 } ) ∈ ( SubRing ‘ ℂfld )
38 subrgsubg ⊢ ( ( ℂfld fldGen { 1 } ) ∈ ( SubRing ‘ ℂfld ) → ( ℂfld fldGen { 1 } ) ∈ ( SubGrp ‘ ℂfld ) )
39 37 38 ax-mp ⊢ ( ℂfld fldGen { 1 } ) ∈ ( SubGrp ‘ ℂfld )
40 1 3 24 fldgenssid ⊢ ( ⊤ → { 1 } ⊆ ( ℂfld fldGen { 1 } ) )
41 1ex ⊢ 1 ∈ V
42 41 snss ⊢ ( 1 ∈ ( ℂfld fldGen { 1 } ) ↔ { 1 } ⊆ ( ℂfld fldGen { 1 } ) )
43 40 42 sylibr ⊢ ( ⊤ → 1 ∈ ( ℂfld fldGen { 1 } ) )
44 43 mptru ⊢ 1 ∈ ( ℂfld fldGen { 1 } )
45 eqid ⊢ ( .g ‘ ℂfld ) = ( .g ‘ ℂfld )
46 45 subgmulgcl ⊢ ( ( ( ℂfld fldGen { 1 } ) ∈ ( SubGrp ‘ ℂfld ) ∧ 𝑝 ∈ ℤ ∧ 1 ∈ ( ℂfld fldGen { 1 } ) ) → ( 𝑝 ( .g ‘ ℂfld ) 1 ) ∈ ( ℂfld fldGen { 1 } ) )
47 39 44 46 mp3an13 ⊢ ( 𝑝 ∈ ℤ → ( 𝑝 ( .g ‘ ℂfld ) 1 ) ∈ ( ℂfld fldGen { 1 } ) )
48 34 47 eqeltrrd ⊢ ( 𝑝 ∈ ℤ → 𝑝 ∈ ( ℂfld fldGen { 1 } ) )
49 48 adantr ⊢ ( ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) → 𝑝 ∈ ( ℂfld fldGen { 1 } ) )
50 48 ssriv ⊢ ℤ ⊆ ( ℂfld fldGen { 1 } )
51 nnz ⊢ ( 𝑞 ∈ ℕ → 𝑞 ∈ ℤ )
52 51 adantl ⊢ ( ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) → 𝑞 ∈ ℤ )
53 50 52 sselid ⊢ ( ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) → 𝑞 ∈ ( ℂfld fldGen { 1 } ) )
54 nnne0 ⊢ ( 𝑞 ∈ ℕ → 𝑞 ≠ 0 )
55 54 adantl ⊢ ( ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) → 𝑞 ≠ 0 )
56 22 23 27 49 53 55 sdrgdvcl ⊢ ( ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) → ( 𝑝 / 𝑞 ) ∈ ( ℂfld fldGen { 1 } ) )
57 eleq1 ⊢ ( 𝑧 = ( 𝑝 / 𝑞 ) → ( 𝑧 ∈ ( ℂfld fldGen { 1 } ) ↔ ( 𝑝 / 𝑞 ) ∈ ( ℂfld fldGen { 1 } ) ) )
58 56 57 syl5ibrcom ⊢ ( ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) → ( 𝑧 = ( 𝑝 / 𝑞 ) → 𝑧 ∈ ( ℂfld fldGen { 1 } ) ) )
59 58 rexlimivv ⊢ ( ∃ 𝑝 ∈ ℤ ∃ 𝑞 ∈ ℕ 𝑧 = ( 𝑝 / 𝑞 ) → 𝑧 ∈ ( ℂfld fldGen { 1 } ) )
60 21 59 sylbi ⊢ ( 𝑧 ∈ ℚ → 𝑧 ∈ ( ℂfld fldGen { 1 } ) )
61 60 ssriv ⊢ ℚ ⊆ ( ℂfld fldGen { 1 } )
62 61 a1i ⊢ ( ⊤ → ℚ ⊆ ( ℂfld fldGen { 1 } ) )
63 20 62 eqssd ⊢ ( ⊤ → ( ℂfld fldGen { 1 } ) = ℚ )
64 63 mptru ⊢ ( ℂfld fldGen { 1 } ) = ℚ