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 )