Metamath Proof Explorer

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) (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 caddc ⊢ +
9 7 8 cop ⊢ ⟨ ( +g ‘ ndx ) , + ⟩
10 cmulr ⊢ .r
11 2 10 cfv ⊢ ( .r ‘ ndx )
12 cmul ⊢ ·
13 11 12 cop ⊢ ⟨ ( .r ‘ ndx ) , · ⟩
14 5 9 13 ctp ⊢ { ⟨ ( Base ‘ ndx ) , ℂ ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( .r ‘ ndx ) , · ⟩ }
15 cstv ⊢ *𝑟
16 2 15 cfv ⊢ ( *𝑟 ‘ ndx )
17 ccj ⊢ ∗
18 16 17 cop ⊢ ⟨ ( *𝑟 ‘ ndx ) , ∗ ⟩
19 18 csn ⊢ { ⟨ ( *𝑟 ‘ ndx ) , ∗ ⟩ }
20 14 19 cun ⊢ ( { ⟨ ( Base ‘ ndx ) , ℂ ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( .r ‘ ndx ) , · ⟩ } ∪ { ⟨ ( *𝑟 ‘ ndx ) , ∗ ⟩ } )
21 cts ⊢ TopSet
22 2 21 cfv ⊢ ( TopSet ‘ ndx )
23 cmopn ⊢ MetOpen
24 cabs ⊢ abs
25 cmin ⊢ −
26 24 25 ccom ⊢ ( abs ∘ − )
27 26 23 cfv ⊢ ( MetOpen ‘ ( abs ∘ − ) )
28 22 27 cop ⊢ ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ ( abs ∘ − ) ) ⟩
29 cple ⊢ le
30 2 29 cfv ⊢ ( le ‘ ndx )
31 cle ⊢ ≤
32 30 31 cop ⊢ ⟨ ( le ‘ ndx ) , ≤ ⟩
33 cds ⊢ dist
34 2 33 cfv ⊢ ( dist ‘ ndx )
35 34 26 cop ⊢ ⟨ ( dist ‘ ndx ) , ( abs ∘ − ) ⟩
36 28 32 35 ctp ⊢ { ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ ( abs ∘ − ) ) ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( dist ‘ ndx ) , ( abs ∘ − ) ⟩ }
37 cunif ⊢ UnifSet
38 2 37 cfv ⊢ ( UnifSet ‘ ndx )
39 cmetu ⊢ metUnif
40 26 39 cfv ⊢ ( metUnif ‘ ( abs ∘ − ) )
41 38 40 cop ⊢ ⟨ ( UnifSet ‘ ndx ) , ( metUnif ‘ ( abs ∘ − ) ) ⟩
42 41 csn ⊢ { ⟨ ( UnifSet ‘ ndx ) , ( metUnif ‘ ( abs ∘ − ) ) ⟩ }
43 36 42 cun ⊢ ( { ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ ( abs ∘ − ) ) ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( dist ‘ ndx ) , ( abs ∘ − ) ⟩ } ∪ { ⟨ ( UnifSet ‘ ndx ) , ( metUnif ‘ ( abs ∘ − ) ) ⟩ } )
44 20 43 cun ⊢ ( ( { ⟨ ( Base ‘ ndx ) , ℂ ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( .r ‘ ndx ) , · ⟩ } ∪ { ⟨ ( *𝑟 ‘ ndx ) , ∗ ⟩ } ) ∪ ( { ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ ( abs ∘ − ) ) ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( dist ‘ ndx ) , ( abs ∘ − ) ⟩ } ∪ { ⟨ ( UnifSet ‘ ndx ) , ( metUnif ‘ ( abs ∘ − ) ) ⟩ } ) )
45 0 44 wceq ⊢ ℂfld = ( ( { ⟨ ( Base ‘ ndx ) , ℂ ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( .r ‘ ndx ) , · ⟩ } ∪ { ⟨ ( *𝑟 ‘ ndx ) , ∗ ⟩ } ) ∪ ( { ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ ( abs ∘ − ) ) ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( dist ‘ ndx ) , ( abs ∘ − ) ⟩ } ∪ { ⟨ ( UnifSet ‘ ndx ) , ( metUnif ‘ ( abs ∘ − ) ) ⟩ } ) )