Definition df-icnfld 13795

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 13797, cnfldadd 13799, cnfldmul 13800, cnfldcj 13801, and cnfldbas 13798.

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 13794	. 2 class ℂfld
2		cnx 12473	. . . . . 6 class ndx
3		cbs 12476	. . . . . 6 class Base
4	2, 3	cfv 5228	. . . . 5 class (Base‘ndx)
5		cc 7823	. . . . 5 class ℂ
6	4, 5	cop 3607	. . . 4 class ⟨(Base‘ndx), ℂ⟩
7		cplusg 12551	. . . . . 6 class +g
8	2, 7	cfv 5228	. . . . 5 class (+g‘ndx)
9		caddc 7828	. . . . 5 class +
10	8, 9	cop 3607	. . . 4 class ⟨(+g‘ndx), + ⟩
11		cmulr 12552	. . . . . 6 class .r
12	2, 11	cfv 5228	. . . . 5 class (.r‘ndx)
13		cmul 7830	. . . . 5 class ·
14	12, 13	cop 3607	. . . 4 class ⟨(.r‘ndx), · ⟩
15	6, 10, 14	ctp 3606	. . 3 class {⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), · ⟩}
16		cstv 12553	. . . . . 6 class *𝑟
17	2, 16	cfv 5228	. . . . 5 class (*𝑟‘ndx)
18		ccj 10862	. . . . 5 class ∗
19	17, 18	cop 3607	. . . 4 class ⟨(*𝑟‘ndx), ∗⟩
20	19	csn 3604	. . 3 class {⟨(*𝑟‘ndx), ∗⟩}
21	15, 20	cun 3139	. 2 class ({⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), · ⟩} ∪ {⟨(*𝑟‘ndx), ∗⟩})
22	1, 21	wceq 1363	1 wff ℂfld = ({⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), · ⟩} ∪ {⟨(*𝑟‘ndx), ∗⟩})

This definition is referenced by:  cnfldstr  13796  cnfldbas  13798  cnfldadd  13799  cnfldmul  13800  cnfldcj  13801