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	⊢ ( 𝜑 → ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) )
	cevathlem1.b	⊢ ( 𝜑 → ( 𝐷 ∈ ℂ ∧ 𝐸 ∈ ℂ ∧ 𝐹 ∈ ℂ ) )
	cevathlem1.c	⊢ ( 𝜑 → ( 𝐺 ∈ ℂ ∧ 𝐻 ∈ ℂ ∧ 𝐾 ∈ ℂ ) )
	cevathlem1.d	⊢ ( 𝜑 → ( 𝐴 ≠ 0 ∧ 𝐸 ≠ 0 ∧ 𝐶 ≠ 0 ) )
	cevathlem1.e	⊢ ( 𝜑 → ( ( 𝐴 · 𝐵 ) = ( 𝐶 · 𝐷 ) ∧ ( 𝐸 · 𝐹 ) = ( 𝐴 · 𝐺 ) ∧ ( 𝐶 · 𝐻 ) = ( 𝐸 · 𝐾 ) ) )
Assertion	cevathlem1	⊢ ( 𝜑 → ( ( 𝐵 · 𝐹 ) · 𝐻 ) = ( ( 𝐷 · 𝐺 ) · 𝐾 ) )

Proof

Step	Hyp	Ref	Expression
1		cevathlem1.a	⊢ ( 𝜑 → ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) )
2		cevathlem1.b	⊢ ( 𝜑 → ( 𝐷 ∈ ℂ ∧ 𝐸 ∈ ℂ ∧ 𝐹 ∈ ℂ ) )
3		cevathlem1.c	⊢ ( 𝜑 → ( 𝐺 ∈ ℂ ∧ 𝐻 ∈ ℂ ∧ 𝐾 ∈ ℂ ) )
4		cevathlem1.d	⊢ ( 𝜑 → ( 𝐴 ≠ 0 ∧ 𝐸 ≠ 0 ∧ 𝐶 ≠ 0 ) )
5		cevathlem1.e	⊢ ( 𝜑 → ( ( 𝐴 · 𝐵 ) = ( 𝐶 · 𝐷 ) ∧ ( 𝐸 · 𝐹 ) = ( 𝐴 · 𝐺 ) ∧ ( 𝐶 · 𝐻 ) = ( 𝐸 · 𝐾 ) ) )
6	1	simp2d	⊢ ( 𝜑 → 𝐵 ∈ ℂ )
7	2	simp3d	⊢ ( 𝜑 → 𝐹 ∈ ℂ )
8	6 7	mulcld	⊢ ( 𝜑 → ( 𝐵 · 𝐹 ) ∈ ℂ )
9	3	simp2d	⊢ ( 𝜑 → 𝐻 ∈ ℂ )
10	8 9	mulcld	⊢ ( 𝜑 → ( ( 𝐵 · 𝐹 ) · 𝐻 ) ∈ ℂ )
11	2	simp1d	⊢ ( 𝜑 → 𝐷 ∈ ℂ )
12	3	simp1d	⊢ ( 𝜑 → 𝐺 ∈ ℂ )
13	11 12	mulcld	⊢ ( 𝜑 → ( 𝐷 · 𝐺 ) ∈ ℂ )
14	3	simp3d	⊢ ( 𝜑 → 𝐾 ∈ ℂ )
15	13 14	mulcld	⊢ ( 𝜑 → ( ( 𝐷 · 𝐺 ) · 𝐾 ) ∈ ℂ )
16	1	simp1d	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
17	2	simp2d	⊢ ( 𝜑 → 𝐸 ∈ ℂ )
18	16 17	mulcld	⊢ ( 𝜑 → ( 𝐴 · 𝐸 ) ∈ ℂ )
19	1	simp3d	⊢ ( 𝜑 → 𝐶 ∈ ℂ )
20	18 19	mulcld	⊢ ( 𝜑 → ( ( 𝐴 · 𝐸 ) · 𝐶 ) ∈ ℂ )
21	4	simp1d	⊢ ( 𝜑 → 𝐴 ≠ 0 )
22	4	simp2d	⊢ ( 𝜑 → 𝐸 ≠ 0 )
23	16 17 21 22	mulne0d	⊢ ( 𝜑 → ( 𝐴 · 𝐸 ) ≠ 0 )
24	4	simp3d	⊢ ( 𝜑 → 𝐶 ≠ 0 )
25	18 19 23 24	mulne0d	⊢ ( 𝜑 → ( ( 𝐴 · 𝐸 ) · 𝐶 ) ≠ 0 )
26	5	simp1d	⊢ ( 𝜑 → ( 𝐴 · 𝐵 ) = ( 𝐶 · 𝐷 ) )
27	5	simp2d	⊢ ( 𝜑 → ( 𝐸 · 𝐹 ) = ( 𝐴 · 𝐺 ) )
28	26 27	oveq12d	⊢ ( 𝜑 → ( ( 𝐴 · 𝐵 ) · ( 𝐸 · 𝐹 ) ) = ( ( 𝐶 · 𝐷 ) · ( 𝐴 · 𝐺 ) ) )
29	16 6 17 7	mul4d	⊢ ( 𝜑 → ( ( 𝐴 · 𝐵 ) · ( 𝐸 · 𝐹 ) ) = ( ( 𝐴 · 𝐸 ) · ( 𝐵 · 𝐹 ) ) )
30	19 11 16 12	mul4d	⊢ ( 𝜑 → ( ( 𝐶 · 𝐷 ) · ( 𝐴 · 𝐺 ) ) = ( ( 𝐶 · 𝐴 ) · ( 𝐷 · 𝐺 ) ) )
31	28 29 30	3eqtr3d	⊢ ( 𝜑 → ( ( 𝐴 · 𝐸 ) · ( 𝐵 · 𝐹 ) ) = ( ( 𝐶 · 𝐴 ) · ( 𝐷 · 𝐺 ) ) )
32	5	simp3d	⊢ ( 𝜑 → ( 𝐶 · 𝐻 ) = ( 𝐸 · 𝐾 ) )
33	31 32	oveq12d	⊢ ( 𝜑 → ( ( ( 𝐴 · 𝐸 ) · ( 𝐵 · 𝐹 ) ) · ( 𝐶 · 𝐻 ) ) = ( ( ( 𝐶 · 𝐴 ) · ( 𝐷 · 𝐺 ) ) · ( 𝐸 · 𝐾 ) ) )
34	18 8 19 9	mul4d	⊢ ( 𝜑 → ( ( ( 𝐴 · 𝐸 ) · ( 𝐵 · 𝐹 ) ) · ( 𝐶 · 𝐻 ) ) = ( ( ( 𝐴 · 𝐸 ) · 𝐶 ) · ( ( 𝐵 · 𝐹 ) · 𝐻 ) ) )
35	19 16	mulcld	⊢ ( 𝜑 → ( 𝐶 · 𝐴 ) ∈ ℂ )
36	35 13 17 14	mul4d	⊢ ( 𝜑 → ( ( ( 𝐶 · 𝐴 ) · ( 𝐷 · 𝐺 ) ) · ( 𝐸 · 𝐾 ) ) = ( ( ( 𝐶 · 𝐴 ) · 𝐸 ) · ( ( 𝐷 · 𝐺 ) · 𝐾 ) ) )
37	33 34 36	3eqtr3d	⊢ ( 𝜑 → ( ( ( 𝐴 · 𝐸 ) · 𝐶 ) · ( ( 𝐵 · 𝐹 ) · 𝐻 ) ) = ( ( ( 𝐶 · 𝐴 ) · 𝐸 ) · ( ( 𝐷 · 𝐺 ) · 𝐾 ) ) )
38	16 17 19	mul32d	⊢ ( 𝜑 → ( ( 𝐴 · 𝐸 ) · 𝐶 ) = ( ( 𝐴 · 𝐶 ) · 𝐸 ) )
39	16 19	mulcomd	⊢ ( 𝜑 → ( 𝐴 · 𝐶 ) = ( 𝐶 · 𝐴 ) )
40	39	oveq1d	⊢ ( 𝜑 → ( ( 𝐴 · 𝐶 ) · 𝐸 ) = ( ( 𝐶 · 𝐴 ) · 𝐸 ) )
41	38 40	eqtrd	⊢ ( 𝜑 → ( ( 𝐴 · 𝐸 ) · 𝐶 ) = ( ( 𝐶 · 𝐴 ) · 𝐸 ) )
42	41	oveq1d	⊢ ( 𝜑 → ( ( ( 𝐴 · 𝐸 ) · 𝐶 ) · ( ( 𝐷 · 𝐺 ) · 𝐾 ) ) = ( ( ( 𝐶 · 𝐴 ) · 𝐸 ) · ( ( 𝐷 · 𝐺 ) · 𝐾 ) ) )
43	37 42	eqtr4d	⊢ ( 𝜑 → ( ( ( 𝐴 · 𝐸 ) · 𝐶 ) · ( ( 𝐵 · 𝐹 ) · 𝐻 ) ) = ( ( ( 𝐴 · 𝐸 ) · 𝐶 ) · ( ( 𝐷 · 𝐺 ) · 𝐾 ) ) )
44	10 15 20 25 43	mulcanad	⊢ ( 𝜑 → ( ( 𝐵 · 𝐹 ) · 𝐻 ) = ( ( 𝐷 · 𝐺 ) · 𝐾 ) )