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 ) } ) )

Metamath Proof Explorer

Theorem angrtmuld

Proof