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 ) ) )`