Axiom ax-mulf 11148

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 11423 or eff 16047. 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 11152. Note that uses of ax-mulf 11148 can be eliminated by using the defined operation (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) in place of ·, as seen in mpomulf 11163.

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

This axiom is referenced by:  mulnzcnf  11824  mulex  12950  cnfldmul  21272  dfcnfldOLD  21280  mulcn  24756  iimulcnOLD  24835  dvdsmulf1o  27106  fsumdvdsmulOLD  27107  cncvcOLD  30512  xrge0pluscn  33930