Definition df-icnfld 14048

Description: The field of complex numbers. Other number fields and rings can be constructed by applying the ↾_s restriction operator.

The contract of this set is defined entirely by cnfldex 14050, cnfldadd 14052, cnfldmul 14054, cnfldcj 14056, and cnfldbas 14051.

We may add additional members to this in the future.

At least for now, this structure does not include a topology, order, a distance function, or function mapping metrics.

(Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Thierry Arnoux, 15-Dec-2017.) (New usage is discouraged.)

Assertion

Ref	Expression
df-icnfld	⊢ ℂfld = ({⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), · ⟩} ∪ {⟨(*𝑟‘ndx), ∗⟩})

Detailed syntax breakdown of Definition df-icnfld

Step	Hyp	Ref	Expression
1		ccnfld 14047	. 2 class ℂfld
2		cnx 12615	. . . . . 6 class ndx
3		cbs 12618	. . . . . 6 class Base
4	2, 3	cfv 5254	. . . . 5 class (Base‘ndx)
5		cc 7870	. . . . 5 class ℂ
6	4, 5	cop 3621	. . . 4 class ⟨(Base‘ndx), ℂ⟩
7		cplusg 12695	. . . . . 6 class +g
8	2, 7	cfv 5254	. . . . 5 class (+g‘ndx)
9		caddc 7875	. . . . 5 class +
10	8, 9	cop 3621	. . . 4 class ⟨(+g‘ndx), + ⟩
11		cmulr 12696	. . . . . 6 class .r
12	2, 11	cfv 5254	. . . . 5 class (.r‘ndx)
13		cmul 7877	. . . . 5 class ·
14	12, 13	cop 3621	. . . 4 class ⟨(.r‘ndx), · ⟩
15	6, 10, 14	ctp 3620	. . 3 class {⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), · ⟩}
16		cstv 12697	. . . . . 6 class *𝑟
17	2, 16	cfv 5254	. . . . 5 class (*𝑟‘ndx)
18		ccj 10983	. . . . 5 class ∗
19	17, 18	cop 3621	. . . 4 class ⟨(*𝑟‘ndx), ∗⟩
20	19	csn 3618	. . 3 class {⟨(*𝑟‘ndx), ∗⟩}
21	15, 20	cun 3151	. 2 class ({⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), · ⟩} ∪ {⟨(*𝑟‘ndx), ∗⟩})
22	1, 21	wceq 1364	1 wff ℂfld = ({⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), · ⟩} ∪ {⟨(*𝑟‘ndx), ∗⟩})

This definition is referenced by:  cnfldstr  14049  cnfldbas  14051  cnfldadd  14052  cnfldmul  14054  cnfldcj  14056