Definition df-cnfld 14754

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 14756, cnfldadd 14759, cnfldmul 14761, cnfldcj 14762, cnfldtset 14763, cnfldle 14764, cnfldds 14765, and cnfldbas 14757. 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 14753	. 2 class ℂfld
2		cnx 13230	. . . . . . 7 class ndx
3		cbs 13233	. . . . . . 7 class Base
4	2, 3	cfv 5354	. . . . . 6 class ( Base ` ndx )
5		cc 8130	. . . . . 6 class CC
6	4, 5	cop 3694	. . . . 5 class <. ( Base ` ndx ) , CC >.
7		cplusg 13311	. . . . . . 7 class +g
8	2, 7	cfv 5354	. . . . . 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 8135	. . . . . . . 8 class +
14	11, 12, 13	co 6052	. . . . . . 7 class ( x + y )
15	9, 10, 5, 5, 14	cmpo 6054	. . . . . 6 class ( x e. CC , y e. CC |-> ( x + y ) )
16	8, 15	cop 3694	. . . . 5 class <. ( +g ` ndx ) , ( x e. CC , y e. CC |-> ( x + y ) ) >.
17		cmulr 13312	. . . . . . 7 class .r
18	2, 17	cfv 5354	. . . . . 6 class ( .r ` ndx )
19		cmul 8137	. . . . . . . 8 class x.
20	11, 12, 19	co 6052	. . . . . . 7 class ( x x. y )
21	9, 10, 5, 5, 20	cmpo 6054	. . . . . 6 class ( x e. CC , y e. CC |-> ( x x. y ) )
22	18, 21	cop 3694	. . . . 5 class <. ( .r ` ndx ) , ( x e. CC , y e. CC |-> ( x x. y ) ) >.
23	6, 16, 22	ctp 3693	. . . 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 13313	. . . . . . 7 class *r
25	2, 24	cfv 5354	. . . . . 6 class ( *r ` ndx )
26		ccj 11532	. . . . . 6 class *
27	25, 26	cop 3694	. . . . 5 class <. ( *r ` ndx ) , * >.
28	27	csn 3691	. . . 4 class { <. ( *r ` ndx ) , * >. }
29	23, 28	cun 3211	. . 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 13317	. . . . . . 7 class TopSet
31	2, 30	cfv 5354	. . . . . 6 class (TopSet ` ndx )
32		cabs 11690	. . . . . . . 8 class abs
33		cmin 8449	. . . . . . . 8 class -
34	32, 33	ccom 4755	. . . . . . 7 class ( abs o. - )
35		cmopn 14738	. . . . . . 7 class MetOpen
36	34, 35	cfv 5354	. . . . . 6 class ( MetOpen ` ( abs o. - ) )
37	31, 36	cop 3694	. . . . 5 class <. (TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >.
38		cple 13318	. . . . . . 7 class le
39	2, 38	cfv 5354	. . . . . 6 class ( le ` ndx )
40		cle 8314	. . . . . 6 class <_
41	39, 40	cop 3694	. . . . 5 class <. ( le ` ndx ) , <_ >.
42		cds 13320	. . . . . . 7 class dist
43	2, 42	cfv 5354	. . . . . 6 class ( dist ` ndx )
44	43, 34	cop 3694	. . . . 5 class <. ( dist ` ndx ) , ( abs o. - ) >.
45	37, 41, 44	ctp 3693	. . . 4 class { <. (TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. }
46		cunif 13321	. . . . . . 7 class UnifSet
47	2, 46	cfv 5354	. . . . . 6 class ( UnifSet ` ndx )
48		cmetu 14739	. . . . . . 7 class metUnif
49	34, 48	cfv 5354	. . . . . 6 class (metUnif ` ( abs o. - ) )
50	47, 49	cop 3694	. . . . 5 class <. ( UnifSet ` ndx ) , (metUnif ` ( abs o. - ) ) >.
51	50	csn 3691	. . . 4 class { <. ( UnifSet ` ndx ) , (metUnif ` ( abs o. - ) ) >. }
52	45, 51	cun 3211	. . 3 class ( { <. (TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. } u. { <. ( UnifSet ` ndx ) , (metUnif ` ( abs o. - ) ) >. } )
53	29, 52	cun 3211	. 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  14755  cnfldbas  14757  mpocnfldadd  14758  mpocnfldmul  14760  cnfldcj  14762  cnfldtset  14763  cnfldle  14764  cnfldds  14765