Definition df-cj 8003

Description: Define the complex conjugate function. See cjcli 8017 for its closure and cjval 8013 for its value.

Assertion

Ref	Expression
df-cj	|- * = {<.x, y>. | (x e. CC /\ y = ((Re` x) - (_i x. (Im` x))))}

Distinct variable group:   x,y

Detailed syntax breakdown of Definition df-cj

Step	Hyp	Ref	Expression
1		ccj 7999	. 2 class *
2		vx	. . . . . 6 set x
3	2	cv 1297	. . . . 5 class x
4		cc 6384	. . . . 5 class CC
5	3, 4	wcel 1300	. . . 4 wff x e. CC
6		vy	. . . . . 6 set y
7	6	cv 1297	. . . . 5 class y
8		cre 7997	. . . . . . 7 class Re
9	3, 8	cfv 3998	. . . . . 6 class (Re` x)
10		ci 6388	. . . . . . 7 class _i
11		cim 7998	. . . . . . . 8 class Im
12	3, 11	cfv 3998	. . . . . . 7 class (Im` x)
13		cmul 6391	. . . . . . 7 class x.
14	10, 12, 13	co 4884	. . . . . 6 class (_i x. (Im` x))
15		cmin 6445	. . . . . 6 class -
16	9, 14, 15	co 4884	. . . . 5 class ((Re` x) - (_i x. (Im` x)))
17	7, 16	wceq 1298	. . . 4 wff y = ((Re` x) - (_i x. (Im` x)))
18	5, 17	wa 240	. . 3 wff (x e. CC /\ y = ((Re` x) - (_i x. (Im` x))))
19	18, 2, 6	copab 3395	. 2 class {<.x, y>. | (x e. CC /\ y = ((Re` x) - (_i x. (Im` x))))}
20	1, 19	wceq 1298	1 wff * = {<.x, y>. | (x e. CC /\ y = ((Re` x) - (_i x. (Im` x))))}

This definition is referenced by:  cjval 8013  cjcncf 8540

Copyright terms: Public domain