Metamath Proof Explorer

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