This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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