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 ⊢ ( 𝜑 → ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) )
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 ⊢ ( 𝜑 → ( ( 𝐵 · 𝐹 ) · 𝐻 ) = ( ( 𝐷 · 𝐺 ) · 𝐾 ) )