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	⊢ ∗ = ( 𝑥 ∈ ℂ ↦ ( ℩ 𝑦 ∈ ℂ ( ( 𝑥 + 𝑦 ) ∈ ℝ ∧ ( i · ( 𝑥 − 𝑦 ) ) ∈ ℝ ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccj	⊢ ∗
1		vx	⊢ 𝑥
2		cc	⊢ ℂ
3		vy	⊢ 𝑦
4	1	cv	⊢ 𝑥
5		caddc	⊢ +
6	3	cv	⊢ 𝑦
7	4 6 5	co	⊢ ( 𝑥 + 𝑦 )
8		cr	⊢ ℝ
9	7 8	wcel	⊢ ( 𝑥 + 𝑦 ) ∈ ℝ
10		ci	⊢ i
11		cmul	⊢ ·
12		cmin	⊢ −
13	4 6 12	co	⊢ ( 𝑥 − 𝑦 )
14	10 13 11	co	⊢ ( i · ( 𝑥 − 𝑦 ) )
15	14 8	wcel	⊢ ( i · ( 𝑥 − 𝑦 ) ) ∈ ℝ
16	9 15	wa	⊢ ( ( 𝑥 + 𝑦 ) ∈ ℝ ∧ ( i · ( 𝑥 − 𝑦 ) ) ∈ ℝ )
17	16 3 2	crio	⊢ ( ℩ 𝑦 ∈ ℂ ( ( 𝑥 + 𝑦 ) ∈ ℝ ∧ ( i · ( 𝑥 − 𝑦 ) ) ∈ ℝ ) )
18	1 2 17	cmpt	⊢ ( 𝑥 ∈ ℂ ↦ ( ℩ 𝑦 ∈ ℂ ( ( 𝑥 + 𝑦 ) ∈ ℝ ∧ ( i · ( 𝑥 − 𝑦 ) ) ∈ ℝ ) ) )
19	0 18	wceq	⊢ ∗ = ( 𝑥 ∈ ℂ ↦ ( ℩ 𝑦 ∈ ℂ ( ( 𝑥 + 𝑦 ) ∈ ℝ ∧ ( i · ( 𝑥 − 𝑦 ) ) ∈ ℝ ) ) )