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

Metamath Proof Explorer

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_{ℂ_{fld}}$

Proof

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