Axiom ax-mulf 11232

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 11507 or eff 16113. 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 11236. Note that uses of ax-mulf 11232 can be eliminated by using the defined operation (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) in place of ·, as seen in mpomulf 11247.

This axiom is justified by Theorem axmulf 11183. (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 11150	. . 3 class ℂ
2	1, 1	cxp 5686	. 2 class (ℂ × ℂ)
3		cmul 11157	. 2 class ·
4	2, 1, 3	wf 6558	1 wff · :(ℂ × ℂ)⟶ℂ

This axiom is referenced by:  mulnzcnf  11906  mulex  13030  cnfldmul  21389  dfcnfldOLD  21397  mulcn  24902  iimulcnOLD  24981  dvdsmulf1o  27253  fsumdvdsmulOLD  27254  cncvcOLD  30611  xrge0pluscn  33900