# 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 ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to \stackrel{‾}{{A}+{B}}=\stackrel{‾}{{A}}+\stackrel{‾}{{B}}$

### Proof

Step Hyp Ref Expression
1 readd ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to \Re \left({A}+{B}\right)=\Re \left({A}\right)+\Re \left({B}\right)$
2 imadd ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to \Im \left({A}+{B}\right)=\Im \left({A}\right)+\Im \left({B}\right)$
3 2 oveq2d ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to \mathrm{i}\Im \left({A}+{B}\right)=\mathrm{i}\left(\Im \left({A}\right)+\Im \left({B}\right)\right)$
4 ax-icn ${⊢}\mathrm{i}\in ℂ$
5 4 a1i ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to \mathrm{i}\in ℂ$
6 imcl ${⊢}{A}\in ℂ\to \Im \left({A}\right)\in ℝ$
7 6 adantr ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to \Im \left({A}\right)\in ℝ$
8 7 recnd ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to \Im \left({A}\right)\in ℂ$
9 imcl ${⊢}{B}\in ℂ\to \Im \left({B}\right)\in ℝ$
10 9 adantl ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to \Im \left({B}\right)\in ℝ$
11 10 recnd ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to \Im \left({B}\right)\in ℂ$
12 5 8 11 adddid ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to \mathrm{i}\left(\Im \left({A}\right)+\Im \left({B}\right)\right)=\mathrm{i}\Im \left({A}\right)+\mathrm{i}\Im \left({B}\right)$
13 3 12 eqtrd ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to \mathrm{i}\Im \left({A}+{B}\right)=\mathrm{i}\Im \left({A}\right)+\mathrm{i}\Im \left({B}\right)$
14 1 13 oveq12d ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to \Re \left({A}+{B}\right)-\mathrm{i}\Im \left({A}+{B}\right)=\Re \left({A}\right)+\Re \left({B}\right)-\left(\mathrm{i}\Im \left({A}\right)+\mathrm{i}\Im \left({B}\right)\right)$
15 recl ${⊢}{A}\in ℂ\to \Re \left({A}\right)\in ℝ$
16 15 adantr ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to \Re \left({A}\right)\in ℝ$
17 16 recnd ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to \Re \left({A}\right)\in ℂ$
18 recl ${⊢}{B}\in ℂ\to \Re \left({B}\right)\in ℝ$
19 18 adantl ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to \Re \left({B}\right)\in ℝ$
20 19 recnd ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to \Re \left({B}\right)\in ℂ$
21 mulcl ${⊢}\left(\mathrm{i}\in ℂ\wedge \Im \left({A}\right)\in ℂ\right)\to \mathrm{i}\Im \left({A}\right)\in ℂ$
22 4 8 21 sylancr ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to \mathrm{i}\Im \left({A}\right)\in ℂ$
23 mulcl ${⊢}\left(\mathrm{i}\in ℂ\wedge \Im \left({B}\right)\in ℂ\right)\to \mathrm{i}\Im \left({B}\right)\in ℂ$
24 4 11 23 sylancr ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to \mathrm{i}\Im \left({B}\right)\in ℂ$
25 17 20 22 24 addsub4d ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to \Re \left({A}\right)+\Re \left({B}\right)-\left(\mathrm{i}\Im \left({A}\right)+\mathrm{i}\Im \left({B}\right)\right)=\left(\Re \left({A}\right)-\mathrm{i}\Im \left({A}\right)\right)+\Re \left({B}\right)-\mathrm{i}\Im \left({B}\right)$
26 14 25 eqtrd ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to \Re \left({A}+{B}\right)-\mathrm{i}\Im \left({A}+{B}\right)=\left(\Re \left({A}\right)-\mathrm{i}\Im \left({A}\right)\right)+\Re \left({B}\right)-\mathrm{i}\Im \left({B}\right)$
27 addcl ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to {A}+{B}\in ℂ$
28 remim ${⊢}{A}+{B}\in ℂ\to \stackrel{‾}{{A}+{B}}=\Re \left({A}+{B}\right)-\mathrm{i}\Im \left({A}+{B}\right)$
29 27 28 syl ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to \stackrel{‾}{{A}+{B}}=\Re \left({A}+{B}\right)-\mathrm{i}\Im \left({A}+{B}\right)$
30 remim ${⊢}{A}\in ℂ\to \stackrel{‾}{{A}}=\Re \left({A}\right)-\mathrm{i}\Im \left({A}\right)$
31 remim ${⊢}{B}\in ℂ\to \stackrel{‾}{{B}}=\Re \left({B}\right)-\mathrm{i}\Im \left({B}\right)$
32 30 31 oveqan12d ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to \stackrel{‾}{{A}}+\stackrel{‾}{{B}}=\left(\Re \left({A}\right)-\mathrm{i}\Im \left({A}\right)\right)+\Re \left({B}\right)-\mathrm{i}\Im \left({B}\right)$
33 26 29 32 3eqtr4d ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to \stackrel{‾}{{A}+{B}}=\stackrel{‾}{{A}}+\stackrel{‾}{{B}}$