Definition df-cnfld 14542

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 14544, cnfldadd 14547, cnfldmul 14549, cnfldcj 14550, cnfldtset 14551, cnfldle 14552, cnfldds 14553, and cnfldbas 14545. 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 14541	. 2 class ℂfld
2		cnx 13050	. . . . . . 7 class ndx
3		cbs 13053	. . . . . . 7 class Base
4	2, 3	cfv 5321	. . . . . 6 class ( Base ` ndx )
5		cc 8013	. . . . . 6 class CC
6	4, 5	cop 3669	. . . . 5 class <. ( Base ` ndx ) , CC >.
7		cplusg 13131	. . . . . . 7 class +g
8	2, 7	cfv 5321	. . . . . 6 class ( +g ` ndx )
9		vx	. . . . . . 7 setvar x
10		vy	. . . . . . 7 setvar y
11	9	cv 1394	. . . . . . . 8 class x
12	10	cv 1394	. . . . . . . 8 class y
13		caddc 8018	. . . . . . . 8 class +
14	11, 12, 13	co 6010	. . . . . . 7 class ( x + y )
15	9, 10, 5, 5, 14	cmpo 6012	. . . . . 6 class ( x e. CC , y e. CC |-> ( x + y ) )
16	8, 15	cop 3669	. . . . 5 class <. ( +g ` ndx ) , ( x e. CC , y e. CC |-> ( x + y ) ) >.
17		cmulr 13132	. . . . . . 7 class .r
18	2, 17	cfv 5321	. . . . . 6 class ( .r ` ndx )
19		cmul 8020	. . . . . . . 8 class x.
20	11, 12, 19	co 6010	. . . . . . 7 class ( x x. y )
21	9, 10, 5, 5, 20	cmpo 6012	. . . . . 6 class ( x e. CC , y e. CC |-> ( x x. y ) )
22	18, 21	cop 3669	. . . . 5 class <. ( .r ` ndx ) , ( x e. CC , y e. CC |-> ( x x. y ) ) >.
23	6, 16, 22	ctp 3668	. . . 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 13133	. . . . . . 7 class *r
25	2, 24	cfv 5321	. . . . . 6 class ( *r ` ndx )
26		ccj 11371	. . . . . 6 class *
27	25, 26	cop 3669	. . . . 5 class <. ( *r ` ndx ) , * >.
28	27	csn 3666	. . . 4 class { <. ( *r ` ndx ) , * >. }
29	23, 28	cun 3195	. . 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 13137	. . . . . . 7 class TopSet
31	2, 30	cfv 5321	. . . . . 6 class (TopSet ` ndx )
32		cabs 11529	. . . . . . . 8 class abs
33		cmin 8333	. . . . . . . 8 class -
34	32, 33	ccom 4724	. . . . . . 7 class ( abs o. - )
35		cmopn 14526	. . . . . . 7 class MetOpen
36	34, 35	cfv 5321	. . . . . 6 class ( MetOpen ` ( abs o. - ) )
37	31, 36	cop 3669	. . . . 5 class <. (TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >.
38		cple 13138	. . . . . . 7 class le
39	2, 38	cfv 5321	. . . . . 6 class ( le ` ndx )
40		cle 8198	. . . . . 6 class <_
41	39, 40	cop 3669	. . . . 5 class <. ( le ` ndx ) , <_ >.
42		cds 13140	. . . . . . 7 class dist
43	2, 42	cfv 5321	. . . . . 6 class ( dist ` ndx )
44	43, 34	cop 3669	. . . . 5 class <. ( dist ` ndx ) , ( abs o. - ) >.
45	37, 41, 44	ctp 3668	. . . 4 class { <. (TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. }
46		cunif 13141	. . . . . . 7 class UnifSet
47	2, 46	cfv 5321	. . . . . 6 class ( UnifSet ` ndx )
48		cmetu 14527	. . . . . . 7 class metUnif
49	34, 48	cfv 5321	. . . . . 6 class (metUnif ` ( abs o. - ) )
50	47, 49	cop 3669	. . . . 5 class <. ( UnifSet ` ndx ) , (metUnif ` ( abs o. - ) ) >.
51	50	csn 3666	. . . 4 class { <. ( UnifSet ` ndx ) , (metUnif ` ( abs o. - ) ) >. }
52	45, 51	cun 3195	. . 3 class ( { <. (TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. } u. { <. ( UnifSet ` ndx ) , (metUnif ` ( abs o. - ) ) >. } )
53	29, 52	cun 3195	. 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 1395	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  14543  cnfldbas  14545  mpocnfldadd  14546  mpocnfldmul  14548  cnfldcj  14550  cnfldtset  14551  cnfldle  14552  cnfldds  14553