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 
|- ( CCfld fldGen { 1 } ) = QQ

Proof

Step Hyp Ref Expression
1 cnfldbas 
 |-  CC = ( Base ` CCfld )
2 cndrng 
 |-  CCfld e. DivRing
3 2 a1i 
 |-  ( T. -> CCfld e. DivRing )
4 qsscn 
 |-  QQ C_ CC
5 4 a1i 
 |-  ( T. -> QQ C_ CC )
6 1z 
 |-  1 e. ZZ
7 snssi 
 |-  ( 1 e. ZZ -> { 1 } C_ ZZ )
8 6 7 ax-mp 
 |-  { 1 } C_ ZZ
9 zssq 
 |-  ZZ C_ QQ
10 8 9 sstri 
 |-  { 1 } C_ QQ
11 10 a1i 
 |-  ( T. -> { 1 } C_ QQ )
12 1 3 5 11 fldgenss 
 |-  ( T. -> ( CCfld fldGen { 1 } ) C_ ( CCfld fldGen QQ ) )
13 qsubdrg 
 |-  ( QQ e. ( SubRing ` CCfld ) /\ ( CCfld |`s QQ ) e. DivRing )
14 13 simpli 
 |-  QQ e. ( SubRing ` CCfld )
15 13 simpri 
 |-  ( CCfld |`s QQ ) e. DivRing
16 issdrg 
 |-  ( QQ e. ( SubDRing ` CCfld ) <-> ( CCfld e. DivRing /\ QQ e. ( SubRing ` CCfld ) /\ ( CCfld |`s QQ ) e. DivRing ) )
17 2 14 15 16 mpbir3an 
 |-  QQ e. ( SubDRing ` CCfld )
18 17 a1i 
 |-  ( T. -> QQ e. ( SubDRing ` CCfld ) )
19 1 3 18 fldgenidfld 
 |-  ( T. -> ( CCfld fldGen QQ ) = QQ )
20 12 19 sseqtrd 
 |-  ( T. -> ( CCfld fldGen { 1 } ) C_ QQ )
21 elq 
 |-  ( z e. QQ <-> E. p e. ZZ E. q e. NN z = ( p / q ) )
22 cnflddiv 
 |-  / = ( /r ` CCfld )
23 cnfld0 
 |-  0 = ( 0g ` CCfld )
24 11 4 sstrdi 
 |-  ( T. -> { 1 } C_ CC )
25 1 3 24 fldgensdrg 
 |-  ( T. -> ( CCfld fldGen { 1 } ) e. ( SubDRing ` CCfld ) )
26 25 mptru 
 |-  ( CCfld fldGen { 1 } ) e. ( SubDRing ` CCfld )
27 26 a1i 
 |-  ( ( p e. ZZ /\ q e. NN ) -> ( CCfld fldGen { 1 } ) e. ( SubDRing ` CCfld ) )
28 ax-1cn 
 |-  1 e. CC
29 cnfldmulg 
 |-  ( ( p e. ZZ /\ 1 e. CC ) -> ( p ( .g ` CCfld ) 1 ) = ( p x. 1 ) )
30 28 29 mpan2 
 |-  ( p e. ZZ -> ( p ( .g ` CCfld ) 1 ) = ( p x. 1 ) )
31 zre 
 |-  ( p e. ZZ -> p e. RR )
32 ax-1rid 
 |-  ( p e. RR -> ( p x. 1 ) = p )
33 31 32 syl 
 |-  ( p e. ZZ -> ( p x. 1 ) = p )
34 30 33 eqtrd 
 |-  ( p e. ZZ -> ( p ( .g ` CCfld ) 1 ) = p )
35 issdrg 
 |-  ( ( CCfld fldGen { 1 } ) e. ( SubDRing ` CCfld ) <-> ( CCfld e. DivRing /\ ( CCfld fldGen { 1 } ) e. ( SubRing ` CCfld ) /\ ( CCfld |`s ( CCfld fldGen { 1 } ) ) e. DivRing ) )
36 26 35 mpbi 
 |-  ( CCfld e. DivRing /\ ( CCfld fldGen { 1 } ) e. ( SubRing ` CCfld ) /\ ( CCfld |`s ( CCfld fldGen { 1 } ) ) e. DivRing )
37 36 simp2i 
 |-  ( CCfld fldGen { 1 } ) e. ( SubRing ` CCfld )
38 subrgsubg 
 |-  ( ( CCfld fldGen { 1 } ) e. ( SubRing ` CCfld ) -> ( CCfld fldGen { 1 } ) e. ( SubGrp ` CCfld ) )
39 37 38 ax-mp 
 |-  ( CCfld fldGen { 1 } ) e. ( SubGrp ` CCfld )
40 1 3 24 fldgenssid 
 |-  ( T. -> { 1 } C_ ( CCfld fldGen { 1 } ) )
41 1ex 
 |-  1 e. _V
42 41 snss 
 |-  ( 1 e. ( CCfld fldGen { 1 } ) <-> { 1 } C_ ( CCfld fldGen { 1 } ) )
43 40 42 sylibr 
 |-  ( T. -> 1 e. ( CCfld fldGen { 1 } ) )
44 43 mptru 
 |-  1 e. ( CCfld fldGen { 1 } )
45 eqid 
 |-  ( .g ` CCfld ) = ( .g ` CCfld )
46 45 subgmulgcl 
 |-  ( ( ( CCfld fldGen { 1 } ) e. ( SubGrp ` CCfld ) /\ p e. ZZ /\ 1 e. ( CCfld fldGen { 1 } ) ) -> ( p ( .g ` CCfld ) 1 ) e. ( CCfld fldGen { 1 } ) )
47 39 44 46 mp3an13 
 |-  ( p e. ZZ -> ( p ( .g ` CCfld ) 1 ) e. ( CCfld fldGen { 1 } ) )
48 34 47 eqeltrrd 
 |-  ( p e. ZZ -> p e. ( CCfld fldGen { 1 } ) )
49 48 adantr 
 |-  ( ( p e. ZZ /\ q e. NN ) -> p e. ( CCfld fldGen { 1 } ) )
50 48 ssriv 
 |-  ZZ C_ ( CCfld fldGen { 1 } )
51 nnz 
 |-  ( q e. NN -> q e. ZZ )
52 51 adantl 
 |-  ( ( p e. ZZ /\ q e. NN ) -> q e. ZZ )
53 50 52 sselid 
 |-  ( ( p e. ZZ /\ q e. NN ) -> q e. ( CCfld fldGen { 1 } ) )
54 nnne0 
 |-  ( q e. NN -> q =/= 0 )
55 54 adantl 
 |-  ( ( p e. ZZ /\ q e. NN ) -> q =/= 0 )
56 22 23 27 49 53 55 sdrgdvcl 
 |-  ( ( p e. ZZ /\ q e. NN ) -> ( p / q ) e. ( CCfld fldGen { 1 } ) )
57 eleq1 
 |-  ( z = ( p / q ) -> ( z e. ( CCfld fldGen { 1 } ) <-> ( p / q ) e. ( CCfld fldGen { 1 } ) ) )
58 56 57 syl5ibrcom 
 |-  ( ( p e. ZZ /\ q e. NN ) -> ( z = ( p / q ) -> z e. ( CCfld fldGen { 1 } ) ) )
59 58 rexlimivv 
 |-  ( E. p e. ZZ E. q e. NN z = ( p / q ) -> z e. ( CCfld fldGen { 1 } ) )
60 21 59 sylbi 
 |-  ( z e. QQ -> z e. ( CCfld fldGen { 1 } ) )
61 60 ssriv 
 |-  QQ C_ ( CCfld fldGen { 1 } )
62 61 a1i 
 |-  ( T. -> QQ C_ ( CCfld fldGen { 1 } ) )
63 20 62 eqssd 
 |-  ( T. -> ( CCfld fldGen { 1 } ) = QQ )
64 63 mptru 
 |-  ( CCfld fldGen { 1 } ) = QQ