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 φ A B C
cevathlem1.b φ D E F
cevathlem1.c φ G H K
cevathlem1.d φ A 0 E 0 C 0
cevathlem1.e φ A B = C D E F = A G C H = E K
Assertion cevathlem1 φ B F H = D G K

Proof

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