Axiom ax-mulf 11096

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 11372 or eff 15998. 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 11100. Note that uses of ax-mulf 11096 can be eliminated by using the defined operation (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) in place of ·, as seen in mpomulf 11111.

This axiom is justified by Theorem axmulf 11047. (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 11014	. . 3 class ℂ
2	1, 1	cxp 5619	. 2 class (ℂ × ℂ)
3		cmul 11021	. 2 class ·
4	2, 1, 3	wf 6485	1 wff · :(ℂ × ℂ)⟶ℂ

This axiom is referenced by:  mulnzcnf  11773  mulex  12899  cnfldmul  21309  dfcnfldOLD  21317  mulcn  24793  iimulcnOLD  24872  dvdsmulf1o  27143  fsumdvdsmulOLD  27144  cncvcOLD  30574  xrge0pluscn  33964