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	$⊢ φ \to (A \in ℂ \land B \in ℂ \land C \in ℂ)$
	cevathlem1.b	$⊢ φ \to (D \in ℂ \land E \in ℂ \land F \in ℂ)$
	cevathlem1.c	$⊢ φ \to (G \in ℂ \land H \in ℂ \land K \in ℂ)$
	cevathlem1.d	$⊢ φ \to (A \neq 0 \land E \neq 0 \land C \neq 0)$
	cevathlem1.e	$⊢ φ \to (A B = C D \land E F = A G \land C H = E K)$
Assertion	cevathlem1	$⊢ φ \to B F H = D G K$

Proof

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

Metamath Proof Explorer

Theorem cevathlem1

Proof