Definition df-cj 4792

Description: Define the complex conjugate function. See cjcl 4804 for its closure and cjvalt 4799 for its value.

Assertion

Ref	Expression
df-cj	⊢ ∗ = {⟨x, y⟩∣(x ∈ ℂ ∧ y = ((ℜ ‘x) − ((ℑ ‘x) · i)))}

Distinct variable group(s):   x,y

Detailed syntax breakdown of Definition df-cj

Step	Hyp	Ref	Expression
1		ccj 4788	. 2 class ∗
2		vx	. . . . . 6 set x
3	2	cv 1089	. . . . 5 class x
4		cc 4026	. . . . 5 class ℂ
5	3, 4	wcel 1092	. . . 4 wff x ∈ ℂ
6		vy	. . . . . 6 set y
7	6	cv 1089	. . . . 5 class y
8		cre 4786	. . . . . . 7 class ℜ
9	3, 8	cfv 2422	. . . . . 6 class (ℜ ‘x)
10		cim 4787	. . . . . . . 8 class ℑ
11	3, 10	cfv 2422	. . . . . . 7 class (ℑ ‘x)
12		ci 4030	. . . . . . 7 class i
13		cmulc 4032	. . . . . . 7 class ·
14	11, 12, 13	co 3001	. . . . . 6 class ((ℑ ‘x) · i)
15		cmin 4089	. . . . . 6 class −
16	9, 14, 15	co 3001	. . . . 5 class ((ℜ ‘x) − ((ℑ ‘x) · i))
17	7, 16	wceq 1091	. . . 4 wff y = ((ℜ ‘x) − ((ℑ ‘x) · i))
18	5, 17	wa 196	. . 3 wff (x ∈ ℂ ∧ y = ((ℜ ‘x) − ((ℑ ‘x) · i)))
19	18, 2, 6	copab 2055	. 2 class {⟨x, y⟩∣(x ∈ ℂ ∧ y = ((ℜ ‘x) − ((ℑ ‘x) · i)))}
20	1, 19	wceq 1091	1 wff ∗ = {⟨x, y⟩∣(x ∈ ℂ ∧ y = ((ℜ ‘x) − ((ℑ ‘x) · i)))}

This definition is referenced by:  cjvalt 4799

metamath.org