Axiom ax-mulf 11155

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 11430 or eff 16054. 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 11159. Note that uses of ax-mulf 11155 can be eliminated by using the defined operation (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) in place of ·, as seen in mpomulf 11170.

This axiom is justified by Theorem axmulf 11106. (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 11073	. . 3 class ℂ
2	1, 1	cxp 5639	. 2 class (ℂ × ℂ)
3		cmul 11080	. 2 class ·
4	2, 1, 3	wf 6510	1 wff · :(ℂ × ℂ)⟶ℂ

This axiom is referenced by:  mulnzcnf  11831  mulex  12957  cnfldmul  21279  dfcnfldOLD  21287  mulcn  24763  iimulcnOLD  24842  dvdsmulf1o  27113  fsumdvdsmulOLD  27114  cncvcOLD  30519  xrge0pluscn  33937