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	⊢ · = ( .r ‘ ℂfld )

Proof

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