Axiom ax-mulf 11110

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 11386 or eff 16008. 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 11114. Note that uses of ax-mulf 11110 can be eliminated by using the defined operation (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) in place of ·, as seen in mpomulf 11125.

This axiom is justified by Theorem axmulf 11061. (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 11028	. . 3 class ℂ
2	1, 1	cxp 5623	. 2 class (ℂ × ℂ)
3		cmul 11035	. 2 class ·
4	2, 1, 3	wf 6489	1 wff · :(ℂ × ℂ)⟶ℂ

This axiom is referenced by:  mulnzcnf  11787  mulex  12908  cnfldmul  21321  dfcnfldOLD  21329  mulcn  24816  iimulcnOLD  24895  dvdsmulf1o  27166  fsumdvdsmulOLD  27167  cncvcOLD  30641  xrge0pluscn  34078