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

Metamath Proof Explorer

Theorem mpocnfldadd

Description: The addition operation of the field of complex numbers. Version of cnfldadd using maps-to notation, which does not require ax-addf . (Contributed by GG, 31-Mar-2025)

Ref Expression
Assertion mpocnfldadd ⊢ x ∈ ℂ , y ∈ ℂ ⟼ x + y = + ℂ fld

Proof

Step Hyp Ref Expression
1 mpoaddex ⊢ x ∈ ℂ , y ∈ ℂ ⟼ x + y ∈ V
2 cnfldstr ⊢ ℂ fld Struct 1 13
3 plusgid ⊢ + 𝑔 = Slot + ndx
4 snsstp2 ⊢ + ndx x ∈ ℂ , y ∈ ℂ ⟼ x + y ⊆ Base ndx ℂ + ndx x ∈ ℂ , y ∈ ℂ ⟼ x + y ⋅ ndx x ∈ ℂ , y ∈ ℂ ⟼ x ⁢ y
5 ssun1 ⊢ Base ndx ℂ + ndx x ∈ ℂ , y ∈ ℂ ⟼ x + y ⋅ ndx x ∈ ℂ , y ∈ ℂ ⟼ x ⁢ y ⊆ Base ndx ℂ + ndx x ∈ ℂ , y ∈ ℂ ⟼ x + y ⋅ ndx x ∈ ℂ , y ∈ ℂ ⟼ x ⁢ y ∪ * ndx *
6 ssun1 ⊢ Base ndx ℂ + ndx x ∈ ℂ , y ∈ ℂ ⟼ x + y ⋅ ndx x ∈ ℂ , y ∈ ℂ ⟼ x ⁢ y ∪ * ndx * ⊆ Base ndx ℂ + ndx x ∈ ℂ , y ∈ ℂ ⟼ x + y ⋅ ndx x ∈ ℂ , y ∈ ℂ ⟼ x ⁢ y ∪ * ndx * ∪ TopSet ⁡ ndx MetOpen ⁡ abs ∘ − ≤ ndx ≤ dist ⁡ ndx abs ∘ − ∪ UnifSet ⁡ ndx metUnif ⁡ abs ∘ −
7 df-cnfld ⊢ ℂ fld = Base ndx ℂ + ndx x ∈ ℂ , y ∈ ℂ ⟼ x + y ⋅ ndx x ∈ ℂ , y ∈ ℂ ⟼ x ⁢ y ∪ * ndx * ∪ TopSet ⁡ ndx MetOpen ⁡ abs ∘ − ≤ ndx ≤ dist ⁡ ndx abs ∘ − ∪ UnifSet ⁡ ndx metUnif ⁡ abs ∘ −
8 6 7 sseqtrri ⊢ Base ndx ℂ + ndx x ∈ ℂ , y ∈ ℂ ⟼ x + y ⋅ ndx x ∈ ℂ , y ∈ ℂ ⟼ x ⁢ y ∪ * ndx * ⊆ ℂ fld
9 5 8 sstri ⊢ Base ndx ℂ + ndx x ∈ ℂ , y ∈ ℂ ⟼ x + y ⋅ ndx x ∈ ℂ , y ∈ ℂ ⟼ x ⁢ y ⊆ ℂ fld
10 4 9 sstri ⊢ + ndx x ∈ ℂ , y ∈ ℂ ⟼ x + y ⊆ ℂ fld
11 2 3 10 strfv ⊢ x ∈ ℂ , y ∈ ℂ ⟼ x + y ∈ V → x ∈ ℂ , y ∈ ℂ ⟼ x + y = + ℂ fld
12 1 11 ax-mp ⊢ x ∈ ℂ , y ∈ ℂ ⟼ x + y = + ℂ fld