Definition df-cnfld

Description: The field of complex numbers. Other number fields and rings can be constructed by applying the ` |``s restriction operator, for instance ( CCfld |`AA ) is the field of algebraic numbers.

The contract of this set is defined entirely by cnfldex , cnfldadd , cnfldmul , cnfldcj , cnfldtset , cnfldle , cnfldds , and cnfldbas . 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.)

	Ref	Expression
Assertion	df-cnfld	⊢ ℂfld = ( ( { ⟨ ( Base ‘ ndx ) , ℂ ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 + 𝑦 ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ⟩ } ∪ { ⟨ ( *𝑟 ‘ ndx ) , ∗ ⟩ } ) ∪ ( { ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ ( abs ∘ − ) ) ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( dist ‘ ndx ) , ( abs ∘ − ) ⟩ } ∪ { ⟨ ( UnifSet ‘ ndx ) , ( metUnif ‘ ( abs ∘ − ) ) ⟩ } ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccnfld	⊢ ℂfld
1		cbs	⊢ Base
2		cnx	⊢ ndx
3	2 1	cfv	⊢ ( Base ‘ ndx )
4		cc	⊢ ℂ
5	3 4	cop	⊢ ⟨ ( Base ‘ ndx ) , ℂ ⟩
6		cplusg	⊢ +g
7	2 6	cfv	⊢ ( +g ‘ ndx )
8		vx	⊢ 𝑥
9		vy	⊢ 𝑦
10	8	cv	⊢ 𝑥
11		caddc	⊢ +
12	9	cv	⊢ 𝑦
13	10 12 11	co	⊢ ( 𝑥 + 𝑦 )
14	8 9 4 4 13	cmpo	⊢ ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 + 𝑦 ) )
15	7 14	cop	⊢ ⟨ ( +g ‘ ndx ) , ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 + 𝑦 ) ) ⟩
16		cmulr	⊢ .r
17	2 16	cfv	⊢ ( .r ‘ ndx )
18		cmul	⊢ ·
19	10 12 18	co	⊢ ( 𝑥 · 𝑦 )
20	8 9 4 4 19	cmpo	⊢ ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) )
21	17 20	cop	⊢ ⟨ ( .r ‘ ndx ) , ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ⟩
22	5 15 21	ctp	⊢ { ⟨ ( Base ‘ ndx ) , ℂ ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 + 𝑦 ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ⟩ }
23		cstv	⊢ *𝑟
24	2 23	cfv	⊢ ( *𝑟 ‘ ndx )
25		ccj	⊢ ∗
26	24 25	cop	⊢ ⟨ ( *𝑟 ‘ ndx ) , ∗ ⟩
27	26	csn	⊢ { ⟨ ( *𝑟 ‘ ndx ) , ∗ ⟩ }
28	22 27	cun	⊢ ( { ⟨ ( Base ‘ ndx ) , ℂ ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 + 𝑦 ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ⟩ } ∪ { ⟨ ( *𝑟 ‘ ndx ) , ∗ ⟩ } )
29		cts	⊢ TopSet
30	2 29	cfv	⊢ ( TopSet ‘ ndx )
31		cmopn	⊢ MetOpen
32		cabs	⊢ abs
33		cmin	⊢ −
34	32 33	ccom	⊢ ( abs ∘ − )
35	34 31	cfv	⊢ ( MetOpen ‘ ( abs ∘ − ) )
36	30 35	cop	⊢ ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ ( abs ∘ − ) ) ⟩
37		cple	⊢ le
38	2 37	cfv	⊢ ( le ‘ ndx )
39		cle	⊢ ≤
40	38 39	cop	⊢ ⟨ ( le ‘ ndx ) , ≤ ⟩
41		cds	⊢ dist
42	2 41	cfv	⊢ ( dist ‘ ndx )
43	42 34	cop	⊢ ⟨ ( dist ‘ ndx ) , ( abs ∘ − ) ⟩
44	36 40 43	ctp	⊢ { ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ ( abs ∘ − ) ) ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( dist ‘ ndx ) , ( abs ∘ − ) ⟩ }
45		cunif	⊢ UnifSet
46	2 45	cfv	⊢ ( UnifSet ‘ ndx )
47		cmetu	⊢ metUnif
48	34 47	cfv	⊢ ( metUnif ‘ ( abs ∘ − ) )
49	46 48	cop	⊢ ⟨ ( UnifSet ‘ ndx ) , ( metUnif ‘ ( abs ∘ − ) ) ⟩
50	49	csn	⊢ { ⟨ ( UnifSet ‘ ndx ) , ( metUnif ‘ ( abs ∘ − ) ) ⟩ }
51	44 50	cun	⊢ ( { ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ ( abs ∘ − ) ) ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( dist ‘ ndx ) , ( abs ∘ − ) ⟩ } ∪ { ⟨ ( UnifSet ‘ ndx ) , ( metUnif ‘ ( abs ∘ − ) ) ⟩ } )
52	28 51	cun	⊢ ( ( { ⟨ ( Base ‘ ndx ) , ℂ ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 + 𝑦 ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ⟩ } ∪ { ⟨ ( *𝑟 ‘ ndx ) , ∗ ⟩ } ) ∪ ( { ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ ( abs ∘ − ) ) ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( dist ‘ ndx ) , ( abs ∘ − ) ⟩ } ∪ { ⟨ ( UnifSet ‘ ndx ) , ( metUnif ‘ ( abs ∘ − ) ) ⟩ } ) )
53	0 52	wceq	⊢ ℂfld = ( ( { ⟨ ( Base ‘ ndx ) , ℂ ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 + 𝑦 ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ⟩ } ∪ { ⟨ ( *𝑟 ‘ ndx ) , ∗ ⟩ } ) ∪ ( { ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ ( abs ∘ − ) ) ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( dist ‘ ndx ) , ( abs ∘ − ) ⟩ } ∪ { ⟨ ( UnifSet ‘ ndx ) , ( metUnif ‘ ( abs ∘ − ) ) ⟩ } ) )