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 ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ℜ ‘ ( 𝐴 · ( ∗ ‘ 𝐵 ) ) ) = ( ( ( ℜ ‘ 𝐴 ) · ( ℜ ‘ 𝐵 ) ) + ( ( ℑ ‘ 𝐴 ) · ( ℑ ‘ 𝐵 ) ) ) )

Proof

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