Definition df-cnfld 14595

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 14597, cnfldadd 14600, cnfldmul 14602, cnfldcj 14603, cnfldtset 14604, cnfldle 14605, cnfldds 14606, and cnfldbas 14598. 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 14594	. 2 class ℂfld
2		cnx 13102	. . . . . . 7 class ndx
3		cbs 13105	. . . . . . 7 class Base
4	2, 3	cfv 5328	. . . . . 6 class ( Base ` ndx )
5		cc 8035	. . . . . 6 class CC
6	4, 5	cop 3673	. . . . 5 class <. ( Base ` ndx ) , CC >.
7		cplusg 13183	. . . . . . 7 class +g
8	2, 7	cfv 5328	. . . . . 6 class ( +g ` ndx )
9		vx	. . . . . . 7 setvar x
10		vy	. . . . . . 7 setvar y
11	9	cv 1396	. . . . . . . 8 class x
12	10	cv 1396	. . . . . . . 8 class y
13		caddc 8040	. . . . . . . 8 class +
14	11, 12, 13	co 6023	. . . . . . 7 class ( x + y )
15	9, 10, 5, 5, 14	cmpo 6025	. . . . . 6 class ( x e. CC , y e. CC |-> ( x + y ) )
16	8, 15	cop 3673	. . . . 5 class <. ( +g ` ndx ) , ( x e. CC , y e. CC |-> ( x + y ) ) >.
17		cmulr 13184	. . . . . . 7 class .r
18	2, 17	cfv 5328	. . . . . 6 class ( .r ` ndx )
19		cmul 8042	. . . . . . . 8 class x.
20	11, 12, 19	co 6023	. . . . . . 7 class ( x x. y )
21	9, 10, 5, 5, 20	cmpo 6025	. . . . . 6 class ( x e. CC , y e. CC |-> ( x x. y ) )
22	18, 21	cop 3673	. . . . 5 class <. ( .r ` ndx ) , ( x e. CC , y e. CC |-> ( x x. y ) ) >.
23	6, 16, 22	ctp 3672	. . . 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 13185	. . . . . . 7 class *r
25	2, 24	cfv 5328	. . . . . 6 class ( *r ` ndx )
26		ccj 11422	. . . . . 6 class *
27	25, 26	cop 3673	. . . . 5 class <. ( *r ` ndx ) , * >.
28	27	csn 3670	. . . 4 class { <. ( *r ` ndx ) , * >. }
29	23, 28	cun 3197	. . 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 13189	. . . . . . 7 class TopSet
31	2, 30	cfv 5328	. . . . . 6 class (TopSet ` ndx )
32		cabs 11580	. . . . . . . 8 class abs
33		cmin 8355	. . . . . . . 8 class -
34	32, 33	ccom 4731	. . . . . . 7 class ( abs o. - )
35		cmopn 14579	. . . . . . 7 class MetOpen
36	34, 35	cfv 5328	. . . . . 6 class ( MetOpen ` ( abs o. - ) )
37	31, 36	cop 3673	. . . . 5 class <. (TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >.
38		cple 13190	. . . . . . 7 class le
39	2, 38	cfv 5328	. . . . . 6 class ( le ` ndx )
40		cle 8220	. . . . . 6 class <_
41	39, 40	cop 3673	. . . . 5 class <. ( le ` ndx ) , <_ >.
42		cds 13192	. . . . . . 7 class dist
43	2, 42	cfv 5328	. . . . . 6 class ( dist ` ndx )
44	43, 34	cop 3673	. . . . 5 class <. ( dist ` ndx ) , ( abs o. - ) >.
45	37, 41, 44	ctp 3672	. . . 4 class { <. (TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. }
46		cunif 13193	. . . . . . 7 class UnifSet
47	2, 46	cfv 5328	. . . . . 6 class ( UnifSet ` ndx )
48		cmetu 14580	. . . . . . 7 class metUnif
49	34, 48	cfv 5328	. . . . . 6 class (metUnif ` ( abs o. - ) )
50	47, 49	cop 3673	. . . . 5 class <. ( UnifSet ` ndx ) , (metUnif ` ( abs o. - ) ) >.
51	50	csn 3670	. . . 4 class { <. ( UnifSet ` ndx ) , (metUnif ` ( abs o. - ) ) >. }
52	45, 51	cun 3197	. . 3 class ( { <. (TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. } u. { <. ( UnifSet ` ndx ) , (metUnif ` ( abs o. - ) ) >. } )
53	29, 52	cun 3197	. 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 1397	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  14596  cnfldbas  14598  mpocnfldadd  14599  mpocnfldmul  14601  cnfldcj  14603  cnfldtset  14604  cnfldle  14605  cnfldds  14606