Metamath Proof Explorer

Theorem cjadd

Description: Complex conjugate distributes over addition. Proposition 10-3.4(a) of Gleason p. 133. (Contributed by NM, 31-Jul-1999) (Revised by Mario Carneiro, 14-Jul-2014)

Ref Expression
Assertion cjadd ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ∗ ‘ ( 𝐴 + 𝐵 ) ) = ( ( ∗ ‘ 𝐴 ) + ( ∗ ‘ 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 readd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ℜ ‘ ( 𝐴 + 𝐵 ) ) = ( ( ℜ ‘ 𝐴 ) + ( ℜ ‘ 𝐵 ) ) )
2 imadd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ℑ ‘ ( 𝐴 + 𝐵 ) ) = ( ( ℑ ‘ 𝐴 ) + ( ℑ ‘ 𝐵 ) ) )
3 2 oveq2d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( i · ( ℑ ‘ ( 𝐴 + 𝐵 ) ) ) = ( i · ( ( ℑ ‘ 𝐴 ) + ( ℑ ‘ 𝐵 ) ) ) )
4 ax-icn ⊢ i ∈ ℂ
5 4 a1i ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → i ∈ ℂ )
6 imcl ⊢ ( 𝐴 ∈ ℂ → ( ℑ ‘ 𝐴 ) ∈ ℝ )
7 6 adantr ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ℑ ‘ 𝐴 ) ∈ ℝ )
8 7 recnd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ℑ ‘ 𝐴 ) ∈ ℂ )
9 imcl ⊢ ( 𝐵 ∈ ℂ → ( ℑ ‘ 𝐵 ) ∈ ℝ )
10 9 adantl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ℑ ‘ 𝐵 ) ∈ ℝ )
11 10 recnd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ℑ ‘ 𝐵 ) ∈ ℂ )
12 5 8 11 adddid ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( i · ( ( ℑ ‘ 𝐴 ) + ( ℑ ‘ 𝐵 ) ) ) = ( ( i · ( ℑ ‘ 𝐴 ) ) + ( i · ( ℑ ‘ 𝐵 ) ) ) )
13 3 12 eqtrd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( i · ( ℑ ‘ ( 𝐴 + 𝐵 ) ) ) = ( ( i · ( ℑ ‘ 𝐴 ) ) + ( i · ( ℑ ‘ 𝐵 ) ) ) )
14 1 13 oveq12d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( ℜ ‘ ( 𝐴 + 𝐵 ) ) − ( i · ( ℑ ‘ ( 𝐴 + 𝐵 ) ) ) ) = ( ( ( ℜ ‘ 𝐴 ) + ( ℜ ‘ 𝐵 ) ) − ( ( i · ( ℑ ‘ 𝐴 ) ) + ( i · ( ℑ ‘ 𝐵 ) ) ) ) )
15 recl ⊢ ( 𝐴 ∈ ℂ → ( ℜ ‘ 𝐴 ) ∈ ℝ )
16 15 adantr ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ℜ ‘ 𝐴 ) ∈ ℝ )
17 16 recnd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ℜ ‘ 𝐴 ) ∈ ℂ )
18 recl ⊢ ( 𝐵 ∈ ℂ → ( ℜ ‘ 𝐵 ) ∈ ℝ )
19 18 adantl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ℜ ‘ 𝐵 ) ∈ ℝ )
20 19 recnd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ℜ ‘ 𝐵 ) ∈ ℂ )
21 mulcl ⊢ ( ( i ∈ ℂ ∧ ( ℑ ‘ 𝐴 ) ∈ ℂ ) → ( i · ( ℑ ‘ 𝐴 ) ) ∈ ℂ )
22 4 8 21 sylancr ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( i · ( ℑ ‘ 𝐴 ) ) ∈ ℂ )
23 mulcl ⊢ ( ( i ∈ ℂ ∧ ( ℑ ‘ 𝐵 ) ∈ ℂ ) → ( i · ( ℑ ‘ 𝐵 ) ) ∈ ℂ )
24 4 11 23 sylancr ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( i · ( ℑ ‘ 𝐵 ) ) ∈ ℂ )
25 17 20 22 24 addsub4d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( ( ℜ ‘ 𝐴 ) + ( ℜ ‘ 𝐵 ) ) − ( ( i · ( ℑ ‘ 𝐴 ) ) + ( i · ( ℑ ‘ 𝐵 ) ) ) ) = ( ( ( ℜ ‘ 𝐴 ) − ( i · ( ℑ ‘ 𝐴 ) ) ) + ( ( ℜ ‘ 𝐵 ) − ( i · ( ℑ ‘ 𝐵 ) ) ) ) )
26 14 25 eqtrd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( ℜ ‘ ( 𝐴 + 𝐵 ) ) − ( i · ( ℑ ‘ ( 𝐴 + 𝐵 ) ) ) ) = ( ( ( ℜ ‘ 𝐴 ) − ( i · ( ℑ ‘ 𝐴 ) ) ) + ( ( ℜ ‘ 𝐵 ) − ( i · ( ℑ ‘ 𝐵 ) ) ) ) )
27 addcl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 + 𝐵 ) ∈ ℂ )
28 remim ⊢ ( ( 𝐴 + 𝐵 ) ∈ ℂ → ( ∗ ‘ ( 𝐴 + 𝐵 ) ) = ( ( ℜ ‘ ( 𝐴 + 𝐵 ) ) − ( i · ( ℑ ‘ ( 𝐴 + 𝐵 ) ) ) ) )
29 27 28 syl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ∗ ‘ ( 𝐴 + 𝐵 ) ) = ( ( ℜ ‘ ( 𝐴 + 𝐵 ) ) − ( i · ( ℑ ‘ ( 𝐴 + 𝐵 ) ) ) ) )
30 remim ⊢ ( 𝐴 ∈ ℂ → ( ∗ ‘ 𝐴 ) = ( ( ℜ ‘ 𝐴 ) − ( i · ( ℑ ‘ 𝐴 ) ) ) )
31 remim ⊢ ( 𝐵 ∈ ℂ → ( ∗ ‘ 𝐵 ) = ( ( ℜ ‘ 𝐵 ) − ( i · ( ℑ ‘ 𝐵 ) ) ) )
32 30 31 oveqan12d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( ∗ ‘ 𝐴 ) + ( ∗ ‘ 𝐵 ) ) = ( ( ( ℜ ‘ 𝐴 ) − ( i · ( ℑ ‘ 𝐴 ) ) ) + ( ( ℜ ‘ 𝐵 ) − ( i · ( ℑ ‘ 𝐵 ) ) ) ) )
33 26 29 32 3eqtr4d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ∗ ‘ ( 𝐴 + 𝐵 ) ) = ( ( ∗ ‘ 𝐴 ) + ( ∗ ‘ 𝐵 ) ) )