Metamath Proof Explorer

Theorem cjreim

Description: The conjugate of a representation of a complex number in terms of real and imaginary parts. (Contributed by NM, 1-Jul-2005)

Ref Expression
Assertion cjreim ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ∗ ‘ ( 𝐴 + ( i · 𝐵 ) ) ) = ( 𝐴 − ( i · 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 recn ⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℂ )
2 ax-icn ⊢ i ∈ ℂ
3 recn ⊢ ( 𝐵 ∈ ℝ → 𝐵 ∈ ℂ )
4 mulcl ⊢ ( ( i ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( i · 𝐵 ) ∈ ℂ )
5 2 3 4 sylancr ⊢ ( 𝐵 ∈ ℝ → ( i · 𝐵 ) ∈ ℂ )
6 cjadd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( i · 𝐵 ) ∈ ℂ ) → ( ∗ ‘ ( 𝐴 + ( i · 𝐵 ) ) ) = ( ( ∗ ‘ 𝐴 ) + ( ∗ ‘ ( i · 𝐵 ) ) ) )
7 1 5 6 syl2an ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ∗ ‘ ( 𝐴 + ( i · 𝐵 ) ) ) = ( ( ∗ ‘ 𝐴 ) + ( ∗ ‘ ( i · 𝐵 ) ) ) )
8 cjre ⊢ ( 𝐴 ∈ ℝ → ( ∗ ‘ 𝐴 ) = 𝐴 )
9 cjmul ⊢ ( ( i ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ∗ ‘ ( i · 𝐵 ) ) = ( ( ∗ ‘ i ) · ( ∗ ‘ 𝐵 ) ) )
10 2 3 9 sylancr ⊢ ( 𝐵 ∈ ℝ → ( ∗ ‘ ( i · 𝐵 ) ) = ( ( ∗ ‘ i ) · ( ∗ ‘ 𝐵 ) ) )
11 cji ⊢ ( ∗ ‘ i ) = - i
12 11 a1i ⊢ ( 𝐵 ∈ ℝ → ( ∗ ‘ i ) = - i )
13 cjre ⊢ ( 𝐵 ∈ ℝ → ( ∗ ‘ 𝐵 ) = 𝐵 )
14 12 13 oveq12d ⊢ ( 𝐵 ∈ ℝ → ( ( ∗ ‘ i ) · ( ∗ ‘ 𝐵 ) ) = ( - i · 𝐵 ) )
15 mulneg1 ⊢ ( ( i ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( - i · 𝐵 ) = - ( i · 𝐵 ) )
16 2 3 15 sylancr ⊢ ( 𝐵 ∈ ℝ → ( - i · 𝐵 ) = - ( i · 𝐵 ) )
17 10 14 16 3eqtrd ⊢ ( 𝐵 ∈ ℝ → ( ∗ ‘ ( i · 𝐵 ) ) = - ( i · 𝐵 ) )
18 8 17 oveqan12d ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( ∗ ‘ 𝐴 ) + ( ∗ ‘ ( i · 𝐵 ) ) ) = ( 𝐴 + - ( i · 𝐵 ) ) )
19 negsub ⊢ ( ( 𝐴 ∈ ℂ ∧ ( i · 𝐵 ) ∈ ℂ ) → ( 𝐴 + - ( i · 𝐵 ) ) = ( 𝐴 − ( i · 𝐵 ) ) )
20 1 5 19 syl2an ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 + - ( i · 𝐵 ) ) = ( 𝐴 − ( i · 𝐵 ) ) )
21 7 18 20 3eqtrd ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ∗ ‘ ( 𝐴 + ( i · 𝐵 ) ) ) = ( 𝐴 − ( i · 𝐵 ) ) )