Theorem cnfldmul

Description: The multiplication 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	cnfldmul	$$⊢\times ={\cdot }_{{ℂ}_{\mathrm{fld}}}$$

Proof

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