Metamath Proof Explorer

Theorem sharhght

Description: Let A B C be a triangle, and let D lie on the line A B . Then (doubled) areas of triangles A D C and C D B relate as lengths of corresponding bases A D and D B . (Contributed by Saveliy Skresanov, 23-Sep-2017)

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

Proof

Step Hyp Ref Expression
1 sharhght.sigar ⊢ 𝐺 = ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( ℑ ‘ ( ( ∗ ‘ 𝑥 ) · 𝑦 ) ) )
2 sharhght.a ⊢ ( 𝜑 → ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) )
3 sharhght.b ⊢ ( 𝜑 → ( 𝐷 ∈ ℂ ∧ ( ( 𝐴 − 𝐷 ) 𝐺 ( 𝐵 − 𝐷 ) ) = 0 ) )
4 2 simp3d ⊢ ( 𝜑 → 𝐶 ∈ ℂ )
5 2 simp1d ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
6 4 5 subcld ⊢ ( 𝜑 → ( 𝐶 − 𝐴 ) ∈ ℂ )
7 6 adantr ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐷 ) → ( 𝐶 − 𝐴 ) ∈ ℂ )
8 3 simpld ⊢ ( 𝜑 → 𝐷 ∈ ℂ )
9 8 5 subcld ⊢ ( 𝜑 → ( 𝐷 − 𝐴 ) ∈ ℂ )
10 9 adantr ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐷 ) → ( 𝐷 − 𝐴 ) ∈ ℂ )
11 1 sigarim ⊢ ( ( ( 𝐶 − 𝐴 ) ∈ ℂ ∧ ( 𝐷 − 𝐴 ) ∈ ℂ ) → ( ( 𝐶 − 𝐴 ) 𝐺 ( 𝐷 − 𝐴 ) ) ∈ ℝ )
12 7 10 11 syl2anc ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐷 ) → ( ( 𝐶 − 𝐴 ) 𝐺 ( 𝐷 − 𝐴 ) ) ∈ ℝ )
13 12 recnd ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐷 ) → ( ( 𝐶 − 𝐴 ) 𝐺 ( 𝐷 − 𝐴 ) ) ∈ ℂ )
14 13 mul01d ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐷 ) → ( ( ( 𝐶 − 𝐴 ) 𝐺 ( 𝐷 − 𝐴 ) ) · 0 ) = 0 )
15 2 simp2d ⊢ ( 𝜑 → 𝐵 ∈ ℂ )
16 15 adantr ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐷 ) → 𝐵 ∈ ℂ )
17 simpr ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐷 ) → 𝐵 = 𝐷 )
18 16 17 subeq0bd ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐷 ) → ( 𝐵 − 𝐷 ) = 0 )
19 18 oveq2d ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐷 ) → ( ( ( 𝐶 − 𝐴 ) 𝐺 ( 𝐷 − 𝐴 ) ) · ( 𝐵 − 𝐷 ) ) = ( ( ( 𝐶 − 𝐴 ) 𝐺 ( 𝐷 − 𝐴 ) ) · 0 ) )
20 4 15 subcld ⊢ ( 𝜑 → ( 𝐶 − 𝐵 ) ∈ ℂ )
21 20 adantr ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐷 ) → ( 𝐶 − 𝐵 ) ∈ ℂ )
22 8 15 subcld ⊢ ( 𝜑 → ( 𝐷 − 𝐵 ) ∈ ℂ )
23 22 adantr ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐷 ) → ( 𝐷 − 𝐵 ) ∈ ℂ )
24 1 sigarval ⊢ ( ( ( 𝐶 − 𝐵 ) ∈ ℂ ∧ ( 𝐷 − 𝐵 ) ∈ ℂ ) → ( ( 𝐶 − 𝐵 ) 𝐺 ( 𝐷 − 𝐵 ) ) = ( ℑ ‘ ( ( ∗ ‘ ( 𝐶 − 𝐵 ) ) · ( 𝐷 − 𝐵 ) ) ) )
25 21 23 24 syl2anc ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐷 ) → ( ( 𝐶 − 𝐵 ) 𝐺 ( 𝐷 − 𝐵 ) ) = ( ℑ ‘ ( ( ∗ ‘ ( 𝐶 − 𝐵 ) ) · ( 𝐷 − 𝐵 ) ) ) )
26 8 adantr ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐷 ) → 𝐷 ∈ ℂ )
27 17 eqcomd ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐷 ) → 𝐷 = 𝐵 )
28 26 27 subeq0bd ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐷 ) → ( 𝐷 − 𝐵 ) = 0 )
29 28 oveq2d ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐷 ) → ( ( ∗ ‘ ( 𝐶 − 𝐵 ) ) · ( 𝐷 − 𝐵 ) ) = ( ( ∗ ‘ ( 𝐶 − 𝐵 ) ) · 0 ) )
30 21 cjcld ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐷 ) → ( ∗ ‘ ( 𝐶 − 𝐵 ) ) ∈ ℂ )
31 30 mul01d ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐷 ) → ( ( ∗ ‘ ( 𝐶 − 𝐵 ) ) · 0 ) = 0 )
32 29 31 eqtrd ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐷 ) → ( ( ∗ ‘ ( 𝐶 − 𝐵 ) ) · ( 𝐷 − 𝐵 ) ) = 0 )
33 32 fveq2d ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐷 ) → ( ℑ ‘ ( ( ∗ ‘ ( 𝐶 − 𝐵 ) ) · ( 𝐷 − 𝐵 ) ) ) = ( ℑ ‘ 0 ) )
34 0red ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐷 ) → 0 ∈ ℝ )
35 34 reim0d ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐷 ) → ( ℑ ‘ 0 ) = 0 )
36 25 33 35 3eqtrd ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐷 ) → ( ( 𝐶 − 𝐵 ) 𝐺 ( 𝐷 − 𝐵 ) ) = 0 )
37 36 oveq1d ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐷 ) → ( ( ( 𝐶 − 𝐵 ) 𝐺 ( 𝐷 − 𝐵 ) ) · ( 𝐴 − 𝐷 ) ) = ( 0 · ( 𝐴 − 𝐷 ) ) )
38 5 adantr ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐷 ) → 𝐴 ∈ ℂ )
39 38 26 subcld ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐷 ) → ( 𝐴 − 𝐷 ) ∈ ℂ )
40 39 mul02d ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐷 ) → ( 0 · ( 𝐴 − 𝐷 ) ) = 0 )
41 37 40 eqtrd ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐷 ) → ( ( ( 𝐶 − 𝐵 ) 𝐺 ( 𝐷 − 𝐵 ) ) · ( 𝐴 − 𝐷 ) ) = 0 )
42 14 19 41 3eqtr4d ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐷 ) → ( ( ( 𝐶 − 𝐴 ) 𝐺 ( 𝐷 − 𝐴 ) ) · ( 𝐵 − 𝐷 ) ) = ( ( ( 𝐶 − 𝐵 ) 𝐺 ( 𝐷 − 𝐵 ) ) · ( 𝐴 − 𝐷 ) ) )
43 4 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝐵 = 𝐷 ) → 𝐶 ∈ ℂ )
44 15 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝐵 = 𝐷 ) → 𝐵 ∈ ℂ )
45 5 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝐵 = 𝐷 ) → 𝐴 ∈ ℂ )
46 43 44 45 npncand ⊢ ( ( 𝜑 ∧ ¬ 𝐵 = 𝐷 ) → ( ( 𝐶 − 𝐵 ) + ( 𝐵 − 𝐴 ) ) = ( 𝐶 − 𝐴 ) )
47 46 oveq1d ⊢ ( ( 𝜑 ∧ ¬ 𝐵 = 𝐷 ) → ( ( ( 𝐶 − 𝐵 ) + ( 𝐵 − 𝐴 ) ) 𝐺 ( 𝐷 − 𝐴 ) ) = ( ( 𝐶 − 𝐴 ) 𝐺 ( 𝐷 − 𝐴 ) ) )
48 43 44 subcld ⊢ ( ( 𝜑 ∧ ¬ 𝐵 = 𝐷 ) → ( 𝐶 − 𝐵 ) ∈ ℂ )
49 9 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝐵 = 𝐷 ) → ( 𝐷 − 𝐴 ) ∈ ℂ )
50 44 45 subcld ⊢ ( ( 𝜑 ∧ ¬ 𝐵 = 𝐷 ) → ( 𝐵 − 𝐴 ) ∈ ℂ )
51 1 sigaraf ⊢ ( ( ( 𝐶 − 𝐵 ) ∈ ℂ ∧ ( 𝐷 − 𝐴 ) ∈ ℂ ∧ ( 𝐵 − 𝐴 ) ∈ ℂ ) → ( ( ( 𝐶 − 𝐵 ) + ( 𝐵 − 𝐴 ) ) 𝐺 ( 𝐷 − 𝐴 ) ) = ( ( ( 𝐶 − 𝐵 ) 𝐺 ( 𝐷 − 𝐴 ) ) + ( ( 𝐵 − 𝐴 ) 𝐺 ( 𝐷 − 𝐴 ) ) ) )
52 48 49 50 51 syl3anc ⊢ ( ( 𝜑 ∧ ¬ 𝐵 = 𝐷 ) → ( ( ( 𝐶 − 𝐵 ) + ( 𝐵 − 𝐴 ) ) 𝐺 ( 𝐷 − 𝐴 ) ) = ( ( ( 𝐶 − 𝐵 ) 𝐺 ( 𝐷 − 𝐴 ) ) + ( ( 𝐵 − 𝐴 ) 𝐺 ( 𝐷 − 𝐴 ) ) ) )
53 47 52 eqtr3d ⊢ ( ( 𝜑 ∧ ¬ 𝐵 = 𝐷 ) → ( ( 𝐶 − 𝐴 ) 𝐺 ( 𝐷 − 𝐴 ) ) = ( ( ( 𝐶 − 𝐵 ) 𝐺 ( 𝐷 − 𝐴 ) ) + ( ( 𝐵 − 𝐴 ) 𝐺 ( 𝐷 − 𝐴 ) ) ) )
54 3 simprd ⊢ ( 𝜑 → ( ( 𝐴 − 𝐷 ) 𝐺 ( 𝐵 − 𝐷 ) ) = 0 )
55 54 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝐵 = 𝐷 ) → ( ( 𝐴 − 𝐷 ) 𝐺 ( 𝐵 − 𝐷 ) ) = 0 )
56 8 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝐵 = 𝐷 ) → 𝐷 ∈ ℂ )
57 1 sigarperm ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐷 ∈ ℂ ) → ( ( 𝐴 − 𝐷 ) 𝐺 ( 𝐵 − 𝐷 ) ) = ( ( 𝐵 − 𝐴 ) 𝐺 ( 𝐷 − 𝐴 ) ) )
58 45 44 56 57 syl3anc ⊢ ( ( 𝜑 ∧ ¬ 𝐵 = 𝐷 ) → ( ( 𝐴 − 𝐷 ) 𝐺 ( 𝐵 − 𝐷 ) ) = ( ( 𝐵 − 𝐴 ) 𝐺 ( 𝐷 − 𝐴 ) ) )
59 55 58 eqtr3d ⊢ ( ( 𝜑 ∧ ¬ 𝐵 = 𝐷 ) → 0 = ( ( 𝐵 − 𝐴 ) 𝐺 ( 𝐷 − 𝐴 ) ) )
60 59 oveq2d ⊢ ( ( 𝜑 ∧ ¬ 𝐵 = 𝐷 ) → ( ( ( 𝐶 − 𝐵 ) 𝐺 ( 𝐷 − 𝐴 ) ) + 0 ) = ( ( ( 𝐶 − 𝐵 ) 𝐺 ( 𝐷 − 𝐴 ) ) + ( ( 𝐵 − 𝐴 ) 𝐺 ( 𝐷 − 𝐴 ) ) ) )
61 1 sigarim ⊢ ( ( ( 𝐶 − 𝐵 ) ∈ ℂ ∧ ( 𝐷 − 𝐴 ) ∈ ℂ ) → ( ( 𝐶 − 𝐵 ) 𝐺 ( 𝐷 − 𝐴 ) ) ∈ ℝ )
62 48 49 61 syl2anc ⊢ ( ( 𝜑 ∧ ¬ 𝐵 = 𝐷 ) → ( ( 𝐶 − 𝐵 ) 𝐺 ( 𝐷 − 𝐴 ) ) ∈ ℝ )
63 62 recnd ⊢ ( ( 𝜑 ∧ ¬ 𝐵 = 𝐷 ) → ( ( 𝐶 − 𝐵 ) 𝐺 ( 𝐷 − 𝐴 ) ) ∈ ℂ )
64 63 addid1d ⊢ ( ( 𝜑 ∧ ¬ 𝐵 = 𝐷 ) → ( ( ( 𝐶 − 𝐵 ) 𝐺 ( 𝐷 − 𝐴 ) ) + 0 ) = ( ( 𝐶 − 𝐵 ) 𝐺 ( 𝐷 − 𝐴 ) ) )
65 53 60 64 3eqtr2d ⊢ ( ( 𝜑 ∧ ¬ 𝐵 = 𝐷 ) → ( ( 𝐶 − 𝐴 ) 𝐺 ( 𝐷 − 𝐴 ) ) = ( ( 𝐶 − 𝐵 ) 𝐺 ( 𝐷 − 𝐴 ) ) )
66 44 56 negsubdi2d ⊢ ( ( 𝜑 ∧ ¬ 𝐵 = 𝐷 ) → - ( 𝐵 − 𝐷 ) = ( 𝐷 − 𝐵 ) )
67 66 eqcomd ⊢ ( ( 𝜑 ∧ ¬ 𝐵 = 𝐷 ) → ( 𝐷 − 𝐵 ) = - ( 𝐵 − 𝐷 ) )
68 67 oveq1d ⊢ ( ( 𝜑 ∧ ¬ 𝐵 = 𝐷 ) → ( ( 𝐷 − 𝐵 ) / ( 𝐵 − 𝐷 ) ) = ( - ( 𝐵 − 𝐷 ) / ( 𝐵 − 𝐷 ) ) )
69 44 56 subcld ⊢ ( ( 𝜑 ∧ ¬ 𝐵 = 𝐷 ) → ( 𝐵 − 𝐷 ) ∈ ℂ )
70 simpr ⊢ ( ( 𝜑 ∧ ¬ 𝐵 = 𝐷 ) → ¬ 𝐵 = 𝐷 )
71 70 neqned ⊢ ( ( 𝜑 ∧ ¬ 𝐵 = 𝐷 ) → 𝐵 ≠ 𝐷 )
72 44 56 71 subne0d ⊢ ( ( 𝜑 ∧ ¬ 𝐵 = 𝐷 ) → ( 𝐵 − 𝐷 ) ≠ 0 )
73 69 69 72 divnegd ⊢ ( ( 𝜑 ∧ ¬ 𝐵 = 𝐷 ) → - ( ( 𝐵 − 𝐷 ) / ( 𝐵 − 𝐷 ) ) = ( - ( 𝐵 − 𝐷 ) / ( 𝐵 − 𝐷 ) ) )
74 69 72 dividd ⊢ ( ( 𝜑 ∧ ¬ 𝐵 = 𝐷 ) → ( ( 𝐵 − 𝐷 ) / ( 𝐵 − 𝐷 ) ) = 1 )
75 74 negeqd ⊢ ( ( 𝜑 ∧ ¬ 𝐵 = 𝐷 ) → - ( ( 𝐵 − 𝐷 ) / ( 𝐵 − 𝐷 ) ) = - 1 )
76 68 73 75 3eqtr2d ⊢ ( ( 𝜑 ∧ ¬ 𝐵 = 𝐷 ) → ( ( 𝐷 − 𝐵 ) / ( 𝐵 − 𝐷 ) ) = - 1 )
77 76 oveq1d ⊢ ( ( 𝜑 ∧ ¬ 𝐵 = 𝐷 ) → ( ( ( 𝐷 − 𝐵 ) / ( 𝐵 − 𝐷 ) ) · ( 𝐴 − 𝐷 ) ) = ( - 1 · ( 𝐴 − 𝐷 ) ) )
78 45 56 subcld ⊢ ( ( 𝜑 ∧ ¬ 𝐵 = 𝐷 ) → ( 𝐴 − 𝐷 ) ∈ ℂ )
79 78 mulm1d ⊢ ( ( 𝜑 ∧ ¬ 𝐵 = 𝐷 ) → ( - 1 · ( 𝐴 − 𝐷 ) ) = - ( 𝐴 − 𝐷 ) )
80 45 56 negsubdi2d ⊢ ( ( 𝜑 ∧ ¬ 𝐵 = 𝐷 ) → - ( 𝐴 − 𝐷 ) = ( 𝐷 − 𝐴 ) )
81 77 79 80 3eqtrd ⊢ ( ( 𝜑 ∧ ¬ 𝐵 = 𝐷 ) → ( ( ( 𝐷 − 𝐵 ) / ( 𝐵 − 𝐷 ) ) · ( 𝐴 − 𝐷 ) ) = ( 𝐷 − 𝐴 ) )
82 56 44 subcld ⊢ ( ( 𝜑 ∧ ¬ 𝐵 = 𝐷 ) → ( 𝐷 − 𝐵 ) ∈ ℂ )
83 82 69 78 72 div32d ⊢ ( ( 𝜑 ∧ ¬ 𝐵 = 𝐷 ) → ( ( ( 𝐷 − 𝐵 ) / ( 𝐵 − 𝐷 ) ) · ( 𝐴 − 𝐷 ) ) = ( ( 𝐷 − 𝐵 ) · ( ( 𝐴 − 𝐷 ) / ( 𝐵 − 𝐷 ) ) ) )
84 81 83 eqtr3d ⊢ ( ( 𝜑 ∧ ¬ 𝐵 = 𝐷 ) → ( 𝐷 − 𝐴 ) = ( ( 𝐷 − 𝐵 ) · ( ( 𝐴 − 𝐷 ) / ( 𝐵 − 𝐷 ) ) ) )
85 84 oveq2d ⊢ ( ( 𝜑 ∧ ¬ 𝐵 = 𝐷 ) → ( ( 𝐶 − 𝐵 ) 𝐺 ( 𝐷 − 𝐴 ) ) = ( ( 𝐶 − 𝐵 ) 𝐺 ( ( 𝐷 − 𝐵 ) · ( ( 𝐴 − 𝐷 ) / ( 𝐵 − 𝐷 ) ) ) ) )
86 56 45 44 3jca ⊢ ( ( 𝜑 ∧ ¬ 𝐵 = 𝐷 ) → ( 𝐷 ∈ ℂ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) )
87 1 86 70 55 sigardiv ⊢ ( ( 𝜑 ∧ ¬ 𝐵 = 𝐷 ) → ( ( 𝐴 − 𝐷 ) / ( 𝐵 − 𝐷 ) ) ∈ ℝ )
88 1 sigarls ⊢ ( ( ( 𝐶 − 𝐵 ) ∈ ℂ ∧ ( 𝐷 − 𝐵 ) ∈ ℂ ∧ ( ( 𝐴 − 𝐷 ) / ( 𝐵 − 𝐷 ) ) ∈ ℝ ) → ( ( 𝐶 − 𝐵 ) 𝐺 ( ( 𝐷 − 𝐵 ) · ( ( 𝐴 − 𝐷 ) / ( 𝐵 − 𝐷 ) ) ) ) = ( ( ( 𝐶 − 𝐵 ) 𝐺 ( 𝐷 − 𝐵 ) ) · ( ( 𝐴 − 𝐷 ) / ( 𝐵 − 𝐷 ) ) ) )
89 48 82 87 88 syl3anc ⊢ ( ( 𝜑 ∧ ¬ 𝐵 = 𝐷 ) → ( ( 𝐶 − 𝐵 ) 𝐺 ( ( 𝐷 − 𝐵 ) · ( ( 𝐴 − 𝐷 ) / ( 𝐵 − 𝐷 ) ) ) ) = ( ( ( 𝐶 − 𝐵 ) 𝐺 ( 𝐷 − 𝐵 ) ) · ( ( 𝐴 − 𝐷 ) / ( 𝐵 − 𝐷 ) ) ) )
90 65 85 89 3eqtrd ⊢ ( ( 𝜑 ∧ ¬ 𝐵 = 𝐷 ) → ( ( 𝐶 − 𝐴 ) 𝐺 ( 𝐷 − 𝐴 ) ) = ( ( ( 𝐶 − 𝐵 ) 𝐺 ( 𝐷 − 𝐵 ) ) · ( ( 𝐴 − 𝐷 ) / ( 𝐵 − 𝐷 ) ) ) )
91 90 oveq1d ⊢ ( ( 𝜑 ∧ ¬ 𝐵 = 𝐷 ) → ( ( ( 𝐶 − 𝐴 ) 𝐺 ( 𝐷 − 𝐴 ) ) · ( 𝐵 − 𝐷 ) ) = ( ( ( ( 𝐶 − 𝐵 ) 𝐺 ( 𝐷 − 𝐵 ) ) · ( ( 𝐴 − 𝐷 ) / ( 𝐵 − 𝐷 ) ) ) · ( 𝐵 − 𝐷 ) ) )
92 1 sigarim ⊢ ( ( ( 𝐶 − 𝐵 ) ∈ ℂ ∧ ( 𝐷 − 𝐵 ) ∈ ℂ ) → ( ( 𝐶 − 𝐵 ) 𝐺 ( 𝐷 − 𝐵 ) ) ∈ ℝ )
93 92 recnd ⊢ ( ( ( 𝐶 − 𝐵 ) ∈ ℂ ∧ ( 𝐷 − 𝐵 ) ∈ ℂ ) → ( ( 𝐶 − 𝐵 ) 𝐺 ( 𝐷 − 𝐵 ) ) ∈ ℂ )
94 48 82 93 syl2anc ⊢ ( ( 𝜑 ∧ ¬ 𝐵 = 𝐷 ) → ( ( 𝐶 − 𝐵 ) 𝐺 ( 𝐷 − 𝐵 ) ) ∈ ℂ )
95 78 69 72 divcld ⊢ ( ( 𝜑 ∧ ¬ 𝐵 = 𝐷 ) → ( ( 𝐴 − 𝐷 ) / ( 𝐵 − 𝐷 ) ) ∈ ℂ )
96 94 95 69 mulassd ⊢ ( ( 𝜑 ∧ ¬ 𝐵 = 𝐷 ) → ( ( ( ( 𝐶 − 𝐵 ) 𝐺 ( 𝐷 − 𝐵 ) ) · ( ( 𝐴 − 𝐷 ) / ( 𝐵 − 𝐷 ) ) ) · ( 𝐵 − 𝐷 ) ) = ( ( ( 𝐶 − 𝐵 ) 𝐺 ( 𝐷 − 𝐵 ) ) · ( ( ( 𝐴 − 𝐷 ) / ( 𝐵 − 𝐷 ) ) · ( 𝐵 − 𝐷 ) ) ) )
97 78 69 72 divcan1d ⊢ ( ( 𝜑 ∧ ¬ 𝐵 = 𝐷 ) → ( ( ( 𝐴 − 𝐷 ) / ( 𝐵 − 𝐷 ) ) · ( 𝐵 − 𝐷 ) ) = ( 𝐴 − 𝐷 ) )
98 97 oveq2d ⊢ ( ( 𝜑 ∧ ¬ 𝐵 = 𝐷 ) → ( ( ( 𝐶 − 𝐵 ) 𝐺 ( 𝐷 − 𝐵 ) ) · ( ( ( 𝐴 − 𝐷 ) / ( 𝐵 − 𝐷 ) ) · ( 𝐵 − 𝐷 ) ) ) = ( ( ( 𝐶 − 𝐵 ) 𝐺 ( 𝐷 − 𝐵 ) ) · ( 𝐴 − 𝐷 ) ) )
99 91 96 98 3eqtrd ⊢ ( ( 𝜑 ∧ ¬ 𝐵 = 𝐷 ) → ( ( ( 𝐶 − 𝐴 ) 𝐺 ( 𝐷 − 𝐴 ) ) · ( 𝐵 − 𝐷 ) ) = ( ( ( 𝐶 − 𝐵 ) 𝐺 ( 𝐷 − 𝐵 ) ) · ( 𝐴 − 𝐷 ) ) )
100 42 99 pm2.61dan ⊢ ( 𝜑 → ( ( ( 𝐶 − 𝐴 ) 𝐺 ( 𝐷 − 𝐴 ) ) · ( 𝐵 − 𝐷 ) ) = ( ( ( 𝐶 − 𝐵 ) 𝐺 ( 𝐷 − 𝐵 ) ) · ( 𝐴 − 𝐷 ) ) )