This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cnfldcj

Description: The conjugation operation of the field of complex numbers. (Contributed by Mario Carneiro, 6-Oct-2015) (Revised by Thierry Arnoux, 17-Dec-2017) (Revised by Thierry Arnoux, 17-Dec-2017) Revise df-cnfld . (Revised by GG, 31-Mar-2025)

Ref Expression
Assertion cnfldcj ⊢ * = * ℂ fld

Proof

Step Hyp Ref Expression
1 cjf ⊢ * : ℂ ⟶ ℂ
2 cnex ⊢ ℂ ∈ V
3 fex2 ⊢ * : ℂ ⟶ ℂ ∧ ℂ ∈ V ∧ ℂ ∈ V → * ∈ V
4 1 2 2 3 mp3an ⊢ * ∈ V
5 cnfldstr ⊢ ℂ fld Struct 1 13
6 starvid ⊢ ∗ 𝑟 = Slot * ndx
7 ssun2 ⊢ * ndx * ⊆ Base ndx ℂ + ndx u ∈ ℂ , v ∈ ℂ ⟼ u + v ⋅ ndx u ∈ ℂ , v ∈ ℂ ⟼ u ⁢ v ∪ * ndx *
8 ssun1 ⊢ Base ndx ℂ + ndx u ∈ ℂ , v ∈ ℂ ⟼ u + v ⋅ ndx u ∈ ℂ , v ∈ ℂ ⟼ u ⁢ v ∪ * ndx * ⊆ Base ndx ℂ + ndx u ∈ ℂ , v ∈ ℂ ⟼ u + v ⋅ ndx u ∈ ℂ , v ∈ ℂ ⟼ u ⁢ v ∪ * ndx * ∪ TopSet ⁡ ndx MetOpen ⁡ abs ∘ − ≤ ndx ≤ dist ⁡ ndx abs ∘ − ∪ UnifSet ⁡ ndx metUnif ⁡ abs ∘ −
9 df-cnfld ⊢ ℂ fld = Base ndx ℂ + ndx u ∈ ℂ , v ∈ ℂ ⟼ u + v ⋅ ndx u ∈ ℂ , v ∈ ℂ ⟼ u ⁢ v ∪ * ndx * ∪ TopSet ⁡ ndx MetOpen ⁡ abs ∘ − ≤ ndx ≤ dist ⁡ ndx abs ∘ − ∪ UnifSet ⁡ ndx metUnif ⁡ abs ∘ −
10 8 9 sseqtrri ⊢ Base ndx ℂ + ndx u ∈ ℂ , v ∈ ℂ ⟼ u + v ⋅ ndx u ∈ ℂ , v ∈ ℂ ⟼ u ⁢ v ∪ * ndx * ⊆ ℂ fld
11 7 10 sstri ⊢ * ndx * ⊆ ℂ fld
12 5 6 11 strfv ⊢ * ∈ V → * = * ℂ fld
13 4 12 ax-mp ⊢ * = * ℂ fld