Metamath Proof Explorer

Theorem ipcnval

Description: Standard inner product on complex numbers. (Contributed by NM, 29-Jul-1999) (Revised by Mario Carneiro, 14-Jul-2014)

Ref Expression
Assertion ipcnval ⊢ A ∈ ℂ ∧ B ∈ ℂ → ℜ ⁡ A ⁢ B ‾ = ℜ ⁡ A ⁢ ℜ ⁡ B + ℑ ⁡ A ⁢ ℑ ⁡ B

Proof

Step Hyp Ref Expression
1 cjcl ⊢ B ∈ ℂ → B ‾ ∈ ℂ
2 remul ⊢ A ∈ ℂ ∧ B ‾ ∈ ℂ → ℜ ⁡ A ⁢ B ‾ = ℜ ⁡ A ⁢ ℜ ⁡ B ‾ − ℑ ⁡ A ⁢ ℑ ⁡ B ‾
3 1 2 sylan2 ⊢ A ∈ ℂ ∧ B ∈ ℂ → ℜ ⁡ A ⁢ B ‾ = ℜ ⁡ A ⁢ ℜ ⁡ B ‾ − ℑ ⁡ A ⁢ ℑ ⁡ B ‾
4 recj ⊢ B ∈ ℂ → ℜ ⁡ B ‾ = ℜ ⁡ B
5 4 adantl ⊢ A ∈ ℂ ∧ B ∈ ℂ → ℜ ⁡ B ‾ = ℜ ⁡ B
6 5 oveq2d ⊢ A ∈ ℂ ∧ B ∈ ℂ → ℜ ⁡ A ⁢ ℜ ⁡ B ‾ = ℜ ⁡ A ⁢ ℜ ⁡ B
7 imcj ⊢ B ∈ ℂ → ℑ ⁡ B ‾ = − ℑ ⁡ B
8 7 adantl ⊢ A ∈ ℂ ∧ B ∈ ℂ → ℑ ⁡ B ‾ = − ℑ ⁡ B
9 8 oveq2d ⊢ A ∈ ℂ ∧ B ∈ ℂ → ℑ ⁡ A ⁢ ℑ ⁡ B ‾ = ℑ ⁡ A ⁢ − ℑ ⁡ B
10 imcl ⊢ A ∈ ℂ → ℑ ⁡ A ∈ ℝ
11 10 recnd ⊢ A ∈ ℂ → ℑ ⁡ A ∈ ℂ
12 imcl ⊢ B ∈ ℂ → ℑ ⁡ B ∈ ℝ
13 12 recnd ⊢ B ∈ ℂ → ℑ ⁡ B ∈ ℂ
14 mulneg2 ⊢ ℑ ⁡ A ∈ ℂ ∧ ℑ ⁡ B ∈ ℂ → ℑ ⁡ A ⁢ − ℑ ⁡ B = − ℑ ⁡ A ⁢ ℑ ⁡ B
15 11 13 14 syl2an ⊢ A ∈ ℂ ∧ B ∈ ℂ → ℑ ⁡ A ⁢ − ℑ ⁡ B = − ℑ ⁡ A ⁢ ℑ ⁡ B
16 9 15 eqtrd ⊢ A ∈ ℂ ∧ B ∈ ℂ → ℑ ⁡ A ⁢ ℑ ⁡ B ‾ = − ℑ ⁡ A ⁢ ℑ ⁡ B
17 6 16 oveq12d ⊢ A ∈ ℂ ∧ B ∈ ℂ → ℜ ⁡ A ⁢ ℜ ⁡ B ‾ − ℑ ⁡ A ⁢ ℑ ⁡ B ‾ = ℜ ⁡ A ⁢ ℜ ⁡ B − − ℑ ⁡ A ⁢ ℑ ⁡ B
18 recl ⊢ A ∈ ℂ → ℜ ⁡ A ∈ ℝ
19 18 recnd ⊢ A ∈ ℂ → ℜ ⁡ A ∈ ℂ
20 recl ⊢ B ∈ ℂ → ℜ ⁡ B ∈ ℝ
21 20 recnd ⊢ B ∈ ℂ → ℜ ⁡ B ∈ ℂ
22 mulcl ⊢ ℜ ⁡ A ∈ ℂ ∧ ℜ ⁡ B ∈ ℂ → ℜ ⁡ A ⁢ ℜ ⁡ B ∈ ℂ
23 19 21 22 syl2an ⊢ A ∈ ℂ ∧ B ∈ ℂ → ℜ ⁡ A ⁢ ℜ ⁡ B ∈ ℂ
24 mulcl ⊢ ℑ ⁡ A ∈ ℂ ∧ ℑ ⁡ B ∈ ℂ → ℑ ⁡ A ⁢ ℑ ⁡ B ∈ ℂ
25 11 13 24 syl2an ⊢ A ∈ ℂ ∧ B ∈ ℂ → ℑ ⁡ A ⁢ ℑ ⁡ B ∈ ℂ
26 23 25 subnegd ⊢ A ∈ ℂ ∧ B ∈ ℂ → ℜ ⁡ A ⁢ ℜ ⁡ B − − ℑ ⁡ A ⁢ ℑ ⁡ B = ℜ ⁡ A ⁢ ℜ ⁡ B + ℑ ⁡ A ⁢ ℑ ⁡ B
27 3 17 26 3eqtrd ⊢ A ∈ ℂ ∧ B ∈ ℂ → ℜ ⁡ A ⁢ B ‾ = ℜ ⁡ A ⁢ ℜ ⁡ B + ℑ ⁡ A ⁢ ℑ ⁡ B