Theorem cnfldbas 21694

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 21691. (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 11291	. 2 ⊢ ℂ ∈ V
2		cnfldstr 21692	. . 3 ⊢ ℂfld Struct ⟨1, ;13⟩
3		baseid 17402	. . 3 ⊢ Base = Slot (Base‘ndx)
4		snsstp1 4774	. . . 4 ⊢ {⟨(Base‘ndx), ℂ⟩} ⊆ {⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), (𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 + 𝑣))⟩, ⟨(.r‘ndx), (𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))⟩}
5		ssun1 4178	. . . . 5 ⊢ {⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), (𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 + 𝑣))⟩, ⟨(.r‘ndx), (𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))⟩} ⊆ ({⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), (𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 + 𝑣))⟩, ⟨(.r‘ndx), (𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))⟩} ∪ {⟨(*𝑟‘ndx), ∗⟩})
6		ssun1 4178	. . . . . 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 21691	. . . . . 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 3961	. . . . 5 ⊢ ({⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), (𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 + 𝑣))⟩, ⟨(.r‘ndx), (𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))⟩} ∪ {⟨(*𝑟‘ndx), ∗⟩}) ⊆ ℂfld
9	5, 8	sstri 3921	. . . 4 ⊢ {⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), (𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 + 𝑣))⟩, ⟨(.r‘ndx), (𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))⟩} ⊆ ℂfld
10	4, 9	sstri 3921	. . 3 ⊢ {⟨(Base‘ndx), ℂ⟩} ⊆ ℂfld
11	2, 3, 10	strfv 17393	. 2 ⊢ (ℂ ∈ V → ℂ = (Base‘ℂfld))
12	1, 11	ax-mp 5	1 ⊢ ℂ = (Base‘ℂfld)

This proof depends on syntax axioms:   = wceq 1569   ∈ wcel 2146  Vcvv 3453   ∪ cun 4151  {csn 4587  {ctp 4591  ⟨cop 4837   ∘ ccom 5658  ‘cfv 6546  (class class class)co 7427   ∈ cmpo 7429  ℂcc 11208  1c1 11211   + caddc 11213   · cmul 11215   ≤ cle 11354   − cmin 11551  3c3 12408  ;cdc 12824  ∗ccj 15275  abscabs 15413  ndxcnx 17383  Basecbs 17399  +_gcplusg 17440  ._rcmulr 17441  *_𝑟cstv 17442  TopSetcts 17446  lecple 17447  distcds 17449  UnifSetcunif 17450  MetOpencmopn 21680  metUnifcmetu 21681  ℂ_fldccnfld 21690

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2196  ax-12 2215  ax-ext 2735  ax-sep 5251  ax-nul 5262  ax-pow 5330  ax-pr 5394  ax-un 7758  ax-cnex 11266  ax-resscn 11267  ax-1cn 11268  ax-icn 11269  ax-addcl 11270  ax-addrcl 11271  ax-mulcl 11272  ax-mulrcl 11273  ax-mulcom 11274  ax-addass 11275  ax-mulass 11276  ax-distr 11277  ax-i2m1 11278  ax-1ne0 11279  ax-1rid 11280  ax-rnegex 11281  ax-rrecex 11282  ax-cnre 11283  ax-pre-lttri 11284  ax-pre-lttrn 11285  ax-pre-ltadd 11286  ax-pre-mulgt0 11287

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2101  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-nel 3065  df-ral 3080  df-rex 3090  df-reu 3369  df-rab 3416  df-v 3455  df-sbc 3742  df-csb 3851  df-ss 3900  df-pss 4016  df-dif 4049  df-in 4093  df-un 4153  df-nul 4281  df-if 4485  df-pw 4561  df-sn 4588  df-pr 4590  df-tp 4592  df-op 4838  df-uni 4870  df-iun 4955  df-br 5106  df-opab 5170  df-mpt 5189  df-tr 5215  df-id 5549  df-eprel 5554  df-po 5562  df-so 5563  df-fr 5607  df-we 5609  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 6310  df-ord 6371  df-on 6372  df-lim 6373  df-suc 6374  df-iota 6500  df-fun 6548  df-fn 6549  df-f 6550  df-f1 6551  df-fo 6552  df-f1o 6553  df-fv 6554  df-riota 7384  df-ov 7430  df-oprab 7431  df-mpo 7432  df-om 7885  df-1st 8008  df-2nd 8009  df-frecs 8310  df-wrecs 8341  df-recs 8390  df-rdg 8429  df-1o 8487  df-er 8728  df-en 8985  df-dom 8986  df-sdom 8987  df-fin 8988  df-pnf 11355  df-mnf 11356  df-xr 11357  df-ltxr 11358  df-le 11359  df-sub 11553  df-neg 11554  df-nn 12346  df-2 12415  df-3 12416  df-4 12417  df-5 12418  df-6 12419  df-7 12420  df-8 12421  df-9 12422  df-n0 12617  df-z 12704  df-dec 12825  df-uz 12976  df-fz 13650  df-struct 17337  df-slot 17372  df-ndx 17384  df-base 17400  df-plusg 17453  df-mulr 17454  df-starv 17455  df-tset 17459  df-ple 17460  df-ds 17462  df-unif 17463  df-cnfld 21691

This theorem is used by:  cncrng  21711  cnfld0  21714  cnfld1  21715  cnfldneg  21716  cnfldplusf  21717  cnfldsub  21718  cndrng  21719  cnflddiv  21720  cnfldinv  21721  cnfldmulg  21722  cnfldexp  21723  cnsrng  21724  cnsubmlem  21733  cnsubglem  21734  cnsubrglem  21735  cnsubdrglem  21736  absabv  21742  cnsubrg  21745  cnmgpabl  21746  cnmgpid  21747  cnmsubglem  21748  gzrngunit  21751  gsumfsum  21752  regsumfsum  21753  expmhm  21754  nn0srg  21755  rge0srg  21756  zringbas  21771  zring0  21776  zringunit  21784  expghm  21793  fermltlchr  21847  cnmsgnbas  21896  psgninv  21900  zrhpsgnmhm  21902  rebase  21924  re0g  21930  regsumsupp  21940  cnfldms  25106  cnfldnm  25109  cnfldtopn  25112  cnfldtopon  25113  clmsscn  25412  cnlmod  25473  cnstrcvs  25474  cnrbas  25475  cncvs  25478  cnncvsaddassdemo  25496  cnncvsmulassdemo  25497  cnncvsabsnegdemo  25498  cphsubrglem  25510  cphreccllem  25511  cphdivcl  25515  cphabscl  25518  cphsqrtcl2  25519  cphsqrtcl3  25520  cphipcl  25524  4cphipval2  25575  cncms  25688  cnflduss  25689  cnfldcusp  25690  resscdrg  25691  ishl2  25703  recms  25713  tdeglem3  26389  tdeglem4  26390  tdeglem2  26391  plypf1  26543  dvply2g  26618  dvply2  26619  dvnply  26621  taylfvallem  26697  taylf  26700  tayl0  26701  taylpfval  26704  taylply2  26707  taylply  26708  efgh  26881  efabl  26890  efsubm  26891  jensenlem1  27326  jensenlem2  27327  jensen  27328  amgmlem  27329  amgm  27330  wilthlem2  27408  wilthlem3  27409  dchrelbas2  27576  dchrelbas3  27577  dchrn0  27589  dchrghm  27595  dchrabs  27599  sum2dchr  27613  lgseisenlem4  27717  qrngbas  27958  cchhllem  29476  cffldtocusgr  30040  gsumzrsum  33679  psgnid  33711  cnmsgn0g  33760  altgnsg  33763  1fldgenq  33937  gsumind  33959  xrge0slmod  33962  znfermltl  33975  psrmonprod  34237  esplyfvaln  34259  ccfldsrarelvec  34356  ccfldextdgrr  34357  constrelextdg2  34432  constrextdg2lem  34433  constrext2chnlem  34435  constrcon  34459  constrsdrg  34460  2sqr3minply  34465  cos9thpiminplylem6  34472  cos9thpiminply  34473  iistmd  34587  xrge0iifmhm  34624  xrge0pluscn  34625  zringnm  34643  cnzh  34653  rezh  34654  cnrrext  34695  esumpfinvallem  34759  cnpwstotbnd  38871  repwsmet  38908  rrnequiv  38909  cnsrexpcl  44307  fsumcnsrcl  44308  cnsrplycl  44309  rngunsnply  44311  proot1ex  44338  deg1mhm  44342  amgm2d  45338  amgm3d  45339  amgm4d  45340  binomcxplemdvbinom  45477  binomcxplemnotnn0  45480  sge0tsms  47529  cnfldsrngbas  49397  2zrng0  49480  aacllem  51153  amgmwlem  51201  amgmlemALT  51202  amgmw2d  51203