This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( 𝐴 ∈ ℂ → ( ∗ ‘ ( ∗ ‘ 𝐴 ) ) = 𝐴 )

Proof

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