Axiom ax-mulf 11307

Description: Multiplication is an operation on the complex numbers. This axiom tells us that · is defined only on complex numbers which is analogous to the way that other operations are defined, for example see subf 11586 or eff 16276. However, while Metamath can handle this axiom, if we wish to work with weaker complex number axioms, we can avoid it by using the less specific mulcl 11311. Note that uses of ax-mulf 11307 can be eliminated by using the defined operation (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) in place of ·, as seen in mpomulf 11322.

This axiom is justified by Theorem axmulf 11258. (New usage is discouraged.) (Contributed by NM, 19-Oct-2004.)

Assertion

Ref	Expression
ax-mulf	⊢ · :(ℂ × ℂ)⟶ℂ

Detailed syntax breakdown of Axiom ax-mulf

Step	Hyp	Ref	Expression
1		cc 11225	. . 3 class ℂ
2	1, 1	cxp 5653	. 2 class (ℂ × ℂ)
3		cmul 11232	. 2 class ·
4	2, 1, 3	wf 6554	1 wff · :(ℂ × ℂ)⟶ℂ

This axiom is used by:  mulnzcnf  11989  mulex  13146  cnfldmul  21716  mulcn  25217  dvdsmulf1o  27553  cncvcOLD  31215  xrge0pluscn  34642