Metamath Proof Explorer

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 ⊢ * = x ∈ ℂ ⟼ ι y ∈ ℂ | x + y ∈ ℝ ∧ i ⁢ x − y ∈ ℝ

Detailed syntax breakdown

Step Hyp Ref Expression
0 ccj class *
1 vx setvar x
2 cc class ℂ
3 vy setvar y
4 1 cv setvar x
5 caddc class +
6 3 cv setvar y
7 4 6 5 co class x + y
8 cr class ℝ
9 7 8 wcel wff x + y ∈ ℝ
10 ci class i
11 cmul class ×
12 cmin class −
13 4 6 12 co class x − y
14 10 13 11 co class i ⁢ x − y
15 14 8 wcel wff i ⁢ x − y ∈ ℝ
16 9 15 wa wff x + y ∈ ℝ ∧ i ⁢ x − y ∈ ℝ
17 16 3 2 crio class ι y ∈ ℂ | x + y ∈ ℝ ∧ i ⁢ x − y ∈ ℝ
18 1 2 17 cmpt class x ∈ ℂ ⟼ ι y ∈ ℂ | x + y ∈ ℝ ∧ i ⁢ x − y ∈ ℝ
19 0 18 wceq wff * = x ∈ ℂ ⟼ ι y ∈ ℂ | x + y ∈ ℝ ∧ i ⁢ x − y ∈ ℝ