Definition df-cj

Description: Define the complex conjugate function. See cjcli for its closure and cjval for its value. (Contributed by NM, 9-May-1999) (Revised by Mario Carneiro, 6-Nov-2013)

	Ref	Expression
Assertion	df-cj	|- * = ( x e. CC |-> ( iota_ y e. CC ( ( x + y ) e. RR /\ ( _i x. ( x - y ) ) e. RR ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccj	|- *
1		vx	|- x
2		cc	|- CC
3		vy	|- y
4	1	cv	|- x
5		caddc	|- +
6	3	cv	|- y
7	4 6 5	co	|- ( x + y )
8		cr	|- RR
9	7 8	wcel	|- ( x + y ) e. RR
10		ci	|- _i
11		cmul	|- x.
12		cmin	|- -
13	4 6 12	co	|- ( x - y )
14	10 13 11	co	|- ( _i x. ( x - y ) )
15	14 8	wcel	|- ( _i x. ( x - y ) ) e. RR
16	9 15	wa	|- ( ( x + y ) e. RR /\ ( _i x. ( x - y ) ) e. RR )
17	16 3 2	crio	|- ( iota_ y e. CC ( ( x + y ) e. RR /\ ( _i x. ( x - y ) ) e. RR ) )
18	1 2 17	cmpt	|- ( x e. CC |-> ( iota_ y e. CC ( ( x + y ) e. RR /\ ( _i x. ( x - y ) ) e. RR ) ) )
19	0 18	wceq	|- * = ( x e. CC |-> ( iota_ y e. CC ( ( x + y ) e. RR /\ ( _i x. ( x - y ) ) e. RR ) ) )