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 ( ( ( 𝐴 ∈ R ∧ 𝐵 ∈ R ) ∧ ( 𝐶 ∈ R ∧ 𝐷 ∈ R ) ) → ( ⟨ 𝐴 , 𝐵 ⟩ · ⟨ 𝐶 , 𝐷 ⟩ ) = ⟨ ( ( 𝐴 ·R 𝐶 ) +R ( -1R ·R ( 𝐵 ·R 𝐷 ) ) ) , ( ( 𝐵 ·R 𝐶 ) +R ( 𝐴 ·R 𝐷 ) ) ⟩ )

Proof

Step Hyp Ref Expression
1 opex ⊢ ⟨ ( ( 𝐴 ·R 𝐶 ) +R ( -1R ·R ( 𝐵 ·R 𝐷 ) ) ) , ( ( 𝐵 ·R 𝐶 ) +R ( 𝐴 ·R 𝐷 ) ) ⟩ ∈ V
2 oveq1 ⊢ ( 𝑤 = 𝐴 → ( 𝑤 ·R 𝑢 ) = ( 𝐴 ·R 𝑢 ) )
3 oveq1 ⊢ ( 𝑣 = 𝐵 → ( 𝑣 ·R 𝑓 ) = ( 𝐵 ·R 𝑓 ) )
4 3 oveq2d ⊢ ( 𝑣 = 𝐵 → ( -1R ·R ( 𝑣 ·R 𝑓 ) ) = ( -1R ·R ( 𝐵 ·R 𝑓 ) ) )
5 2 4 oveqan12d ⊢ ( ( 𝑤 = 𝐴 ∧ 𝑣 = 𝐵 ) → ( ( 𝑤 ·R 𝑢 ) +R ( -1R ·R ( 𝑣 ·R 𝑓 ) ) ) = ( ( 𝐴 ·R 𝑢 ) +R ( -1R ·R ( 𝐵 ·R 𝑓 ) ) ) )
6 oveq1 ⊢ ( 𝑣 = 𝐵 → ( 𝑣 ·R 𝑢 ) = ( 𝐵 ·R 𝑢 ) )
7 oveq1 ⊢ ( 𝑤 = 𝐴 → ( 𝑤 ·R 𝑓 ) = ( 𝐴 ·R 𝑓 ) )
8 6 7 oveqan12rd ⊢ ( ( 𝑤 = 𝐴 ∧ 𝑣 = 𝐵 ) → ( ( 𝑣 ·R 𝑢 ) +R ( 𝑤 ·R 𝑓 ) ) = ( ( 𝐵 ·R 𝑢 ) +R ( 𝐴 ·R 𝑓 ) ) )
9 5 8 opeq12d ⊢ ( ( 𝑤 = 𝐴 ∧ 𝑣 = 𝐵 ) → ⟨ ( ( 𝑤 ·R 𝑢 ) +R ( -1R ·R ( 𝑣 ·R 𝑓 ) ) ) , ( ( 𝑣 ·R 𝑢 ) +R ( 𝑤 ·R 𝑓 ) ) ⟩ = ⟨ ( ( 𝐴 ·R 𝑢 ) +R ( -1R ·R ( 𝐵 ·R 𝑓 ) ) ) , ( ( 𝐵 ·R 𝑢 ) +R ( 𝐴 ·R 𝑓 ) ) ⟩ )
10 oveq2 ⊢ ( 𝑢 = 𝐶 → ( 𝐴 ·R 𝑢 ) = ( 𝐴 ·R 𝐶 ) )
11 oveq2 ⊢ ( 𝑓 = 𝐷 → ( 𝐵 ·R 𝑓 ) = ( 𝐵 ·R 𝐷 ) )
12 11 oveq2d ⊢ ( 𝑓 = 𝐷 → ( -1R ·R ( 𝐵 ·R 𝑓 ) ) = ( -1R ·R ( 𝐵 ·R 𝐷 ) ) )
13 10 12 oveqan12d ⊢ ( ( 𝑢 = 𝐶 ∧ 𝑓 = 𝐷 ) → ( ( 𝐴 ·R 𝑢 ) +R ( -1R ·R ( 𝐵 ·R 𝑓 ) ) ) = ( ( 𝐴 ·R 𝐶 ) +R ( -1R ·R ( 𝐵 ·R 𝐷 ) ) ) )
14 oveq2 ⊢ ( 𝑢 = 𝐶 → ( 𝐵 ·R 𝑢 ) = ( 𝐵 ·R 𝐶 ) )
15 oveq2 ⊢ ( 𝑓 = 𝐷 → ( 𝐴 ·R 𝑓 ) = ( 𝐴 ·R 𝐷 ) )
16 14 15 oveqan12d ⊢ ( ( 𝑢 = 𝐶 ∧ 𝑓 = 𝐷 ) → ( ( 𝐵 ·R 𝑢 ) +R ( 𝐴 ·R 𝑓 ) ) = ( ( 𝐵 ·R 𝐶 ) +R ( 𝐴 ·R 𝐷 ) ) )
17 13 16 opeq12d ⊢ ( ( 𝑢 = 𝐶 ∧ 𝑓 = 𝐷 ) → ⟨ ( ( 𝐴 ·R 𝑢 ) +R ( -1R ·R ( 𝐵 ·R 𝑓 ) ) ) , ( ( 𝐵 ·R 𝑢 ) +R ( 𝐴 ·R 𝑓 ) ) ⟩ = ⟨ ( ( 𝐴 ·R 𝐶 ) +R ( -1R ·R ( 𝐵 ·R 𝐷 ) ) ) , ( ( 𝐵 ·R 𝐶 ) +R ( 𝐴 ·R 𝐷 ) ) ⟩ )
18 9 17 sylan9eq ⊢ ( ( ( 𝑤 = 𝐴 ∧ 𝑣 = 𝐵 ) ∧ ( 𝑢 = 𝐶 ∧ 𝑓 = 𝐷 ) ) → ⟨ ( ( 𝑤 ·R 𝑢 ) +R ( -1R ·R ( 𝑣 ·R 𝑓 ) ) ) , ( ( 𝑣 ·R 𝑢 ) +R ( 𝑤 ·R 𝑓 ) ) ⟩ = ⟨ ( ( 𝐴 ·R 𝐶 ) +R ( -1R ·R ( 𝐵 ·R 𝐷 ) ) ) , ( ( 𝐵 ·R 𝐶 ) +R ( 𝐴 ·R 𝐷 ) ) ⟩ )
19 df-mul ⊢ · = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) ∧ ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ∃ 𝑓 ( ( 𝑥 = ⟨ 𝑤 , 𝑣 ⟩ ∧ 𝑦 = ⟨ 𝑢 , 𝑓 ⟩ ) ∧ 𝑧 = ⟨ ( ( 𝑤 ·R 𝑢 ) +R ( -1R ·R ( 𝑣 ·R 𝑓 ) ) ) , ( ( 𝑣 ·R 𝑢 ) +R ( 𝑤 ·R 𝑓 ) ) ⟩ ) ) }
20 df-c ⊢ ℂ = ( R × R )
21 20 eleq2i ⊢ ( 𝑥 ∈ ℂ ↔ 𝑥 ∈ ( R × R ) )
22 20 eleq2i ⊢ ( 𝑦 ∈ ℂ ↔ 𝑦 ∈ ( R × R ) )
23 21 22 anbi12i ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) ↔ ( 𝑥 ∈ ( R × R ) ∧ 𝑦 ∈ ( R × R ) ) )
24 23 anbi1i ⊢ ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) ∧ ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ∃ 𝑓 ( ( 𝑥 = ⟨ 𝑤 , 𝑣 ⟩ ∧ 𝑦 = ⟨ 𝑢 , 𝑓 ⟩ ) ∧ 𝑧 = ⟨ ( ( 𝑤 ·R 𝑢 ) +R ( -1R ·R ( 𝑣 ·R 𝑓 ) ) ) , ( ( 𝑣 ·R 𝑢 ) +R ( 𝑤 ·R 𝑓 ) ) ⟩ ) ) ↔ ( ( 𝑥 ∈ ( R × R ) ∧ 𝑦 ∈ ( R × R ) ) ∧ ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ∃ 𝑓 ( ( 𝑥 = ⟨ 𝑤 , 𝑣 ⟩ ∧ 𝑦 = ⟨ 𝑢 , 𝑓 ⟩ ) ∧ 𝑧 = ⟨ ( ( 𝑤 ·R 𝑢 ) +R ( -1R ·R ( 𝑣 ·R 𝑓 ) ) ) , ( ( 𝑣 ·R 𝑢 ) +R ( 𝑤 ·R 𝑓 ) ) ⟩ ) ) )
25 24 oprabbii ⊢ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) ∧ ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ∃ 𝑓 ( ( 𝑥 = ⟨ 𝑤 , 𝑣 ⟩ ∧ 𝑦 = ⟨ 𝑢 , 𝑓 ⟩ ) ∧ 𝑧 = ⟨ ( ( 𝑤 ·R 𝑢 ) +R ( -1R ·R ( 𝑣 ·R 𝑓 ) ) ) , ( ( 𝑣 ·R 𝑢 ) +R ( 𝑤 ·R 𝑓 ) ) ⟩ ) ) } = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ ( R × R ) ∧ 𝑦 ∈ ( R × R ) ) ∧ ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ∃ 𝑓 ( ( 𝑥 = ⟨ 𝑤 , 𝑣 ⟩ ∧ 𝑦 = ⟨ 𝑢 , 𝑓 ⟩ ) ∧ 𝑧 = ⟨ ( ( 𝑤 ·R 𝑢 ) +R ( -1R ·R ( 𝑣 ·R 𝑓 ) ) ) , ( ( 𝑣 ·R 𝑢 ) +R ( 𝑤 ·R 𝑓 ) ) ⟩ ) ) }
26 19 25 eqtri ⊢ · = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ ( R × R ) ∧ 𝑦 ∈ ( R × R ) ) ∧ ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ∃ 𝑓 ( ( 𝑥 = ⟨ 𝑤 , 𝑣 ⟩ ∧ 𝑦 = ⟨ 𝑢 , 𝑓 ⟩ ) ∧ 𝑧 = ⟨ ( ( 𝑤 ·R 𝑢 ) +R ( -1R ·R ( 𝑣 ·R 𝑓 ) ) ) , ( ( 𝑣 ·R 𝑢 ) +R ( 𝑤 ·R 𝑓 ) ) ⟩ ) ) }
27 1 18 26 ov3 ⊢ ( ( ( 𝐴 ∈ R ∧ 𝐵 ∈ R ) ∧ ( 𝐶 ∈ R ∧ 𝐷 ∈ R ) ) → ( ⟨ 𝐴 , 𝐵 ⟩ · ⟨ 𝐶 , 𝐷 ⟩ ) = ⟨ ( ( 𝐴 ·R 𝐶 ) +R ( -1R ·R ( 𝐵 ·R 𝐷 ) ) ) , ( ( 𝐵 ·R 𝐶 ) +R ( 𝐴 ·R 𝐷 ) ) ⟩ )