Theorem cnfldbas 21351

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 21348. (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 11110	. 2 ⊢ ℂ ∈ V
2		cnfldstr 21349	. . 3 ⊢ ℂfld Struct ⟨1, ;13⟩
3		baseid 17173	. . 3 ⊢ Base = Slot (Base‘ndx)
4		snsstp1 4747	. . . 4 ⊢ {⟨(Base‘ndx), ℂ⟩} ⊆ {⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), (𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 + 𝑣))⟩, ⟨(.r‘ndx), (𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))⟩}
5		ssun1 4107	. . . . 5 ⊢ {⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), (𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 + 𝑣))⟩, ⟨(.r‘ndx), (𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))⟩} ⊆ ({⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), (𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 + 𝑣))⟩, ⟨(.r‘ndx), (𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))⟩} ∪ {⟨(*𝑟‘ndx), ∗⟩})
6		ssun1 4107	. . . . . 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 21348	. . . . . 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 3964	. . . . 5 ⊢ ({⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), (𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 + 𝑣))⟩, ⟨(.r‘ndx), (𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))⟩} ∪ {⟨(*𝑟‘ndx), ∗⟩}) ⊆ ℂfld
9	5, 8	sstri 3924	. . . 4 ⊢ {⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), (𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 + 𝑣))⟩, ⟨(.r‘ndx), (𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))⟩} ⊆ ℂfld
10	4, 9	sstri 3924	. . 3 ⊢ {⟨(Base‘ndx), ℂ⟩} ⊆ ℂfld
11	2, 3, 10	strfv 17164	. 2 ⊢ (ℂ ∈ V → ℂ = (Base‘ℂfld))
12	1, 11	ax-mp 5	1 ⊢ ℂ = (Base‘ℂfld)

Syntax hints:   = wceq 1547   ∈ wcel 2119  Vcvv 3431   ∪ cun 3881  {csn 4555  {ctp 4559  ⟨cop 4561   ∘ ccom 5622  ‘cfv 6485  (class class class)co 7356   ∈ cmpo 7358  ℂcc 11027  1c1 11030   + caddc 11032   · cmul 11034   ≤ cle 11171   − cmin 11368  3c3 12228  ;cdc 12635  ∗ccj 15049  abscabs 15187  ndxcnx 17154  Basecbs 17170  +_gcplusg 17211  ._rcmulr 17212  *_𝑟cstv 17213  TopSetcts 17217  lecple 17218  distcds 17220  UnifSetcunif 17221  MetOpencmopn 21337  metUnifcmetu 21338  ℂ_fldccnfld 21347

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711  ax-sep 5218  ax-nul 5228  ax-pow 5294  ax-pr 5362  ax-un 7678  ax-cnex 11085  ax-resscn 11086  ax-1cn 11087  ax-icn 11088  ax-addcl 11089  ax-addrcl 11090  ax-mulcl 11091  ax-mulrcl 11092  ax-mulcom 11093  ax-addass 11094  ax-mulass 11095  ax-distr 11096  ax-i2m1 11097  ax-1ne0 11098  ax-1rid 11099  ax-rnegex 11100  ax-rrecex 11101  ax-cnre 11102  ax-pre-lttri 11103  ax-pre-lttrn 11104  ax-pre-ltadd 11105  ax-pre-mulgt0 11106

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3or 1093  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2718  df-cleq 2731  df-clel 2814  df-nfc 2888  df-ne 2935  df-nel 3039  df-ral 3054  df-rex 3064  df-reu 3345  df-rab 3392  df-v 3433  df-sbc 3724  df-csb 3832  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3903  df-nul 4262  df-if 4455  df-pw 4531  df-sn 4556  df-pr 4558  df-tp 4560  df-op 4562  df-uni 4839  df-iun 4923  df-br 5073  df-opab 5135  df-mpt 5154  df-tr 5180  df-id 5513  df-eprel 5518  df-po 5526  df-so 5527  df-fr 5571  df-we 5573  df-xp 5624  df-rel 5625  df-cnv 5626  df-co 5627  df-dm 5628  df-rn 5629  df-res 5630  df-ima 5631  df-pred 6252  df-ord 6313  df-on 6314  df-lim 6315  df-suc 6316  df-iota 6441  df-fun 6487  df-fn 6488  df-f 6489  df-f1 6490  df-fo 6491  df-f1o 6492  df-fv 6493  df-riota 7313  df-ov 7359  df-oprab 7360  df-mpo 7361  df-om 7807  df-1st 7931  df-2nd 7932  df-frecs 8221  df-wrecs 8252  df-recs 8301  df-rdg 8339  df-1o 8395  df-er 8633  df-en 8884  df-dom 8885  df-sdom 8886  df-fin 8887  df-pnf 11172  df-mnf 11173  df-xr 11174  df-ltxr 11175  df-le 11176  df-sub 11370  df-neg 11371  df-nn 12166  df-2 12235  df-3 12236  df-4 12237  df-5 12238  df-6 12239  df-7 12240  df-8 12241  df-9 12242  df-n0 12429  df-z 12516  df-dec 12636  df-uz 12780  df-fz 13453  df-struct 17108  df-slot 17143  df-ndx 17155  df-base 17171  df-plusg 17224  df-mulr 17225  df-starv 17226  df-tset 17230  df-ple 17231  df-ds 17233  df-unif 17234  df-cnfld 21348

This theorem is referenced by:  cncrng  21368  cnfld0  21371  cnfld1  21372  cnfldneg  21373  cnfldplusf  21374  cnfldsub  21375  cndrng  21376  cnflddiv  21377  cnfldinv  21378  cnfldmulg  21379  cnfldexp  21380  cnsrng  21381  cnsubmlem  21390  cnsubglem  21391  cnsubrglem  21392  cnsubdrglem  21393  absabv  21399  cnsubrg  21402  cnmgpabl  21403  cnmgpid  21404  cnmsubglem  21405  gzrngunit  21408  gsumfsum  21409  regsumfsum  21410  expmhm  21411  nn0srg  21412  rge0srg  21413  zringbas  21428  zring0  21433  zringunit  21441  expghm  21450  fermltlchr  21504  cnmsgnbas  21553  psgninv  21557  zrhpsgnmhm  21559  rebase  21581  re0g  21587  regsumsupp  21597  cnfldms  24758  cnfldnm  24761  cnfldtopn  24764  cnfldtopon  24765  clmsscn  25064  cnlmod  25125  cnstrcvs  25126  cnrbas  25127  cncvs  25130  cnncvsaddassdemo  25148  cnncvsmulassdemo  25149  cnncvsabsnegdemo  25150  cphsubrglem  25162  cphreccllem  25163  cphdivcl  25167  cphabscl  25170  cphsqrtcl2  25171  cphsqrtcl3  25172  cphipcl  25176  4cphipval2  25227  cncms  25340  cnflduss  25341  cnfldcusp  25342  resscdrg  25343  ishl2  25355  recms  25365  tdeglem3  26042  tdeglem4  26043  tdeglem2  26044  plypf1  26195  dvply2g  26269  dvply2  26270  dvnply  26272  taylfvallem  26341  taylf  26344  tayl0  26345  taylpfval  26348  taylply2  26351  taylply  26352  efgh  26523  efabl  26532  efsubm  26533  jensenlem1  26968  jensenlem2  26969  jensen  26970  amgmlem  26971  amgm  26972  wilthlem2  27050  wilthlem3  27051  dchrelbas2  27218  dchrelbas3  27219  dchrn0  27231  dchrghm  27237  dchrabs  27241  sum2dchr  27255  lgseisenlem4  27359  qrngbas  27600  cchhllem  28973  cffldtocusgr  29534  gsumzrsum  33146  psgnid  33178  cnmsgn0g  33227  altgnsg  33230  1fldgenq  33406  gsumind  33428  xrge0slmod  33431  znfermltl  33449  psrmonprod  33736  esplyfvaln  33758  ccfldsrarelvec  33855  ccfldextdgrr  33856  constrelextdg2  33931  constrextdg2lem  33932  constrext2chnlem  33934  constrcon  33958  constrsdrg  33959  2sqr3minply  33964  cos9thpiminplylem6  33971  cos9thpiminply  33972  iistmd  34086  xrge0iifmhm  34123  xrge0pluscn  34124  zringnm  34142  cnzh  34152  rezh  34153  cnrrext  34194  esumpfinvallem  34258  cnpwstotbnd  38164  repwsmet  38201  rrnequiv  38202  cnsrexpcl  43610  fsumcnsrcl  43611  cnsrplycl  43612  rngunsnply  43614  proot1ex  43641  deg1mhm  43645  amgm2d  44642  amgm3d  44643  amgm4d  44644  binomcxplemdvbinom  44797  binomcxplemnotnn0  44800  sge0tsms  46823  cnfldsrngbas  48652  2zrng0  48735  aacllem  50291  amgmwlem  50292  amgmlemALT  50293  amgmw2d  50294