Definition df-cj 11024

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

Assertion

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

Distinct variable group:   x, y

Detailed syntax breakdown of Definition df-cj

Step	Hyp	Ref	Expression
1		ccj 11021	. 2 class *
2		vx	. . 3 setvar x
3		cc 7894	. . 3 class CC
4	2	cv 1363	. . . . . . 7 class x
5		vy	. . . . . . . 8 setvar y
6	5	cv 1363	. . . . . . 7 class y
7		caddc 7899	. . . . . . 7 class +
8	4, 6, 7	co 5925	. . . . . 6 class ( x + y )
9		cr 7895	. . . . . 6 class RR
10	8, 9	wcel 2167	. . . . 5 wff ( x + y ) e. RR
11		ci 7898	. . . . . . 7 class _i
12		cmin 8214	. . . . . . . 8 class -
13	4, 6, 12	co 5925	. . . . . . 7 class ( x - y )
14		cmul 7901	. . . . . . 7 class x.
15	11, 13, 14	co 5925	. . . . . 6 class ( _i x. ( x - y ) )
16	15, 9	wcel 2167	. . . . 5 wff ( _i x. ( x - y ) ) e. RR
17	10, 16	wa 104	. . . 4 wff ( ( x + y ) e. RR /\ ( _i x. ( x - y ) ) e. RR )
18	17, 5, 3	crio 5879	. . 3 class ( iota_ y e. CC ( ( x + y ) e. RR /\ ( _i x. ( x - y ) ) e. RR ) )
19	2, 3, 18	cmpt 4095	. 2 class ( x e. CC |-> ( iota_ y e. CC ( ( x + y ) e. RR /\ ( _i x. ( x - y ) ) e. RR ) ) )
20	1, 19	wceq 1364	1 wff * = ( x e. CC |-> ( iota_ y e. CC ( ( x + y ) e. RR /\ ( _i x. ( x - y ) ) e. RR ) ) )

This definition is referenced by:  cjval  11027  cjf  11029