Metamath Proof Explorer

Theorem remim

Description: Value of the conjugate of a complex number. The value is the real part minus _i times the imaginary part. Definition 10-3.2 of Gleason p. 132. (Contributed by NM, 10-May-1999) (Revised by Mario Carneiro, 7-Nov-2013)

Ref Expression
Assertion remim 
|- ( A e. CC -> ( * ` A ) = ( ( Re ` A ) - ( _i x. ( Im ` A ) ) ) )

Proof

Step Hyp Ref Expression
1 cjval 
 |-  ( A e. CC -> ( * ` A ) = ( iota_ x e. CC ( ( A + x ) e. RR /\ ( _i x. ( A - x ) ) e. RR ) ) )
2 replim 
 |-  ( A e. CC -> A = ( ( Re ` A ) + ( _i x. ( Im ` A ) ) ) )
3 2 oveq1d 
 |-  ( A e. CC -> ( A + ( ( Re ` A ) - ( _i x. ( Im ` A ) ) ) ) = ( ( ( Re ` A ) + ( _i x. ( Im ` A ) ) ) + ( ( Re ` A ) - ( _i x. ( Im ` A ) ) ) ) )
4 recl 
 |-  ( A e. CC -> ( Re ` A ) e. RR )
5 4 recnd 
 |-  ( A e. CC -> ( Re ` A ) e. CC )
6 ax-icn 
 |-  _i e. CC
7 imcl 
 |-  ( A e. CC -> ( Im ` A ) e. RR )
8 7 recnd 
 |-  ( A e. CC -> ( Im ` A ) e. CC )
9 mulcl 
 |-  ( ( _i e. CC /\ ( Im ` A ) e. CC ) -> ( _i x. ( Im ` A ) ) e. CC )
10 6 8 9 sylancr 
 |-  ( A e. CC -> ( _i x. ( Im ` A ) ) e. CC )
11 5 10 5 ppncand 
 |-  ( A e. CC -> ( ( ( Re ` A ) + ( _i x. ( Im ` A ) ) ) + ( ( Re ` A ) - ( _i x. ( Im ` A ) ) ) ) = ( ( Re ` A ) + ( Re ` A ) ) )
12 3 11 eqtrd 
 |-  ( A e. CC -> ( A + ( ( Re ` A ) - ( _i x. ( Im ` A ) ) ) ) = ( ( Re ` A ) + ( Re ` A ) ) )
13 4 4 readdcld 
 |-  ( A e. CC -> ( ( Re ` A ) + ( Re ` A ) ) e. RR )
14 12 13 eqeltrd 
 |-  ( A e. CC -> ( A + ( ( Re ` A ) - ( _i x. ( Im ` A ) ) ) ) e. RR )
15 5 10 10 pnncand 
 |-  ( A e. CC -> ( ( ( Re ` A ) + ( _i x. ( Im ` A ) ) ) - ( ( Re ` A ) - ( _i x. ( Im ` A ) ) ) ) = ( ( _i x. ( Im ` A ) ) + ( _i x. ( Im ` A ) ) ) )
16 2 oveq1d 
 |-  ( A e. CC -> ( A - ( ( Re ` A ) - ( _i x. ( Im ` A ) ) ) ) = ( ( ( Re ` A ) + ( _i x. ( Im ` A ) ) ) - ( ( Re ` A ) - ( _i x. ( Im ` A ) ) ) ) )
17 6 a1i 
 |-  ( A e. CC -> _i e. CC )
18 17 8 8 adddid 
 |-  ( A e. CC -> ( _i x. ( ( Im ` A ) + ( Im ` A ) ) ) = ( ( _i x. ( Im ` A ) ) + ( _i x. ( Im ` A ) ) ) )
19 15 16 18 3eqtr4d 
 |-  ( A e. CC -> ( A - ( ( Re ` A ) - ( _i x. ( Im ` A ) ) ) ) = ( _i x. ( ( Im ` A ) + ( Im ` A ) ) ) )
20 19 oveq2d 
 |-  ( A e. CC -> ( _i x. ( A - ( ( Re ` A ) - ( _i x. ( Im ` A ) ) ) ) ) = ( _i x. ( _i x. ( ( Im ` A ) + ( Im ` A ) ) ) ) )
21 7 7 readdcld 
 |-  ( A e. CC -> ( ( Im ` A ) + ( Im ` A ) ) e. RR )
22 21 recnd 
 |-  ( A e. CC -> ( ( Im ` A ) + ( Im ` A ) ) e. CC )
23 mulass 
 |-  ( ( _i e. CC /\ _i e. CC /\ ( ( Im ` A ) + ( Im ` A ) ) e. CC ) -> ( ( _i x. _i ) x. ( ( Im ` A ) + ( Im ` A ) ) ) = ( _i x. ( _i x. ( ( Im ` A ) + ( Im ` A ) ) ) ) )
24 6 6 22 23 mp3an12i 
 |-  ( A e. CC -> ( ( _i x. _i ) x. ( ( Im ` A ) + ( Im ` A ) ) ) = ( _i x. ( _i x. ( ( Im ` A ) + ( Im ` A ) ) ) ) )
25 20 24 eqtr4d 
 |-  ( A e. CC -> ( _i x. ( A - ( ( Re ` A ) - ( _i x. ( Im ` A ) ) ) ) ) = ( ( _i x. _i ) x. ( ( Im ` A ) + ( Im ` A ) ) ) )
26 ixi 
 |-  ( _i x. _i ) = -u 1
27 neg1rr 
 |-  -u 1 e. RR
28 26 27 eqeltri 
 |-  ( _i x. _i ) e. RR
29 remulcl 
 |-  ( ( ( _i x. _i ) e. RR /\ ( ( Im ` A ) + ( Im ` A ) ) e. RR ) -> ( ( _i x. _i ) x. ( ( Im ` A ) + ( Im ` A ) ) ) e. RR )
30 28 21 29 sylancr 
 |-  ( A e. CC -> ( ( _i x. _i ) x. ( ( Im ` A ) + ( Im ` A ) ) ) e. RR )
31 25 30 eqeltrd 
 |-  ( A e. CC -> ( _i x. ( A - ( ( Re ` A ) - ( _i x. ( Im ` A ) ) ) ) ) e. RR )
32 5 10 subcld 
 |-  ( A e. CC -> ( ( Re ` A ) - ( _i x. ( Im ` A ) ) ) e. CC )
33 cju 
 |-  ( A e. CC -> E! x e. CC ( ( A + x ) e. RR /\ ( _i x. ( A - x ) ) e. RR ) )
34 oveq2 
 |-  ( x = ( ( Re ` A ) - ( _i x. ( Im ` A ) ) ) -> ( A + x ) = ( A + ( ( Re ` A ) - ( _i x. ( Im ` A ) ) ) ) )
35 34 eleq1d 
 |-  ( x = ( ( Re ` A ) - ( _i x. ( Im ` A ) ) ) -> ( ( A + x ) e. RR <-> ( A + ( ( Re ` A ) - ( _i x. ( Im ` A ) ) ) ) e. RR ) )
36 oveq2 
 |-  ( x = ( ( Re ` A ) - ( _i x. ( Im ` A ) ) ) -> ( A - x ) = ( A - ( ( Re ` A ) - ( _i x. ( Im ` A ) ) ) ) )
37 36 oveq2d 
 |-  ( x = ( ( Re ` A ) - ( _i x. ( Im ` A ) ) ) -> ( _i x. ( A - x ) ) = ( _i x. ( A - ( ( Re ` A ) - ( _i x. ( Im ` A ) ) ) ) ) )
38 37 eleq1d 
 |-  ( x = ( ( Re ` A ) - ( _i x. ( Im ` A ) ) ) -> ( ( _i x. ( A - x ) ) e. RR <-> ( _i x. ( A - ( ( Re ` A ) - ( _i x. ( Im ` A ) ) ) ) ) e. RR ) )
39 35 38 anbi12d 
 |-  ( x = ( ( Re ` A ) - ( _i x. ( Im ` A ) ) ) -> ( ( ( A + x ) e. RR /\ ( _i x. ( A - x ) ) e. RR ) <-> ( ( A + ( ( Re ` A ) - ( _i x. ( Im ` A ) ) ) ) e. RR /\ ( _i x. ( A - ( ( Re ` A ) - ( _i x. ( Im ` A ) ) ) ) ) e. RR ) ) )
40 39 riota2 
 |-  ( ( ( ( Re ` A ) - ( _i x. ( Im ` A ) ) ) e. CC /\ E! x e. CC ( ( A + x ) e. RR /\ ( _i x. ( A - x ) ) e. RR ) ) -> ( ( ( A + ( ( Re ` A ) - ( _i x. ( Im ` A ) ) ) ) e. RR /\ ( _i x. ( A - ( ( Re ` A ) - ( _i x. ( Im ` A ) ) ) ) ) e. RR ) <-> ( iota_ x e. CC ( ( A + x ) e. RR /\ ( _i x. ( A - x ) ) e. RR ) ) = ( ( Re ` A ) - ( _i x. ( Im ` A ) ) ) ) )
41 32 33 40 syl2anc 
 |-  ( A e. CC -> ( ( ( A + ( ( Re ` A ) - ( _i x. ( Im ` A ) ) ) ) e. RR /\ ( _i x. ( A - ( ( Re ` A ) - ( _i x. ( Im ` A ) ) ) ) ) e. RR ) <-> ( iota_ x e. CC ( ( A + x ) e. RR /\ ( _i x. ( A - x ) ) e. RR ) ) = ( ( Re ` A ) - ( _i x. ( Im ` A ) ) ) ) )
42 14 31 41 mpbi2and 
 |-  ( A e. CC -> ( iota_ x e. CC ( ( A + x ) e. RR /\ ( _i x. ( A - x ) ) e. RR ) ) = ( ( Re ` A ) - ( _i x. ( Im ` A ) ) ) )
43 1 42 eqtrd 
 |-  ( A e. CC -> ( * ` A ) = ( ( Re ` A ) - ( _i x. ( Im ` A ) ) ) )