# 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 ${⊢}*=\left({x}\in ℂ⟼\left(\iota {y}\in ℂ|\left({x}+{y}\in ℝ\wedge \mathrm{i}\left({x}-{y}\right)\in ℝ\right)\right)\right)$

### 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}\left({x}+{y}\right)$
8 cr ${class}ℝ$
9 7 8 wcel ${wff}{x}+{y}\in ℝ$
10 ci ${class}\mathrm{i}$
11 cmul ${class}×$
12 cmin ${class}-$
13 4 6 12 co ${class}\left({x}-{y}\right)$
14 10 13 11 co ${class}\mathrm{i}\left({x}-{y}\right)$
15 14 8 wcel ${wff}\mathrm{i}\left({x}-{y}\right)\in ℝ$
16 9 15 wa ${wff}\left({x}+{y}\in ℝ\wedge \mathrm{i}\left({x}-{y}\right)\in ℝ\right)$
17 16 3 2 crio ${class}\left(\iota {y}\in ℂ|\left({x}+{y}\in ℝ\wedge \mathrm{i}\left({x}-{y}\right)\in ℝ\right)\right)$
18 1 2 17 cmpt ${class}\left({x}\in ℂ⟼\left(\iota {y}\in ℂ|\left({x}+{y}\in ℝ\wedge \mathrm{i}\left({x}-{y}\right)\in ℝ\right)\right)\right)$
19 0 18 wceq ${wff}*=\left({x}\in ℂ⟼\left(\iota {y}\in ℂ|\left({x}+{y}\in ℝ\wedge \mathrm{i}\left({x}-{y}\right)\in ℝ\right)\right)\right)$