cjcj

Description: The conjugate of the conjugate is the original complex number. Proposition 10-3.4(e) of Gleason p. 133. (Contributed by NM, 29-Jul-1999) (Proof shortened by Mario Carneiro, 14-Jul-2014)

		Ref	Expression
	Assertion	cjcj	$⊢ A \in ℂ \to \overline{\overline{A}} = A$

Proof

Step	Hyp	Ref	Expression
1		cjcl	$⊢ A \in ℂ \to \overline{A} \in ℂ$
2		recj	$⊢ \overline{A} \in ℂ \to ℜ (\overline{\overline{A}}) = ℜ (\overline{A})$
3	1 2	syl	$⊢ A \in ℂ \to ℜ (\overline{\overline{A}}) = ℜ (\overline{A})$
4		recj	$⊢ A \in ℂ \to ℜ (\overline{A}) = ℜ (A)$
5	3 4	eqtrd	$⊢ A \in ℂ \to ℜ (\overline{\overline{A}}) = ℜ (A)$
6		imcj	$⊢ \overline{A} \in ℂ \to ℑ (\overline{\overline{A}}) = - ℑ (\overline{A})$
7	1 6	syl	$⊢ A \in ℂ \to ℑ (\overline{\overline{A}}) = - ℑ (\overline{A})$
8		imcj	$⊢ A \in ℂ \to ℑ (\overline{A}) = - ℑ (A)$
9	8	negeqd	$⊢ A \in ℂ \to - ℑ (\overline{A}) = - (- ℑ (A))$
10		imcl	$⊢ A \in ℂ \to ℑ (A) \in ℝ$
11	10	recnd	$⊢ A \in ℂ \to ℑ (A) \in ℂ$
12	11	negnegd	$⊢ A \in ℂ \to - (- ℑ (A)) = ℑ (A)$
13	9 12	eqtrd	$⊢ A \in ℂ \to - ℑ (\overline{A}) = ℑ (A)$
14	7 13	eqtrd	$⊢ A \in ℂ \to ℑ (\overline{\overline{A}}) = ℑ (A)$
15	14	oveq2d	$⊢ A \in ℂ \to i ℑ (\overline{\overline{A}}) = i ℑ (A)$
16	5 15	oveq12d	$⊢ A \in ℂ \to ℜ (\overline{\overline{A}}) + i ℑ (\overline{\overline{A}}) = ℜ (A) + i ℑ (A)$
17		cjcl	$⊢ \overline{A} \in ℂ \to \overline{\overline{A}} \in ℂ$
18		replim	$⊢ \overline{\overline{A}} \in ℂ \to \overline{\overline{A}} = ℜ (\overline{\overline{A}}) + i ℑ (\overline{\overline{A}})$
19	1 17 18	3syl	$⊢ A \in ℂ \to \overline{\overline{A}} = ℜ (\overline{\overline{A}}) + i ℑ (\overline{\overline{A}})$
20		replim	$⊢ A \in ℂ \to A = ℜ (A) + i ℑ (A)$
21	16 19 20	3eqtr4d	$⊢ A \in ℂ \to \overline{\overline{A}} = A$

Metamath Proof Explorer

Theorem cjcj

Proof