Theorem 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	⊢ 𝐺 = ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( ℑ ‘ ( ( ∗ ‘ 𝑥 ) · 𝑦 ) ) )
	cevath.a	⊢ ( 𝜑 → ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) )
	cevath.b	⊢ ( 𝜑 → ( 𝐹 ∈ ℂ ∧ 𝐷 ∈ ℂ ∧ 𝐸 ∈ ℂ ) )
	cevath.c	⊢ ( 𝜑 → 𝑂 ∈ ℂ )
	cevath.d	⊢ ( 𝜑 → ( ( ( 𝐴 − 𝑂 ) 𝐺 ( 𝐷 − 𝑂 ) ) = 0 ∧ ( ( 𝐵 − 𝑂 ) 𝐺 ( 𝐸 − 𝑂 ) ) = 0 ∧ ( ( 𝐶 − 𝑂 ) 𝐺 ( 𝐹 − 𝑂 ) ) = 0 ) )
	cevath.e	⊢ ( 𝜑 → ( ( ( 𝐴 − 𝐹 ) 𝐺 ( 𝐵 − 𝐹 ) ) = 0 ∧ ( ( 𝐵 − 𝐷 ) 𝐺 ( 𝐶 − 𝐷 ) ) = 0 ∧ ( ( 𝐶 − 𝐸 ) 𝐺 ( 𝐴 − 𝐸 ) ) = 0 ) )
	cevath.f	⊢ ( 𝜑 → ( ( ( 𝐴 − 𝑂 ) 𝐺 ( 𝐵 − 𝑂 ) ) ≠ 0 ∧ ( ( 𝐵 − 𝑂 ) 𝐺 ( 𝐶 − 𝑂 ) ) ≠ 0 ∧ ( ( 𝐶 − 𝑂 ) 𝐺 ( 𝐴 − 𝑂 ) ) ≠ 0 ) )
Assertion	cevathlem2	⊢ ( 𝜑 → ( ( ( 𝐶 − 𝑂 ) 𝐺 ( 𝐴 − 𝑂 ) ) · ( 𝐵 − 𝐷 ) ) = ( ( ( 𝐴 − 𝑂 ) 𝐺 ( 𝐵 − 𝑂 ) ) · ( 𝐷 − 𝐶 ) ) )

Proof

Step	Hyp	Ref	Expression
1		cevath.sigar	⊢ 𝐺 = ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( ℑ ‘ ( ( ∗ ‘ 𝑥 ) · 𝑦 ) ) )
2		cevath.a	⊢ ( 𝜑 → ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) )
3		cevath.b	⊢ ( 𝜑 → ( 𝐹 ∈ ℂ ∧ 𝐷 ∈ ℂ ∧ 𝐸 ∈ ℂ ) )
4		cevath.c	⊢ ( 𝜑 → 𝑂 ∈ ℂ )
5		cevath.d	⊢ ( 𝜑 → ( ( ( 𝐴 − 𝑂 ) 𝐺 ( 𝐷 − 𝑂 ) ) = 0 ∧ ( ( 𝐵 − 𝑂 ) 𝐺 ( 𝐸 − 𝑂 ) ) = 0 ∧ ( ( 𝐶 − 𝑂 ) 𝐺 ( 𝐹 − 𝑂 ) ) = 0 ) )
6		cevath.e	⊢ ( 𝜑 → ( ( ( 𝐴 − 𝐹 ) 𝐺 ( 𝐵 − 𝐹 ) ) = 0 ∧ ( ( 𝐵 − 𝐷 ) 𝐺 ( 𝐶 − 𝐷 ) ) = 0 ∧ ( ( 𝐶 − 𝐸 ) 𝐺 ( 𝐴 − 𝐸 ) ) = 0 ) )
7		cevath.f	⊢ ( 𝜑 → ( ( ( 𝐴 − 𝑂 ) 𝐺 ( 𝐵 − 𝑂 ) ) ≠ 0 ∧ ( ( 𝐵 − 𝑂 ) 𝐺 ( 𝐶 − 𝑂 ) ) ≠ 0 ∧ ( ( 𝐶 − 𝑂 ) 𝐺 ( 𝐴 − 𝑂 ) ) ≠ 0 ) )
8	3	simp2d	⊢ ( 𝜑 → 𝐷 ∈ ℂ )
9	2	simp1d	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
10	2	simp2d	⊢ ( 𝜑 → 𝐵 ∈ ℂ )
11	8 9 10	3jca	⊢ ( 𝜑 → ( 𝐷 ∈ ℂ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) )
12	9 4	subcld	⊢ ( 𝜑 → ( 𝐴 − 𝑂 ) ∈ ℂ )
13	8 4	subcld	⊢ ( 𝜑 → ( 𝐷 − 𝑂 ) ∈ ℂ )
14	12 13	jca	⊢ ( 𝜑 → ( ( 𝐴 − 𝑂 ) ∈ ℂ ∧ ( 𝐷 − 𝑂 ) ∈ ℂ ) )
15	5	simp1d	⊢ ( 𝜑 → ( ( 𝐴 − 𝑂 ) 𝐺 ( 𝐷 − 𝑂 ) ) = 0 )
16	1 14 15	sigariz	⊢ ( 𝜑 → ( ( 𝐷 − 𝑂 ) 𝐺 ( 𝐴 − 𝑂 ) ) = 0 )
17	4 16	jca	⊢ ( 𝜑 → ( 𝑂 ∈ ℂ ∧ ( ( 𝐷 − 𝑂 ) 𝐺 ( 𝐴 − 𝑂 ) ) = 0 ) )
18	1 11 17	sigaradd	⊢ ( 𝜑 → ( ( ( 𝐴 − 𝐵 ) 𝐺 ( 𝐷 − 𝐵 ) ) − ( ( 𝑂 − 𝐵 ) 𝐺 ( 𝐷 − 𝐵 ) ) ) = ( ( 𝐴 − 𝐵 ) 𝐺 ( 𝑂 − 𝐵 ) ) )
19	1	sigarperm	⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐴 ∈ ℂ ∧ 𝑂 ∈ ℂ ) → ( ( 𝐵 − 𝑂 ) 𝐺 ( 𝐴 − 𝑂 ) ) = ( ( 𝐴 − 𝐵 ) 𝐺 ( 𝑂 − 𝐵 ) ) )
20	10 9 4 19	syl3anc	⊢ ( 𝜑 → ( ( 𝐵 − 𝑂 ) 𝐺 ( 𝐴 − 𝑂 ) ) = ( ( 𝐴 − 𝐵 ) 𝐺 ( 𝑂 − 𝐵 ) ) )
21	18 20	eqtr4d	⊢ ( 𝜑 → ( ( ( 𝐴 − 𝐵 ) 𝐺 ( 𝐷 − 𝐵 ) ) − ( ( 𝑂 − 𝐵 ) 𝐺 ( 𝐷 − 𝐵 ) ) ) = ( ( 𝐵 − 𝑂 ) 𝐺 ( 𝐴 − 𝑂 ) ) )
22	21	oveq1d	⊢ ( 𝜑 → ( ( ( ( 𝐴 − 𝐵 ) 𝐺 ( 𝐷 − 𝐵 ) ) − ( ( 𝑂 − 𝐵 ) 𝐺 ( 𝐷 − 𝐵 ) ) ) · ( 𝐶 − 𝐷 ) ) = ( ( ( 𝐵 − 𝑂 ) 𝐺 ( 𝐴 − 𝑂 ) ) · ( 𝐶 − 𝐷 ) ) )
23	9 10	subcld	⊢ ( 𝜑 → ( 𝐴 − 𝐵 ) ∈ ℂ )
24	8 10	subcld	⊢ ( 𝜑 → ( 𝐷 − 𝐵 ) ∈ ℂ )
25	23 24	jca	⊢ ( 𝜑 → ( ( 𝐴 − 𝐵 ) ∈ ℂ ∧ ( 𝐷 − 𝐵 ) ∈ ℂ ) )
26	1 25	sigarimcd	⊢ ( 𝜑 → ( ( 𝐴 − 𝐵 ) 𝐺 ( 𝐷 − 𝐵 ) ) ∈ ℂ )
27	4 10	subcld	⊢ ( 𝜑 → ( 𝑂 − 𝐵 ) ∈ ℂ )
28	27 24	jca	⊢ ( 𝜑 → ( ( 𝑂 − 𝐵 ) ∈ ℂ ∧ ( 𝐷 − 𝐵 ) ∈ ℂ ) )
29	1 28	sigarimcd	⊢ ( 𝜑 → ( ( 𝑂 − 𝐵 ) 𝐺 ( 𝐷 − 𝐵 ) ) ∈ ℂ )
30	2	simp3d	⊢ ( 𝜑 → 𝐶 ∈ ℂ )
31	30 8	subcld	⊢ ( 𝜑 → ( 𝐶 − 𝐷 ) ∈ ℂ )
32	26 29 31	subdird	⊢ ( 𝜑 → ( ( ( ( 𝐴 − 𝐵 ) 𝐺 ( 𝐷 − 𝐵 ) ) − ( ( 𝑂 − 𝐵 ) 𝐺 ( 𝐷 − 𝐵 ) ) ) · ( 𝐶 − 𝐷 ) ) = ( ( ( ( 𝐴 − 𝐵 ) 𝐺 ( 𝐷 − 𝐵 ) ) · ( 𝐶 − 𝐷 ) ) − ( ( ( 𝑂 − 𝐵 ) 𝐺 ( 𝐷 − 𝐵 ) ) · ( 𝐶 − 𝐷 ) ) ) )
33	22 32	eqtr3d	⊢ ( 𝜑 → ( ( ( 𝐵 − 𝑂 ) 𝐺 ( 𝐴 − 𝑂 ) ) · ( 𝐶 − 𝐷 ) ) = ( ( ( ( 𝐴 − 𝐵 ) 𝐺 ( 𝐷 − 𝐵 ) ) · ( 𝐶 − 𝐷 ) ) − ( ( ( 𝑂 − 𝐵 ) 𝐺 ( 𝐷 − 𝐵 ) ) · ( 𝐶 − 𝐷 ) ) ) )
34	10 30 9	3jca	⊢ ( 𝜑 → ( 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ∧ 𝐴 ∈ ℂ ) )
35	6	simp2d	⊢ ( 𝜑 → ( ( 𝐵 − 𝐷 ) 𝐺 ( 𝐶 − 𝐷 ) ) = 0 )
36	8 35	jca	⊢ ( 𝜑 → ( 𝐷 ∈ ℂ ∧ ( ( 𝐵 − 𝐷 ) 𝐺 ( 𝐶 − 𝐷 ) ) = 0 ) )
37	1 34 36	sharhght	⊢ ( 𝜑 → ( ( ( 𝐴 − 𝐵 ) 𝐺 ( 𝐷 − 𝐵 ) ) · ( 𝐶 − 𝐷 ) ) = ( ( ( 𝐴 − 𝐶 ) 𝐺 ( 𝐷 − 𝐶 ) ) · ( 𝐵 − 𝐷 ) ) )
38	10 30 4	3jca	⊢ ( 𝜑 → ( 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ∧ 𝑂 ∈ ℂ ) )
39	1 38 36	sharhght	⊢ ( 𝜑 → ( ( ( 𝑂 − 𝐵 ) 𝐺 ( 𝐷 − 𝐵 ) ) · ( 𝐶 − 𝐷 ) ) = ( ( ( 𝑂 − 𝐶 ) 𝐺 ( 𝐷 − 𝐶 ) ) · ( 𝐵 − 𝐷 ) ) )
40	37 39	oveq12d	⊢ ( 𝜑 → ( ( ( ( 𝐴 − 𝐵 ) 𝐺 ( 𝐷 − 𝐵 ) ) · ( 𝐶 − 𝐷 ) ) − ( ( ( 𝑂 − 𝐵 ) 𝐺 ( 𝐷 − 𝐵 ) ) · ( 𝐶 − 𝐷 ) ) ) = ( ( ( ( 𝐴 − 𝐶 ) 𝐺 ( 𝐷 − 𝐶 ) ) · ( 𝐵 − 𝐷 ) ) − ( ( ( 𝑂 − 𝐶 ) 𝐺 ( 𝐷 − 𝐶 ) ) · ( 𝐵 − 𝐷 ) ) ) )
41	9 30	subcld	⊢ ( 𝜑 → ( 𝐴 − 𝐶 ) ∈ ℂ )
42	8 30	subcld	⊢ ( 𝜑 → ( 𝐷 − 𝐶 ) ∈ ℂ )
43	1	sigarim	⊢ ( ( ( 𝐴 − 𝐶 ) ∈ ℂ ∧ ( 𝐷 − 𝐶 ) ∈ ℂ ) → ( ( 𝐴 − 𝐶 ) 𝐺 ( 𝐷 − 𝐶 ) ) ∈ ℝ )
44	41 42 43	syl2anc	⊢ ( 𝜑 → ( ( 𝐴 − 𝐶 ) 𝐺 ( 𝐷 − 𝐶 ) ) ∈ ℝ )
45	44	recnd	⊢ ( 𝜑 → ( ( 𝐴 − 𝐶 ) 𝐺 ( 𝐷 − 𝐶 ) ) ∈ ℂ )
46	4 30	subcld	⊢ ( 𝜑 → ( 𝑂 − 𝐶 ) ∈ ℂ )
47	46 42	jca	⊢ ( 𝜑 → ( ( 𝑂 − 𝐶 ) ∈ ℂ ∧ ( 𝐷 − 𝐶 ) ∈ ℂ ) )
48	1 47	sigarimcd	⊢ ( 𝜑 → ( ( 𝑂 − 𝐶 ) 𝐺 ( 𝐷 − 𝐶 ) ) ∈ ℂ )
49	10 8	subcld	⊢ ( 𝜑 → ( 𝐵 − 𝐷 ) ∈ ℂ )
50	45 48 49	subdird	⊢ ( 𝜑 → ( ( ( ( 𝐴 − 𝐶 ) 𝐺 ( 𝐷 − 𝐶 ) ) − ( ( 𝑂 − 𝐶 ) 𝐺 ( 𝐷 − 𝐶 ) ) ) · ( 𝐵 − 𝐷 ) ) = ( ( ( ( 𝐴 − 𝐶 ) 𝐺 ( 𝐷 − 𝐶 ) ) · ( 𝐵 − 𝐷 ) ) − ( ( ( 𝑂 − 𝐶 ) 𝐺 ( 𝐷 − 𝐶 ) ) · ( 𝐵 − 𝐷 ) ) ) )
51	8 9 30	3jca	⊢ ( 𝜑 → ( 𝐷 ∈ ℂ ∧ 𝐴 ∈ ℂ ∧ 𝐶 ∈ ℂ ) )
52	1 51 17	sigaradd	⊢ ( 𝜑 → ( ( ( 𝐴 − 𝐶 ) 𝐺 ( 𝐷 − 𝐶 ) ) − ( ( 𝑂 − 𝐶 ) 𝐺 ( 𝐷 − 𝐶 ) ) ) = ( ( 𝐴 − 𝐶 ) 𝐺 ( 𝑂 − 𝐶 ) ) )
53	1	sigarperm	⊢ ( ( 𝐶 ∈ ℂ ∧ 𝐴 ∈ ℂ ∧ 𝑂 ∈ ℂ ) → ( ( 𝐶 − 𝑂 ) 𝐺 ( 𝐴 − 𝑂 ) ) = ( ( 𝐴 − 𝐶 ) 𝐺 ( 𝑂 − 𝐶 ) ) )
54	30 9 4 53	syl3anc	⊢ ( 𝜑 → ( ( 𝐶 − 𝑂 ) 𝐺 ( 𝐴 − 𝑂 ) ) = ( ( 𝐴 − 𝐶 ) 𝐺 ( 𝑂 − 𝐶 ) ) )
55	52 54	eqtr4d	⊢ ( 𝜑 → ( ( ( 𝐴 − 𝐶 ) 𝐺 ( 𝐷 − 𝐶 ) ) − ( ( 𝑂 − 𝐶 ) 𝐺 ( 𝐷 − 𝐶 ) ) ) = ( ( 𝐶 − 𝑂 ) 𝐺 ( 𝐴 − 𝑂 ) ) )
56	55	oveq1d	⊢ ( 𝜑 → ( ( ( ( 𝐴 − 𝐶 ) 𝐺 ( 𝐷 − 𝐶 ) ) − ( ( 𝑂 − 𝐶 ) 𝐺 ( 𝐷 − 𝐶 ) ) ) · ( 𝐵 − 𝐷 ) ) = ( ( ( 𝐶 − 𝑂 ) 𝐺 ( 𝐴 − 𝑂 ) ) · ( 𝐵 − 𝐷 ) ) )
57	50 56	eqtr3d	⊢ ( 𝜑 → ( ( ( ( 𝐴 − 𝐶 ) 𝐺 ( 𝐷 − 𝐶 ) ) · ( 𝐵 − 𝐷 ) ) − ( ( ( 𝑂 − 𝐶 ) 𝐺 ( 𝐷 − 𝐶 ) ) · ( 𝐵 − 𝐷 ) ) ) = ( ( ( 𝐶 − 𝑂 ) 𝐺 ( 𝐴 − 𝑂 ) ) · ( 𝐵 − 𝐷 ) ) )
58	33 40 57	3eqtrrd	⊢ ( 𝜑 → ( ( ( 𝐶 − 𝑂 ) 𝐺 ( 𝐴 − 𝑂 ) ) · ( 𝐵 − 𝐷 ) ) = ( ( ( 𝐵 − 𝑂 ) 𝐺 ( 𝐴 − 𝑂 ) ) · ( 𝐶 − 𝐷 ) ) )
59	10 4	subcld	⊢ ( 𝜑 → ( 𝐵 − 𝑂 ) ∈ ℂ )
60	1	sigarac	⊢ ( ( ( 𝐵 − 𝑂 ) ∈ ℂ ∧ ( 𝐴 − 𝑂 ) ∈ ℂ ) → ( ( 𝐵 − 𝑂 ) 𝐺 ( 𝐴 − 𝑂 ) ) = - ( ( 𝐴 − 𝑂 ) 𝐺 ( 𝐵 − 𝑂 ) ) )
61	59 12 60	syl2anc	⊢ ( 𝜑 → ( ( 𝐵 − 𝑂 ) 𝐺 ( 𝐴 − 𝑂 ) ) = - ( ( 𝐴 − 𝑂 ) 𝐺 ( 𝐵 − 𝑂 ) ) )
62	61	oveq1d	⊢ ( 𝜑 → ( ( ( 𝐵 − 𝑂 ) 𝐺 ( 𝐴 − 𝑂 ) ) · ( 𝐶 − 𝐷 ) ) = ( - ( ( 𝐴 − 𝑂 ) 𝐺 ( 𝐵 − 𝑂 ) ) · ( 𝐶 − 𝐷 ) ) )
63	12 59	jca	⊢ ( 𝜑 → ( ( 𝐴 − 𝑂 ) ∈ ℂ ∧ ( 𝐵 − 𝑂 ) ∈ ℂ ) )
64	1 63	sigarimcd	⊢ ( 𝜑 → ( ( 𝐴 − 𝑂 ) 𝐺 ( 𝐵 − 𝑂 ) ) ∈ ℂ )
65		mulneg12	⊢ ( ( ( ( 𝐴 − 𝑂 ) 𝐺 ( 𝐵 − 𝑂 ) ) ∈ ℂ ∧ ( 𝐶 − 𝐷 ) ∈ ℂ ) → ( - ( ( 𝐴 − 𝑂 ) 𝐺 ( 𝐵 − 𝑂 ) ) · ( 𝐶 − 𝐷 ) ) = ( ( ( 𝐴 − 𝑂 ) 𝐺 ( 𝐵 − 𝑂 ) ) · - ( 𝐶 − 𝐷 ) ) )
66	64 31 65	syl2anc	⊢ ( 𝜑 → ( - ( ( 𝐴 − 𝑂 ) 𝐺 ( 𝐵 − 𝑂 ) ) · ( 𝐶 − 𝐷 ) ) = ( ( ( 𝐴 − 𝑂 ) 𝐺 ( 𝐵 − 𝑂 ) ) · - ( 𝐶 − 𝐷 ) ) )
67	30 8	negsubdi2d	⊢ ( 𝜑 → - ( 𝐶 − 𝐷 ) = ( 𝐷 − 𝐶 ) )
68	67	oveq2d	⊢ ( 𝜑 → ( ( ( 𝐴 − 𝑂 ) 𝐺 ( 𝐵 − 𝑂 ) ) · - ( 𝐶 − 𝐷 ) ) = ( ( ( 𝐴 − 𝑂 ) 𝐺 ( 𝐵 − 𝑂 ) ) · ( 𝐷 − 𝐶 ) ) )
69	66 68	eqtrd	⊢ ( 𝜑 → ( - ( ( 𝐴 − 𝑂 ) 𝐺 ( 𝐵 − 𝑂 ) ) · ( 𝐶 − 𝐷 ) ) = ( ( ( 𝐴 − 𝑂 ) 𝐺 ( 𝐵 − 𝑂 ) ) · ( 𝐷 − 𝐶 ) ) )
70	58 62 69	3eqtrd	⊢ ( 𝜑 → ( ( ( 𝐶 − 𝑂 ) 𝐺 ( 𝐴 − 𝑂 ) ) · ( 𝐵 − 𝐷 ) ) = ( ( ( 𝐴 − 𝑂 ) 𝐺 ( 𝐵 − 𝑂 ) ) · ( 𝐷 − 𝐶 ) ) )