Definition df-cnfld 14123

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 14125, cnfldadd 14128, cnfldmul 14130, cnfldcj 14131, cnfldtset 14132, cnfldle 14133, cnfldds 14134, and cnfldbas 14126. 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 14122	. 2 class ℂfld
2		cnx 12685	. . . . . . 7 class ndx
3		cbs 12688	. . . . . . 7 class Base
4	2, 3	cfv 5259	. . . . . 6 class ( Base ` ndx )
5		cc 7879	. . . . . 6 class CC
6	4, 5	cop 3626	. . . . 5 class <. ( Base ` ndx ) , CC >.
7		cplusg 12765	. . . . . . 7 class +g
8	2, 7	cfv 5259	. . . . . 6 class ( +g ` ndx )
9		vx	. . . . . . 7 setvar x
10		vy	. . . . . . 7 setvar y
11	9	cv 1363	. . . . . . . 8 class x
12	10	cv 1363	. . . . . . . 8 class y
13		caddc 7884	. . . . . . . 8 class +
14	11, 12, 13	co 5923	. . . . . . 7 class ( x + y )
15	9, 10, 5, 5, 14	cmpo 5925	. . . . . 6 class ( x e. CC , y e. CC |-> ( x + y ) )
16	8, 15	cop 3626	. . . . 5 class <. ( +g ` ndx ) , ( x e. CC , y e. CC |-> ( x + y ) ) >.
17		cmulr 12766	. . . . . . 7 class .r
18	2, 17	cfv 5259	. . . . . 6 class ( .r ` ndx )
19		cmul 7886	. . . . . . . 8 class x.
20	11, 12, 19	co 5923	. . . . . . 7 class ( x x. y )
21	9, 10, 5, 5, 20	cmpo 5925	. . . . . 6 class ( x e. CC , y e. CC |-> ( x x. y ) )
22	18, 21	cop 3626	. . . . 5 class <. ( .r ` ndx ) , ( x e. CC , y e. CC |-> ( x x. y ) ) >.
23	6, 16, 22	ctp 3625	. . . 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 12767	. . . . . . 7 class *r
25	2, 24	cfv 5259	. . . . . 6 class ( *r ` ndx )
26		ccj 11006	. . . . . 6 class *
27	25, 26	cop 3626	. . . . 5 class <. ( *r ` ndx ) , * >.
28	27	csn 3623	. . . 4 class { <. ( *r ` ndx ) , * >. }
29	23, 28	cun 3155	. . 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 12771	. . . . . . 7 class TopSet
31	2, 30	cfv 5259	. . . . . 6 class (TopSet ` ndx )
32		cabs 11164	. . . . . . . 8 class abs
33		cmin 8199	. . . . . . . 8 class -
34	32, 33	ccom 4668	. . . . . . 7 class ( abs o. - )
35		cmopn 14107	. . . . . . 7 class MetOpen
36	34, 35	cfv 5259	. . . . . 6 class ( MetOpen ` ( abs o. - ) )
37	31, 36	cop 3626	. . . . 5 class <. (TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >.
38		cple 12772	. . . . . . 7 class le
39	2, 38	cfv 5259	. . . . . 6 class ( le ` ndx )
40		cle 8064	. . . . . 6 class <_
41	39, 40	cop 3626	. . . . 5 class <. ( le ` ndx ) , <_ >.
42		cds 12774	. . . . . . 7 class dist
43	2, 42	cfv 5259	. . . . . 6 class ( dist ` ndx )
44	43, 34	cop 3626	. . . . 5 class <. ( dist ` ndx ) , ( abs o. - ) >.
45	37, 41, 44	ctp 3625	. . . 4 class { <. (TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. }
46		cunif 12775	. . . . . . 7 class UnifSet
47	2, 46	cfv 5259	. . . . . 6 class ( UnifSet ` ndx )
48		cmetu 14108	. . . . . . 7 class metUnif
49	34, 48	cfv 5259	. . . . . 6 class (metUnif ` ( abs o. - ) )
50	47, 49	cop 3626	. . . . 5 class <. ( UnifSet ` ndx ) , (metUnif ` ( abs o. - ) ) >.
51	50	csn 3623	. . . 4 class { <. ( UnifSet ` ndx ) , (metUnif ` ( abs o. - ) ) >. }
52	45, 51	cun 3155	. . 3 class ( { <. (TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. } u. { <. ( UnifSet ` ndx ) , (metUnif ` ( abs o. - ) ) >. } )
53	29, 52	cun 3155	. 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 1364	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  14124  cnfldbas  14126  mpocnfldadd  14127  mpocnfldmul  14129  cnfldcj  14131  cnfldtset  14132  cnfldle  14133  cnfldds  14134