# 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 𝐷 ) ) ⟩ )