Definition df-icnfld 13541

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 13543, cnfldadd 13545, cnfldmul 13546, cnfldcj 13547, and cnfldbas 13544.

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 13540	. 2 class ℂfld
2		cnx 12461	. . . . . 6 class ndx
3		cbs 12464	. . . . . 6 class Base
4	2, 3	cfv 5218	. . . . 5 class ( Base ` ndx )
5		cc 7811	. . . . 5 class CC
6	4, 5	cop 3597	. . . 4 class <. ( Base ` ndx ) , CC >.
7		cplusg 12538	. . . . . 6 class +g
8	2, 7	cfv 5218	. . . . 5 class ( +g ` ndx )
9		caddc 7816	. . . . 5 class +
10	8, 9	cop 3597	. . . 4 class <. ( +g ` ndx ) , + >.
11		cmulr 12539	. . . . . 6 class .r
12	2, 11	cfv 5218	. . . . 5 class ( .r ` ndx )
13		cmul 7818	. . . . 5 class x.
14	12, 13	cop 3597	. . . 4 class <. ( .r ` ndx ) , x. >.
15	6, 10, 14	ctp 3596	. . 3 class { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , + >. , <. ( .r ` ndx ) , x. >. }
16		cstv 12540	. . . . . 6 class *r
17	2, 16	cfv 5218	. . . . 5 class ( *r ` ndx )
18		ccj 10850	. . . . 5 class *
19	17, 18	cop 3597	. . . 4 class <. ( *r ` ndx ) , * >.
20	19	csn 3594	. . 3 class { <. ( *r ` ndx ) , * >. }
21	15, 20	cun 3129	. 2 class ( { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , + >. , <. ( .r ` ndx ) , x. >. } u. { <. ( *r ` ndx ) , * >. } )
22	1, 21	wceq 1353	1 wff ℂfld = ( { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , + >. , <. ( .r ` ndx ) , x. >. } u. { <. ( *r ` ndx ) , * >. } )

This definition is referenced by:  cnfldstr  13542  cnfldbas  13544  cnfldadd  13545  cnfldmul  13546  cnfldcj  13547