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 e. CC , y e. CC |-> ( Im ` ( ( * ` x ) x. y ) ) )
sharhght.a 
|- ( ph -> ( A e. CC /\ B e. CC /\ C e. CC ) )
sharhght.b 
|- ( ph -> ( D e. CC /\ ( ( A - D ) G ( B - D ) ) = 0 ) )
Assertion sharhght 
|- ( ph -> ( ( ( C - A ) G ( D - A ) ) x. ( B - D ) ) = ( ( ( C - B ) G ( D - B ) ) x. ( A - D ) ) )

Proof

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