Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  mulcnsr Structured version   Visualization version   GIF version

Theorem mulcnsr 9836
 Description: Multiplication of complex numbers in terms of signed reals. (Contributed by NM, 9-Aug-1995.) (New usage is discouraged.)
Assertion
Ref Expression
mulcnsr (((𝐴R𝐵R) ∧ (𝐶R𝐷R)) → (⟨𝐴, 𝐵⟩ · ⟨𝐶, 𝐷⟩) = ⟨((𝐴 ·R 𝐶) +R (-1R ·R (𝐵 ·R 𝐷))), ((𝐵 ·R 𝐶) +R (𝐴 ·R 𝐷))⟩)

Proof of Theorem mulcnsr
Dummy variables 𝑥 𝑦 𝑧 𝑤 𝑣 𝑢 𝑓 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 opex 4859 . 2 ⟨((𝐴 ·R 𝐶) +R (-1R ·R (𝐵 ·R 𝐷))), ((𝐵 ·R 𝐶) +R (𝐴 ·R 𝐷))⟩ ∈ V
2 oveq1 6556 . . . . 5 (𝑤 = 𝐴 → (𝑤 ·R 𝑢) = (𝐴 ·R 𝑢))
3 oveq1 6556 . . . . . 6 (𝑣 = 𝐵 → (𝑣 ·R 𝑓) = (𝐵 ·R 𝑓))
43oveq2d 6565 . . . . 5 (𝑣 = 𝐵 → (-1R ·R (𝑣 ·R 𝑓)) = (-1R ·R (𝐵 ·R 𝑓)))
52, 4oveqan12d 6568 . . . 4 ((𝑤 = 𝐴𝑣 = 𝐵) → ((𝑤 ·R 𝑢) +R (-1R ·R (𝑣 ·R 𝑓))) = ((𝐴 ·R 𝑢) +R (-1R ·R (𝐵 ·R 𝑓))))
6 oveq1 6556 . . . . 5 (𝑣 = 𝐵 → (𝑣 ·R 𝑢) = (𝐵 ·R 𝑢))
7 oveq1 6556 . . . . 5 (𝑤 = 𝐴 → (𝑤 ·R 𝑓) = (𝐴 ·R 𝑓))
86, 7oveqan12rd 6569 . . . 4 ((𝑤 = 𝐴𝑣 = 𝐵) → ((𝑣 ·R 𝑢) +R (𝑤 ·R 𝑓)) = ((𝐵 ·R 𝑢) +R (𝐴 ·R 𝑓)))
95, 8opeq12d 4348 . . 3 ((𝑤 = 𝐴𝑣 = 𝐵) → ⟨((𝑤 ·R 𝑢) +R (-1R ·R (𝑣 ·R 𝑓))), ((𝑣 ·R 𝑢) +R (𝑤 ·R 𝑓))⟩ = ⟨((𝐴 ·R 𝑢) +R (-1R ·R (𝐵 ·R 𝑓))), ((𝐵 ·R 𝑢) +R (𝐴 ·R 𝑓))⟩)
10 oveq2 6557 . . . . 5 (𝑢 = 𝐶 → (𝐴 ·R 𝑢) = (𝐴 ·R 𝐶))
11 oveq2 6557 . . . . . 6 (𝑓 = 𝐷 → (𝐵 ·R 𝑓) = (𝐵 ·R 𝐷))
1211oveq2d 6565 . . . . 5 (𝑓 = 𝐷 → (-1R ·R (𝐵 ·R 𝑓)) = (-1R ·R (𝐵 ·R 𝐷)))
1310, 12oveqan12d 6568 . . . 4 ((𝑢 = 𝐶𝑓 = 𝐷) → ((𝐴 ·R 𝑢) +R (-1R ·R (𝐵 ·R 𝑓))) = ((𝐴 ·R 𝐶) +R (-1R ·R (𝐵 ·R 𝐷))))
14 oveq2 6557 . . . . 5 (𝑢 = 𝐶 → (𝐵 ·R 𝑢) = (𝐵 ·R 𝐶))
15 oveq2 6557 . . . . 5 (𝑓 = 𝐷 → (𝐴 ·R 𝑓) = (𝐴 ·R 𝐷))
1614, 15oveqan12d 6568 . . . 4 ((𝑢 = 𝐶𝑓 = 𝐷) → ((𝐵 ·R 𝑢) +R (𝐴 ·R 𝑓)) = ((𝐵 ·R 𝐶) +R (𝐴 ·R 𝐷)))
1713, 16opeq12d 4348 . . 3 ((𝑢 = 𝐶𝑓 = 𝐷) → ⟨((𝐴 ·R 𝑢) +R (-1R ·R (𝐵 ·R 𝑓))), ((𝐵 ·R 𝑢) +R (𝐴 ·R 𝑓))⟩ = ⟨((𝐴 ·R 𝐶) +R (-1R ·R (𝐵 ·R 𝐷))), ((𝐵 ·R 𝐶) +R (𝐴 ·R 𝐷))⟩)
189, 17sylan9eq 2664 . 2 (((𝑤 = 𝐴𝑣 = 𝐵) ∧ (𝑢 = 𝐶𝑓 = 𝐷)) → ⟨((𝑤 ·R 𝑢) +R (-1R ·R (𝑣 ·R 𝑓))), ((𝑣 ·R 𝑢) +R (𝑤 ·R 𝑓))⟩ = ⟨((𝐴 ·R 𝐶) +R (-1R ·R (𝐵 ·R 𝐷))), ((𝐵 ·R 𝐶) +R (𝐴 ·R 𝐷))⟩)
19 df-mul 9827 . . 3 · = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) ∧ ∃𝑤𝑣𝑢𝑓((𝑥 = ⟨𝑤, 𝑣⟩ ∧ 𝑦 = ⟨𝑢, 𝑓⟩) ∧ 𝑧 = ⟨((𝑤 ·R 𝑢) +R (-1R ·R (𝑣 ·R 𝑓))), ((𝑣 ·R 𝑢) +R (𝑤 ·R 𝑓))⟩))}
20 df-c 9821 . . . . . . 7 ℂ = (R × R)
2120eleq2i 2680 . . . . . 6 (𝑥 ∈ ℂ ↔ 𝑥 ∈ (R × R))
2220eleq2i 2680 . . . . . 6 (𝑦 ∈ ℂ ↔ 𝑦 ∈ (R × R))
2321, 22anbi12i 729 . . . . 5 ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) ↔ (𝑥 ∈ (R × R) ∧ 𝑦 ∈ (R × R)))
2423anbi1i 727 . . . 4 (((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) ∧ ∃𝑤𝑣𝑢𝑓((𝑥 = ⟨𝑤, 𝑣⟩ ∧ 𝑦 = ⟨𝑢, 𝑓⟩) ∧ 𝑧 = ⟨((𝑤 ·R 𝑢) +R (-1R ·R (𝑣 ·R 𝑓))), ((𝑣 ·R 𝑢) +R (𝑤 ·R 𝑓))⟩)) ↔ ((𝑥 ∈ (R × R) ∧ 𝑦 ∈ (R × R)) ∧ ∃𝑤𝑣𝑢𝑓((𝑥 = ⟨𝑤, 𝑣⟩ ∧ 𝑦 = ⟨𝑢, 𝑓⟩) ∧ 𝑧 = ⟨((𝑤 ·R 𝑢) +R (-1R ·R (𝑣 ·R 𝑓))), ((𝑣 ·R 𝑢) +R (𝑤 ·R 𝑓))⟩)))
2524oprabbii 6608 . . 3 {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) ∧ ∃𝑤𝑣𝑢𝑓((𝑥 = ⟨𝑤, 𝑣⟩ ∧ 𝑦 = ⟨𝑢, 𝑓⟩) ∧ 𝑧 = ⟨((𝑤 ·R 𝑢) +R (-1R ·R (𝑣 ·R 𝑓))), ((𝑣 ·R 𝑢) +R (𝑤 ·R 𝑓))⟩))} = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ (R × R) ∧ 𝑦 ∈ (R × R)) ∧ ∃𝑤𝑣𝑢𝑓((𝑥 = ⟨𝑤, 𝑣⟩ ∧ 𝑦 = ⟨𝑢, 𝑓⟩) ∧ 𝑧 = ⟨((𝑤 ·R 𝑢) +R (-1R ·R (𝑣 ·R 𝑓))), ((𝑣 ·R 𝑢) +R (𝑤 ·R 𝑓))⟩))}
2619, 25eqtri 2632 . 2 · = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ (R × R) ∧ 𝑦 ∈ (R × R)) ∧ ∃𝑤𝑣𝑢𝑓((𝑥 = ⟨𝑤, 𝑣⟩ ∧ 𝑦 = ⟨𝑢, 𝑓⟩) ∧ 𝑧 = ⟨((𝑤 ·R 𝑢) +R (-1R ·R (𝑣 ·R 𝑓))), ((𝑣 ·R 𝑢) +R (𝑤 ·R 𝑓))⟩))}
271, 18, 26ov3 6695 1 (((𝐴R𝐵R) ∧ (𝐶R𝐷R)) → (⟨𝐴, 𝐵⟩ · ⟨𝐶, 𝐷⟩) = ⟨((𝐴 ·R 𝐶) +R (-1R ·R (𝐵 ·R 𝐷))), ((𝐵 ·R 𝐶) +R (𝐴 ·R 𝐷))⟩)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 383   = wceq 1475  ∃wex 1695   ∈ wcel 1977  ⟨cop 4131   × cxp 5036  (class class class)co 6549  {coprab 6550  Rcnr 9566  -1Rcm1r 9569   +R cplr 9570   ·R cmr 9571  ℂcc 9813   · cmul 9820 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pr 4833 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-sbc 3403  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-br 4584  df-opab 4644  df-id 4953  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-iota 5768  df-fun 5806  df-fv 5812  df-ov 6552  df-oprab 6553  df-c 9821  df-mul 9827 This theorem is referenced by:  mulresr  9839  mulcnsrec  9844  axmulf  9846  axi2m1  9859  axcnre  9864
 Copyright terms: Public domain W3C validator