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 ⊢G=x∈ℂ,y∈ℂ⟼ℑ⁡x‾⁢y
sharhght.a ⊢φ→A∈ℂ∧B∈ℂ∧C∈ℂ
sharhght.b ⊢φ→D∈ℂ∧A−DGB−D=0
Assertion sharhght ⊢φ→C−AGD−A⁢B−D=C−BGD−B⁢A−D

Proof

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