cevathlem2

Description: Ceva's theorem second lemma. Relate (doubled) areas of triangles C A O and A B O with of segments B D and D C . (Contributed by Saveliy Skresanov, 24-Sep-2017)

	Ref	Expression
Hypotheses	cevath.sigar	$⊢ G = (x \in ℂ, y \in ℂ ⟼ ℑ (\overline{x} y))$
	cevath.a	$⊢ φ \to (A \in ℂ \land B \in ℂ \land C \in ℂ)$
	cevath.b	$⊢ φ \to (F \in ℂ \land D \in ℂ \land E \in ℂ)$
	cevath.c	$⊢ φ \to O \in ℂ$
	cevath.d	$⊢ φ \to ((A - O) G (D - O) = 0 \land (B - O) G (E - O) = 0 \land (C - O) G (F - O) = 0)$
	cevath.e	$⊢ φ \to ((A - F) G (B - F) = 0 \land (B - D) G (C - D) = 0 \land (C - E) G (A - E) = 0)$
	cevath.f	$⊢ φ \to ((A - O) G (B - O) \neq 0 \land (B - O) G (C - O) \neq 0 \land (C - O) G (A - O) \neq 0)$
Assertion	cevathlem2	$⊢ φ \to ((C - O) G (A - O)) (B - D) = ((A - O) G (B - O)) (D - C)$

Proof

Step	Hyp	Ref	Expression
1		cevath.sigar	$⊢ G = (x \in ℂ, y \in ℂ ⟼ ℑ (\overline{x} y))$
2		cevath.a	$⊢ φ \to (A \in ℂ \land B \in ℂ \land C \in ℂ)$
3		cevath.b	$⊢ φ \to (F \in ℂ \land D \in ℂ \land E \in ℂ)$
4		cevath.c	$⊢ φ \to O \in ℂ$
5		cevath.d	$⊢ φ \to ((A - O) G (D - O) = 0 \land (B - O) G (E - O) = 0 \land (C - O) G (F - O) = 0)$
6		cevath.e	$⊢ φ \to ((A - F) G (B - F) = 0 \land (B - D) G (C - D) = 0 \land (C - E) G (A - E) = 0)$
7		cevath.f	$⊢ φ \to ((A - O) G (B - O) \neq 0 \land (B - O) G (C - O) \neq 0 \land (C - O) G (A - O) \neq 0)$
8	3	simp2d	$⊢ φ \to D \in ℂ$
9	2	simp1d	$⊢ φ \to A \in ℂ$
10	2	simp2d	$⊢ φ \to B \in ℂ$
11	8 9 10	3jca	$⊢ φ \to (D \in ℂ \land A \in ℂ \land B \in ℂ)$
12	9 4	subcld	$⊢ φ \to A - O \in ℂ$
13	8 4	subcld	$⊢ φ \to D - O \in ℂ$
14	12 13	jca	$⊢ φ \to (A - O \in ℂ \land D - O \in ℂ)$
15	5	simp1d	$⊢ φ \to (A - O) G (D - O) = 0$
16	1 14 15	sigariz	$⊢ φ \to (D - O) G (A - O) = 0$
17	4 16	jca	$⊢ φ \to (O \in ℂ \land (D - O) G (A - O) = 0)$
18	1 11 17	sigaradd	$⊢ φ \to ((A - B) G (D - B)) - ((O - B) G (D - B)) = (A - B) G (O - B)$
19	1	sigarperm	$⊢ (B \in ℂ \land A \in ℂ \land O \in ℂ) \to (B - O) G (A - O) = (A - B) G (O - B)$
20	10 9 4 19	syl3anc	$⊢ φ \to (B - O) G (A - O) = (A - B) G (O - B)$
21	18 20	eqtr4d	$⊢ φ \to ((A - B) G (D - B)) - ((O - B) G (D - B)) = (B - O) G (A - O)$
22	21	oveq1d	$⊢ φ \to (((A - B) G (D - B)) - ((O - B) G (D - B))) (C - D) = ((B - O) G (A - O)) (C - D)$
23	9 10	subcld	$⊢ φ \to A - B \in ℂ$
24	8 10	subcld	$⊢ φ \to D - B \in ℂ$
25	23 24	jca	$⊢ φ \to (A - B \in ℂ \land D - B \in ℂ)$
26	1 25	sigarimcd	$⊢ φ \to (A - B) G (D - B) \in ℂ$
27	4 10	subcld	$⊢ φ \to O - B \in ℂ$
28	27 24	jca	$⊢ φ \to (O - B \in ℂ \land D - B \in ℂ)$
29	1 28	sigarimcd	$⊢ φ \to (O - B) G (D - B) \in ℂ$
30	2	simp3d	$⊢ φ \to C \in ℂ$
31	30 8	subcld	$⊢ φ \to C - D \in ℂ$
32	26 29 31	subdird	$⊢ φ \to (((A - B) G (D - B)) - ((O - B) G (D - B))) (C - D) = ((A - B) G (D - B)) (C - D) - ((O - B) G (D - B)) (C - D)$
33	22 32	eqtr3d	$⊢ φ \to ((B - O) G (A - O)) (C - D) = ((A - B) G (D - B)) (C - D) - ((O - B) G (D - B)) (C - D)$
34	10 30 9	3jca	$⊢ φ \to (B \in ℂ \land C \in ℂ \land A \in ℂ)$
35	6	simp2d	$⊢ φ \to (B - D) G (C - D) = 0$
36	8 35	jca	$⊢ φ \to (D \in ℂ \land (B - D) G (C - D) = 0)$
37	1 34 36	sharhght	$⊢ φ \to ((A - B) G (D - B)) (C - D) = ((A - C) G (D - C)) (B - D)$
38	10 30 4	3jca	$⊢ φ \to (B \in ℂ \land C \in ℂ \land O \in ℂ)$
39	1 38 36	sharhght	$⊢ φ \to ((O - B) G (D - B)) (C - D) = ((O - C) G (D - C)) (B - D)$
40	37 39	oveq12d	$⊢ φ \to ((A - B) G (D - B)) (C - D) - ((O - B) G (D - B)) (C - D) = ((A - C) G (D - C)) (B - D) - ((O - C) G (D - C)) (B - D)$
41	9 30	subcld	$⊢ φ \to A - C \in ℂ$
42	8 30	subcld	$⊢ φ \to D - C \in ℂ$
43	1	sigarim	$⊢ (A - C \in ℂ \land D - C \in ℂ) \to (A - C) G (D - C) \in ℝ$
44	41 42 43	syl2anc	$⊢ φ \to (A - C) G (D - C) \in ℝ$
45	44	recnd	$⊢ φ \to (A - C) G (D - C) \in ℂ$
46	4 30	subcld	$⊢ φ \to O - C \in ℂ$
47	46 42	jca	$⊢ φ \to (O - C \in ℂ \land D - C \in ℂ)$
48	1 47	sigarimcd	$⊢ φ \to (O - C) G (D - C) \in ℂ$
49	10 8	subcld	$⊢ φ \to B - D \in ℂ$
50	45 48 49	subdird	$⊢ φ \to (((A - C) G (D - C)) - ((O - C) G (D - C))) (B - D) = ((A - C) G (D - C)) (B - D) - ((O - C) G (D - C)) (B - D)$
51	8 9 30	3jca	$⊢ φ \to (D \in ℂ \land A \in ℂ \land C \in ℂ)$
52	1 51 17	sigaradd	$⊢ φ \to ((A - C) G (D - C)) - ((O - C) G (D - C)) = (A - C) G (O - C)$
53	1	sigarperm	$⊢ (C \in ℂ \land A \in ℂ \land O \in ℂ) \to (C - O) G (A - O) = (A - C) G (O - C)$
54	30 9 4 53	syl3anc	$⊢ φ \to (C - O) G (A - O) = (A - C) G (O - C)$
55	52 54	eqtr4d	$⊢ φ \to ((A - C) G (D - C)) - ((O - C) G (D - C)) = (C - O) G (A - O)$
56	55	oveq1d	$⊢ φ \to (((A - C) G (D - C)) - ((O - C) G (D - C))) (B - D) = ((C - O) G (A - O)) (B - D)$
57	50 56	eqtr3d	$⊢ φ \to ((A - C) G (D - C)) (B - D) - ((O - C) G (D - C)) (B - D) = ((C - O) G (A - O)) (B - D)$
58	33 40 57	3eqtrrd	$⊢ φ \to ((C - O) G (A - O)) (B - D) = ((B - O) G (A - O)) (C - D)$
59	10 4	subcld	$⊢ φ \to B - O \in ℂ$
60	1	sigarac	$⊢ (B - O \in ℂ \land A - O \in ℂ) \to (B - O) G (A - O) = - ((A - O) G (B - O))$
61	59 12 60	syl2anc	$⊢ φ \to (B - O) G (A - O) = - ((A - O) G (B - O))$
62	61	oveq1d	$⊢ φ \to ((B - O) G (A - O)) (C - D) = (- ((A - O) G (B - O))) (C - D)$
63	12 59	jca	$⊢ φ \to (A - O \in ℂ \land B - O \in ℂ)$
64	1 63	sigarimcd	$⊢ φ \to (A - O) G (B - O) \in ℂ$
65		mulneg12	$⊢ ((A - O) G (B - O) \in ℂ \land C - D \in ℂ) \to (- ((A - O) G (B - O))) (C - D) = ((A - O) G (B - O)) (- (C - D))$
66	64 31 65	syl2anc	$⊢ φ \to (- ((A - O) G (B - O))) (C - D) = ((A - O) G (B - O)) (- (C - D))$
67	30 8	negsubdi2d	$⊢ φ \to - (C - D) = D - C$
68	67	oveq2d	$⊢ φ \to ((A - O) G (B - O)) (- (C - D)) = ((A - O) G (B - O)) (D - C)$
69	66 68	eqtrd	$⊢ φ \to (- ((A - O) G (B - O))) (C - D) = ((A - O) G (B - O)) (D - C)$
70	58 62 69	3eqtrd	$⊢ φ \to ((C - O) G (A - O)) (B - D) = ((A - O) G (B - O)) (D - C)$

Metamath Proof Explorer

Theorem cevathlem2

Proof