HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Theorem axmulopr 5278
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 5285.
Assertion
Ref Expression
axmulopr |- x. :(CC X. CC)-->CC
Proof of Theorem axmulopr
StepHypRef Expression
1 ffnoprval 4020 . 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 3199 . . 3 |- ( x. Fn (CC X. CC) <-> (Fun x. /\ dom x. = (CC X. CC)))
3 moeq 1923 . . . . . . . . 9 |- E*z z = <.((w .R u) +R (-1R .R (v .R f))), ((v .R u) +R (w .R f))>.
43mosubop 2811 . . . . . . . 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 2811 . . . . . . 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 441 . . . . . . . . . . 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 1054 . . . . . . . . . 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 1312 . . . . . . . . . 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, 8bitr 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))>.)))
1092exbii 1054 . . . . . . . 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 1407 . . . . . . 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 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))>.)
1312moani 1425 . . . . 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 4017 . . . 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 5258 . . . . 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 3541 . . . . 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 190 . . 3 |- Fun x.
1915dmeqi 3318 . . . . 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 4009 . . . . 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, 20eqsstr 2094 . . . 4 |- dom x. (_ (CC X. CC)
22 0ncn 5263 . . . . 5 |- -. (/) e. CC
23 df-c 5252 . . . . . . 7 |- CC = (R. X. R.)
24 opreq1 3974 . . . . . . . 8 |- (<.z, w>. = x -> (<.z, w>. x. <.v, u>.) = (x x. <.v, u>.))
2524eleq1d 1543 . . . . . . 7 |- (<.z, w>. = x -> ((<.z, w>. x. <.v, u>.) e. (R. X. R.) <-> (x x. <.v, u>.) e. (R. X. R.)))
26 opreq2 3975 . . . . . . . 8 |- (<.v, u>. = y -> (x x. <.v, u>.) = (x x. y))
2726eleq1d 1543 . . . . . . 7 |- (<.v, u>. = y -> ((x x. <.v, u>.) e. (R. X. R.) <-> (x x. y) e. (R. X. R.)))
28 mulcnsr 5266 . . . . . . . 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 3223 . . . . . . . . 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 5204 . . . . . . . . . . 11 |- (((z .R v) e. R. /\ (-1R .R (w .R u)) e. R.) -> ((z .R v) +R (-1R .R (w .R u))) e.