Metamath Proof Explorer

Theorem sigarcol

Description: Given three points A , B and C such that -. A = B , the point C lies on the line going through A and B iff the corresponding signed area is zero. That justifies the usage of signed area as a collinearity indicator. (Contributed by Saveliy Skresanov, 22-Sep-2017)

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

Proof

Step Hyp Ref Expression
1 sigarcol.sigar ⊢ 𝐺 = ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( ℑ ‘ ( ( ∗ ‘ 𝑥 ) · 𝑦 ) ) )
2 sigarcol.a ⊢ ( 𝜑 → ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) )
3 sigarcol.b ⊢ ( 𝜑 → ¬ 𝐴 = 𝐵 )
4 2 simp2d ⊢ ( 𝜑 → 𝐵 ∈ ℂ )
5 2 simp3d ⊢ ( 𝜑 → 𝐶 ∈ ℂ )
6 2 simp1d ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
7 4 5 6 3jca ⊢ ( 𝜑 → ( 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ∧ 𝐴 ∈ ℂ ) )
8 7 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝐴 − 𝐶 ) 𝐺 ( 𝐵 − 𝐶 ) ) = 0 ) → ( 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ∧ 𝐴 ∈ ℂ ) )
9 3 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝐴 − 𝐶 ) 𝐺 ( 𝐵 − 𝐶 ) ) = 0 ) → ¬ 𝐴 = 𝐵 )
10 1 sigarperm ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ( 𝐴 − 𝐶 ) 𝐺 ( 𝐵 − 𝐶 ) ) = ( ( 𝐵 − 𝐴 ) 𝐺 ( 𝐶 − 𝐴 ) ) )
11 2 10 syl ⊢ ( 𝜑 → ( ( 𝐴 − 𝐶 ) 𝐺 ( 𝐵 − 𝐶 ) ) = ( ( 𝐵 − 𝐴 ) 𝐺 ( 𝐶 − 𝐴 ) ) )
12 1 sigarperm ⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( ( 𝐵 − 𝐴 ) 𝐺 ( 𝐶 − 𝐴 ) ) = ( ( 𝐶 − 𝐵 ) 𝐺 ( 𝐴 − 𝐵 ) ) )
13 7 12 syl ⊢ ( 𝜑 → ( ( 𝐵 − 𝐴 ) 𝐺 ( 𝐶 − 𝐴 ) ) = ( ( 𝐶 − 𝐵 ) 𝐺 ( 𝐴 − 𝐵 ) ) )
14 11 13 eqtrd ⊢ ( 𝜑 → ( ( 𝐴 − 𝐶 ) 𝐺 ( 𝐵 − 𝐶 ) ) = ( ( 𝐶 − 𝐵 ) 𝐺 ( 𝐴 − 𝐵 ) ) )
15 14 eqeq1d ⊢ ( 𝜑 → ( ( ( 𝐴 − 𝐶 ) 𝐺 ( 𝐵 − 𝐶 ) ) = 0 ↔ ( ( 𝐶 − 𝐵 ) 𝐺 ( 𝐴 − 𝐵 ) ) = 0 ) )
16 15 biimpa ⊢ ( ( 𝜑 ∧ ( ( 𝐴 − 𝐶 ) 𝐺 ( 𝐵 − 𝐶 ) ) = 0 ) → ( ( 𝐶 − 𝐵 ) 𝐺 ( 𝐴 − 𝐵 ) ) = 0 )
17 1 8 9 16 sigardiv ⊢ ( ( 𝜑 ∧ ( ( 𝐴 − 𝐶 ) 𝐺 ( 𝐵 − 𝐶 ) ) = 0 ) → ( ( 𝐶 − 𝐵 ) / ( 𝐴 − 𝐵 ) ) ∈ ℝ )
18 5 4 subcld ⊢ ( 𝜑 → ( 𝐶 − 𝐵 ) ∈ ℂ )
19 18 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝐴 − 𝐶 ) 𝐺 ( 𝐵 − 𝐶 ) ) = 0 ) → ( 𝐶 − 𝐵 ) ∈ ℂ )
20 6 4 subcld ⊢ ( 𝜑 → ( 𝐴 − 𝐵 ) ∈ ℂ )
21 20 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝐴 − 𝐶 ) 𝐺 ( 𝐵 − 𝐶 ) ) = 0 ) → ( 𝐴 − 𝐵 ) ∈ ℂ )
22 6 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝐴 − 𝐶 ) 𝐺 ( 𝐵 − 𝐶 ) ) = 0 ) → 𝐴 ∈ ℂ )
23 4 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝐴 − 𝐶 ) 𝐺 ( 𝐵 − 𝐶 ) ) = 0 ) → 𝐵 ∈ ℂ )
24 9 neqned ⊢ ( ( 𝜑 ∧ ( ( 𝐴 − 𝐶 ) 𝐺 ( 𝐵 − 𝐶 ) ) = 0 ) → 𝐴 ≠ 𝐵 )
25 22 23 24 subne0d ⊢ ( ( 𝜑 ∧ ( ( 𝐴 − 𝐶 ) 𝐺 ( 𝐵 − 𝐶 ) ) = 0 ) → ( 𝐴 − 𝐵 ) ≠ 0 )
26 19 21 25 divcan1d ⊢ ( ( 𝜑 ∧ ( ( 𝐴 − 𝐶 ) 𝐺 ( 𝐵 − 𝐶 ) ) = 0 ) → ( ( ( 𝐶 − 𝐵 ) / ( 𝐴 − 𝐵 ) ) · ( 𝐴 − 𝐵 ) ) = ( 𝐶 − 𝐵 ) )
27 26 oveq2d ⊢ ( ( 𝜑 ∧ ( ( 𝐴 − 𝐶 ) 𝐺 ( 𝐵 − 𝐶 ) ) = 0 ) → ( 𝐵 + ( ( ( 𝐶 − 𝐵 ) / ( 𝐴 − 𝐵 ) ) · ( 𝐴 − 𝐵 ) ) ) = ( 𝐵 + ( 𝐶 − 𝐵 ) ) )
28 5 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝐴 − 𝐶 ) 𝐺 ( 𝐵 − 𝐶 ) ) = 0 ) → 𝐶 ∈ ℂ )
29 23 28 pncan3d ⊢ ( ( 𝜑 ∧ ( ( 𝐴 − 𝐶 ) 𝐺 ( 𝐵 − 𝐶 ) ) = 0 ) → ( 𝐵 + ( 𝐶 − 𝐵 ) ) = 𝐶 )
30 27 29 eqtr2d ⊢ ( ( 𝜑 ∧ ( ( 𝐴 − 𝐶 ) 𝐺 ( 𝐵 − 𝐶 ) ) = 0 ) → 𝐶 = ( 𝐵 + ( ( ( 𝐶 − 𝐵 ) / ( 𝐴 − 𝐵 ) ) · ( 𝐴 − 𝐵 ) ) ) )
31 oveq1 ⊢ ( 𝑡 = ( ( 𝐶 − 𝐵 ) / ( 𝐴 − 𝐵 ) ) → ( 𝑡 · ( 𝐴 − 𝐵 ) ) = ( ( ( 𝐶 − 𝐵 ) / ( 𝐴 − 𝐵 ) ) · ( 𝐴 − 𝐵 ) ) )
32 31 oveq2d ⊢ ( 𝑡 = ( ( 𝐶 − 𝐵 ) / ( 𝐴 − 𝐵 ) ) → ( 𝐵 + ( 𝑡 · ( 𝐴 − 𝐵 ) ) ) = ( 𝐵 + ( ( ( 𝐶 − 𝐵 ) / ( 𝐴 − 𝐵 ) ) · ( 𝐴 − 𝐵 ) ) ) )
33 32 rspceeqv ⊢ ( ( ( ( 𝐶 − 𝐵 ) / ( 𝐴 − 𝐵 ) ) ∈ ℝ ∧ 𝐶 = ( 𝐵 + ( ( ( 𝐶 − 𝐵 ) / ( 𝐴 − 𝐵 ) ) · ( 𝐴 − 𝐵 ) ) ) ) → ∃ 𝑡 ∈ ℝ 𝐶 = ( 𝐵 + ( 𝑡 · ( 𝐴 − 𝐵 ) ) ) )
34 17 30 33 syl2anc ⊢ ( ( 𝜑 ∧ ( ( 𝐴 − 𝐶 ) 𝐺 ( 𝐵 − 𝐶 ) ) = 0 ) → ∃ 𝑡 ∈ ℝ 𝐶 = ( 𝐵 + ( 𝑡 · ( 𝐴 − 𝐵 ) ) ) )
35 34 ex ⊢ ( 𝜑 → ( ( ( 𝐴 − 𝐶 ) 𝐺 ( 𝐵 − 𝐶 ) ) = 0 → ∃ 𝑡 ∈ ℝ 𝐶 = ( 𝐵 + ( 𝑡 · ( 𝐴 − 𝐵 ) ) ) ) )
36 14 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ ∧ 𝐶 = ( 𝐵 + ( 𝑡 · ( 𝐴 − 𝐵 ) ) ) ) → ( ( 𝐴 − 𝐶 ) 𝐺 ( 𝐵 − 𝐶 ) ) = ( ( 𝐶 − 𝐵 ) 𝐺 ( 𝐴 − 𝐵 ) ) )
37 4 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ ∧ 𝐶 = ( 𝐵 + ( 𝑡 · ( 𝐴 − 𝐵 ) ) ) ) → 𝐵 ∈ ℂ )
38 simp2 ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ ∧ 𝐶 = ( 𝐵 + ( 𝑡 · ( 𝐴 − 𝐵 ) ) ) ) → 𝑡 ∈ ℝ )
39 38 recnd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ ∧ 𝐶 = ( 𝐵 + ( 𝑡 · ( 𝐴 − 𝐵 ) ) ) ) → 𝑡 ∈ ℂ )
40 6 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ ∧ 𝐶 = ( 𝐵 + ( 𝑡 · ( 𝐴 − 𝐵 ) ) ) ) → 𝐴 ∈ ℂ )
41 40 37 subcld ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ ∧ 𝐶 = ( 𝐵 + ( 𝑡 · ( 𝐴 − 𝐵 ) ) ) ) → ( 𝐴 − 𝐵 ) ∈ ℂ )
42 39 41 mulcld ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ ∧ 𝐶 = ( 𝐵 + ( 𝑡 · ( 𝐴 − 𝐵 ) ) ) ) → ( 𝑡 · ( 𝐴 − 𝐵 ) ) ∈ ℂ )
43 simp3 ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ ∧ 𝐶 = ( 𝐵 + ( 𝑡 · ( 𝐴 − 𝐵 ) ) ) ) → 𝐶 = ( 𝐵 + ( 𝑡 · ( 𝐴 − 𝐵 ) ) ) )
44 37 42 43 mvrladdd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ ∧ 𝐶 = ( 𝐵 + ( 𝑡 · ( 𝐴 − 𝐵 ) ) ) ) → ( 𝐶 − 𝐵 ) = ( 𝑡 · ( 𝐴 − 𝐵 ) ) )
45 44 oveq1d ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ ∧ 𝐶 = ( 𝐵 + ( 𝑡 · ( 𝐴 − 𝐵 ) ) ) ) → ( ( 𝐶 − 𝐵 ) 𝐺 ( 𝐴 − 𝐵 ) ) = ( ( 𝑡 · ( 𝐴 − 𝐵 ) ) 𝐺 ( 𝐴 − 𝐵 ) ) )
46 39 41 mulcomd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ ∧ 𝐶 = ( 𝐵 + ( 𝑡 · ( 𝐴 − 𝐵 ) ) ) ) → ( 𝑡 · ( 𝐴 − 𝐵 ) ) = ( ( 𝐴 − 𝐵 ) · 𝑡 ) )
47 46 oveq1d ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ ∧ 𝐶 = ( 𝐵 + ( 𝑡 · ( 𝐴 − 𝐵 ) ) ) ) → ( ( 𝑡 · ( 𝐴 − 𝐵 ) ) 𝐺 ( 𝐴 − 𝐵 ) ) = ( ( ( 𝐴 − 𝐵 ) · 𝑡 ) 𝐺 ( 𝐴 − 𝐵 ) ) )
48 45 47 eqtrd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ ∧ 𝐶 = ( 𝐵 + ( 𝑡 · ( 𝐴 − 𝐵 ) ) ) ) → ( ( 𝐶 − 𝐵 ) 𝐺 ( 𝐴 − 𝐵 ) ) = ( ( ( 𝐴 − 𝐵 ) · 𝑡 ) 𝐺 ( 𝐴 − 𝐵 ) ) )
49 41 39 mulcld ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ ∧ 𝐶 = ( 𝐵 + ( 𝑡 · ( 𝐴 − 𝐵 ) ) ) ) → ( ( 𝐴 − 𝐵 ) · 𝑡 ) ∈ ℂ )
50 1 sigarac ⊢ ( ( ( ( 𝐴 − 𝐵 ) · 𝑡 ) ∈ ℂ ∧ ( 𝐴 − 𝐵 ) ∈ ℂ ) → ( ( ( 𝐴 − 𝐵 ) · 𝑡 ) 𝐺 ( 𝐴 − 𝐵 ) ) = - ( ( 𝐴 − 𝐵 ) 𝐺 ( ( 𝐴 − 𝐵 ) · 𝑡 ) ) )
51 49 41 50 syl2anc ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ ∧ 𝐶 = ( 𝐵 + ( 𝑡 · ( 𝐴 − 𝐵 ) ) ) ) → ( ( ( 𝐴 − 𝐵 ) · 𝑡 ) 𝐺 ( 𝐴 − 𝐵 ) ) = - ( ( 𝐴 − 𝐵 ) 𝐺 ( ( 𝐴 − 𝐵 ) · 𝑡 ) ) )
52 1 sigarls ⊢ ( ( ( 𝐴 − 𝐵 ) ∈ ℂ ∧ ( 𝐴 − 𝐵 ) ∈ ℂ ∧ 𝑡 ∈ ℝ ) → ( ( 𝐴 − 𝐵 ) 𝐺 ( ( 𝐴 − 𝐵 ) · 𝑡 ) ) = ( ( ( 𝐴 − 𝐵 ) 𝐺 ( 𝐴 − 𝐵 ) ) · 𝑡 ) )
53 41 41 38 52 syl3anc ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ ∧ 𝐶 = ( 𝐵 + ( 𝑡 · ( 𝐴 − 𝐵 ) ) ) ) → ( ( 𝐴 − 𝐵 ) 𝐺 ( ( 𝐴 − 𝐵 ) · 𝑡 ) ) = ( ( ( 𝐴 − 𝐵 ) 𝐺 ( 𝐴 − 𝐵 ) ) · 𝑡 ) )
54 1 sigarid ⊢ ( ( 𝐴 − 𝐵 ) ∈ ℂ → ( ( 𝐴 − 𝐵 ) 𝐺 ( 𝐴 − 𝐵 ) ) = 0 )
55 41 54 syl ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ ∧ 𝐶 = ( 𝐵 + ( 𝑡 · ( 𝐴 − 𝐵 ) ) ) ) → ( ( 𝐴 − 𝐵 ) 𝐺 ( 𝐴 − 𝐵 ) ) = 0 )
56 55 oveq1d ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ ∧ 𝐶 = ( 𝐵 + ( 𝑡 · ( 𝐴 − 𝐵 ) ) ) ) → ( ( ( 𝐴 − 𝐵 ) 𝐺 ( 𝐴 − 𝐵 ) ) · 𝑡 ) = ( 0 · 𝑡 ) )
57 39 mul02d ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ ∧ 𝐶 = ( 𝐵 + ( 𝑡 · ( 𝐴 − 𝐵 ) ) ) ) → ( 0 · 𝑡 ) = 0 )
58 53 56 57 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ ∧ 𝐶 = ( 𝐵 + ( 𝑡 · ( 𝐴 − 𝐵 ) ) ) ) → ( ( 𝐴 − 𝐵 ) 𝐺 ( ( 𝐴 − 𝐵 ) · 𝑡 ) ) = 0 )
59 58 negeqd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ ∧ 𝐶 = ( 𝐵 + ( 𝑡 · ( 𝐴 − 𝐵 ) ) ) ) → - ( ( 𝐴 − 𝐵 ) 𝐺 ( ( 𝐴 − 𝐵 ) · 𝑡 ) ) = - 0 )
60 neg0 ⊢ - 0 = 0
61 60 a1i ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ ∧ 𝐶 = ( 𝐵 + ( 𝑡 · ( 𝐴 − 𝐵 ) ) ) ) → - 0 = 0 )
62 51 59 61 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ ∧ 𝐶 = ( 𝐵 + ( 𝑡 · ( 𝐴 − 𝐵 ) ) ) ) → ( ( ( 𝐴 − 𝐵 ) · 𝑡 ) 𝐺 ( 𝐴 − 𝐵 ) ) = 0 )
63 36 48 62 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ ∧ 𝐶 = ( 𝐵 + ( 𝑡 · ( 𝐴 − 𝐵 ) ) ) ) → ( ( 𝐴 − 𝐶 ) 𝐺 ( 𝐵 − 𝐶 ) ) = 0 )
64 63 rexlimdv3a ⊢ ( 𝜑 → ( ∃ 𝑡 ∈ ℝ 𝐶 = ( 𝐵 + ( 𝑡 · ( 𝐴 − 𝐵 ) ) ) → ( ( 𝐴 − 𝐶 ) 𝐺 ( 𝐵 − 𝐶 ) ) = 0 ) )
65 35 64 impbid ⊢ ( 𝜑 → ( ( ( 𝐴 − 𝐶 ) 𝐺 ( 𝐵 − 𝐶 ) ) = 0 ↔ ∃ 𝑡 ∈ ℝ 𝐶 = ( 𝐵 + ( 𝑡 · ( 𝐴 − 𝐵 ) ) ) ) )