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 
|- ( A e. CC -> ( * ` ( * ` A ) ) = A )

Proof

Step Hyp Ref Expression
1 cjcl 
 |-  ( A e. CC -> ( * ` A ) e. CC )
2 recj 
 |-  ( ( * ` A ) e. CC -> ( Re ` ( * ` ( * ` A ) ) ) = ( Re ` ( * ` A ) ) )
3 1 2 syl 
 |-  ( A e. CC -> ( Re ` ( * ` ( * ` A ) ) ) = ( Re ` ( * ` A ) ) )
4 recj 
 |-  ( A e. CC -> ( Re ` ( * ` A ) ) = ( Re ` A ) )
5 3 4 eqtrd 
 |-  ( A e. CC -> ( Re ` ( * ` ( * ` A ) ) ) = ( Re ` A ) )
6 imcj 
 |-  ( ( * ` A ) e. CC -> ( Im ` ( * ` ( * ` A ) ) ) = -u ( Im ` ( * ` A ) ) )
7 1 6 syl 
 |-  ( A e. CC -> ( Im ` ( * ` ( * ` A ) ) ) = -u ( Im ` ( * ` A ) ) )
8 imcj 
 |-  ( A e. CC -> ( Im ` ( * ` A ) ) = -u ( Im ` A ) )
9 8 negeqd 
 |-  ( A e. CC -> -u ( Im ` ( * ` A ) ) = -u -u ( Im ` A ) )
10 imcl 
 |-  ( A e. CC -> ( Im ` A ) e. RR )
11 10 recnd 
 |-  ( A e. CC -> ( Im ` A ) e. CC )
12 11 negnegd 
 |-  ( A e. CC -> -u -u ( Im ` A ) = ( Im ` A ) )
13 9 12 eqtrd 
 |-  ( A e. CC -> -u ( Im ` ( * ` A ) ) = ( Im ` A ) )
14 7 13 eqtrd 
 |-  ( A e. CC -> ( Im ` ( * ` ( * ` A ) ) ) = ( Im ` A ) )
15 14 oveq2d 
 |-  ( A e. CC -> ( _i x. ( Im ` ( * ` ( * ` A ) ) ) ) = ( _i x. ( Im ` A ) ) )
16 5 15 oveq12d 
 |-  ( A e. CC -> ( ( Re ` ( * ` ( * ` A ) ) ) + ( _i x. ( Im ` ( * ` ( * ` A ) ) ) ) ) = ( ( Re ` A ) + ( _i x. ( Im ` A ) ) ) )
17 cjcl 
 |-  ( ( * ` A ) e. CC -> ( * ` ( * ` A ) ) e. CC )
18 replim 
 |-  ( ( * ` ( * ` A ) ) e. CC -> ( * ` ( * ` A ) ) = ( ( Re ` ( * ` ( * ` A ) ) ) + ( _i x. ( Im ` ( * ` ( * ` A ) ) ) ) ) )
19 1 17 18 3syl 
 |-  ( A e. CC -> ( * ` ( * ` A ) ) = ( ( Re ` ( * ` ( * ` A ) ) ) + ( _i x. ( Im ` ( * ` ( * ` A ) ) ) ) ) )
20 replim 
 |-  ( A e. CC -> A = ( ( Re ` A ) + ( _i x. ( Im ` A ) ) ) )
21 16 19 20 3eqtr4d 
 |-  ( A e. CC -> ( * ` ( * ` A ) ) = A )