Theorem cnfldbas 21428

Description: The base set of the field of complex numbers. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 6-Oct-2015.) (Revised by Thierry Arnoux, 17-Dec-2017.) Revise df-cnfld 21425. (Revised by GG, 31-Mar-2025.)

Assertion

Ref	Expression
cnfldbas	⊢ ℂ = (Base‘ℂfld)

Proof of Theorem cnfldbas

Dummy variables 𝑣 𝑢 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		cnex 11154	. 2 ⊢ ℂ ∈ V
2		cnfldstr 21426	. . 3 ⊢ ℂfld Struct ⟨1, ;13⟩
3		baseid 17248	. . 3 ⊢ Base = Slot (Base‘ndx)
4		snsstp1 4774	. . . 4 ⊢ {⟨(Base‘ndx), ℂ⟩} ⊆ {⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), (𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 + 𝑣))⟩, ⟨(.r‘ndx), (𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))⟩}
5		ssun1 4130	. . . . 5 ⊢ {⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), (𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 + 𝑣))⟩, ⟨(.r‘ndx), (𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))⟩} ⊆ ({⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), (𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 + 𝑣))⟩, ⟨(.r‘ndx), (𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))⟩} ∪ {⟨(*𝑟‘ndx), ∗⟩})
6		ssun1 4130	. . . . . 6 ⊢ ({⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), (𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 + 𝑣))⟩, ⟨(.r‘ndx), (𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))⟩} ∪ {⟨(*𝑟‘ndx), ∗⟩}) ⊆ (({⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), (𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 + 𝑣))⟩, ⟨(.r‘ndx), (𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))⟩} ∪ {⟨(*𝑟‘ndx), ∗⟩}) ∪ ({⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ − )⟩} ∪ {⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩}))
7		df-cnfld 21425	. . . . . 6 ⊢ ℂfld = (({⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), (𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 + 𝑣))⟩, ⟨(.r‘ndx), (𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))⟩} ∪ {⟨(*𝑟‘ndx), ∗⟩}) ∪ ({⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ − )⟩} ∪ {⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩}))
8	6, 7	sseqtrri 3985	. . . . 5 ⊢ ({⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), (𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 + 𝑣))⟩, ⟨(.r‘ndx), (𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))⟩} ∪ {⟨(*𝑟‘ndx), ∗⟩}) ⊆ ℂfld
9	5, 8	sstri 3945	. . . 4 ⊢ {⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), (𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 + 𝑣))⟩, ⟨(.r‘ndx), (𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))⟩} ⊆ ℂfld
10	4, 9	sstri 3945	. . 3 ⊢ {⟨(Base‘ndx), ℂ⟩} ⊆ ℂfld
11	2, 3, 10	strfv 17239	. 2 ⊢ (ℂ ∈ V → ℂ = (Base‘ℂfld))
12	1, 11	ax-mp 5	1 ⊢ ℂ = (Base‘ℂfld)

Syntax hints:   = wceq 1560   ∈ wcel 2142  Vcvv 3454   ∪ cun 3902  {csn 4582  {ctp 4586  ⟨cop 4588   ∘ ccom 5651  ‘cfv 6521  (class class class)co 7396   ∈ cmpo 7398  ℂcc 11071  1c1 11074   + caddc 11076   · cmul 11078   ≤ cle 11217   − cmin 11414  3c3 12273  ;cdc 12688  ∗ccj 15123  abscabs 15261  ndxcnx 17229  Basecbs 17245  +_gcplusg 17286  ._rcmulr 17287  *_𝑟cstv 17288  TopSetcts 17292  lecple 17293  distcds 17295  UnifSetcunif 17296  MetOpencmopn 21414  metUnifcmetu 21415  ℂ_fldccnfld 21424

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-10 2175  ax-11 2191  ax-12 2212  ax-ext 2734  ax-sep 5246  ax-nul 5256  ax-pow 5322  ax-pr 5390  ax-un 7718  ax-cnex 11129  ax-resscn 11130  ax-1cn 11131  ax-icn 11132  ax-addcl 11133  ax-addrcl 11134  ax-mulcl 11135  ax-mulrcl 11136  ax-mulcom 11137  ax-addass 11138  ax-mulass 11139  ax-distr 11140  ax-i2m1 11141  ax-1ne0 11142  ax-1rid 11143  ax-rnegex 11144  ax-rrecex 11145  ax-cnre 11146  ax-pre-lttri 11147  ax-pre-lttrn 11148  ax-pre-ltadd 11149  ax-pre-mulgt0 11150

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1099  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-nf 1804  df-sb 2091  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-nel 3062  df-ral 3077  df-rex 3087  df-reu 3368  df-rab 3415  df-v 3456  df-sbc 3745  df-csb 3853  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-pss 3924  df-nul 4286  df-if 4481  df-pw 4557  df-sn 4583  df-pr 4585  df-tp 4587  df-op 4589  df-uni 4866  df-iun 4951  df-br 5101  df-opab 5163  df-mpt 5182  df-tr 5208  df-id 5542  df-eprel 5547  df-po 5555  df-so 5556  df-fr 5600  df-we 5602  df-xp 5653  df-rel 5654  df-cnv 5655  df-co 5656  df-dm 5657  df-rn 5658  df-res 5659  df-ima 5660  df-pred 6288  df-ord 6349  df-on 6350  df-lim 6351  df-suc 6352  df-iota 6477  df-fun 6523  df-fn 6524  df-f 6525  df-f1 6526  df-fo 6527  df-f1o 6528  df-fv 6529  df-riota 7353  df-ov 7399  df-oprab 7400  df-mpo 7401  df-om 7847  df-1st 7970  df-2nd 7971  df-frecs 8262  df-wrecs 8293  df-recs 8342  df-rdg 8381  df-1o 8437  df-er 8678  df-en 8928  df-dom 8929  df-sdom 8930  df-fin 8931  df-pnf 11218  df-mnf 11219  df-xr 11220  df-ltxr 11221  df-le 11222  df-sub 11416  df-neg 11417  df-nn 12211  df-2 12280  df-3 12281  df-4 12282  df-5 12283  df-6 12284  df-7 12285  df-8 12286  df-9 12287  df-n0 12482  df-z 12569  df-dec 12689  df-uz 12840  df-fz 13513  df-struct 17183  df-slot 17218  df-ndx 17230  df-base 17246  df-plusg 17299  df-mulr 17300  df-starv 17301  df-tset 17305  df-ple 17306  df-ds 17308  df-unif 17309  df-cnfld 21425

This theorem is referenced by:  cncrng  21445  cnfld0  21448  cnfld1  21449  cnfldneg  21450  cnfldplusf  21451  cnfldsub  21452  cndrng  21453  cnflddiv  21454  cnfldinv  21455  cnfldmulg  21456  cnfldexp  21457  cnsrng  21458  cnsubmlem  21467  cnsubglem  21468  cnsubrglem  21469  cnsubdrglem  21470  absabv  21476  cnsubrg  21479  cnmgpabl  21480  cnmgpid  21481  cnmsubglem  21482  gzrngunit  21485  gsumfsum  21486  regsumfsum  21487  expmhm  21488  nn0srg  21489  rge0srg  21490  zringbas  21505  zring0  21510  zringunit  21518  expghm  21527  fermltlchr  21581  cnmsgnbas  21630  psgninv  21634  zrhpsgnmhm  21636  rebase  21658  re0g  21664  regsumsupp  21674  cnfldms  24835  cnfldnm  24838  cnfldtopn  24841  cnfldtopon  24842  clmsscn  25141  cnlmod  25202  cnstrcvs  25203  cnrbas  25204  cncvs  25207  cnncvsaddassdemo  25225  cnncvsmulassdemo  25226  cnncvsabsnegdemo  25227  cphsubrglem  25239  cphreccllem  25240  cphdivcl  25244  cphabscl  25247  cphsqrtcl2  25248  cphsqrtcl3  25249  cphipcl  25253  4cphipval2  25304  cncms  25417  cnflduss  25418  cnfldcusp  25419  resscdrg  25420  ishl2  25432  recms  25442  tdeglem3  26119  tdeglem4  26120  tdeglem2  26121  plypf1  26272  dvply2g  26349  dvply2  26350  dvnply  26352  taylfvallem  26421  taylf  26424  tayl0  26425  taylpfval  26428  taylply2  26431  taylply  26432  efgh  26606  efabl  26615  efsubm  26616  jensenlem1  27051  jensenlem2  27052  jensen  27053  amgmlem  27054  amgm  27055  wilthlem2  27133  wilthlem3  27134  dchrelbas2  27301  dchrelbas3  27302  dchrn0  27314  dchrghm  27320  dchrabs  27324  sum2dchr  27338  lgseisenlem4  27442  qrngbas  27683  cchhllem  29087  cffldtocusgr  29648  gsumzrsum  33245  psgnid  33277  cnmsgn0g  33326  altgnsg  33329  1fldgenq  33509  gsumind  33531  xrge0slmod  33534  znfermltl  33552  psrmonprod  33849  esplyfvaln  33871  ccfldsrarelvec  33968  ccfldextdgrr  33969  constrelextdg2  34044  constrextdg2lem  34045  constrext2chnlem  34047  constrcon  34071  constrsdrg  34072  2sqr3minply  34077  cos9thpiminplylem6  34084  cos9thpiminply  34085  iistmd  34199  xrge0iifmhm  34236  xrge0pluscn  34237  zringnm  34255  cnzh  34265  rezh  34266  cnrrext  34307  esumpfinvallem  34371  cnpwstotbnd  38296  repwsmet  38333  rrnequiv  38334  cnsrexpcl  43742  fsumcnsrcl  43743  cnsrplycl  43744  rngunsnply  43746  proot1ex  43773  deg1mhm  43777  amgm2d  44774  amgm3d  44775  amgm4d  44776  binomcxplemdvbinom  44929  binomcxplemnotnn0  44932  sge0tsms  46954  cnfldsrngbas  48783  2zrng0  48866  aacllem  50422  amgmwlem  50423  amgmlemALT  50424  amgmw2d  50425