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 ⊢ 𝐹 = ( 𝑥 ∈ ( ℂ ∖ { 0 } ) , 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( ℑ ‘ ( log ‘ ( 𝑦 / 𝑥 ) ) ) )
angrtmuld.1 ⊢ ( 𝜑 → 𝑋 ∈ ℂ )
angrtmuld.2 ⊢ ( 𝜑 → 𝑌 ∈ ℂ )
angrtmuld.3 ⊢ ( 𝜑 → 𝑍 ∈ ℂ )
angrtmuld.4 ⊢ ( 𝜑 → 𝑋 ≠ 0 )
angrtmuld.5 ⊢ ( 𝜑 → 𝑌 ≠ 0 )
angrtmuld.6 ⊢ ( 𝜑 → 𝑍 ≠ 0 )
angrtmuld.7 ⊢ ( 𝜑 → ( 𝑍 / 𝑌 ) ∈ ℝ )
Assertion angrtmuld ( 𝜑 → ( ( 𝑋 𝐹 𝑌 ) ∈ { ( π / 2 ) , - ( π / 2 ) } ↔ ( 𝑋 𝐹 𝑍 ) ∈ { ( π / 2 ) , - ( π / 2 ) } ) )

Proof

Step Hyp Ref Expression
1 ang.1 ⊢ 𝐹 = ( 𝑥 ∈ ( ℂ ∖ { 0 } ) , 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( ℑ ‘ ( log ‘ ( 𝑦 / 𝑥 ) ) ) )
2 angrtmuld.1 ⊢ ( 𝜑 → 𝑋 ∈ ℂ )
3 angrtmuld.2 ⊢ ( 𝜑 → 𝑌 ∈ ℂ )
4 angrtmuld.3 ⊢ ( 𝜑 → 𝑍 ∈ ℂ )
5 angrtmuld.4 ⊢ ( 𝜑 → 𝑋 ≠ 0 )
6 angrtmuld.5 ⊢ ( 𝜑 → 𝑌 ≠ 0 )
7 angrtmuld.6 ⊢ ( 𝜑 → 𝑍 ≠ 0 )
8 angrtmuld.7 ⊢ ( 𝜑 → ( 𝑍 / 𝑌 ) ∈ ℝ )
9 4 3 7 6 divne0d ⊢ ( 𝜑 → ( 𝑍 / 𝑌 ) ≠ 0 )
10 9 neneqd ⊢ ( 𝜑 → ¬ ( 𝑍 / 𝑌 ) = 0 )
11 biorf ⊢ ( ¬ ( 𝑍 / 𝑌 ) = 0 → ( ( ℜ ‘ ( 𝑌 / 𝑋 ) ) = 0 ↔ ( ( 𝑍 / 𝑌 ) = 0 ∨ ( ℜ ‘ ( 𝑌 / 𝑋 ) ) = 0 ) ) )
12 10 11 syl ⊢ ( 𝜑 → ( ( ℜ ‘ ( 𝑌 / 𝑋 ) ) = 0 ↔ ( ( 𝑍 / 𝑌 ) = 0 ∨ ( ℜ ‘ ( 𝑌 / 𝑋 ) ) = 0 ) ) )
13 1 2 5 3 6 angrteqvd ⊢ ( 𝜑 → ( ( 𝑋 𝐹 𝑌 ) ∈ { ( π / 2 ) , - ( π / 2 ) } ↔ ( ℜ ‘ ( 𝑌 / 𝑋 ) ) = 0 ) )
14 1 2 5 4 7 angrteqvd ⊢ ( 𝜑 → ( ( 𝑋 𝐹 𝑍 ) ∈ { ( π / 2 ) , - ( π / 2 ) } ↔ ( ℜ ‘ ( 𝑍 / 𝑋 ) ) = 0 ) )
15 4 3 2 6 5 dmdcan2d ⊢ ( 𝜑 → ( ( 𝑍 / 𝑌 ) · ( 𝑌 / 𝑋 ) ) = ( 𝑍 / 𝑋 ) )
16 15 fveq2d ⊢ ( 𝜑 → ( ℜ ‘ ( ( 𝑍 / 𝑌 ) · ( 𝑌 / 𝑋 ) ) ) = ( ℜ ‘ ( 𝑍 / 𝑋 ) ) )
17 3 2 5 divcld ⊢ ( 𝜑 → ( 𝑌 / 𝑋 ) ∈ ℂ )
18 8 17 remul2d ⊢ ( 𝜑 → ( ℜ ‘ ( ( 𝑍 / 𝑌 ) · ( 𝑌 / 𝑋 ) ) ) = ( ( 𝑍 / 𝑌 ) · ( ℜ ‘ ( 𝑌 / 𝑋 ) ) ) )
19 16 18 eqtr3d ⊢ ( 𝜑 → ( ℜ ‘ ( 𝑍 / 𝑋 ) ) = ( ( 𝑍 / 𝑌 ) · ( ℜ ‘ ( 𝑌 / 𝑋 ) ) ) )
20 19 eqeq1d ⊢ ( 𝜑 → ( ( ℜ ‘ ( 𝑍 / 𝑋 ) ) = 0 ↔ ( ( 𝑍 / 𝑌 ) · ( ℜ ‘ ( 𝑌 / 𝑋 ) ) ) = 0 ) )
21 4 3 6 divcld ⊢ ( 𝜑 → ( 𝑍 / 𝑌 ) ∈ ℂ )
22 17 recld ⊢ ( 𝜑 → ( ℜ ‘ ( 𝑌 / 𝑋 ) ) ∈ ℝ )
23 22 recnd ⊢ ( 𝜑 → ( ℜ ‘ ( 𝑌 / 𝑋 ) ) ∈ ℂ )
24 21 23 mul0ord ⊢ ( 𝜑 → ( ( ( 𝑍 / 𝑌 ) · ( ℜ ‘ ( 𝑌 / 𝑋 ) ) ) = 0 ↔ ( ( 𝑍 / 𝑌 ) = 0 ∨ ( ℜ ‘ ( 𝑌 / 𝑋 ) ) = 0 ) ) )
25 14 20 24 3bitrd ⊢ ( 𝜑 → ( ( 𝑋 𝐹 𝑍 ) ∈ { ( π / 2 ) , - ( π / 2 ) } ↔ ( ( 𝑍 / 𝑌 ) = 0 ∨ ( ℜ ‘ ( 𝑌 / 𝑋 ) ) = 0 ) ) )
26 12 13 25 3bitr4d ⊢ ( 𝜑 → ( ( 𝑋 𝐹 𝑌 ) ∈ { ( π / 2 ) , - ( π / 2 ) } ↔ ( 𝑋 𝐹 𝑍 ) ∈ { ( π / 2 ) , - ( π / 2 ) } ) )