Theorem axmulopr 5246

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 5253.

Assertion

Ref	Expression
axmulopr	|- x. :(CC X. CC)-->CC

Proof of Theorem axmulopr

Step	Hyp	Ref	Expression
1		ffnoprval 4005	. 2 |- ( x. :(CC X. CC)-->CC <-> ( x. Fn (CC X. CC) /\ A.x e. CC A.y e. CC (x x. y) e. CC))
2		df-fn 3188	. . 3 |- ( x. Fn (CC X. CC) <-> (Fun x. /\ dom x. = (CC X. CC)))
3		moeq 1916	. . . . . . . . 9 |- E*z z = <.((w .R u) +R (-1R .R (v .R f))), ((v .R u) +R (w .R f))>.
4	3	mosubop 2800	. . . . . . . 8 |- E*zE.uE.f(y = <.u, f>. /\ z = <.((w .R u) +R (-1R .R (v .R f))), ((v .R u) +R (w .R f))>.)
5	4	mosubop 2800	. . . . . . 7 |- E*zE.wE.v(x = <.w, v>. /\ E.uE.f(y = <.u, f>. /\ z = <.((w .R u) +R (-1R .R (v .R f))), ((v .R u) +R (w .R f))>.))
6		anass 439	. . . . . . . . . . 11 |- (((x = <.w, v>. /\ y = <.u, f>.) /\ z = <.((w .R u) +R (-1R .R (v .R f))), ((v .R u) +R (w .R f))>.) <-> (x = <.w, v>. /\ (y = <.u, f>. /\ z = <.((w .R u) +R (-1R .R (v .R f))), ((v .R u) +R (w .R f))>.)))
7	6	2exbii 1050	. . . . . . . . . 10 |- (E.uE.f((x = <.w, v>. /\ y = <.u, f>.) /\ z = <.((w .R u) +R (-1R .R (v .R f))), ((v .R u) +R (w .R f))>.) <-> E.uE.f(x = <.w, v>. /\ (y = <.u, f>. /\ z = <.((w .R u) +R (-1R .R (v .R f))), ((v .R u) +R (w .R f))>.)))
8		19.42vv 1308	. . . . . . . . . 10 |- (E.uE.f(x = <.w, v>. /\ (y = <.u, f>. /\ z = <.((w .R u) +R (-1R .R (v .R f))), ((v .R u) +R (w .R f))>.)) <-> (x = <.w, v>. /\ E.uE.f(y = <.u, f>. /\ z = <.((w .R u) +R (-1R .R (v .R f))), ((v .R u) +R (w .R f))>.)))
9	7, 8	bitr 173	. . . . . . . . 9 |- (E.uE.f((x = <.w, v>. /\ y = <.u, f>.) /\ z = <.((w .R u) +R (-1R .R (v .R f))), ((v .R u) +R (w .R f))>.) <-> (x = <.w, v>. /\ E.uE.f(y = <.u, f>. /\ z = <.((w .R u) +R (-1R .R (v .R f))), ((v .R u) +R (w .R f))>.)))
10	9	2exbii 1050	. . . . . . . 8 |- (E.wE.vE.uE.f((x = <.w, v>. /\ y = <.u, f>.) /\ z = <.((w .R u) +R (-1R .R (v .R f))), ((v .R u) +R (w .R f))>.) <-> E.wE.v(x = <.w, v>. /\ E.uE.f(y = <.u, f>. /\ z = <.((w .R u) +R (-1R .R (v .R f))), ((v .R u) +R (w .R f))>.)))
11	10	mobii 1403	. . . . . . 7 |- (E*zE.wE.vE.uE.f((x = <.w, v>. /\ y = <.u, f>.) /\ z = <.((w .R u) +R (-1R .R (v .R f))), ((v .R u) +R (w .R f))>.) <-> E*zE.wE.v(x = <.w, v>. /\ E.uE.f(y = <.u, f>. /\ z = <.((w .R u) +R (-1R .R (v .R f))), ((v .R u) +R (w .R f))>.)))
12	5, 11	mpbir 190	. . . . . 6 |- E*zE.wE.vE.uE.f((x = <.w, v>. /\ y = <.u, f>.) /\ z = <.((w .R u) +R (-1R .R (v .R f))), ((v .R u) +R (w .R f))>.)
13	12	moani 1421	. . . . 5 |- E*z((x e. CC /\ y e. CC) /\ E.wE.vE.uE.f((x = <.w, v>. /\ y = <.u, f>.) /\ z = <.((w .R u) +R (-1R .R (v .R f))), ((v .R u) +R (w .R f))>.))
14	13	funoprab 4002	. . . 4 |- Fun {<.<.x, y>., z>. | ((x e. CC /\ y e. CC) /\ E.wE.vE.uE.f((x = <.w, v>. /\ y = <.u, f>.) /\ z = <.((w .R u) +R (-1R .R (v .R f))), ((v .R u) +R (w .R f))>.))}
15		df-mul 5226	. . . . 5 |- x. = {<.<.x, y>., z>. | ((x e. CC /\ y e. CC) /\ E.wE.vE.uE.f((x = <.w, v>. /\ y = <.u, f>.) /\ z = <.((w .R u) +R (-1R .R (v .R f))), ((v .R u) +R (w .R f))>.))}
16		funeq 3527	. . . . 5 |- ( x. = {<.<.x, y>., z>. | ((x e. CC /\ y e. CC) /\ E.wE.vE.uE.f((x = <.w, v>. /\ y = <.u, f>.) /\ z = <.((w .R u) +R (-1R .R (v .R f))), ((v .R u) +R (w .R f))>.))} -> (Fun x. <-> Fun {<.<.x, y>., z>. | ((x e. CC /\ y e. CC) /\ E.wE.vE.uE.f((x = <.w, v>. /\ y = <.u, f>.) /\ z = <.((w .R u) +R (-1R .R (v .R f))), ((v .R u) +R (w .R f))>.))}))
17	15, 16	ax-mp 7	. . . 4 |- (Fun x. <-> Fun {<.<.x, y>., z>. | ((x e. CC /\ y e. CC) /\ E.wE.vE.uE.f((x = <.w, v>. /\ y = <.u, f>.) /\ z = <.((w .R u) +R (-1R .R (v .R f))), ((v .R u) +R (w .R f))>.))})
18	14, 17	mpbir 190	. . 3 |- Fun x.
19	15	dmeqi 3307	. . . . 5 |- dom x. = dom {<.<.x, y>., z>. | ((x e. CC /\ y e. CC) /\ E.wE.vE.uE.f((x = <.w, v>. /\ y = <.u, f>.) /\ z = <.((w .R u) +R (-1R .R (v .R f))), ((v .R u) +R (w .R f))>.))}
20		dmoprabss 3994	. . . . 5 |- dom {<.<.x, y>., z>. | ((x e. CC /\ y e. CC) /\ E.wE.vE.uE.f((x = <.w, v>. /\ y = <.u, f>.) /\ z = <.((w .R u) +R (-1R .R (v .R f))), ((v .R u) +R (w .R f))>.))} (_ (CC X. CC)
21	19, 20	eqsstr 2087	. . . 4 |- dom x. (_ (CC X. CC)
22		0ncn 5231	. . . . 5 |- -. (/) e. CC
23		df-c 5220	. . . . . . 7 |- CC = (R. X. R.)
24		opreq1 3959	. . . . . . . 8 |- (<.z, w>. = x -> (<.z, w>. x. <.v, u>.) = (x x. <.v, u>.))
25	24	eleq1d 1537	. . . . . . 7 |- (<.z, w>. = x -> ((<.z, w>. x. <.v, u>.) e. (R. X. R.) <-> (x x. <.v, u>.) e. (R. X. R.)))
26		opreq2 3960	. . . . . . . 8 |- (<.v, u>. = y -> (x x. <.v, u>.) = (x x. y))
27	26	eleq1d 1537	. . . . . . 7 |- (<.v, u>. = y -> ((x x. <.v, u>.) e. (R. X. R.) <-> (x x. y) e. (R. X. R.)))
28		mulcnsr 5234	. . . . . . . 8 |- (((z e. R. /\ w e. R.) /\ (v e. R. /\ u e. R.)) -> (<.z, w>. x. <.v, u>.) = <.((z .R v) +R (-1R .R (w .R u))), ((w .R v) +R (z .R u))>.)
29		opelxpi 3212	. . . . . . . . 9 |- ((((z .R v) +R (-1R .R (w .R u))) e. R. /\ ((w .R v) +R (z .R u)) e. R.) -> <.((z .R v) +R (-1R .R (w .R u))), ((w .R v) +R (z .R u))>. e. (R. X. R.))
30		addclsr 5172	. . . . . . . . . . 11 |- (((z .R v) e. R. /\ (-1R .R (w .R u)) e. R.) -> ((z .R v) +R (-1R .R (w .R u))) e. R.