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 ⊢A∈ℂ∧B∈ℂ→A+B‾=A‾+B‾

Proof

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