Definition df-cnfld 14692

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 14694, cnfldadd 14697, cnfldmul 14699, cnfldcj 14700, cnfldtset 14701, cnfldle 14702, cnfldds 14703, and cnfldbas 14695. 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.)

Assertion

Ref	Expression
df-cnfld	|- ℂfld = ( ( { <. ( 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. - ) ) >. } ) )

Distinct variable group:   x, y

Detailed syntax breakdown of Definition df-cnfld

Step	Hyp	Ref	Expression
1		ccnfld 14691	. 2 class ℂfld
2		cnx 13198	. . . . . . 7 class ndx
3		cbs 13201	. . . . . . 7 class Base
4	2, 3	cfv 5351	. . . . . 6 class ( Base ` ndx )
5		cc 8121	. . . . . 6 class CC
6	4, 5	cop 3691	. . . . 5 class <. ( Base ` ndx ) , CC >.
7		cplusg 13279	. . . . . . 7 class +g
8	2, 7	cfv 5351	. . . . . 6 class ( +g ` ndx )
9		vx	. . . . . . 7 setvar x
10		vy	. . . . . . 7 setvar y
11	9	cv 1397	. . . . . . . 8 class x
12	10	cv 1397	. . . . . . . 8 class y
13		caddc 8126	. . . . . . . 8 class +
14	11, 12, 13	co 6049	. . . . . . 7 class ( x + y )
15	9, 10, 5, 5, 14	cmpo 6051	. . . . . 6 class ( x e. CC , y e. CC |-> ( x + y ) )
16	8, 15	cop 3691	. . . . 5 class <. ( +g ` ndx ) , ( x e. CC , y e. CC |-> ( x + y ) ) >.
17		cmulr 13280	. . . . . . 7 class .r
18	2, 17	cfv 5351	. . . . . 6 class ( .r ` ndx )
19		cmul 8128	. . . . . . . 8 class x.
20	11, 12, 19	co 6049	. . . . . . 7 class ( x x. y )
21	9, 10, 5, 5, 20	cmpo 6051	. . . . . 6 class ( x e. CC , y e. CC |-> ( x x. y ) )
22	18, 21	cop 3691	. . . . 5 class <. ( .r ` ndx ) , ( x e. CC , y e. CC |-> ( x x. y ) ) >.
23	6, 16, 22	ctp 3690	. . . 4 class { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , ( x e. CC , y e. CC |-> ( x + y ) ) >. , <. ( .r ` ndx ) , ( x e. CC , y e. CC |-> ( x x. y ) ) >. }
24		cstv 13281	. . . . . . 7 class *r
25	2, 24	cfv 5351	. . . . . 6 class ( *r ` ndx )
26		ccj 11517	. . . . . 6 class *
27	25, 26	cop 3691	. . . . 5 class <. ( *r ` ndx ) , * >.
28	27	csn 3688	. . . 4 class { <. ( *r ` ndx ) , * >. }
29	23, 28	cun 3208	. . 3 class ( { <. ( 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 ) , * >. } )
30		cts 13285	. . . . . . 7 class TopSet
31	2, 30	cfv 5351	. . . . . 6 class (TopSet ` ndx )
32		cabs 11675	. . . . . . . 8 class abs
33		cmin 8440	. . . . . . . 8 class -
34	32, 33	ccom 4752	. . . . . . 7 class ( abs o. - )
35		cmopn 14676	. . . . . . 7 class MetOpen
36	34, 35	cfv 5351	. . . . . 6 class ( MetOpen ` ( abs o. - ) )
37	31, 36	cop 3691	. . . . 5 class <. (TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >.
38		cple 13286	. . . . . . 7 class le
39	2, 38	cfv 5351	. . . . . 6 class ( le ` ndx )
40		cle 8305	. . . . . 6 class <_
41	39, 40	cop 3691	. . . . 5 class <. ( le ` ndx ) , <_ >.
42		cds 13288	. . . . . . 7 class dist
43	2, 42	cfv 5351	. . . . . 6 class ( dist ` ndx )
44	43, 34	cop 3691	. . . . 5 class <. ( dist ` ndx ) , ( abs o. - ) >.
45	37, 41, 44	ctp 3690	. . . 4 class { <. (TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. }
46		cunif 13289	. . . . . . 7 class UnifSet
47	2, 46	cfv 5351	. . . . . 6 class ( UnifSet ` ndx )
48		cmetu 14677	. . . . . . 7 class metUnif
49	34, 48	cfv 5351	. . . . . 6 class (metUnif ` ( abs o. - ) )
50	47, 49	cop 3691	. . . . 5 class <. ( UnifSet ` ndx ) , (metUnif ` ( abs o. - ) ) >.
51	50	csn 3688	. . . 4 class { <. ( UnifSet ` ndx ) , (metUnif ` ( abs o. - ) ) >. }
52	45, 51	cun 3208	. . 3 class ( { <. (TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. } u. { <. ( UnifSet ` ndx ) , (metUnif ` ( abs o. - ) ) >. } )
53	29, 52	cun 3208	. 2 class ( ( { <. ( 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. - ) ) >. } ) )
54	1, 53	wceq 1398	1 wff ℂfld = ( ( { <. ( 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. - ) ) >. } ) )

This definition is referenced by:  cnfldstr  14693  cnfldbas  14695  mpocnfldadd  14696  mpocnfldmul  14698  cnfldcj  14700  cnfldtset  14701  cnfldle  14702  cnfldds  14703