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	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to \overline{A+B}=\bar{A}+\bar{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 \overline{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 \overline{A+B}=\Re \left(A+B\right)-\mathrm{i}\Im \left(A+B\right)$$
30		remim	$$⊢A\in ℂ\to \bar{A}=\Re \left(A\right)-\mathrm{i}\Im \left(A\right)$$
31		remim	$$⊢B\in ℂ\to \bar{B}=\Re \left(B\right)-\mathrm{i}\Im \left(B\right)$$
32	30 31	oveqan12d	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to \bar{A}+\bar{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 \overline{A+B}=\bar{A}+\bar{B}$$