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

Metamath Proof Explorer

Theorem mpocnfldmul

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

Ref Expression
Assertion mpocnfldmul ⊢ x ∈ ℂ , y ∈ ℂ ⟼ x ⁢ y = ⋅ ℂ fld

Proof

Step Hyp Ref Expression
1 mpomulex ⊢ x ∈ ℂ , y ∈ ℂ ⟼ x ⁢ y ∈ V
2 cnfldstr ⊢ ℂ fld Struct 1 13
3 mulridx ⊢ ⋅ 𝑟 = Slot ⋅ ndx
4 snsstp3 ⊢ ⋅ 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