Definition df-icnfld 13325

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 13327, cnfldadd 13329, cnfldmul 13330, cnfldcj 13331, and cnfldbas 13328.

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 13324	. 2 class ℂfld
2		cnx 12451	. . . . . 6 class ndx
3		cbs 12454	. . . . . 6 class Base
4	2, 3	cfv 5215	. . . . 5 class (Base‘ndx)
5		cc 7806	. . . . 5 class ℂ
6	4, 5	cop 3595	. . . 4 class ⟨(Base‘ndx), ℂ⟩
7		cplusg 12528	. . . . . 6 class +g
8	2, 7	cfv 5215	. . . . 5 class (+g‘ndx)
9		caddc 7811	. . . . 5 class +
10	8, 9	cop 3595	. . . 4 class ⟨(+g‘ndx), + ⟩
11		cmulr 12529	. . . . . 6 class .r
12	2, 11	cfv 5215	. . . . 5 class (.r‘ndx)
13		cmul 7813	. . . . 5 class ·
14	12, 13	cop 3595	. . . 4 class ⟨(.r‘ndx), · ⟩
15	6, 10, 14	ctp 3594	. . 3 class {⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), · ⟩}
16		cstv 12530	. . . . . 6 class *𝑟
17	2, 16	cfv 5215	. . . . 5 class (*𝑟‘ndx)
18		ccj 10841	. . . . 5 class ∗
19	17, 18	cop 3595	. . . 4 class ⟨(*𝑟‘ndx), ∗⟩
20	19	csn 3592	. . 3 class {⟨(*𝑟‘ndx), ∗⟩}
21	15, 20	cun 3127	. 2 class ({⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), · ⟩} ∪ {⟨(*𝑟‘ndx), ∗⟩})
22	1, 21	wceq 1353	1 wff ℂfld = ({⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), · ⟩} ∪ {⟨(*𝑟‘ndx), ∗⟩})

This definition is referenced by:  cnfldstr  13326  cnfldbas  13328  cnfldadd  13329  cnfldmul  13330  cnfldcj  13331