Definition df-icnfld 13738

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 13740, cnfldadd 13742, cnfldmul 13743, cnfldcj 13744, and cnfldbas 13741.

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 ) , CC >. , <. ( +g ` ndx ) , + >. , <. ( .r ` ndx ) , x. >. } u. { <. ( *r ` ndx ) , * >. } )

Detailed syntax breakdown of Definition df-icnfld

Step	Hyp	Ref	Expression
1		ccnfld 13737	. 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 CC
6	4, 5	cop 3607	. . . 4 class <. ( Base ` ndx ) , CC >.
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 x.
14	12, 13	cop 3607	. . . 4 class <. ( .r ` ndx ) , x. >.
15	6, 10, 14	ctp 3606	. . 3 class { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , + >. , <. ( .r ` ndx ) , x. >. }
16		cstv 12553	. . . . . 6 class *r
17	2, 16	cfv 5228	. . . . 5 class ( *r ` ndx )
18		ccj 10862	. . . . 5 class *
19	17, 18	cop 3607	. . . 4 class <. ( *r ` ndx ) , * >.
20	19	csn 3604	. . 3 class { <. ( *r ` ndx ) , * >. }
21	15, 20	cun 3139	. 2 class ( { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , + >. , <. ( .r ` ndx ) , x. >. } u. { <. ( *r ` ndx ) , * >. } )
22	1, 21	wceq 1363	1 wff ℂfld = ( { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , + >. , <. ( .r ` ndx ) , x. >. } u. { <. ( *r ` ndx ) , * >. } )

This definition is referenced by:  cnfldstr  13739  cnfldbas  13741  cnfldadd  13742  cnfldmul  13743  cnfldcj  13744