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

Metamath Proof Explorer

Theorem cnfldadd

Description: The addition operation of the field of complex numbers. (Contributed by Stefan O'Rear, 27-Nov-2014) (Revised by Mario Carneiro, 6-Oct-2015) (Revised by Thierry Arnoux, 17-Dec-2017) Revise df-cnfld . (Revised by GG, 27-Apr-2025)

Ref Expression
Assertion cnfldadd + = ( +g ‘ ℂfld )

Proof

Step Hyp Ref Expression
1 ax-addf ⊢ + : ( ℂ × ℂ ) ⟶ ℂ
2 ffn ⊢ ( + : ( ℂ × ℂ ) ⟶ ℂ → + Fn ( ℂ × ℂ ) )
3 1 2 ax-mp ⊢ + Fn ( ℂ × ℂ )
4 fnov ⊢ ( + Fn ( ℂ × ℂ ) ↔ + = ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 + 𝑦 ) ) )
5 3 4 mpbi ⊢ + = ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 + 𝑦 ) )
6 mpocnfldadd ⊢ ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 + 𝑦 ) ) = ( +g ‘ ℂfld )
7 5 6 eqtri ⊢ + = ( +g ‘ ℂfld )