Definition df-cnfld 14834

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 14836, cnfldadd 14839, cnfldmul 14841, cnfldcj 14842, cnfldtset 14843, cnfldle 14844, cnfldds 14845, and cnfldbas 14837. 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 14833	. 2 class ℂfld
2		cnx 13296	. . . . . . 7 class ndx
3		cbs 13299	. . . . . . 7 class Base
4	2, 3	cfv 5357	. . . . . 6 class ( Base ` ndx )
5		cc 8141	. . . . . 6 class CC
6	4, 5	cop 3697	. . . . 5 class <. ( Base ` ndx ) , CC >.
7		cplusg 13377	. . . . . . 7 class +g
8	2, 7	cfv 5357	. . . . . 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 8146	. . . . . . . 8 class +
14	11, 12, 13	co 6058	. . . . . . 7 class ( x + y )
15	9, 10, 5, 5, 14	cmpo 6060	. . . . . 6 class ( x e. CC , y e. CC |-> ( x + y ) )
16	8, 15	cop 3697	. . . . 5 class <. ( +g ` ndx ) , ( x e. CC , y e. CC |-> ( x + y ) ) >.
17		cmulr 13378	. . . . . . 7 class .r
18	2, 17	cfv 5357	. . . . . 6 class ( .r ` ndx )
19		cmul 8148	. . . . . . . 8 class x.
20	11, 12, 19	co 6058	. . . . . . 7 class ( x x. y )
21	9, 10, 5, 5, 20	cmpo 6060	. . . . . 6 class ( x e. CC , y e. CC |-> ( x x. y ) )
22	18, 21	cop 3697	. . . . 5 class <. ( .r ` ndx ) , ( x e. CC , y e. CC |-> ( x x. y ) ) >.
23	6, 16, 22	ctp 3696	. . . 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 13379	. . . . . . 7 class *r
25	2, 24	cfv 5357	. . . . . 6 class ( *r ` ndx )
26		ccj 11552	. . . . . 6 class *
27	25, 26	cop 3697	. . . . 5 class <. ( *r ` ndx ) , * >.
28	27	csn 3694	. . . 4 class { <. ( *r ` ndx ) , * >. }
29	23, 28	cun 3212	. . 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 13383	. . . . . . 7 class TopSet
31	2, 30	cfv 5357	. . . . . 6 class (TopSet ` ndx )
32		cabs 11710	. . . . . . . 8 class abs
33		cmin 8461	. . . . . . . 8 class -
34	32, 33	ccom 4758	. . . . . . 7 class ( abs o. - )
35		cmopn 14818	. . . . . . 7 class MetOpen
36	34, 35	cfv 5357	. . . . . 6 class ( MetOpen ` ( abs o. - ) )
37	31, 36	cop 3697	. . . . 5 class <. (TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >.
38		cple 13384	. . . . . . 7 class le
39	2, 38	cfv 5357	. . . . . 6 class ( le ` ndx )
40		cle 8325	. . . . . 6 class <_
41	39, 40	cop 3697	. . . . 5 class <. ( le ` ndx ) , <_ >.
42		cds 13386	. . . . . . 7 class dist
43	2, 42	cfv 5357	. . . . . 6 class ( dist ` ndx )
44	43, 34	cop 3697	. . . . 5 class <. ( dist ` ndx ) , ( abs o. - ) >.
45	37, 41, 44	ctp 3696	. . . 4 class { <. (TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. }
46		cunif 13387	. . . . . . 7 class UnifSet
47	2, 46	cfv 5357	. . . . . 6 class ( UnifSet ` ndx )
48		cmetu 14819	. . . . . . 7 class metUnif
49	34, 48	cfv 5357	. . . . . 6 class (metUnif ` ( abs o. - ) )
50	47, 49	cop 3697	. . . . 5 class <. ( UnifSet ` ndx ) , (metUnif ` ( abs o. - ) ) >.
51	50	csn 3694	. . . 4 class { <. ( UnifSet ` ndx ) , (metUnif ` ( abs o. - ) ) >. }
52	45, 51	cun 3212	. . 3 class ( { <. (TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. } u. { <. ( UnifSet ` ndx ) , (metUnif ` ( abs o. - ) ) >. } )
53	29, 52	cun 3212	. 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  14835  cnfldbas  14837  mpocnfldadd  14838  mpocnfldmul  14840  cnfldcj  14842  cnfldtset  14843  cnfldle  14844  cnfldds  14845