HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Theorem axmulopr 5331
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 5338.
Assertion
Ref Expression
axmulopr |- x. :(CC X. CC)-->CC
Proof of Theorem axmulopr
StepHypRef Expression
1 ffnoprval 4072 . 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 3250 . . 3 |- ( x. Fn (CC X. CC) <-> (Fun x. /\ dom x. = (CC X. CC)))
3 moeq 1967 . . . . . . . . 9 |- E*z z = <.((w .R u) +R (-1R .R (v .R f))), ((v .R u) +R (w .R f))>.
43mosubop 2861 . . . . . . . 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))>.)
54mosubop 2861 . . . . . . 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 450 . . . . . . . . . . 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))>.)))
762exbii 1093 . . . . . . . . . 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 1352 . . . . . . . . . 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))>.)))
97, 8bitri 180 . . . . . . . . 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))>.)))
1092exbii 1093 . . . . . . . 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))>.)))
1110mobii 1447 . . . . . . 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))>.)))
125, 11mpbir 197 . . . . . 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))>.)
1312moani 1465 . . . . 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))>.))
1413funoprab 4069 . . . 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 5311 . . . . 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 3592 . . . . 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))>.))}))
1715, 16ax-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))>.))})
1814, 17mpbir 197 . . 3 |- Fun x.
1915dmeqi 3369 . . . . 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 4061 . . . . 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)
2119, 20eqsstri 2142 . . . 4 |- dom x. (_ (CC X. CC)
22 0ncn 5316 . . . . 5 |- -. (/) e. CC
23 df-c 5305 . . . . . . 7 |- CC = (R. X. R.)
24 opreq1 4026 . . . . . . . 8 |- (<.z, w>. = x -> (<.z, w>. x. <.v, u>.) = (x x. <.v, u>.))
2524eleq1d 1587 . . . . . . 7 |- (<.z, w>. = x -> ((<.z, w>. x. <.v, u>.) e. (R. X. R.) <-> (x x. <.v, u>.) e. (R. X. R.)))
26 opreq2 4027 . . . . . . . 8 |- (<.v, u>. = y -> (x x. <.v, u>.) = (x x. y))
2726eleq1d 1587 . . . . . . 7 |- (<.v, u>. = y -> ((x x. <.v, u>.) e. (R. X. R.) <-> (x x. y) e. (R. X. R.)))
28 mulcnsr 5319 . . . . . . . 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 3274 . . . . . . . . 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 5257 . . . . . . . . . . 11 |- (((z .R v) e. R. /\ (-1R .R (w .R u)) e. R.) -> ((z .R v) +R (-1R .R (w .R u))) e.