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