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

Metamath Proof Explorer

Theorem cjval

Description: The value of the conjugate of a complex number. (Contributed by Mario Carneiro, 6-Nov-2013)

Ref Expression
Assertion cjval ( 𝐴 ∈ ℂ → ( ∗ ‘ 𝐴 ) = ( ℩ 𝑥 ∈ ℂ ( ( 𝐴 + 𝑥 ) ∈ ℝ ∧ ( i · ( 𝐴 − 𝑥 ) ) ∈ ℝ ) ) )

Proof

Step Hyp Ref Expression
1 oveq1 ⊢ ( 𝑦 = 𝐴 → ( 𝑦 + 𝑥 ) = ( 𝐴 + 𝑥 ) )
2 1 eleq1d ⊢ ( 𝑦 = 𝐴 → ( ( 𝑦 + 𝑥 ) ∈ ℝ ↔ ( 𝐴 + 𝑥 ) ∈ ℝ ) )
3 oveq1 ⊢ ( 𝑦 = 𝐴 → ( 𝑦 − 𝑥 ) = ( 𝐴 − 𝑥 ) )
4 3 oveq2d ⊢ ( 𝑦 = 𝐴 → ( i · ( 𝑦 − 𝑥 ) ) = ( i · ( 𝐴 − 𝑥 ) ) )
5 4 eleq1d ⊢ ( 𝑦 = 𝐴 → ( ( i · ( 𝑦 − 𝑥 ) ) ∈ ℝ ↔ ( i · ( 𝐴 − 𝑥 ) ) ∈ ℝ ) )
6 2 5 anbi12d ⊢ ( 𝑦 = 𝐴 → ( ( ( 𝑦 + 𝑥 ) ∈ ℝ ∧ ( i · ( 𝑦 − 𝑥 ) ) ∈ ℝ ) ↔ ( ( 𝐴 + 𝑥 ) ∈ ℝ ∧ ( i · ( 𝐴 − 𝑥 ) ) ∈ ℝ ) ) )
7 6 riotabidv ⊢ ( 𝑦 = 𝐴 → ( ℩ 𝑥 ∈ ℂ ( ( 𝑦 + 𝑥 ) ∈ ℝ ∧ ( i · ( 𝑦 − 𝑥 ) ) ∈ ℝ ) ) = ( ℩ 𝑥 ∈ ℂ ( ( 𝐴 + 𝑥 ) ∈ ℝ ∧ ( i · ( 𝐴 − 𝑥 ) ) ∈ ℝ ) ) )
8 df-cj ⊢ ∗ = ( 𝑦 ∈ ℂ ↦ ( ℩ 𝑥 ∈ ℂ ( ( 𝑦 + 𝑥 ) ∈ ℝ ∧ ( i · ( 𝑦 − 𝑥 ) ) ∈ ℝ ) ) )
9 riotaex ⊢ ( ℩ 𝑥 ∈ ℂ ( ( 𝐴 + 𝑥 ) ∈ ℝ ∧ ( i · ( 𝐴 − 𝑥 ) ) ∈ ℝ ) ) ∈ V
10 7 8 9 fvmpt ⊢ ( 𝐴 ∈ ℂ → ( ∗ ‘ 𝐴 ) = ( ℩ 𝑥 ∈ ℂ ( ( 𝐴 + 𝑥 ) ∈ ℝ ∧ ( i · ( 𝐴 − 𝑥 ) ) ∈ ℝ ) ) )