Definition df-cj 15292

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

Assertion

Ref	Expression
df-cj	⊢ ∗ = (𝑥 ∈ ℂ ↦ (℩𝑦 ∈ ℂ ((𝑥 + 𝑦) ∈ ℝ ∧ (i · (𝑥 − 𝑦)) ∈ ℝ)))

Distinct variable group:   𝑥,𝑦

Detailed syntax breakdown of Definition df-cj

Step	Hyp	Ref	Expression
1		ccj 15289	. 2 class ∗
2		vx	. . 3 setvar 𝑥
3		cc 11222	. . 3 class ℂ
4	2	cv 1569	. . . . . . 7 class 𝑥
5		vy	. . . . . . . 8 setvar 𝑦
6	5	cv 1569	. . . . . . 7 class 𝑦
7		caddc 11227	. . . . . . 7 class +
8	4, 6, 7	co 7440	. . . . . 6 class (𝑥 + 𝑦)
9		cr 11223	. . . . . 6 class ℝ
10	8, 9	wcel 2147	. . . . 5 wff (𝑥 + 𝑦) ∈ ℝ
11		ci 11226	. . . . . . 7 class i
12		cmin 11565	. . . . . . . 8 class −
13	4, 6, 12	co 7440	. . . . . . 7 class (𝑥 − 𝑦)
14		cmul 11229	. . . . . . 7 class ·
15	11, 13, 14	co 7440	. . . . . 6 class (i · (𝑥 − 𝑦))
16	15, 9	wcel 2147	. . . . 5 wff (i · (𝑥 − 𝑦)) ∈ ℝ
17	10, 16	wa 401	. . . 4 wff ((𝑥 + 𝑦) ∈ ℝ ∧ (i · (𝑥 − 𝑦)) ∈ ℝ)
18	17, 5, 3	crio 7396	. . 3 class (℩𝑦 ∈ ℂ ((𝑥 + 𝑦) ∈ ℝ ∧ (i · (𝑥 − 𝑦)) ∈ ℝ))
19	2, 3, 18	cmpt 5189	. 2 class (𝑥 ∈ ℂ ↦ (℩𝑦 ∈ ℂ ((𝑥 + 𝑦) ∈ ℝ ∧ (i · (𝑥 − 𝑦)) ∈ ℝ)))
20	1, 19	wceq 1570	1 wff ∗ = (𝑥 ∈ ℂ ↦ (℩𝑦 ∈ ℂ ((𝑥 + 𝑦) ∈ ℝ ∧ (i · (𝑥 − 𝑦)) ∈ ℝ)))

This definition is used by:  cjval  15295  cjf  15297