Definition df-cnfld 21349

Description: The field of complex numbers. Other number fields and rings can be constructed by applying the ↾_s restriction operator, for instance (ℂ_fld ↾ 𝔸) is the field of algebraic numbers.

The contract of this set is defined entirely by cnfldex 21351, cnfldadd 21354, cnfldmul 21356, cnfldcj 21357, cnfldtset 21358, cnfldle 21359, cnfldds 21360, and cnfldbas 21352. We may add additional members to this in the future. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Thierry Arnoux, 15-Dec-2017.) Use maps-to notation for addition and multiplication. (Revised by GG, 31-Mar-2025.) (New usage is discouraged.)

Assertion

Ref	Expression
df-cnfld	⊢ ℂfld = (({⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))⟩, ⟨(.r‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))⟩} ∪ {⟨(*𝑟‘ndx), ∗⟩}) ∪ ({⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ − )⟩} ∪ {⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩}))

Distinct variable group:   𝑥,𝑦

Detailed syntax breakdown of Definition df-cnfld

Step	Hyp	Ref	Expression
1		ccnfld 21348	. 2 class ℂfld
2		cnx 17155	. . . . . . 7 class ndx
3		cbs 17171	. . . . . . 7 class Base
4	2, 3	cfv 6486	. . . . . 6 class (Base‘ndx)
5		cc 11028	. . . . . 6 class ℂ
6	4, 5	cop 4562	. . . . 5 class ⟨(Base‘ndx), ℂ⟩
7		cplusg 17212	. . . . . . 7 class +g
8	2, 7	cfv 6486	. . . . . 6 class (+g‘ndx)
9		vx	. . . . . . 7 setvar 𝑥
10		vy	. . . . . . 7 setvar 𝑦
11	9	cv 1546	. . . . . . . 8 class 𝑥
12	10	cv 1546	. . . . . . . 8 class 𝑦
13		caddc 11033	. . . . . . . 8 class +
14	11, 12, 13	co 7357	. . . . . . 7 class (𝑥 + 𝑦)
15	9, 10, 5, 5, 14	cmpo 7359	. . . . . 6 class (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))
16	8, 15	cop 4562	. . . . 5 class ⟨(+g‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))⟩
17		cmulr 17213	. . . . . . 7 class .r
18	2, 17	cfv 6486	. . . . . 6 class (.r‘ndx)
19		cmul 11035	. . . . . . . 8 class ·
20	11, 12, 19	co 7357	. . . . . . 7 class (𝑥 · 𝑦)
21	9, 10, 5, 5, 20	cmpo 7359	. . . . . 6 class (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))
22	18, 21	cop 4562	. . . . 5 class ⟨(.r‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))⟩
23	6, 16, 22	ctp 4560	. . . 4 class {⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))⟩, ⟨(.r‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))⟩}
24		cstv 17214	. . . . . . 7 class *𝑟
25	2, 24	cfv 6486	. . . . . 6 class (*𝑟‘ndx)
26		ccj 15050	. . . . . 6 class ∗
27	25, 26	cop 4562	. . . . 5 class ⟨(*𝑟‘ndx), ∗⟩
28	27	csn 4556	. . . 4 class {⟨(*𝑟‘ndx), ∗⟩}
29	23, 28	cun 3881	. . 3 class ({⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))⟩, ⟨(.r‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))⟩} ∪ {⟨(*𝑟‘ndx), ∗⟩})
30		cts 17218	. . . . . . 7 class TopSet
31	2, 30	cfv 6486	. . . . . 6 class (TopSet‘ndx)
32		cabs 15188	. . . . . . . 8 class abs
33		cmin 11369	. . . . . . . 8 class −
34	32, 33	ccom 5623	. . . . . . 7 class (abs ∘ − )
35		cmopn 21338	. . . . . . 7 class MetOpen
36	34, 35	cfv 6486	. . . . . 6 class (MetOpen‘(abs ∘ − ))
37	31, 36	cop 4562	. . . . 5 class ⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩
38		cple 17219	. . . . . . 7 class le
39	2, 38	cfv 6486	. . . . . 6 class (le‘ndx)
40		cle 11172	. . . . . 6 class ≤
41	39, 40	cop 4562	. . . . 5 class ⟨(le‘ndx), ≤ ⟩
42		cds 17221	. . . . . . 7 class dist
43	2, 42	cfv 6486	. . . . . 6 class (dist‘ndx)
44	43, 34	cop 4562	. . . . 5 class ⟨(dist‘ndx), (abs ∘ − )⟩
45	37, 41, 44	ctp 4560	. . . 4 class {⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ − )⟩}
46		cunif 17222	. . . . . . 7 class UnifSet
47	2, 46	cfv 6486	. . . . . 6 class (UnifSet‘ndx)
48		cmetu 21339	. . . . . . 7 class metUnif
49	34, 48	cfv 6486	. . . . . 6 class (metUnif‘(abs ∘ − ))
50	47, 49	cop 4562	. . . . 5 class ⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩
51	50	csn 4556	. . . 4 class {⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩}
52	45, 51	cun 3881	. . 3 class ({⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ − )⟩} ∪ {⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩})
53	29, 52	cun 3881	. 2 class (({⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))⟩, ⟨(.r‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))⟩} ∪ {⟨(*𝑟‘ndx), ∗⟩}) ∪ ({⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ − )⟩} ∪ {⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩}))
54	1, 53	wceq 1547	1 wff ℂfld = (({⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))⟩, ⟨(.r‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))⟩} ∪ {⟨(*𝑟‘ndx), ∗⟩}) ∪ ({⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ − )⟩} ∪ {⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩}))

This definition is referenced by:  cnfldstr  21350  cnfldex  21351  cnfldbas  21352  mpocnfldadd  21353  mpocnfldmul  21355  cnfldcj  21357  cnfldtset  21358  cnfldle  21359  cnfldds  21360  cnfldunif  21361  cnfldfun  21362  cnfldfunALT  21363  cffldtocusgr  29535