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 \in (ℂ ∖ \{0\}), y \in (ℂ ∖ \{0\}) ⟼ ℑ (\log (\frac{y}{x})))$
	angrtmuld.1	$⊢ φ \to X \in ℂ$
	angrtmuld.2	$⊢ φ \to Y \in ℂ$
	angrtmuld.3	$⊢ φ \to Z \in ℂ$
	angrtmuld.4	$⊢ φ \to X \neq 0$
	angrtmuld.5	$⊢ φ \to Y \neq 0$
	angrtmuld.6	$⊢ φ \to Z \neq 0$
	angrtmuld.7	$⊢ φ \to \frac{Z}{Y} \in ℝ$
Assertion	angrtmuld	$⊢ φ \to (X F Y \in \{\frac{π}{2}, - \frac{π}{2}\} \leftrightarrow X F Z \in \{\frac{π}{2}, - \frac{π}{2}\})$

Proof

Step	Hyp	Ref	Expression
1		ang.1	$⊢ F = (x \in (ℂ ∖ \{0\}), y \in (ℂ ∖ \{0\}) ⟼ ℑ (\log (\frac{y}{x})))$
2		angrtmuld.1	$⊢ φ \to X \in ℂ$
3		angrtmuld.2	$⊢ φ \to Y \in ℂ$
4		angrtmuld.3	$⊢ φ \to Z \in ℂ$
5		angrtmuld.4	$⊢ φ \to X \neq 0$
6		angrtmuld.5	$⊢ φ \to Y \neq 0$
7		angrtmuld.6	$⊢ φ \to Z \neq 0$
8		angrtmuld.7	$⊢ φ \to \frac{Z}{Y} \in ℝ$
9	4 3 7 6	divne0d	$⊢ φ \to \frac{Z}{Y} \neq 0$
10	9	neneqd	$⊢ φ \to \neg \frac{Z}{Y} = 0$
11		biorf	$⊢ \neg \frac{Z}{Y} = 0 \to (ℜ (\frac{Y}{X}) = 0 \leftrightarrow (\frac{Z}{Y} = 0 \lor ℜ (\frac{Y}{X}) = 0))$
12	10 11	syl	$⊢ φ \to (ℜ (\frac{Y}{X}) = 0 \leftrightarrow (\frac{Z}{Y} = 0 \lor ℜ (\frac{Y}{X}) = 0))$
13	1 2 5 3 6	angrteqvd	$⊢ φ \to (X F Y \in \{\frac{π}{2}, - \frac{π}{2}\} \leftrightarrow ℜ (\frac{Y}{X}) = 0)$
14	1 2 5 4 7	angrteqvd	$⊢ φ \to (X F Z \in \{\frac{π}{2}, - \frac{π}{2}\} \leftrightarrow ℜ (\frac{Z}{X}) = 0)$
15	4 3 2 6 5	dmdcan2d	$⊢ φ \to (\frac{Z}{Y}) (\frac{Y}{X}) = \frac{Z}{X}$
16	15	fveq2d	$⊢ φ \to ℜ ((\frac{Z}{Y}) (\frac{Y}{X})) = ℜ (\frac{Z}{X})$
17	3 2 5	divcld	$⊢ φ \to \frac{Y}{X} \in ℂ$
18	8 17	remul2d	$⊢ φ \to ℜ ((\frac{Z}{Y}) (\frac{Y}{X})) = (\frac{Z}{Y}) ℜ (\frac{Y}{X})$
19	16 18	eqtr3d	$⊢ φ \to ℜ (\frac{Z}{X}) = (\frac{Z}{Y}) ℜ (\frac{Y}{X})$
20	19	eqeq1d	$⊢ φ \to (ℜ (\frac{Z}{X}) = 0 \leftrightarrow (\frac{Z}{Y}) ℜ (\frac{Y}{X}) = 0)$
21	4 3 6	divcld	$⊢ φ \to \frac{Z}{Y} \in ℂ$
22	17	recld	$⊢ φ \to ℜ (\frac{Y}{X}) \in ℝ$
23	22	recnd	$⊢ φ \to ℜ (\frac{Y}{X}) \in ℂ$
24	21 23	mul0ord	$⊢ φ \to ((\frac{Z}{Y}) ℜ (\frac{Y}{X}) = 0 \leftrightarrow (\frac{Z}{Y} = 0 \lor ℜ (\frac{Y}{X}) = 0))$
25	14 20 24	3bitrd	$⊢ φ \to (X F Z \in \{\frac{π}{2}, - \frac{π}{2}\} \leftrightarrow (\frac{Z}{Y} = 0 \lor ℜ (\frac{Y}{X}) = 0))$
26	12 13 25	3bitr4d	$⊢ φ \to (X F Y \in \{\frac{π}{2}, - \frac{π}{2}\} \leftrightarrow X F Z \in \{\frac{π}{2}, - \frac{π}{2}\})$

Metamath Proof Explorer

Theorem angrtmuld

Proof