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 
|- ( A e. CC -> ( * ` A ) = ( iota_ x e. CC ( ( A + x ) e. RR /\ ( _i x. ( A - x ) ) e. RR ) ) )

Proof

Step Hyp Ref Expression
1 oveq1 
 |-  ( y = A -> ( y + x ) = ( A + x ) )
2 1 eleq1d 
 |-  ( y = A -> ( ( y + x ) e. RR <-> ( A + x ) e. RR ) )
3 oveq1 
 |-  ( y = A -> ( y - x ) = ( A - x ) )
4 3 oveq2d 
 |-  ( y = A -> ( _i x. ( y - x ) ) = ( _i x. ( A - x ) ) )
5 4 eleq1d 
 |-  ( y = A -> ( ( _i x. ( y - x ) ) e. RR <-> ( _i x. ( A - x ) ) e. RR ) )
6 2 5 anbi12d 
 |-  ( y = A -> ( ( ( y + x ) e. RR /\ ( _i x. ( y - x ) ) e. RR ) <-> ( ( A + x ) e. RR /\ ( _i x. ( A - x ) ) e. RR ) ) )
7 6 riotabidv 
 |-  ( y = A -> ( iota_ x e. CC ( ( y + x ) e. RR /\ ( _i x. ( y - x ) ) e. RR ) ) = ( iota_ x e. CC ( ( A + x ) e. RR /\ ( _i x. ( A - x ) ) e. RR ) ) )
8 df-cj 
 |-  * = ( y e. CC |-> ( iota_ x e. CC ( ( y + x ) e. RR /\ ( _i x. ( y - x ) ) e. RR ) ) )
9 riotaex 
 |-  ( iota_ x e. CC ( ( A + x ) e. RR /\ ( _i x. ( A - x ) ) e. RR ) ) e. _V
10 7 8 9 fvmpt 
 |-  ( A e. CC -> ( * ` A ) = ( iota_ x e. CC ( ( A + x ) e. RR /\ ( _i x. ( A - x ) ) e. RR ) ) )