Definition df-icnfld 13596

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 13598, cnfldadd 13600, cnfldmul 13601, cnfldcj 13602, and cnfldbas 13599.

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 13595	. 2 class ℂfld
2		cnx 12462	. . . . . 6 class ndx
3		cbs 12465	. . . . . 6 class Base
4	2, 3	cfv 5218	. . . . 5 class (Base‘ndx)
5		cc 7812	. . . . 5 class ℂ
6	4, 5	cop 3597	. . . 4 class ⟨(Base‘ndx), ℂ⟩
7		cplusg 12539	. . . . . 6 class +g
8	2, 7	cfv 5218	. . . . 5 class (+g‘ndx)
9		caddc 7817	. . . . 5 class +
10	8, 9	cop 3597	. . . 4 class ⟨(+g‘ndx), + ⟩
11		cmulr 12540	. . . . . 6 class .r
12	2, 11	cfv 5218	. . . . 5 class (.r‘ndx)
13		cmul 7819	. . . . 5 class ·
14	12, 13	cop 3597	. . . 4 class ⟨(.r‘ndx), · ⟩
15	6, 10, 14	ctp 3596	. . 3 class {⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), · ⟩}
16		cstv 12541	. . . . . 6 class *𝑟
17	2, 16	cfv 5218	. . . . 5 class (*𝑟‘ndx)
18		ccj 10851	. . . . 5 class ∗
19	17, 18	cop 3597	. . . 4 class ⟨(*𝑟‘ndx), ∗⟩
20	19	csn 3594	. . 3 class {⟨(*𝑟‘ndx), ∗⟩}
21	15, 20	cun 3129	. 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  13597  cnfldbas  13599  cnfldadd  13600  cnfldmul  13601  cnfldcj  13602