# 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 )`