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	$$⊢+={+}_{{ℂ}_{\mathrm{fld}}}$$

Proof

Step	Hyp	Ref	Expression
1		ax-addf	$$⊢+:ℂ\times ℂ⟶ℂ$$
2		ffn	$$⊢+:ℂ\times ℂ⟶ℂ\to +Fn\left(ℂ\times ℂ\right)$$
3	1 2	ax-mp	$$⊢+Fn\left(ℂ\times ℂ\right)$$
4		fnov	$$⊢+Fn\left(ℂ\times ℂ\right)\leftrightarrow +=\left(x\in ℂ,y\in ℂ⟼x+y\right)$$
5	3 4	mpbi	$$⊢+=\left(x\in ℂ,y\in ℂ⟼x+y\right)$$
6		mpocnfldadd	$$⊢\left(x\in ℂ,y\in ℂ⟼x+y\right)={+}_{{ℂ}_{\mathrm{fld}}}$$
7	5 6	eqtri	$$⊢+={+}_{{ℂ}_{\mathrm{fld}}}$$