Definition df-cnfld

Description: The field of complex numbers. Other number fields and rings can be constructed by applying the ` |``s restriction operator, for instance ( CCfld |`AA ) is the field of algebraic numbers.

The contract of this set is defined entirely by cnfldex , cnfldadd , cnfldmul , cnfldcj , cnfldtset , cnfldle , cnfldds , and cnfldbas . We may add additional members to this in the future. (Contributed by Stefan O'Rear, 27-Nov-2014) (Revised by Thierry Arnoux, 15-Dec-2017) Use maps-to notation for addition and multiplication. (Revised by GG, 31-Mar-2025) (New usage is discouraged.)

	Ref	Expression
Assertion	df-cnfld	|- CCfld = ( ( { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , ( x e. CC , y e. CC |-> ( x + y ) ) >. , <. ( .r ` ndx ) , ( x e. CC , y e. CC |-> ( x x. y ) ) >. } u. { <. ( *r ` ndx ) , * >. } ) u. ( { <. ( TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. } u. { <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >. } ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccnfld	|- CCfld
1		cbs	|- Base
2		cnx	|- ndx
3	2 1	cfv	|- ( Base ` ndx )
4		cc	|- CC
5	3 4	cop	|- <. ( Base ` ndx ) , CC >.
6		cplusg	|- +g
7	2 6	cfv	|- ( +g ` ndx )
8		vx	|- x
9		vy	|- y
10	8	cv	|- x
11		caddc	|- +
12	9	cv	|- y
13	10 12 11	co	|- ( x + y )
14	8 9 4 4 13	cmpo	|- ( x e. CC , y e. CC |-> ( x + y ) )
15	7 14	cop	|- <. ( +g ` ndx ) , ( x e. CC , y e. CC |-> ( x + y ) ) >.
16		cmulr	|- .r
17	2 16	cfv	|- ( .r ` ndx )
18		cmul	|- x.
19	10 12 18	co	|- ( x x. y )
20	8 9 4 4 19	cmpo	|- ( x e. CC , y e. CC |-> ( x x. y ) )
21	17 20	cop	|- <. ( .r ` ndx ) , ( x e. CC , y e. CC |-> ( x x. y ) ) >.
22	5 15 21	ctp	|- { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , ( x e. CC , y e. CC |-> ( x + y ) ) >. , <. ( .r ` ndx ) , ( x e. CC , y e. CC |-> ( x x. y ) ) >. }
23		cstv	|- *r
24	2 23	cfv	|- ( *r ` ndx )
25		ccj	|- *
26	24 25	cop	|- <. ( *r ` ndx ) , * >.
27	26	csn	|- { <. ( *r ` ndx ) , * >. }
28	22 27	cun	|- ( { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , ( x e. CC , y e. CC |-> ( x + y ) ) >. , <. ( .r ` ndx ) , ( x e. CC , y e. CC |-> ( x x. y ) ) >. } u. { <. ( *r ` ndx ) , * >. } )
29		cts	|- TopSet
30	2 29	cfv	|- ( TopSet ` ndx )
31		cmopn	|- MetOpen
32		cabs	|- abs
33		cmin	|- -
34	32 33	ccom	|- ( abs o. - )
35	34 31	cfv	|- ( MetOpen ` ( abs o. - ) )
36	30 35	cop	|- <. ( TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >.
37		cple	|- le
38	2 37	cfv	|- ( le ` ndx )
39		cle	|- <_
40	38 39	cop	|- <. ( le ` ndx ) , <_ >.
41		cds	|- dist
42	2 41	cfv	|- ( dist ` ndx )
43	42 34	cop	|- <. ( dist ` ndx ) , ( abs o. - ) >.
44	36 40 43	ctp	|- { <. ( TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. }
45		cunif	|- UnifSet
46	2 45	cfv	|- ( UnifSet ` ndx )
47		cmetu	|- metUnif
48	34 47	cfv	|- ( metUnif ` ( abs o. - ) )
49	46 48	cop	|- <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >.
50	49	csn	|- { <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >. }
51	44 50	cun	|- ( { <. ( TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. } u. { <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >. } )
52	28 51	cun	|- ( ( { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , ( x e. CC , y e. CC |-> ( x + y ) ) >. , <. ( .r ` ndx ) , ( x e. CC , y e. CC |-> ( x x. y ) ) >. } u. { <. ( *r ` ndx ) , * >. } ) u. ( { <. ( TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. } u. { <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >. } ) )
53	0 52	wceq	|- CCfld = ( ( { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , ( x e. CC , y e. CC |-> ( x + y ) ) >. , <. ( .r ` ndx ) , ( x e. CC , y e. CC |-> ( x x. y ) ) >. } u. { <. ( *r ` ndx ) , * >. } ) u. ( { <. ( TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. } u. { <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >. } ) )