Metamath Proof Explorer

Theorem sigardiv

Description: If signed area between vectors B - A and C - A is zero, then those vectors lie on the same line. (Contributed by Saveliy Skresanov, 22-Sep-2017)

Ref Expression
Hypotheses sigar ⊢ 𝐺 = ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( ℑ ‘ ( ( ∗ ‘ 𝑥 ) · 𝑦 ) ) )
sigardiv.a ⊢ ( 𝜑 → ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) )
sigardiv.b ⊢ ( 𝜑 → ¬ 𝐶 = 𝐴 )
sigardiv.c ⊢ ( 𝜑 → ( ( 𝐵 − 𝐴 ) 𝐺 ( 𝐶 − 𝐴 ) ) = 0 )
Assertion sigardiv ( 𝜑 → ( ( 𝐵 − 𝐴 ) / ( 𝐶 − 𝐴 ) ) ∈ ℝ )

Proof

Step Hyp Ref Expression
1 sigar ⊢ 𝐺 = ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( ℑ ‘ ( ( ∗ ‘ 𝑥 ) · 𝑦 ) ) )
2 sigardiv.a ⊢ ( 𝜑 → ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) )
3 sigardiv.b ⊢ ( 𝜑 → ¬ 𝐶 = 𝐴 )
4 sigardiv.c ⊢ ( 𝜑 → ( ( 𝐵 − 𝐴 ) 𝐺 ( 𝐶 − 𝐴 ) ) = 0 )
5 2 simp2d ⊢ ( 𝜑 → 𝐵 ∈ ℂ )
6 2 simp1d ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
7 5 6 subcld ⊢ ( 𝜑 → ( 𝐵 − 𝐴 ) ∈ ℂ )
8 2 simp3d ⊢ ( 𝜑 → 𝐶 ∈ ℂ )
9 8 6 subcld ⊢ ( 𝜑 → ( 𝐶 − 𝐴 ) ∈ ℂ )
10 3 neqned ⊢ ( 𝜑 → 𝐶 ≠ 𝐴 )
11 8 6 10 subne0d ⊢ ( 𝜑 → ( 𝐶 − 𝐴 ) ≠ 0 )
12 7 9 11 cjdivd ⊢ ( 𝜑 → ( ∗ ‘ ( ( 𝐵 − 𝐴 ) / ( 𝐶 − 𝐴 ) ) ) = ( ( ∗ ‘ ( 𝐵 − 𝐴 ) ) / ( ∗ ‘ ( 𝐶 − 𝐴 ) ) ) )
13 7 cjcld ⊢ ( 𝜑 → ( ∗ ‘ ( 𝐵 − 𝐴 ) ) ∈ ℂ )
14 9 cjcld ⊢ ( 𝜑 → ( ∗ ‘ ( 𝐶 − 𝐴 ) ) ∈ ℂ )
15 9 11 cjne0d ⊢ ( 𝜑 → ( ∗ ‘ ( 𝐶 − 𝐴 ) ) ≠ 0 )
16 13 14 9 15 11 divcan5rd ⊢ ( 𝜑 → ( ( ( ∗ ‘ ( 𝐵 − 𝐴 ) ) · ( 𝐶 − 𝐴 ) ) / ( ( ∗ ‘ ( 𝐶 − 𝐴 ) ) · ( 𝐶 − 𝐴 ) ) ) = ( ( ∗ ‘ ( 𝐵 − 𝐴 ) ) / ( ∗ ‘ ( 𝐶 − 𝐴 ) ) ) )
17 13 9 mulcld ⊢ ( 𝜑 → ( ( ∗ ‘ ( 𝐵 − 𝐴 ) ) · ( 𝐶 − 𝐴 ) ) ∈ ℂ )
18 1 sigarval ⊢ ( ( ( 𝐵 − 𝐴 ) ∈ ℂ ∧ ( 𝐶 − 𝐴 ) ∈ ℂ ) → ( ( 𝐵 − 𝐴 ) 𝐺 ( 𝐶 − 𝐴 ) ) = ( ℑ ‘ ( ( ∗ ‘ ( 𝐵 − 𝐴 ) ) · ( 𝐶 − 𝐴 ) ) ) )
19 7 9 18 syl2anc ⊢ ( 𝜑 → ( ( 𝐵 − 𝐴 ) 𝐺 ( 𝐶 − 𝐴 ) ) = ( ℑ ‘ ( ( ∗ ‘ ( 𝐵 − 𝐴 ) ) · ( 𝐶 − 𝐴 ) ) ) )
20 19 4 eqtr3d ⊢ ( 𝜑 → ( ℑ ‘ ( ( ∗ ‘ ( 𝐵 − 𝐴 ) ) · ( 𝐶 − 𝐴 ) ) ) = 0 )
21 17 20 reim0bd ⊢ ( 𝜑 → ( ( ∗ ‘ ( 𝐵 − 𝐴 ) ) · ( 𝐶 − 𝐴 ) ) ∈ ℝ )
22 9 14 mulcomd ⊢ ( 𝜑 → ( ( 𝐶 − 𝐴 ) · ( ∗ ‘ ( 𝐶 − 𝐴 ) ) ) = ( ( ∗ ‘ ( 𝐶 − 𝐴 ) ) · ( 𝐶 − 𝐴 ) ) )
23 9 cjmulrcld ⊢ ( 𝜑 → ( ( 𝐶 − 𝐴 ) · ( ∗ ‘ ( 𝐶 − 𝐴 ) ) ) ∈ ℝ )
24 22 23 eqeltrrd ⊢ ( 𝜑 → ( ( ∗ ‘ ( 𝐶 − 𝐴 ) ) · ( 𝐶 − 𝐴 ) ) ∈ ℝ )
25 14 9 15 11 mulne0d ⊢ ( 𝜑 → ( ( ∗ ‘ ( 𝐶 − 𝐴 ) ) · ( 𝐶 − 𝐴 ) ) ≠ 0 )
26 21 24 25 redivcld ⊢ ( 𝜑 → ( ( ( ∗ ‘ ( 𝐵 − 𝐴 ) ) · ( 𝐶 − 𝐴 ) ) / ( ( ∗ ‘ ( 𝐶 − 𝐴 ) ) · ( 𝐶 − 𝐴 ) ) ) ∈ ℝ )
27 16 26 eqeltrrd ⊢ ( 𝜑 → ( ( ∗ ‘ ( 𝐵 − 𝐴 ) ) / ( ∗ ‘ ( 𝐶 − 𝐴 ) ) ) ∈ ℝ )
28 12 27 eqeltrd ⊢ ( 𝜑 → ( ∗ ‘ ( ( 𝐵 − 𝐴 ) / ( 𝐶 − 𝐴 ) ) ) ∈ ℝ )
29 28 cjred ⊢ ( 𝜑 → ( ∗ ‘ ( ∗ ‘ ( ( 𝐵 − 𝐴 ) / ( 𝐶 − 𝐴 ) ) ) ) = ( ∗ ‘ ( ( 𝐵 − 𝐴 ) / ( 𝐶 − 𝐴 ) ) ) )
30 7 9 11 divcld ⊢ ( 𝜑 → ( ( 𝐵 − 𝐴 ) / ( 𝐶 − 𝐴 ) ) ∈ ℂ )
31 30 cjcjd ⊢ ( 𝜑 → ( ∗ ‘ ( ∗ ‘ ( ( 𝐵 − 𝐴 ) / ( 𝐶 − 𝐴 ) ) ) ) = ( ( 𝐵 − 𝐴 ) / ( 𝐶 − 𝐴 ) ) )
32 29 31 eqtr3d ⊢ ( 𝜑 → ( ∗ ‘ ( ( 𝐵 − 𝐴 ) / ( 𝐶 − 𝐴 ) ) ) = ( ( 𝐵 − 𝐴 ) / ( 𝐶 − 𝐴 ) ) )
33 32 28 eqeltrrd ⊢ ( 𝜑 → ( ( 𝐵 − 𝐴 ) / ( 𝐶 − 𝐴 ) ) ∈ ℝ )