Definition df-cnfld 14486

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 14488, cnfldadd 14491, cnfldmul 14493, cnfldcj 14494, cnfldtset 14495, cnfldle 14496, cnfldds 14497, and cnfldbas 14489. 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 14485	. 2 class ℂfld
2		cnx 12995	. . . . . . 7 class ndx
3		cbs 12998	. . . . . . 7 class Base
4	2, 3	cfv 5294	. . . . . 6 class ( Base ` ndx )
5		cc 7965	. . . . . 6 class CC
6	4, 5	cop 3649	. . . . 5 class <. ( Base ` ndx ) , CC >.
7		cplusg 13076	. . . . . . 7 class +g
8	2, 7	cfv 5294	. . . . . 6 class ( +g ` ndx )
9		vx	. . . . . . 7 setvar x
10		vy	. . . . . . 7 setvar y
11	9	cv 1374	. . . . . . . 8 class x
12	10	cv 1374	. . . . . . . 8 class y
13		caddc 7970	. . . . . . . 8 class +
14	11, 12, 13	co 5974	. . . . . . 7 class ( x + y )
15	9, 10, 5, 5, 14	cmpo 5976	. . . . . 6 class ( x e. CC , y e. CC |-> ( x + y ) )
16	8, 15	cop 3649	. . . . 5 class <. ( +g ` ndx ) , ( x e. CC , y e. CC |-> ( x + y ) ) >.
17		cmulr 13077	. . . . . . 7 class .r
18	2, 17	cfv 5294	. . . . . 6 class ( .r ` ndx )
19		cmul 7972	. . . . . . . 8 class x.
20	11, 12, 19	co 5974	. . . . . . 7 class ( x x. y )
21	9, 10, 5, 5, 20	cmpo 5976	. . . . . 6 class ( x e. CC , y e. CC |-> ( x x. y ) )
22	18, 21	cop 3649	. . . . 5 class <. ( .r ` ndx ) , ( x e. CC , y e. CC |-> ( x x. y ) ) >.
23	6, 16, 22	ctp 3648	. . . 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 13078	. . . . . . 7 class *r
25	2, 24	cfv 5294	. . . . . 6 class ( *r ` ndx )
26		ccj 11316	. . . . . 6 class *
27	25, 26	cop 3649	. . . . 5 class <. ( *r ` ndx ) , * >.
28	27	csn 3646	. . . 4 class { <. ( *r ` ndx ) , * >. }
29	23, 28	cun 3175	. . 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 13082	. . . . . . 7 class TopSet
31	2, 30	cfv 5294	. . . . . 6 class (TopSet ` ndx )
32		cabs 11474	. . . . . . . 8 class abs
33		cmin 8285	. . . . . . . 8 class -
34	32, 33	ccom 4700	. . . . . . 7 class ( abs o. - )
35		cmopn 14470	. . . . . . 7 class MetOpen
36	34, 35	cfv 5294	. . . . . 6 class ( MetOpen ` ( abs o. - ) )
37	31, 36	cop 3649	. . . . 5 class <. (TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >.
38		cple 13083	. . . . . . 7 class le
39	2, 38	cfv 5294	. . . . . 6 class ( le ` ndx )
40		cle 8150	. . . . . 6 class <_
41	39, 40	cop 3649	. . . . 5 class <. ( le ` ndx ) , <_ >.
42		cds 13085	. . . . . . 7 class dist
43	2, 42	cfv 5294	. . . . . 6 class ( dist ` ndx )
44	43, 34	cop 3649	. . . . 5 class <. ( dist ` ndx ) , ( abs o. - ) >.
45	37, 41, 44	ctp 3648	. . . 4 class { <. (TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. }
46		cunif 13086	. . . . . . 7 class UnifSet
47	2, 46	cfv 5294	. . . . . 6 class ( UnifSet ` ndx )
48		cmetu 14471	. . . . . . 7 class metUnif
49	34, 48	cfv 5294	. . . . . 6 class (metUnif ` ( abs o. - ) )
50	47, 49	cop 3649	. . . . 5 class <. ( UnifSet ` ndx ) , (metUnif ` ( abs o. - ) ) >.
51	50	csn 3646	. . . 4 class { <. ( UnifSet ` ndx ) , (metUnif ` ( abs o. - ) ) >. }
52	45, 51	cun 3175	. . 3 class ( { <. (TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. } u. { <. ( UnifSet ` ndx ) , (metUnif ` ( abs o. - ) ) >. } )
53	29, 52	cun 3175	. 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 1375	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  14487  cnfldbas  14489  mpocnfldadd  14490  mpocnfldmul  14492  cnfldcj  14494  cnfldtset  14495  cnfldle  14496  cnfldds  14497