Metamath Proof Explorer

Theorem angrtmuld

Description: Perpendicularity of two vectors does not change under rescaling the second. (Contributed by David Moews, 28-Feb-2017)

Ref Expression
Hypotheses ang.1 
|- F = ( x e. ( CC \ { 0 } ) , y e. ( CC \ { 0 } ) |-> ( Im ` ( log ` ( y / x ) ) ) )
angrtmuld.1 
|- ( ph -> X e. CC )
angrtmuld.2 
|- ( ph -> Y e. CC )
angrtmuld.3 
|- ( ph -> Z e. CC )
angrtmuld.4 
|- ( ph -> X =/= 0 )
angrtmuld.5 
|- ( ph -> Y =/= 0 )
angrtmuld.6 
|- ( ph -> Z =/= 0 )
angrtmuld.7 
|- ( ph -> ( Z / Y ) e. RR )
Assertion angrtmuld 
|- ( ph -> ( ( X F Y ) e. { ( _pi / 2 ) , -u ( _pi / 2 ) } <-> ( X F Z ) e. { ( _pi / 2 ) , -u ( _pi / 2 ) } ) )

Proof

Step Hyp Ref Expression
1 ang.1 
 |-  F = ( x e. ( CC \ { 0 } ) , y e. ( CC \ { 0 } ) |-> ( Im ` ( log ` ( y / x ) ) ) )
2 angrtmuld.1 
 |-  ( ph -> X e. CC )
3 angrtmuld.2 
 |-  ( ph -> Y e. CC )
4 angrtmuld.3 
 |-  ( ph -> Z e. CC )
5 angrtmuld.4 
 |-  ( ph -> X =/= 0 )
6 angrtmuld.5 
 |-  ( ph -> Y =/= 0 )
7 angrtmuld.6 
 |-  ( ph -> Z =/= 0 )
8 angrtmuld.7 
 |-  ( ph -> ( Z / Y ) e. RR )
9 4 3 7 6 divne0d 
 |-  ( ph -> ( Z / Y ) =/= 0 )
10 9 neneqd 
 |-  ( ph -> -. ( Z / Y ) = 0 )
11 biorf 
 |-  ( -. ( Z / Y ) = 0 -> ( ( Re ` ( Y / X ) ) = 0 <-> ( ( Z / Y ) = 0 \/ ( Re ` ( Y / X ) ) = 0 ) ) )
12 10 11 syl 
 |-  ( ph -> ( ( Re ` ( Y / X ) ) = 0 <-> ( ( Z / Y ) = 0 \/ ( Re ` ( Y / X ) ) = 0 ) ) )
13 1 2 5 3 6 angrteqvd 
 |-  ( ph -> ( ( X F Y ) e. { ( _pi / 2 ) , -u ( _pi / 2 ) } <-> ( Re ` ( Y / X ) ) = 0 ) )
14 1 2 5 4 7 angrteqvd 
 |-  ( ph -> ( ( X F Z ) e. { ( _pi / 2 ) , -u ( _pi / 2 ) } <-> ( Re ` ( Z / X ) ) = 0 ) )
15 4 3 2 6 5 dmdcan2d 
 |-  ( ph -> ( ( Z / Y ) x. ( Y / X ) ) = ( Z / X ) )
16 15 fveq2d 
 |-  ( ph -> ( Re ` ( ( Z / Y ) x. ( Y / X ) ) ) = ( Re ` ( Z / X ) ) )
17 3 2 5 divcld 
 |-  ( ph -> ( Y / X ) e. CC )
18 8 17 remul2d 
 |-  ( ph -> ( Re ` ( ( Z / Y ) x. ( Y / X ) ) ) = ( ( Z / Y ) x. ( Re ` ( Y / X ) ) ) )
19 16 18 eqtr3d 
 |-  ( ph -> ( Re ` ( Z / X ) ) = ( ( Z / Y ) x. ( Re ` ( Y / X ) ) ) )
20 19 eqeq1d 
 |-  ( ph -> ( ( Re ` ( Z / X ) ) = 0 <-> ( ( Z / Y ) x. ( Re ` ( Y / X ) ) ) = 0 ) )
21 4 3 6 divcld 
 |-  ( ph -> ( Z / Y ) e. CC )
22 17 recld 
 |-  ( ph -> ( Re ` ( Y / X ) ) e. RR )
23 22 recnd 
 |-  ( ph -> ( Re ` ( Y / X ) ) e. CC )
24 21 23 mul0ord 
 |-  ( ph -> ( ( ( Z / Y ) x. ( Re ` ( Y / X ) ) ) = 0 <-> ( ( Z / Y ) = 0 \/ ( Re ` ( Y / X ) ) = 0 ) ) )
25 14 20 24 3bitrd 
 |-  ( ph -> ( ( X F Z ) e. { ( _pi / 2 ) , -u ( _pi / 2 ) } <-> ( ( Z / Y ) = 0 \/ ( Re ` ( Y / X ) ) = 0 ) ) )
26 12 13 25 3bitr4d 
 |-  ( ph -> ( ( X F Y ) e. { ( _pi / 2 ) , -u ( _pi / 2 ) } <-> ( X F Z ) e. { ( _pi / 2 ) , -u ( _pi / 2 ) } ) )