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

Metamath Proof Explorer

Theorem cjth

Description: The defining property of the complex conjugate. (Contributed by Mario Carneiro, 6-Nov-2013)

Ref Expression
Assertion cjth 
|- ( A e. CC -> ( ( A + ( * ` A ) ) e. RR /\ ( _i x. ( A - ( * ` A ) ) ) e. RR ) )

Proof

Step Hyp Ref Expression
1 cju 
 |-  ( A e. CC -> E! x e. CC ( ( A + x ) e. RR /\ ( _i x. ( A - x ) ) e. RR ) )
2 riotasbc 
 |-  ( E! x e. CC ( ( A + x ) e. RR /\ ( _i x. ( A - x ) ) e. RR ) -> [. ( iota_ x e. CC ( ( A + x ) e. RR /\ ( _i x. ( A - x ) ) e. RR ) ) / x ]. ( ( A + x ) e. RR /\ ( _i x. ( A - x ) ) e. RR ) )
3 1 2 syl 
 |-  ( A e. CC -> [. ( iota_ x e. CC ( ( A + x ) e. RR /\ ( _i x. ( A - x ) ) e. RR ) ) / x ]. ( ( A + x ) e. RR /\ ( _i x. ( A - x ) ) e. RR ) )
4 cjval 
 |-  ( A e. CC -> ( * ` A ) = ( iota_ x e. CC ( ( A + x ) e. RR /\ ( _i x. ( A - x ) ) e. RR ) ) )
5 4 sbceq1d 
 |-  ( A e. CC -> ( [. ( * ` A ) / x ]. ( ( A + x ) e. RR /\ ( _i x. ( A - x ) ) e. RR ) <-> [. ( iota_ x e. CC ( ( A + x ) e. RR /\ ( _i x. ( A - x ) ) e. RR ) ) / x ]. ( ( A + x ) e. RR /\ ( _i x. ( A - x ) ) e. RR ) ) )
6 3 5 mpbird 
 |-  ( A e. CC -> [. ( * ` A ) / x ]. ( ( A + x ) e. RR /\ ( _i x. ( A - x ) ) e. RR ) )
7 fvex 
 |-  ( * ` A ) e. _V
8 oveq2 
 |-  ( x = ( * ` A ) -> ( A + x ) = ( A + ( * ` A ) ) )
9 8 eleq1d 
 |-  ( x = ( * ` A ) -> ( ( A + x ) e. RR <-> ( A + ( * ` A ) ) e. RR ) )
10 oveq2 
 |-  ( x = ( * ` A ) -> ( A - x ) = ( A - ( * ` A ) ) )
11 10 oveq2d 
 |-  ( x = ( * ` A ) -> ( _i x. ( A - x ) ) = ( _i x. ( A - ( * ` A ) ) ) )
12 11 eleq1d 
 |-  ( x = ( * ` A ) -> ( ( _i x. ( A - x ) ) e. RR <-> ( _i x. ( A - ( * ` A ) ) ) e. RR ) )
13 9 12 anbi12d 
 |-  ( x = ( * ` A ) -> ( ( ( A + x ) e. RR /\ ( _i x. ( A - x ) ) e. RR ) <-> ( ( A + ( * ` A ) ) e. RR /\ ( _i x. ( A - ( * ` A ) ) ) e. RR ) ) )
14 7 13 sbcie 
 |-  ( [. ( * ` A ) / x ]. ( ( A + x ) e. RR /\ ( _i x. ( A - x ) ) e. RR ) <-> ( ( A + ( * ` A ) ) e. RR /\ ( _i x. ( A - ( * ` A ) ) ) e. RR ) )
15 6 14 sylib 
 |-  ( A e. CC -> ( ( A + ( * ` A ) ) e. RR /\ ( _i x. ( A - ( * ` A ) ) ) e. RR ) )