Axiom ax-mulf 11118

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 11394 or eff 16016. 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 11122. Note that uses of ax-mulf 11118 can be eliminated by using the defined operation (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) in place of ·, as seen in mpomulf 11133.

This axiom is justified by Theorem axmulf 11069. (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 11036	. . 3 class ℂ
2	1, 1	cxp 5630	. 2 class (ℂ × ℂ)
3		cmul 11043	. 2 class ·
4	2, 1, 3	wf 6496	1 wff · :(ℂ × ℂ)⟶ℂ

This axiom is referenced by:  mulnzcnf  11795  mulex  12916  cnfldmul  21329  dfcnfldOLD  21337  mulcn  24824  iimulcnOLD  24903  dvdsmulf1o  27174  fsumdvdsmulOLD  27175  cncvcOLD  30670  xrge0pluscn  34117