Metamath Proof Explorer

Theorem recan

Description: Cancellation law involving the real part of a complex number. (Contributed by NM, 12-May-2005)

Ref Expression
Assertion recan 
|- ( ( A e. CC /\ B e. CC ) -> ( A. x e. CC ( Re ` ( x x. A ) ) = ( Re ` ( x x. B ) ) <-> A = B ) )

Proof

Step Hyp Ref Expression
1 ax-1cn 
 |-  1 e. CC
2 fvoveq1 
 |-  ( x = 1 -> ( Re ` ( x x. A ) ) = ( Re ` ( 1 x. A ) ) )
3 fvoveq1 
 |-  ( x = 1 -> ( Re ` ( x x. B ) ) = ( Re ` ( 1 x. B ) ) )
4 2 3 eqeq12d 
 |-  ( x = 1 -> ( ( Re ` ( x x. A ) ) = ( Re ` ( x x. B ) ) <-> ( Re ` ( 1 x. A ) ) = ( Re ` ( 1 x. B ) ) ) )
5 4 rspcv 
 |-  ( 1 e. CC -> ( A. x e. CC ( Re ` ( x x. A ) ) = ( Re ` ( x x. B ) ) -> ( Re ` ( 1 x. A ) ) = ( Re ` ( 1 x. B ) ) ) )
6 1 5 ax-mp 
 |-  ( A. x e. CC ( Re ` ( x x. A ) ) = ( Re ` ( x x. B ) ) -> ( Re ` ( 1 x. A ) ) = ( Re ` ( 1 x. B ) ) )
7 negicn 
 |-  -u _i e. CC
8 fvoveq1 
 |-  ( x = -u _i -> ( Re ` ( x x. A ) ) = ( Re ` ( -u _i x. A ) ) )
9 fvoveq1 
 |-  ( x = -u _i -> ( Re ` ( x x. B ) ) = ( Re ` ( -u _i x. B ) ) )
10 8 9 eqeq12d 
 |-  ( x = -u _i -> ( ( Re ` ( x x. A ) ) = ( Re ` ( x x. B ) ) <-> ( Re ` ( -u _i x. A ) ) = ( Re ` ( -u _i x. B ) ) ) )
11 10 rspcv 
 |-  ( -u _i e. CC -> ( A. x e. CC ( Re ` ( x x. A ) ) = ( Re ` ( x x. B ) ) -> ( Re ` ( -u _i x. A ) ) = ( Re ` ( -u _i x. B ) ) ) )
12 7 11 ax-mp 
 |-  ( A. x e. CC ( Re ` ( x x. A ) ) = ( Re ` ( x x. B ) ) -> ( Re ` ( -u _i x. A ) ) = ( Re ` ( -u _i x. B ) ) )
13 12 oveq2d 
 |-  ( A. x e. CC ( Re ` ( x x. A ) ) = ( Re ` ( x x. B ) ) -> ( _i x. ( Re ` ( -u _i x. A ) ) ) = ( _i x. ( Re ` ( -u _i x. B ) ) ) )
14 6 13 oveq12d 
 |-  ( A. x e. CC ( Re ` ( x x. A ) ) = ( Re ` ( x x. B ) ) -> ( ( Re ` ( 1 x. A ) ) + ( _i x. ( Re ` ( -u _i x. A ) ) ) ) = ( ( Re ` ( 1 x. B ) ) + ( _i x. ( Re ` ( -u _i x. B ) ) ) ) )
15 replim 
 |-  ( A e. CC -> A = ( ( Re ` A ) + ( _i x. ( Im ` A ) ) ) )
16 mullid 
 |-  ( A e. CC -> ( 1 x. A ) = A )
17 16 eqcomd 
 |-  ( A e. CC -> A = ( 1 x. A ) )
18 17 fveq2d 
 |-  ( A e. CC -> ( Re ` A ) = ( Re ` ( 1 x. A ) ) )
19 imre 
 |-  ( A e. CC -> ( Im ` A ) = ( Re ` ( -u _i x. A ) ) )
20 19 oveq2d 
 |-  ( A e. CC -> ( _i x. ( Im ` A ) ) = ( _i x. ( Re ` ( -u _i x. A ) ) ) )
21 18 20 oveq12d 
 |-  ( A e. CC -> ( ( Re ` A ) + ( _i x. ( Im ` A ) ) ) = ( ( Re ` ( 1 x. A ) ) + ( _i x. ( Re ` ( -u _i x. A ) ) ) ) )
22 15 21 eqtrd 
 |-  ( A e. CC -> A = ( ( Re ` ( 1 x. A ) ) + ( _i x. ( Re ` ( -u _i x. A ) ) ) ) )
23 replim 
 |-  ( B e. CC -> B = ( ( Re ` B ) + ( _i x. ( Im ` B ) ) ) )
24 mullid 
 |-  ( B e. CC -> ( 1 x. B ) = B )
25 24 eqcomd 
 |-  ( B e. CC -> B = ( 1 x. B ) )
26 25 fveq2d 
 |-  ( B e. CC -> ( Re ` B ) = ( Re ` ( 1 x. B ) ) )
27 imre 
 |-  ( B e. CC -> ( Im ` B ) = ( Re ` ( -u _i x. B ) ) )
28 27 oveq2d 
 |-  ( B e. CC -> ( _i x. ( Im ` B ) ) = ( _i x. ( Re ` ( -u _i x. B ) ) ) )
29 26 28 oveq12d 
 |-  ( B e. CC -> ( ( Re ` B ) + ( _i x. ( Im ` B ) ) ) = ( ( Re ` ( 1 x. B ) ) + ( _i x. ( Re ` ( -u _i x. B ) ) ) ) )
30 23 29 eqtrd 
 |-  ( B e. CC -> B = ( ( Re ` ( 1 x. B ) ) + ( _i x. ( Re ` ( -u _i x. B ) ) ) ) )
31 22 30 eqeqan12d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( A = B <-> ( ( Re ` ( 1 x. A ) ) + ( _i x. ( Re ` ( -u _i x. A ) ) ) ) = ( ( Re ` ( 1 x. B ) ) + ( _i x. ( Re ` ( -u _i x. B ) ) ) ) ) )
32 14 31 imbitrrid 
 |-  ( ( A e. CC /\ B e. CC ) -> ( A. x e. CC ( Re ` ( x x. A ) ) = ( Re ` ( x x. B ) ) -> A = B ) )
33 oveq2 
 |-  ( A = B -> ( x x. A ) = ( x x. B ) )
34 33 fveq2d 
 |-  ( A = B -> ( Re ` ( x x. A ) ) = ( Re ` ( x x. B ) ) )
35 34 ralrimivw 
 |-  ( A = B -> A. x e. CC ( Re ` ( x x. A ) ) = ( Re ` ( x x. B ) ) )
36 32 35 impbid1 
 |-  ( ( A e. CC /\ B e. CC ) -> ( A. x e. CC ( Re ` ( x x. A ) ) = ( Re ` ( x x. B ) ) <-> A = B ) )