Axiom ax-mulf 11108

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 11383 or eff 16006. 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 11112. Note that uses of ax-mulf 11108 can be eliminated by using the defined operation (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) in place of ·, as seen in mpomulf 11123.

This axiom is justified by Theorem axmulf 11059. (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 11026	. . 3 class ℂ
2	1, 1	cxp 5621	. 2 class (ℂ × ℂ)
3		cmul 11033	. 2 class ·
4	2, 1, 3	wf 6482	1 wff · :(ℂ × ℂ)⟶ℂ

This axiom is referenced by:  mulnzcnf  11784  mulex  12910  cnfldmul  21287  dfcnfldOLD  21295  mulcn  24772  iimulcnOLD  24851  dvdsmulf1o  27122  fsumdvdsmulOLD  27123  cncvcOLD  30545  xrge0pluscn  33906