Axiom ax-mulf 11078

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 11354 or eff 15980. 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 11082. Note that uses of ax-mulf 11078 can be eliminated by using the defined operation (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) in place of ·, as seen in mpomulf 11093.

This axiom is justified by Theorem axmulf 11029. (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 10996	. . 3 class ℂ
2	1, 1	cxp 5612	. 2 class (ℂ × ℂ)
3		cmul 11003	. 2 class ·
4	2, 1, 3	wf 6473	1 wff · :(ℂ × ℂ)⟶ℂ

This axiom is referenced by:  mulnzcnf  11755  mulex  12881  cnfldmul  21292  dfcnfldOLD  21300  mulcn  24776  iimulcnOLD  24855  dvdsmulf1o  27126  fsumdvdsmulOLD  27127  cncvcOLD  30553  xrge0pluscn  33943