Metamath Proof Explorer

Theorem 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 ∈ ℂ → A ‾ ‾ = A

Proof

Step Hyp Ref Expression
1 cjcl ⊢ A ∈ ℂ → A ‾ ∈ ℂ
2 recj ⊢ A ‾ ∈ ℂ → ℜ ⁡ A ‾ ‾ = ℜ ⁡ A ‾
3 1 2 syl ⊢ A ∈ ℂ → ℜ ⁡ A ‾ ‾ = ℜ ⁡ A ‾
4 recj ⊢ A ∈ ℂ → ℜ ⁡ A ‾ = ℜ ⁡ A
5 3 4 eqtrd ⊢ A ∈ ℂ → ℜ ⁡ A ‾ ‾ = ℜ ⁡ A
6 imcj ⊢ A ‾ ∈ ℂ → ℑ ⁡ A ‾ ‾ = − ℑ ⁡ A ‾
7 1 6 syl ⊢ A ∈ ℂ → ℑ ⁡ A ‾ ‾ = − ℑ ⁡ A ‾
8 imcj ⊢ A ∈ ℂ → ℑ ⁡ A ‾ = − ℑ ⁡ A
9 8 negeqd ⊢ A ∈ ℂ → − ℑ ⁡ A ‾ = − − ℑ ⁡ A
10 imcl ⊢ A ∈ ℂ → ℑ ⁡ A ∈ ℝ
11 10 recnd ⊢ A ∈ ℂ → ℑ ⁡ A ∈ ℂ
12 11 negnegd ⊢ A ∈ ℂ → − − ℑ ⁡ A = ℑ ⁡ A
13 9 12 eqtrd ⊢ A ∈ ℂ → − ℑ ⁡ A ‾ = ℑ ⁡ A
14 7 13 eqtrd ⊢ A ∈ ℂ → ℑ ⁡ A ‾ ‾ = ℑ ⁡ A
15 14 oveq2d ⊢ A ∈ ℂ → i ⁢ ℑ ⁡ A ‾ ‾ = i ⁢ ℑ ⁡ A
16 5 15 oveq12d ⊢ A ∈ ℂ → ℜ ⁡ A ‾ ‾ + i ⁢ ℑ ⁡ A ‾ ‾ = ℜ ⁡ A + i ⁢ ℑ ⁡ A
17 cjcl ⊢ A ‾ ∈ ℂ → A ‾ ‾ ∈ ℂ
18 replim ⊢ A ‾ ‾ ∈ ℂ → A ‾ ‾ = ℜ ⁡ A ‾ ‾ + i ⁢ ℑ ⁡ A ‾ ‾
19 1 17 18 3syl ⊢ A ∈ ℂ → A ‾ ‾ = ℜ ⁡ A ‾ ‾ + i ⁢ ℑ ⁡ A ‾ ‾
20 replim ⊢ A ∈ ℂ → A = ℜ ⁡ A + i ⁢ ℑ ⁡ A
21 16 19 20 3eqtr4d ⊢ A ∈ ℂ → A ‾ ‾ = A