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 ∈ ℂ ∖ 0 , y ∈ ℂ ∖ 0 ⟼ ℑ ⁡ log ⁡ y x
angrtmuld.1 ⊢ φ → X ∈ ℂ
angrtmuld.2 ⊢ φ → Y ∈ ℂ
angrtmuld.3 ⊢ φ → Z ∈ ℂ
angrtmuld.4 ⊢ φ → X ≠ 0
angrtmuld.5 ⊢ φ → Y ≠ 0
angrtmuld.6 ⊢ φ → Z ≠ 0
angrtmuld.7 ⊢ φ → Z Y ∈ ℝ
Assertion angrtmuld ⊢ φ → X F Y ∈ π 2 − π 2 ↔ X F Z ∈ π 2 − π 2

Proof

Step Hyp Ref Expression
1 ang.1 ⊢ F = x ∈ ℂ ∖ 0 , y ∈ ℂ ∖ 0 ⟼ ℑ ⁡ log ⁡ y x
2 angrtmuld.1 ⊢ φ → X ∈ ℂ
3 angrtmuld.2 ⊢ φ → Y ∈ ℂ
4 angrtmuld.3 ⊢ φ → Z ∈ ℂ
5 angrtmuld.4 ⊢ φ → X ≠ 0
6 angrtmuld.5 ⊢ φ → Y ≠ 0
7 angrtmuld.6 ⊢ φ → Z ≠ 0
8 angrtmuld.7 ⊢ φ → Z Y ∈ ℝ
9 4 3 7 6 divne0d ⊢ φ → Z Y ≠ 0
10 9 neneqd ⊢ φ → ¬ Z Y = 0
11 biorf ⊢ ¬ Z Y = 0 → ℜ ⁡ Y X = 0 ↔ Z Y = 0 ∨ ℜ ⁡ Y X = 0
12 10 11 syl ⊢ φ → ℜ ⁡ Y X = 0 ↔ Z Y = 0 ∨ ℜ ⁡ Y X = 0
13 1 2 5 3 6 angrteqvd ⊢ φ → X F Y ∈ π 2 − π 2 ↔ ℜ ⁡ Y X = 0
14 1 2 5 4 7 angrteqvd ⊢ φ → X F Z ∈ π 2 − π 2 ↔ ℜ ⁡ Z X = 0
15 4 3 2 6 5 dmdcan2d ⊢ φ → Z Y ⁢ Y X = Z X
16 15 fveq2d ⊢ φ → ℜ ⁡ Z Y ⁢ Y X = ℜ ⁡ Z X
17 3 2 5 divcld ⊢ φ → Y X ∈ ℂ
18 8 17 remul2d ⊢ φ → ℜ ⁡ Z Y ⁢ Y X = Z Y ⁢ ℜ ⁡ Y X
19 16 18 eqtr3d ⊢ φ → ℜ ⁡ Z X = Z Y ⁢ ℜ ⁡ Y X
20 19 eqeq1d ⊢ φ → ℜ ⁡ Z X = 0 ↔ Z Y ⁢ ℜ ⁡ Y X = 0
21 4 3 6 divcld ⊢ φ → Z Y ∈ ℂ
22 17 recld ⊢ φ → ℜ ⁡ Y X ∈ ℝ
23 22 recnd ⊢ φ → ℜ ⁡ Y X ∈ ℂ
24 21 23 mul0ord ⊢ φ → Z Y ⁢ ℜ ⁡ Y X = 0 ↔ Z Y = 0 ∨ ℜ ⁡ Y X = 0
25 14 20 24 3bitrd ⊢ φ → X F Z ∈ π 2 − π 2 ↔ Z Y = 0 ∨ ℜ ⁡ Y X = 0
26 12 13 25 3bitr4d ⊢ φ → X F Y ∈ π 2 − π 2 ↔ X F Z ∈ π 2 − π 2