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 ⊢ A ∈ 𝑹 ∧ B ∈ 𝑹 ∧ C ∈ 𝑹 ∧ D ∈ 𝑹 → A B ⁢ C D = A ⋅ 𝑹 C + 𝑹 -1 𝑹 ⋅ 𝑹 B ⋅ 𝑹 D B ⋅ 𝑹 C + 𝑹 A ⋅ 𝑹 D

Proof

Step Hyp Ref Expression
1 opex ⊢ A ⋅ 𝑹 C + 𝑹 -1 𝑹 ⋅ 𝑹 B ⋅ 𝑹 D B ⋅ 𝑹 C + 𝑹 A ⋅ 𝑹 D ∈ V
2 oveq1 ⊢ w = A → w ⋅ 𝑹 u = A ⋅ 𝑹 u
3 oveq1 ⊢ v = B → v ⋅ 𝑹 f = B ⋅ 𝑹 f
4 3 oveq2d ⊢ v = B → -1 𝑹 ⋅ 𝑹 v ⋅ 𝑹 f = -1 𝑹 ⋅ 𝑹 B ⋅ 𝑹 f
5 2 4 oveqan12d ⊢ w = A ∧ v = B → w ⋅ 𝑹 u + 𝑹 -1 𝑹 ⋅ 𝑹 v ⋅ 𝑹 f = A ⋅ 𝑹 u + 𝑹 -1 𝑹 ⋅ 𝑹 B ⋅ 𝑹 f
6 oveq1 ⊢ v = B → v ⋅ 𝑹 u = B ⋅ 𝑹 u
7 oveq1 ⊢ w = A → w ⋅ 𝑹 f = A ⋅ 𝑹 f
8 6 7 oveqan12rd ⊢ w = A ∧ v = B → v ⋅ 𝑹 u + 𝑹 w ⋅ 𝑹 f = B ⋅ 𝑹 u + 𝑹 A ⋅ 𝑹 f
9 5 8 opeq12d ⊢ w = A ∧ v = B → w ⋅ 𝑹 u + 𝑹 -1 𝑹 ⋅ 𝑹 v ⋅ 𝑹 f v ⋅ 𝑹 u + 𝑹 w ⋅ 𝑹 f = A ⋅ 𝑹 u + 𝑹 -1 𝑹 ⋅ 𝑹 B ⋅ 𝑹 f B ⋅ 𝑹 u + 𝑹 A ⋅ 𝑹 f
10 oveq2 ⊢ u = C → A ⋅ 𝑹 u = A ⋅ 𝑹 C
11 oveq2 ⊢ f = D → B ⋅ 𝑹 f = B ⋅ 𝑹 D
12 11 oveq2d ⊢ f = D → -1 𝑹 ⋅ 𝑹 B ⋅ 𝑹 f = -1 𝑹 ⋅ 𝑹 B ⋅ 𝑹 D
13 10 12 oveqan12d ⊢ u = C ∧ f = D → A ⋅ 𝑹 u + 𝑹 -1 𝑹 ⋅ 𝑹 B ⋅ 𝑹 f = A ⋅ 𝑹 C + 𝑹 -1 𝑹 ⋅ 𝑹 B ⋅ 𝑹 D
14 oveq2 ⊢ u = C → B ⋅ 𝑹 u = B ⋅ 𝑹 C
15 oveq2 ⊢ f = D → A ⋅ 𝑹 f = A ⋅ 𝑹 D
16 14 15 oveqan12d ⊢ u = C ∧ f = D → B ⋅ 𝑹 u + 𝑹 A ⋅ 𝑹 f = B ⋅ 𝑹 C + 𝑹 A ⋅ 𝑹 D
17 13 16 opeq12d ⊢ u = C ∧ f = D → A ⋅ 𝑹 u + 𝑹 -1 𝑹 ⋅ 𝑹 B ⋅ 𝑹 f B ⋅ 𝑹 u + 𝑹 A ⋅ 𝑹 f = A ⋅ 𝑹 C + 𝑹 -1 𝑹 ⋅ 𝑹 B ⋅ 𝑹 D B ⋅ 𝑹 C + 𝑹 A ⋅ 𝑹 D
18 9 17 sylan9eq ⊢ w = A ∧ v = B ∧ u = C ∧ f = D → w ⋅ 𝑹 u + 𝑹 -1 𝑹 ⋅ 𝑹 v ⋅ 𝑹 f v ⋅ 𝑹 u + 𝑹 w ⋅ 𝑹 f = A ⋅ 𝑹 C + 𝑹 -1 𝑹 ⋅ 𝑹 B ⋅ 𝑹 D B ⋅ 𝑹 C + 𝑹 A ⋅ 𝑹 D
19 df-mul ⊢ × = x y z | x ∈ ℂ ∧ y ∈ ℂ ∧ ∃ w ∃ v ∃ u ∃ f x = w v ∧ y = u f ∧ z = w ⋅ 𝑹 u + 𝑹 -1 𝑹 ⋅ 𝑹 v ⋅ 𝑹 f v ⋅ 𝑹 u + 𝑹 w ⋅ 𝑹 f
20 df-c ⊢ ℂ = 𝑹 × 𝑹
21 20 eleq2i ⊢ x ∈ ℂ ↔ x ∈ 𝑹 × 𝑹
22 20 eleq2i ⊢ y ∈ ℂ ↔ y ∈ 𝑹 × 𝑹
23 21 22 anbi12i ⊢ x ∈ ℂ ∧ y ∈ ℂ ↔ x ∈ 𝑹 × 𝑹 ∧ y ∈ 𝑹 × 𝑹
24 23 anbi1i ⊢ x ∈ ℂ ∧ y ∈ ℂ ∧ ∃ w ∃ v ∃ u ∃ f x = w v ∧ y = u f ∧ z = w ⋅ 𝑹 u + 𝑹 -1 𝑹 ⋅ 𝑹 v ⋅ 𝑹 f v ⋅ 𝑹 u + 𝑹 w ⋅ 𝑹 f ↔ x ∈ 𝑹 × 𝑹 ∧ y ∈ 𝑹 × 𝑹 ∧ ∃ w ∃ v ∃ u ∃ f x = w v ∧ y = u f ∧ z = w ⋅ 𝑹 u + 𝑹 -1 𝑹 ⋅ 𝑹 v ⋅ 𝑹 f v ⋅ 𝑹 u + 𝑹 w ⋅ 𝑹 f
25 24 oprabbii ⊢ x y z | x ∈ ℂ ∧ y ∈ ℂ ∧ ∃ w ∃ v ∃ u ∃ f x = w v ∧ y = u f ∧ z = w ⋅ 𝑹 u + 𝑹 -1 𝑹 ⋅ 𝑹 v ⋅ 𝑹 f v ⋅ 𝑹 u + 𝑹 w ⋅ 𝑹 f = x y z | x ∈ 𝑹 × 𝑹 ∧ y ∈ 𝑹 × 𝑹 ∧ ∃ w ∃ v ∃ u ∃ f x = w v ∧ y = u f ∧ z = w ⋅ 𝑹 u + 𝑹 -1 𝑹 ⋅ 𝑹 v ⋅ 𝑹 f v ⋅ 𝑹 u + 𝑹 w ⋅ 𝑹 f
26 19 25 eqtri ⊢ × = x y z | x ∈ 𝑹 × 𝑹 ∧ y ∈ 𝑹 × 𝑹 ∧ ∃ w ∃ v ∃ u ∃ f x = w v ∧ y = u f ∧ z = w ⋅ 𝑹 u + 𝑹 -1 𝑹 ⋅ 𝑹 v ⋅ 𝑹 f v ⋅ 𝑹 u + 𝑹 w ⋅ 𝑹 f
27 1 18 26 ov3 ⊢ A ∈ 𝑹 ∧ B ∈ 𝑹 ∧ C ∈ 𝑹 ∧ D ∈ 𝑹 → A B ⁢ C D = A ⋅ 𝑹 C + 𝑹 -1 𝑹 ⋅ 𝑹 B ⋅ 𝑹 D B ⋅ 𝑹 C + 𝑹 A ⋅ 𝑹 D