# Metamath Proof Explorer

## Theorem mulcnsr

Description: Multiplication of complex numbers in terms of signed reals. (Contributed by NM, 9-Aug-1995) (New usage is discouraged.)

Ref Expression
Assertion mulcnsr ${⊢}\left(\left({A}\in 𝑹\wedge {B}\in 𝑹\right)\wedge \left({C}\in 𝑹\wedge {D}\in 𝑹\right)\right)\to ⟨{A},{B}⟩⟨{C},{D}⟩=⟨\left({A}{\cdot }_{𝑹}{C}\right){+}_{𝑹}\left({-1}_{𝑹}{\cdot }_{𝑹}\left({B}{\cdot }_{𝑹}{D}\right)\right),\left({B}{\cdot }_{𝑹}{C}\right){+}_{𝑹}\left({A}{\cdot }_{𝑹}{D}\right)⟩$

### Proof

Step Hyp Ref Expression
1 opex ${⊢}⟨\left({A}{\cdot }_{𝑹}{C}\right){+}_{𝑹}\left({-1}_{𝑹}{\cdot }_{𝑹}\left({B}{\cdot }_{𝑹}{D}\right)\right),\left({B}{\cdot }_{𝑹}{C}\right){+}_{𝑹}\left({A}{\cdot }_{𝑹}{D}\right)⟩\in \mathrm{V}$
2 oveq1 ${⊢}{w}={A}\to {w}{\cdot }_{𝑹}{u}={A}{\cdot }_{𝑹}{u}$
3 oveq1 ${⊢}{v}={B}\to {v}{\cdot }_{𝑹}{f}={B}{\cdot }_{𝑹}{f}$
4 3 oveq2d ${⊢}{v}={B}\to {-1}_{𝑹}{\cdot }_{𝑹}\left({v}{\cdot }_{𝑹}{f}\right)={-1}_{𝑹}{\cdot }_{𝑹}\left({B}{\cdot }_{𝑹}{f}\right)$
5 2 4 oveqan12d ${⊢}\left({w}={A}\wedge {v}={B}\right)\to \left({w}{\cdot }_{𝑹}{u}\right){+}_{𝑹}\left({-1}_{𝑹}{\cdot }_{𝑹}\left({v}{\cdot }_{𝑹}{f}\right)\right)=\left({A}{\cdot }_{𝑹}{u}\right){+}_{𝑹}\left({-1}_{𝑹}{\cdot }_{𝑹}\left({B}{\cdot }_{𝑹}{f}\right)\right)$
6 oveq1 ${⊢}{v}={B}\to {v}{\cdot }_{𝑹}{u}={B}{\cdot }_{𝑹}{u}$
7 oveq1 ${⊢}{w}={A}\to {w}{\cdot }_{𝑹}{f}={A}{\cdot }_{𝑹}{f}$
8 6 7 oveqan12rd ${⊢}\left({w}={A}\wedge {v}={B}\right)\to \left({v}{\cdot }_{𝑹}{u}\right){+}_{𝑹}\left({w}{\cdot }_{𝑹}{f}\right)=\left({B}{\cdot }_{𝑹}{u}\right){+}_{𝑹}\left({A}{\cdot }_{𝑹}{f}\right)$
9 5 8 opeq12d ${⊢}\left({w}={A}\wedge {v}={B}\right)\to ⟨\left({w}{\cdot }_{𝑹}{u}\right){+}_{𝑹}\left({-1}_{𝑹}{\cdot }_{𝑹}\left({v}{\cdot }_{𝑹}{f}\right)\right),\left({v}{\cdot }_{𝑹}{u}\right){+}_{𝑹}\left({w}{\cdot }_{𝑹}{f}\right)⟩=⟨\left({A}{\cdot }_{𝑹}{u}\right){+}_{𝑹}\left({-1}_{𝑹}{\cdot }_{𝑹}\left({B}{\cdot }_{𝑹}{f}\right)\right),\left({B}{\cdot }_{𝑹}{u}\right){+}_{𝑹}\left({A}{\cdot }_{𝑹}{f}\right)⟩$
10 oveq2 ${⊢}{u}={C}\to {A}{\cdot }_{𝑹}{u}={A}{\cdot }_{𝑹}{C}$
11 oveq2 ${⊢}{f}={D}\to {B}{\cdot }_{𝑹}{f}={B}{\cdot }_{𝑹}{D}$
12 11 oveq2d ${⊢}{f}={D}\to {-1}_{𝑹}{\cdot }_{𝑹}\left({B}{\cdot }_{𝑹}{f}\right)={-1}_{𝑹}{\cdot }_{𝑹}\left({B}{\cdot }_{𝑹}{D}\right)$
13 10 12 oveqan12d ${⊢}\left({u}={C}\wedge {f}={D}\right)\to \left({A}{\cdot }_{𝑹}{u}\right){+}_{𝑹}\left({-1}_{𝑹}{\cdot }_{𝑹}\left({B}{\cdot }_{𝑹}{f}\right)\right)=\left({A}{\cdot }_{𝑹}{C}\right){+}_{𝑹}\left({-1}_{𝑹}{\cdot }_{𝑹}\left({B}{\cdot }_{𝑹}{D}\right)\right)$
14 oveq2 ${⊢}{u}={C}\to {B}{\cdot }_{𝑹}{u}={B}{\cdot }_{𝑹}{C}$
15 oveq2 ${⊢}{f}={D}\to {A}{\cdot }_{𝑹}{f}={A}{\cdot }_{𝑹}{D}$
16 14 15 oveqan12d ${⊢}\left({u}={C}\wedge {f}={D}\right)\to \left({B}{\cdot }_{𝑹}{u}\right){+}_{𝑹}\left({A}{\cdot }_{𝑹}{f}\right)=\left({B}{\cdot }_{𝑹}{C}\right){+}_{𝑹}\left({A}{\cdot }_{𝑹}{D}\right)$
17 13 16 opeq12d ${⊢}\left({u}={C}\wedge {f}={D}\right)\to ⟨\left({A}{\cdot }_{𝑹}{u}\right){+}_{𝑹}\left({-1}_{𝑹}{\cdot }_{𝑹}\left({B}{\cdot }_{𝑹}{f}\right)\right),\left({B}{\cdot }_{𝑹}{u}\right){+}_{𝑹}\left({A}{\cdot }_{𝑹}{f}\right)⟩=⟨\left({A}{\cdot }_{𝑹}{C}\right){+}_{𝑹}\left({-1}_{𝑹}{\cdot }_{𝑹}\left({B}{\cdot }_{𝑹}{D}\right)\right),\left({B}{\cdot }_{𝑹}{C}\right){+}_{𝑹}\left({A}{\cdot }_{𝑹}{D}\right)⟩$
18 9 17 sylan9eq ${⊢}\left(\left({w}={A}\wedge {v}={B}\right)\wedge \left({u}={C}\wedge {f}={D}\right)\right)\to ⟨\left({w}{\cdot }_{𝑹}{u}\right){+}_{𝑹}\left({-1}_{𝑹}{\cdot }_{𝑹}\left({v}{\cdot }_{𝑹}{f}\right)\right),\left({v}{\cdot }_{𝑹}{u}\right){+}_{𝑹}\left({w}{\cdot }_{𝑹}{f}\right)⟩=⟨\left({A}{\cdot }_{𝑹}{C}\right){+}_{𝑹}\left({-1}_{𝑹}{\cdot }_{𝑹}\left({B}{\cdot }_{𝑹}{D}\right)\right),\left({B}{\cdot }_{𝑹}{C}\right){+}_{𝑹}\left({A}{\cdot }_{𝑹}{D}\right)⟩$
19 df-mul ${⊢}×=\left\{⟨⟨{x},{y}⟩,{z}⟩|\left(\left({x}\in ℂ\wedge {y}\in ℂ\right)\wedge \exists {w}\phantom{\rule{.4em}{0ex}}\exists {v}\phantom{\rule{.4em}{0ex}}\exists {u}\phantom{\rule{.4em}{0ex}}\exists {f}\phantom{\rule{.4em}{0ex}}\left(\left({x}=⟨{w},{v}⟩\wedge {y}=⟨{u},{f}⟩\right)\wedge {z}=⟨\left({w}{\cdot }_{𝑹}{u}\right){+}_{𝑹}\left({-1}_{𝑹}{\cdot }_{𝑹}\left({v}{\cdot }_{𝑹}{f}\right)\right),\left({v}{\cdot }_{𝑹}{u}\right){+}_{𝑹}\left({w}{\cdot }_{𝑹}{f}\right)⟩\right)\right)\right\}$
20 df-c ${⊢}ℂ=𝑹×𝑹$
21 20 eleq2i ${⊢}{x}\in ℂ↔{x}\in \left(𝑹×𝑹\right)$
22 20 eleq2i ${⊢}{y}\in ℂ↔{y}\in \left(𝑹×𝑹\right)$
23 21 22 anbi12i ${⊢}\left({x}\in ℂ\wedge {y}\in ℂ\right)↔\left({x}\in \left(𝑹×𝑹\right)\wedge {y}\in \left(𝑹×𝑹\right)\right)$
24 23 anbi1i ${⊢}\left(\left({x}\in ℂ\wedge {y}\in ℂ\right)\wedge \exists {w}\phantom{\rule{.4em}{0ex}}\exists {v}\phantom{\rule{.4em}{0ex}}\exists {u}\phantom{\rule{.4em}{0ex}}\exists {f}\phantom{\rule{.4em}{0ex}}\left(\left({x}=⟨{w},{v}⟩\wedge {y}=⟨{u},{f}⟩\right)\wedge {z}=⟨\left({w}{\cdot }_{𝑹}{u}\right){+}_{𝑹}\left({-1}_{𝑹}{\cdot }_{𝑹}\left({v}{\cdot }_{𝑹}{f}\right)\right),\left({v}{\cdot }_{𝑹}{u}\right){+}_{𝑹}\left({w}{\cdot }_{𝑹}{f}\right)⟩\right)\right)↔\left(\left({x}\in \left(𝑹×𝑹\right)\wedge {y}\in \left(𝑹×𝑹\right)\right)\wedge \exists {w}\phantom{\rule{.4em}{0ex}}\exists {v}\phantom{\rule{.4em}{0ex}}\exists {u}\phantom{\rule{.4em}{0ex}}\exists {f}\phantom{\rule{.4em}{0ex}}\left(\left({x}=⟨{w},{v}⟩\wedge {y}=⟨{u},{f}⟩\right)\wedge {z}=⟨\left({w}{\cdot }_{𝑹}{u}\right){+}_{𝑹}\left({-1}_{𝑹}{\cdot }_{𝑹}\left({v}{\cdot }_{𝑹}{f}\right)\right),\left({v}{\cdot }_{𝑹}{u}\right){+}_{𝑹}\left({w}{\cdot }_{𝑹}{f}\right)⟩\right)\right)$
25 24 oprabbii ${⊢}\left\{⟨⟨{x},{y}⟩,{z}⟩|\left(\left({x}\in ℂ\wedge {y}\in ℂ\right)\wedge \exists {w}\phantom{\rule{.4em}{0ex}}\exists {v}\phantom{\rule{.4em}{0ex}}\exists {u}\phantom{\rule{.4em}{0ex}}\exists {f}\phantom{\rule{.4em}{0ex}}\left(\left({x}=⟨{w},{v}⟩\wedge {y}=⟨{u},{f}⟩\right)\wedge {z}=⟨\left({w}{\cdot }_{𝑹}{u}\right){+}_{𝑹}\left({-1}_{𝑹}{\cdot }_{𝑹}\left({v}{\cdot }_{𝑹}{f}\right)\right),\left({v}{\cdot }_{𝑹}{u}\right){+}_{𝑹}\left({w}{\cdot }_{𝑹}{f}\right)⟩\right)\right)\right\}=\left\{⟨⟨{x},{y}⟩,{z}⟩|\left(\left({x}\in \left(𝑹×𝑹\right)\wedge {y}\in \left(𝑹×𝑹\right)\right)\wedge \exists {w}\phantom{\rule{.4em}{0ex}}\exists {v}\phantom{\rule{.4em}{0ex}}\exists {u}\phantom{\rule{.4em}{0ex}}\exists {f}\phantom{\rule{.4em}{0ex}}\left(\left({x}=⟨{w},{v}⟩\wedge {y}=⟨{u},{f}⟩\right)\wedge {z}=⟨\left({w}{\cdot }_{𝑹}{u}\right){+}_{𝑹}\left({-1}_{𝑹}{\cdot }_{𝑹}\left({v}{\cdot }_{𝑹}{f}\right)\right),\left({v}{\cdot }_{𝑹}{u}\right){+}_{𝑹}\left({w}{\cdot }_{𝑹}{f}\right)⟩\right)\right)\right\}$
26 19 25 eqtri ${⊢}×=\left\{⟨⟨{x},{y}⟩,{z}⟩|\left(\left({x}\in \left(𝑹×𝑹\right)\wedge {y}\in \left(𝑹×𝑹\right)\right)\wedge \exists {w}\phantom{\rule{.4em}{0ex}}\exists {v}\phantom{\rule{.4em}{0ex}}\exists {u}\phantom{\rule{.4em}{0ex}}\exists {f}\phantom{\rule{.4em}{0ex}}\left(\left({x}=⟨{w},{v}⟩\wedge {y}=⟨{u},{f}⟩\right)\wedge {z}=⟨\left({w}{\cdot }_{𝑹}{u}\right){+}_{𝑹}\left({-1}_{𝑹}{\cdot }_{𝑹}\left({v}{\cdot }_{𝑹}{f}\right)\right),\left({v}{\cdot }_{𝑹}{u}\right){+}_{𝑹}\left({w}{\cdot }_{𝑹}{f}\right)⟩\right)\right)\right\}$
27 1 18 26 ov3 ${⊢}\left(\left({A}\in 𝑹\wedge {B}\in 𝑹\right)\wedge \left({C}\in 𝑹\wedge {D}\in 𝑹\right)\right)\to ⟨{A},{B}⟩⟨{C},{D}⟩=⟨\left({A}{\cdot }_{𝑹}{C}\right){+}_{𝑹}\left({-1}_{𝑹}{\cdot }_{𝑹}\left({B}{\cdot }_{𝑹}{D}\right)\right),\left({B}{\cdot }_{𝑹}{C}\right){+}_{𝑹}\left({A}{\cdot }_{𝑹}{D}\right)⟩$