MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ax-mulf Structured version   Visualization version   GIF version

Axiom ax-mulf 11235
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 11510 or eff 16117. 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 11239. Note that uses of ax-mulf 11235 can be eliminated by using the defined operation (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) in place of ·, as seen in mpomulf 11250.

This axiom is justified by Theorem axmulf 11186. (New usage is discouraged.) (Contributed by NM, 19-Oct-2004.)

Assertion
Ref Expression
ax-mulf · :(ℂ × ℂ)⟶ℂ

Detailed syntax breakdown of Axiom ax-mulf
StepHypRef Expression
1 cc 11153 . . 3 class
21, 1cxp 5683 . 2 class (ℂ × ℂ)
3 cmul 11160 . 2 class ·
42, 1, 3wf 6557 1 wff · :(ℂ × ℂ)⟶ℂ
Colors of variables: wff setvar class
This axiom is referenced by:  mulnzcnf  11909  mulex  13033  cnfldmul  21372  dfcnfldOLD  21380  mulcn  24889  iimulcnOLD  24968  dvdsmulf1o  27239  fsumdvdsmulOLD  27240  cncvcOLD  30602  xrge0pluscn  33939
  Copyright terms: Public domain W3C validator