Theorem cnfldbas 21317

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 21314. (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 11208	. 2 ⊢ ℂ ∈ V
2		cnfldstr 21315	. . 3 ⊢ ℂfld Struct ⟨1, ;13⟩
3		baseid 17229	. . 3 ⊢ Base = Slot (Base‘ndx)
4		snsstp1 4792	. . . 4 ⊢ {⟨(Base‘ndx), ℂ⟩} ⊆ {⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), (𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 + 𝑣))⟩, ⟨(.r‘ndx), (𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))⟩}
5		ssun1 4153	. . . . 5 ⊢ {⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), (𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 + 𝑣))⟩, ⟨(.r‘ndx), (𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))⟩} ⊆ ({⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), (𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 + 𝑣))⟩, ⟨(.r‘ndx), (𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))⟩} ∪ {⟨(*𝑟‘ndx), ∗⟩})
6		ssun1 4153	. . . . . 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 21314	. . . . . 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 4008	. . . . 5 ⊢ ({⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), (𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 + 𝑣))⟩, ⟨(.r‘ndx), (𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))⟩} ∪ {⟨(*𝑟‘ndx), ∗⟩}) ⊆ ℂfld
9	5, 8	sstri 3968	. . . 4 ⊢ {⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), (𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 + 𝑣))⟩, ⟨(.r‘ndx), (𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))⟩} ⊆ ℂfld
10	4, 9	sstri 3968	. . 3 ⊢ {⟨(Base‘ndx), ℂ⟩} ⊆ ℂfld
11	2, 3, 10	strfv 17220	. 2 ⊢ (ℂ ∈ V → ℂ = (Base‘ℂfld))
12	1, 11	ax-mp 5	1 ⊢ ℂ = (Base‘ℂfld)

Syntax hints:   = wceq 1540   ∈ wcel 2108  Vcvv 3459   ∪ cun 3924  {csn 4601  {ctp 4605  ⟨cop 4607   ∘ ccom 5658  ‘cfv 6530  (class class class)co 7403   ∈ cmpo 7405  ℂcc 11125  1c1 11128   + caddc 11130   · cmul 11132   ≤ cle 11268   − cmin 11464  3c3 12294  ;cdc 12706  ∗ccj 15113  abscabs 15251  ndxcnx 17210  Basecbs 17226  +_gcplusg 17269  ._rcmulr 17270  *_𝑟cstv 17271  TopSetcts 17275  lecple 17276  distcds 17278  UnifSetcunif 17279  MetOpencmopn 21303  metUnifcmetu 21304  ℂ_fldccnfld 21313

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pow 5335  ax-pr 5402  ax-un 7727  ax-cnex 11183  ax-resscn 11184  ax-1cn 11185  ax-icn 11186  ax-addcl 11187  ax-addrcl 11188  ax-mulcl 11189  ax-mulrcl 11190  ax-mulcom 11191  ax-addass 11192  ax-mulass 11193  ax-distr 11194  ax-i2m1 11195  ax-1ne0 11196  ax-1rid 11197  ax-rnegex 11198  ax-rrecex 11199  ax-cnre 11200  ax-pre-lttri 11201  ax-pre-lttrn 11202  ax-pre-ltadd 11203  ax-pre-mulgt0 11204

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-ne 2933  df-nel 3037  df-ral 3052  df-rex 3061  df-reu 3360  df-rab 3416  df-v 3461  df-sbc 3766  df-csb 3875  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-pss 3946  df-nul 4309  df-if 4501  df-pw 4577  df-sn 4602  df-pr 4604  df-tp 4606  df-op 4608  df-uni 4884  df-iun 4969  df-br 5120  df-opab 5182  df-mpt 5202  df-tr 5230  df-id 5548  df-eprel 5553  df-po 5561  df-so 5562  df-fr 5606  df-we 5608  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-res 5666  df-ima 5667  df-pred 6290  df-ord 6355  df-on 6356  df-lim 6357  df-suc 6358  df-iota 6483  df-fun 6532  df-fn 6533  df-f 6534  df-f1 6535  df-fo 6536  df-f1o 6537  df-fv 6538  df-riota 7360  df-ov 7406  df-oprab 7407  df-mpo 7408  df-om 7860  df-1st 7986  df-2nd 7987  df-frecs 8278  df-wrecs 8309  df-recs 8383  df-rdg 8422  df-1o 8478  df-er 8717  df-en 8958  df-dom 8959  df-sdom 8960  df-fin 8961  df-pnf 11269  df-mnf 11270  df-xr 11271  df-ltxr 11272  df-le 11273  df-sub 11466  df-neg 11467  df-nn 12239  df-2 12301  df-3 12302  df-4 12303  df-5 12304  df-6 12305  df-7 12306  df-8 12307  df-9 12308  df-n0 12500  df-z 12587  df-dec 12707  df-uz 12851  df-fz 13523  df-struct 17164  df-slot 17199  df-ndx 17211  df-base 17227  df-plusg 17282  df-mulr 17283  df-starv 17284  df-tset 17288  df-ple 17289  df-ds 17291  df-unif 17292  df-cnfld 21314

This theorem is referenced by:  cncrng  21349  cncrngOLD  21350  cnfld0  21353  cnfld1  21354  cnfld1OLD  21355  cnfldneg  21356  cnfldplusf  21357  cnfldsub  21358  cndrng  21359  cndrngOLD  21360  cnflddiv  21361  cnflddivOLD  21362  cnfldinv  21363  cnfldmulg  21364  cnfldexp  21365  cnsrng  21366  cnsubmlem  21380  cnsubglem  21381  cnsubrglem  21382  cnsubrglemOLD  21383  cnsubdrglem  21384  absabv  21390  cnsubrg  21393  cnmgpabl  21394  cnmgpid  21395  cnmsubglem  21396  gzrngunit  21399  gsumfsum  21400  regsumfsum  21401  expmhm  21402  nn0srg  21403  rge0srg  21404  zringbas  21412  zring0  21417  zringunit  21425  expghm  21434  fermltlchr  21488  cnmsgnbas  21536  psgninv  21540  zrhpsgnmhm  21542  rebase  21564  re0g  21570  regsumsupp  21580  cnfldms  24712  cnfldnm  24715  cnfldtopn  24718  cnfldtopon  24719  clmsscn  25028  cnlmod  25089  cnstrcvs  25090  cnrbas  25091  cncvs  25094  cnncvsaddassdemo  25113  cnncvsmulassdemo  25114  cnncvsabsnegdemo  25115  cphsubrglem  25127  cphreccllem  25128  cphdivcl  25132  cphabscl  25135  cphsqrtcl2  25136  cphsqrtcl3  25137  cphipcl  25141  4cphipval2  25192  cncms  25305  cnflduss  25306  cnfldcusp  25307  resscdrg  25308  ishl2  25320  recms  25330  tdeglem3  26014  tdeglem4  26015  tdeglem2  26016  plypf1  26167  dvply2g  26242  dvply2gOLD  26243  dvply2  26244  dvnply  26246  taylfvallem  26315  taylf  26318  tayl0  26319  taylpfval  26322  taylply2  26325  taylply2OLD  26326  taylply  26327  efgh  26500  efabl  26509  efsubm  26510  jensenlem1  26947  jensenlem2  26948  jensen  26949  amgmlem  26950  amgm  26951  wilthlem2  27029  wilthlem3  27030  dchrelbas2  27198  dchrelbas3  27199  dchrn0  27211  dchrghm  27217  dchrabs  27221  sum2dchr  27235  lgseisenlem4  27339  qrngbas  27580  cchhllem  28812  cffldtocusgr  29372  cffldtocusgrOLD  29373  gsumzrsum  32999  psgnid  33054  cnmsgn0g  33103  altgnsg  33106  1fldgenq  33262  xrge0slmod  33309  znfermltl  33327  ccfldsrarelvec  33658  ccfldextdgrr  33659  constrelextdg2  33727  constrextdg2lem  33728  constrext2chnlem  33730  constrcon  33754  constrsdrg  33755  2sqr3minply  33760  cos9thpiminplylem6  33767  cos9thpiminply  33768  iistmd  33879  xrge0iifmhm  33916  xrge0pluscn  33917  zringnm  33935  cnzh  33945  rezh  33946  cnrrext  33987  esumpfinvallem  34051  cnpwstotbnd  37767  repwsmet  37804  rrnequiv  37805  cnsrexpcl  43136  fsumcnsrcl  43137  cnsrplycl  43138  rngunsnply  43140  proot1ex  43167  deg1mhm  43171  amgm2d  44169  amgm3d  44170  amgm4d  44171  binomcxplemdvbinom  44325  binomcxplemnotnn0  44328  sge0tsms  46357  cnfldsrngbas  48084  2zrng0  48167  aacllem  49613  amgmwlem  49614  amgmlemALT  49615  amgmw2d  49616