Home

Metamath Proof Explorer

< Previous   Next > Related theorems Unicode version

---

Theorem axmulopr 5238

Description: Multiplication is an operation on the complex numbers. This theorem can be used as an alternate axiom for complex numbers in place of the less specific axmulcl 5245.

Assertion

Ref	Expression
axmulopr

---

Proof of Theorem axmulopr

Step	Hyp	Ref	Expression
1		ffnoprval 3999	. 2
2		df-fn 3183	. . 3
3		moeq 1911	. . . . . . . . 9
4	3	mosubop 2794	. . . . . . . 8
5	4	mosubop 2794	. . . . . . 7
6		anass 439	. . . . . . . . . . 11
7	6	2exbii 1048	. . . . . . . . . 10
8		19.42vv 1305	. . . . . . . . . 10
9	7, 8	bitr 173	. . . . . . . . 9
10	9	2exbii 1048	. . . . . . . 8
11	10	mobii 1398	. . . . . . 7
12	5, 11	mpbir 190	. . . . . 6
13	12	moani 1416	. . . . 5
14	13	funoprab 3996	. . . 4
15		df-mul 5218	. . . . 5
16		funeq 3521	. . . . 5
17	15, 16	ax-mp 7	. . . 4
18	14, 17	mpbir 190	. . 3
19	15	dmeqi 3301	. . . . 5
20		dmoprabss 3988	. . . . 5
21	19, 20	eqsstr 2081	. . . 4
22		0ncn 5223	. . . . 5
23		df-c 5212	. . . . . . 7
24		opreq1 3953	. . . . . . . 8
25	24	eleq1d 1532	. . . . . . 7
26		opreq2 3954	. . . . . . . 8
27	26	eleq1d 1532	. . . . . . 7
28		mulcnsr 5226	. . . . . . . 8
29		opelxpi 3207	. . . . . . . . 9
30		addclsr 5164	. . . . . . . . . . 11