Axiom ax-mulf

Description: Multiplication is an operation on the complex numbers. This axiom tells us that x. is defined only on complex numbers which is analogous to the way that other operations are defined, for example see subf or eff . 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 . Note that uses of ax-mulf can be eliminated by using the defined operation ( x e. CC , y e. CC |-> ( x x. y ) ) in place of x. , as seen in mpomulf .

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

	Ref	Expression
Assertion	ax-mulf	|- x. : ( CC X. CC ) --> CC

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmul	|- x.
1		cc	|- CC
2	1 1	cxp	|- ( CC X. CC )
3	2 1 0	wf	|- x. : ( CC X. CC ) --> CC