Definition df-cnfld 14877

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 14879, cnfldadd 14882, cnfldmul 14884, cnfldcj 14885, cnfldtset 14886, cnfldle 14887, cnfldds 14888, and cnfldbas 14880. 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 14876	. 2 class ℂfld
2		cnx 13332	. . . . . . 7 class ndx
3		cbs 13335	. . . . . . 7 class Base
4	2, 3	cfv 5375	. . . . . 6 class ( Base ` ndx )
5		cc 8171	. . . . . 6 class CC
6	4, 5	cop 3711	. . . . 5 class <. ( Base ` ndx ) , CC >.
7		cplusg 13414	. . . . . . 7 class +g
8	2, 7	cfv 5375	. . . . . 6 class ( +g ` ndx )
9		vx	. . . . . . 7 setvar x
10		vy	. . . . . . 7 setvar y
11	9	cv 1401	. . . . . . . 8 class x
12	10	cv 1401	. . . . . . . 8 class y
13		caddc 8176	. . . . . . . 8 class +
14	11, 12, 13	co 6079	. . . . . . 7 class ( x + y )
15	9, 10, 5, 5, 14	cmpo 6081	. . . . . 6 class ( x e. CC , y e. CC |-> ( x + y ) )
16	8, 15	cop 3711	. . . . 5 class <. ( +g ` ndx ) , ( x e. CC , y e. CC |-> ( x + y ) ) >.
17		cmulr 13415	. . . . . . 7 class .r
18	2, 17	cfv 5375	. . . . . 6 class ( .r ` ndx )
19		cmul 8178	. . . . . . . 8 class x.
20	11, 12, 19	co 6079	. . . . . . 7 class ( x x. y )
21	9, 10, 5, 5, 20	cmpo 6081	. . . . . 6 class ( x e. CC , y e. CC |-> ( x x. y ) )
22	18, 21	cop 3711	. . . . 5 class <. ( .r ` ndx ) , ( x e. CC , y e. CC |-> ( x x. y ) ) >.
23	6, 16, 22	ctp 3710	. . . 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 13416	. . . . . . 7 class *r
25	2, 24	cfv 5375	. . . . . 6 class ( *r ` ndx )
26		ccj 11587	. . . . . 6 class *
27	25, 26	cop 3711	. . . . 5 class <. ( *r ` ndx ) , * >.
28	27	csn 3708	. . . 4 class { <. ( *r ` ndx ) , * >. }
29	23, 28	cun 3218	. . 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 13420	. . . . . . 7 class TopSet
31	2, 30	cfv 5375	. . . . . 6 class (TopSet ` ndx )
32		cabs 11746	. . . . . . . 8 class abs
33		cmin 8491	. . . . . . . 8 class -
34	32, 33	ccom 4776	. . . . . . 7 class ( abs o. - )
35		cmopn 14861	. . . . . . 7 class MetOpen
36	34, 35	cfv 5375	. . . . . 6 class ( MetOpen ` ( abs o. - ) )
37	31, 36	cop 3711	. . . . 5 class <. (TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >.
38		cple 13421	. . . . . . 7 class le
39	2, 38	cfv 5375	. . . . . 6 class ( le ` ndx )
40		cle 8355	. . . . . 6 class <_
41	39, 40	cop 3711	. . . . 5 class <. ( le ` ndx ) , <_ >.
42		cds 13423	. . . . . . 7 class dist
43	2, 42	cfv 5375	. . . . . 6 class ( dist ` ndx )
44	43, 34	cop 3711	. . . . 5 class <. ( dist ` ndx ) , ( abs o. - ) >.
45	37, 41, 44	ctp 3710	. . . 4 class { <. (TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. }
46		cunif 13424	. . . . . . 7 class UnifSet
47	2, 46	cfv 5375	. . . . . 6 class ( UnifSet ` ndx )
48		cmetu 14862	. . . . . . 7 class metUnif
49	34, 48	cfv 5375	. . . . . 6 class (metUnif ` ( abs o. - ) )
50	47, 49	cop 3711	. . . . 5 class <. ( UnifSet ` ndx ) , (metUnif ` ( abs o. - ) ) >.
51	50	csn 3708	. . . 4 class { <. ( UnifSet ` ndx ) , (metUnif ` ( abs o. - ) ) >. }
52	45, 51	cun 3218	. . 3 class ( { <. (TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. } u. { <. ( UnifSet ` ndx ) , (metUnif ` ( abs o. - ) ) >. } )
53	29, 52	cun 3218	. 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 1402	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  14878  cnfldbas  14880  mpocnfldadd  14881  mpocnfldmul  14883  cnfldcj  14885  cnfldtset  14886  cnfldle  14887  cnfldds  14888