Metamath Proof Explorer

Theorem cevathlem1

Description: Ceva's theorem first lemma. Multiplies three identities and divides by the common factors. (Contributed by Saveliy Skresanov, 24-Sep-2017)

Ref Expression
Hypotheses cevathlem1.a 
|- ( ph -> ( A e. CC /\ B e. CC /\ C e. CC ) )
cevathlem1.b 
|- ( ph -> ( D e. CC /\ E e. CC /\ F e. CC ) )
cevathlem1.c 
|- ( ph -> ( G e. CC /\ H e. CC /\ K e. CC ) )
cevathlem1.d 
|- ( ph -> ( A =/= 0 /\ E =/= 0 /\ C =/= 0 ) )
cevathlem1.e 
|- ( ph -> ( ( A x. B ) = ( C x. D ) /\ ( E x. F ) = ( A x. G ) /\ ( C x. H ) = ( E x. K ) ) )
Assertion cevathlem1 
|- ( ph -> ( ( B x. F ) x. H ) = ( ( D x. G ) x. K ) )

Proof

Step Hyp Ref Expression
1 cevathlem1.a 
 |-  ( ph -> ( A e. CC /\ B e. CC /\ C e. CC ) )
2 cevathlem1.b 
 |-  ( ph -> ( D e. CC /\ E e. CC /\ F e. CC ) )
3 cevathlem1.c 
 |-  ( ph -> ( G e. CC /\ H e. CC /\ K e. CC ) )
4 cevathlem1.d 
 |-  ( ph -> ( A =/= 0 /\ E =/= 0 /\ C =/= 0 ) )
5 cevathlem1.e 
 |-  ( ph -> ( ( A x. B ) = ( C x. D ) /\ ( E x. F ) = ( A x. G ) /\ ( C x. H ) = ( E x. K ) ) )
6 1 simp2d 
 |-  ( ph -> B e. CC )
7 2 simp3d 
 |-  ( ph -> F e. CC )
8 6 7 mulcld 
 |-  ( ph -> ( B x. F ) e. CC )
9 3 simp2d 
 |-  ( ph -> H e. CC )
10 8 9 mulcld 
 |-  ( ph -> ( ( B x. F ) x. H ) e. CC )
11 2 simp1d 
 |-  ( ph -> D e. CC )
12 3 simp1d 
 |-  ( ph -> G e. CC )
13 11 12 mulcld 
 |-  ( ph -> ( D x. G ) e. CC )
14 3 simp3d 
 |-  ( ph -> K e. CC )
15 13 14 mulcld 
 |-  ( ph -> ( ( D x. G ) x. K ) e. CC )
16 1 simp1d 
 |-  ( ph -> A e. CC )
17 2 simp2d 
 |-  ( ph -> E e. CC )
18 16 17 mulcld 
 |-  ( ph -> ( A x. E ) e. CC )
19 1 simp3d 
 |-  ( ph -> C e. CC )
20 18 19 mulcld 
 |-  ( ph -> ( ( A x. E ) x. C ) e. CC )
21 4 simp1d 
 |-  ( ph -> A =/= 0 )
22 4 simp2d 
 |-  ( ph -> E =/= 0 )
23 16 17 21 22 mulne0d 
 |-  ( ph -> ( A x. E ) =/= 0 )
24 4 simp3d 
 |-  ( ph -> C =/= 0 )
25 18 19 23 24 mulne0d 
 |-  ( ph -> ( ( A x. E ) x. C ) =/= 0 )
26 5 simp1d 
 |-  ( ph -> ( A x. B ) = ( C x. D ) )
27 5 simp2d 
 |-  ( ph -> ( E x. F ) = ( A x. G ) )
28 26 27 oveq12d 
 |-  ( ph -> ( ( A x. B ) x. ( E x. F ) ) = ( ( C x. D ) x. ( A x. G ) ) )
29 16 6 17 7 mul4d 
 |-  ( ph -> ( ( A x. B ) x. ( E x. F ) ) = ( ( A x. E ) x. ( B x. F ) ) )
30 19 11 16 12 mul4d 
 |-  ( ph -> ( ( C x. D ) x. ( A x. G ) ) = ( ( C x. A ) x. ( D x. G ) ) )
31 28 29 30 3eqtr3d 
 |-  ( ph -> ( ( A x. E ) x. ( B x. F ) ) = ( ( C x. A ) x. ( D x. G ) ) )
32 5 simp3d 
 |-  ( ph -> ( C x. H ) = ( E x. K ) )
33 31 32 oveq12d 
 |-  ( ph -> ( ( ( A x. E ) x. ( B x. F ) ) x. ( C x. H ) ) = ( ( ( C x. A ) x. ( D x. G ) ) x. ( E x. K ) ) )
34 18 8 19 9 mul4d 
 |-  ( ph -> ( ( ( A x. E ) x. ( B x. F ) ) x. ( C x. H ) ) = ( ( ( A x. E ) x. C ) x. ( ( B x. F ) x. H ) ) )
35 19 16 mulcld 
 |-  ( ph -> ( C x. A ) e. CC )
36 35 13 17 14 mul4d 
 |-  ( ph -> ( ( ( C x. A ) x. ( D x. G ) ) x. ( E x. K ) ) = ( ( ( C x. A ) x. E ) x. ( ( D x. G ) x. K ) ) )
37 33 34 36 3eqtr3d 
 |-  ( ph -> ( ( ( A x. E ) x. C ) x. ( ( B x. F ) x. H ) ) = ( ( ( C x. A ) x. E ) x. ( ( D x. G ) x. K ) ) )
38 16 17 19 mul32d 
 |-  ( ph -> ( ( A x. E ) x. C ) = ( ( A x. C ) x. E ) )
39 16 19 mulcomd 
 |-  ( ph -> ( A x. C ) = ( C x. A ) )
40 39 oveq1d 
 |-  ( ph -> ( ( A x. C ) x. E ) = ( ( C x. A ) x. E ) )
41 38 40 eqtrd 
 |-  ( ph -> ( ( A x. E ) x. C ) = ( ( C x. A ) x. E ) )
42 41 oveq1d 
 |-  ( ph -> ( ( ( A x. E ) x. C ) x. ( ( D x. G ) x. K ) ) = ( ( ( C x. A ) x. E ) x. ( ( D x. G ) x. K ) ) )
43 37 42 eqtr4d 
 |-  ( ph -> ( ( ( A x. E ) x. C ) x. ( ( B x. F ) x. H ) ) = ( ( ( A x. E ) x. C ) x. ( ( D x. G ) x. K ) ) )
44 10 15 20 25 43 mulcanad 
 |-  ( ph -> ( ( B x. F ) x. H ) = ( ( D x. G ) x. K ) )