Metamath Proof Explorer

Theorem colinearalglem1

Description: Lemma for colinearalg . Expand out a multiplication. (Contributed by Scott Fenton, 24-Jun-2013)

Ref Expression
Assertion colinearalglem1 ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐷 ∈ ℂ ∧ 𝐸 ∈ ℂ ∧ 𝐹 ∈ ℂ ) ) → ( ( ( 𝐵 − 𝐴 ) · ( 𝐹 − 𝐷 ) ) = ( ( 𝐸 − 𝐷 ) · ( 𝐶 − 𝐴 ) ) ↔ ( ( 𝐵 · 𝐹 ) − ( ( 𝐴 · 𝐹 ) + ( 𝐵 · 𝐷 ) ) ) = ( ( 𝐶 · 𝐸 ) − ( ( 𝐴 · 𝐸 ) + ( 𝐶 · 𝐷 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 simpl2 ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐷 ∈ ℂ ∧ 𝐸 ∈ ℂ ∧ 𝐹 ∈ ℂ ) ) → 𝐵 ∈ ℂ )
2 simpl1 ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐷 ∈ ℂ ∧ 𝐸 ∈ ℂ ∧ 𝐹 ∈ ℂ ) ) → 𝐴 ∈ ℂ )
3 1 2 subcld ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐷 ∈ ℂ ∧ 𝐸 ∈ ℂ ∧ 𝐹 ∈ ℂ ) ) → ( 𝐵 − 𝐴 ) ∈ ℂ )
4 simpr3 ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐷 ∈ ℂ ∧ 𝐸 ∈ ℂ ∧ 𝐹 ∈ ℂ ) ) → 𝐹 ∈ ℂ )
5 simpr1 ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐷 ∈ ℂ ∧ 𝐸 ∈ ℂ ∧ 𝐹 ∈ ℂ ) ) → 𝐷 ∈ ℂ )
6 3 4 5 subdid ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐷 ∈ ℂ ∧ 𝐸 ∈ ℂ ∧ 𝐹 ∈ ℂ ) ) → ( ( 𝐵 − 𝐴 ) · ( 𝐹 − 𝐷 ) ) = ( ( ( 𝐵 − 𝐴 ) · 𝐹 ) − ( ( 𝐵 − 𝐴 ) · 𝐷 ) ) )
7 1 2 4 subdird ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐷 ∈ ℂ ∧ 𝐸 ∈ ℂ ∧ 𝐹 ∈ ℂ ) ) → ( ( 𝐵 − 𝐴 ) · 𝐹 ) = ( ( 𝐵 · 𝐹 ) − ( 𝐴 · 𝐹 ) ) )
8 1 2 5 subdird ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐷 ∈ ℂ ∧ 𝐸 ∈ ℂ ∧ 𝐹 ∈ ℂ ) ) → ( ( 𝐵 − 𝐴 ) · 𝐷 ) = ( ( 𝐵 · 𝐷 ) − ( 𝐴 · 𝐷 ) ) )
9 7 8 oveq12d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐷 ∈ ℂ ∧ 𝐸 ∈ ℂ ∧ 𝐹 ∈ ℂ ) ) → ( ( ( 𝐵 − 𝐴 ) · 𝐹 ) − ( ( 𝐵 − 𝐴 ) · 𝐷 ) ) = ( ( ( 𝐵 · 𝐹 ) − ( 𝐴 · 𝐹 ) ) − ( ( 𝐵 · 𝐷 ) − ( 𝐴 · 𝐷 ) ) ) )
10 simp2 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → 𝐵 ∈ ℂ )
11 simp3 ⊢ ( ( 𝐷 ∈ ℂ ∧ 𝐸 ∈ ℂ ∧ 𝐹 ∈ ℂ ) → 𝐹 ∈ ℂ )
12 mulcl ⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐹 ∈ ℂ ) → ( 𝐵 · 𝐹 ) ∈ ℂ )
13 10 11 12 syl2an ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐷 ∈ ℂ ∧ 𝐸 ∈ ℂ ∧ 𝐹 ∈ ℂ ) ) → ( 𝐵 · 𝐹 ) ∈ ℂ )
14 simp1 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → 𝐴 ∈ ℂ )
15 mulcl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐹 ∈ ℂ ) → ( 𝐴 · 𝐹 ) ∈ ℂ )
16 14 11 15 syl2an ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐷 ∈ ℂ ∧ 𝐸 ∈ ℂ ∧ 𝐹 ∈ ℂ ) ) → ( 𝐴 · 𝐹 ) ∈ ℂ )
17 13 16 subcld ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐷 ∈ ℂ ∧ 𝐸 ∈ ℂ ∧ 𝐹 ∈ ℂ ) ) → ( ( 𝐵 · 𝐹 ) − ( 𝐴 · 𝐹 ) ) ∈ ℂ )
18 simp1 ⊢ ( ( 𝐷 ∈ ℂ ∧ 𝐸 ∈ ℂ ∧ 𝐹 ∈ ℂ ) → 𝐷 ∈ ℂ )
19 mulcl ⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐷 ∈ ℂ ) → ( 𝐵 · 𝐷 ) ∈ ℂ )
20 10 18 19 syl2an ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐷 ∈ ℂ ∧ 𝐸 ∈ ℂ ∧ 𝐹 ∈ ℂ ) ) → ( 𝐵 · 𝐷 ) ∈ ℂ )
21 mulcl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐷 ∈ ℂ ) → ( 𝐴 · 𝐷 ) ∈ ℂ )
22 14 18 21 syl2an ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐷 ∈ ℂ ∧ 𝐸 ∈ ℂ ∧ 𝐹 ∈ ℂ ) ) → ( 𝐴 · 𝐷 ) ∈ ℂ )
23 17 20 22 subsub3d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐷 ∈ ℂ ∧ 𝐸 ∈ ℂ ∧ 𝐹 ∈ ℂ ) ) → ( ( ( 𝐵 · 𝐹 ) − ( 𝐴 · 𝐹 ) ) − ( ( 𝐵 · 𝐷 ) − ( 𝐴 · 𝐷 ) ) ) = ( ( ( ( 𝐵 · 𝐹 ) − ( 𝐴 · 𝐹 ) ) + ( 𝐴 · 𝐷 ) ) − ( 𝐵 · 𝐷 ) ) )
24 17 22 20 addsubd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐷 ∈ ℂ ∧ 𝐸 ∈ ℂ ∧ 𝐹 ∈ ℂ ) ) → ( ( ( ( 𝐵 · 𝐹 ) − ( 𝐴 · 𝐹 ) ) + ( 𝐴 · 𝐷 ) ) − ( 𝐵 · 𝐷 ) ) = ( ( ( ( 𝐵 · 𝐹 ) − ( 𝐴 · 𝐹 ) ) − ( 𝐵 · 𝐷 ) ) + ( 𝐴 · 𝐷 ) ) )
25 9 23 24 3eqtrrd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐷 ∈ ℂ ∧ 𝐸 ∈ ℂ ∧ 𝐹 ∈ ℂ ) ) → ( ( ( ( 𝐵 · 𝐹 ) − ( 𝐴 · 𝐹 ) ) − ( 𝐵 · 𝐷 ) ) + ( 𝐴 · 𝐷 ) ) = ( ( ( 𝐵 − 𝐴 ) · 𝐹 ) − ( ( 𝐵 − 𝐴 ) · 𝐷 ) ) )
26 13 16 20 subsub4d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐷 ∈ ℂ ∧ 𝐸 ∈ ℂ ∧ 𝐹 ∈ ℂ ) ) → ( ( ( 𝐵 · 𝐹 ) − ( 𝐴 · 𝐹 ) ) − ( 𝐵 · 𝐷 ) ) = ( ( 𝐵 · 𝐹 ) − ( ( 𝐴 · 𝐹 ) + ( 𝐵 · 𝐷 ) ) ) )
27 26 oveq1d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐷 ∈ ℂ ∧ 𝐸 ∈ ℂ ∧ 𝐹 ∈ ℂ ) ) → ( ( ( ( 𝐵 · 𝐹 ) − ( 𝐴 · 𝐹 ) ) − ( 𝐵 · 𝐷 ) ) + ( 𝐴 · 𝐷 ) ) = ( ( ( 𝐵 · 𝐹 ) − ( ( 𝐴 · 𝐹 ) + ( 𝐵 · 𝐷 ) ) ) + ( 𝐴 · 𝐷 ) ) )
28 6 25 27 3eqtr2d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐷 ∈ ℂ ∧ 𝐸 ∈ ℂ ∧ 𝐹 ∈ ℂ ) ) → ( ( 𝐵 − 𝐴 ) · ( 𝐹 − 𝐷 ) ) = ( ( ( 𝐵 · 𝐹 ) − ( ( 𝐴 · 𝐹 ) + ( 𝐵 · 𝐷 ) ) ) + ( 𝐴 · 𝐷 ) ) )
29 simpr2 ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐷 ∈ ℂ ∧ 𝐸 ∈ ℂ ∧ 𝐹 ∈ ℂ ) ) → 𝐸 ∈ ℂ )
30 29 5 subcld ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐷 ∈ ℂ ∧ 𝐸 ∈ ℂ ∧ 𝐹 ∈ ℂ ) ) → ( 𝐸 − 𝐷 ) ∈ ℂ )
31 simpl3 ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐷 ∈ ℂ ∧ 𝐸 ∈ ℂ ∧ 𝐹 ∈ ℂ ) ) → 𝐶 ∈ ℂ )
32 31 2 subcld ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐷 ∈ ℂ ∧ 𝐸 ∈ ℂ ∧ 𝐹 ∈ ℂ ) ) → ( 𝐶 − 𝐴 ) ∈ ℂ )
33 30 32 mulcomd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐷 ∈ ℂ ∧ 𝐸 ∈ ℂ ∧ 𝐹 ∈ ℂ ) ) → ( ( 𝐸 − 𝐷 ) · ( 𝐶 − 𝐴 ) ) = ( ( 𝐶 − 𝐴 ) · ( 𝐸 − 𝐷 ) ) )
34 32 29 5 subdid ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐷 ∈ ℂ ∧ 𝐸 ∈ ℂ ∧ 𝐹 ∈ ℂ ) ) → ( ( 𝐶 − 𝐴 ) · ( 𝐸 − 𝐷 ) ) = ( ( ( 𝐶 − 𝐴 ) · 𝐸 ) − ( ( 𝐶 − 𝐴 ) · 𝐷 ) ) )
35 31 2 29 subdird ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐷 ∈ ℂ ∧ 𝐸 ∈ ℂ ∧ 𝐹 ∈ ℂ ) ) → ( ( 𝐶 − 𝐴 ) · 𝐸 ) = ( ( 𝐶 · 𝐸 ) − ( 𝐴 · 𝐸 ) ) )
36 31 2 5 subdird ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐷 ∈ ℂ ∧ 𝐸 ∈ ℂ ∧ 𝐹 ∈ ℂ ) ) → ( ( 𝐶 − 𝐴 ) · 𝐷 ) = ( ( 𝐶 · 𝐷 ) − ( 𝐴 · 𝐷 ) ) )
37 35 36 oveq12d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐷 ∈ ℂ ∧ 𝐸 ∈ ℂ ∧ 𝐹 ∈ ℂ ) ) → ( ( ( 𝐶 − 𝐴 ) · 𝐸 ) − ( ( 𝐶 − 𝐴 ) · 𝐷 ) ) = ( ( ( 𝐶 · 𝐸 ) − ( 𝐴 · 𝐸 ) ) − ( ( 𝐶 · 𝐷 ) − ( 𝐴 · 𝐷 ) ) ) )
38 simp3 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → 𝐶 ∈ ℂ )
39 simp2 ⊢ ( ( 𝐷 ∈ ℂ ∧ 𝐸 ∈ ℂ ∧ 𝐹 ∈ ℂ ) → 𝐸 ∈ ℂ )
40 mulcl ⊢ ( ( 𝐶 ∈ ℂ ∧ 𝐸 ∈ ℂ ) → ( 𝐶 · 𝐸 ) ∈ ℂ )
41 38 39 40 syl2an ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐷 ∈ ℂ ∧ 𝐸 ∈ ℂ ∧ 𝐹 ∈ ℂ ) ) → ( 𝐶 · 𝐸 ) ∈ ℂ )
42 mulcl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐸 ∈ ℂ ) → ( 𝐴 · 𝐸 ) ∈ ℂ )
43 14 39 42 syl2an ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐷 ∈ ℂ ∧ 𝐸 ∈ ℂ ∧ 𝐹 ∈ ℂ ) ) → ( 𝐴 · 𝐸 ) ∈ ℂ )
44 41 43 subcld ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐷 ∈ ℂ ∧ 𝐸 ∈ ℂ ∧ 𝐹 ∈ ℂ ) ) → ( ( 𝐶 · 𝐸 ) − ( 𝐴 · 𝐸 ) ) ∈ ℂ )
45 mulcl ⊢ ( ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) → ( 𝐶 · 𝐷 ) ∈ ℂ )
46 38 18 45 syl2an ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐷 ∈ ℂ ∧ 𝐸 ∈ ℂ ∧ 𝐹 ∈ ℂ ) ) → ( 𝐶 · 𝐷 ) ∈ ℂ )
47 44 46 22 subsub3d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐷 ∈ ℂ ∧ 𝐸 ∈ ℂ ∧ 𝐹 ∈ ℂ ) ) → ( ( ( 𝐶 · 𝐸 ) − ( 𝐴 · 𝐸 ) ) − ( ( 𝐶 · 𝐷 ) − ( 𝐴 · 𝐷 ) ) ) = ( ( ( ( 𝐶 · 𝐸 ) − ( 𝐴 · 𝐸 ) ) + ( 𝐴 · 𝐷 ) ) − ( 𝐶 · 𝐷 ) ) )
48 44 22 46 addsubd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐷 ∈ ℂ ∧ 𝐸 ∈ ℂ ∧ 𝐹 ∈ ℂ ) ) → ( ( ( ( 𝐶 · 𝐸 ) − ( 𝐴 · 𝐸 ) ) + ( 𝐴 · 𝐷 ) ) − ( 𝐶 · 𝐷 ) ) = ( ( ( ( 𝐶 · 𝐸 ) − ( 𝐴 · 𝐸 ) ) − ( 𝐶 · 𝐷 ) ) + ( 𝐴 · 𝐷 ) ) )
49 37 47 48 3eqtrrd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐷 ∈ ℂ ∧ 𝐸 ∈ ℂ ∧ 𝐹 ∈ ℂ ) ) → ( ( ( ( 𝐶 · 𝐸 ) − ( 𝐴 · 𝐸 ) ) − ( 𝐶 · 𝐷 ) ) + ( 𝐴 · 𝐷 ) ) = ( ( ( 𝐶 − 𝐴 ) · 𝐸 ) − ( ( 𝐶 − 𝐴 ) · 𝐷 ) ) )
50 41 43 46 subsub4d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐷 ∈ ℂ ∧ 𝐸 ∈ ℂ ∧ 𝐹 ∈ ℂ ) ) → ( ( ( 𝐶 · 𝐸 ) − ( 𝐴 · 𝐸 ) ) − ( 𝐶 · 𝐷 ) ) = ( ( 𝐶 · 𝐸 ) − ( ( 𝐴 · 𝐸 ) + ( 𝐶 · 𝐷 ) ) ) )
51 50 oveq1d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐷 ∈ ℂ ∧ 𝐸 ∈ ℂ ∧ 𝐹 ∈ ℂ ) ) → ( ( ( ( 𝐶 · 𝐸 ) − ( 𝐴 · 𝐸 ) ) − ( 𝐶 · 𝐷 ) ) + ( 𝐴 · 𝐷 ) ) = ( ( ( 𝐶 · 𝐸 ) − ( ( 𝐴 · 𝐸 ) + ( 𝐶 · 𝐷 ) ) ) + ( 𝐴 · 𝐷 ) ) )
52 49 51 eqtr3d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐷 ∈ ℂ ∧ 𝐸 ∈ ℂ ∧ 𝐹 ∈ ℂ ) ) → ( ( ( 𝐶 − 𝐴 ) · 𝐸 ) − ( ( 𝐶 − 𝐴 ) · 𝐷 ) ) = ( ( ( 𝐶 · 𝐸 ) − ( ( 𝐴 · 𝐸 ) + ( 𝐶 · 𝐷 ) ) ) + ( 𝐴 · 𝐷 ) ) )
53 33 34 52 3eqtrd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐷 ∈ ℂ ∧ 𝐸 ∈ ℂ ∧ 𝐹 ∈ ℂ ) ) → ( ( 𝐸 − 𝐷 ) · ( 𝐶 − 𝐴 ) ) = ( ( ( 𝐶 · 𝐸 ) − ( ( 𝐴 · 𝐸 ) + ( 𝐶 · 𝐷 ) ) ) + ( 𝐴 · 𝐷 ) ) )
54 28 53 eqeq12d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐷 ∈ ℂ ∧ 𝐸 ∈ ℂ ∧ 𝐹 ∈ ℂ ) ) → ( ( ( 𝐵 − 𝐴 ) · ( 𝐹 − 𝐷 ) ) = ( ( 𝐸 − 𝐷 ) · ( 𝐶 − 𝐴 ) ) ↔ ( ( ( 𝐵 · 𝐹 ) − ( ( 𝐴 · 𝐹 ) + ( 𝐵 · 𝐷 ) ) ) + ( 𝐴 · 𝐷 ) ) = ( ( ( 𝐶 · 𝐸 ) − ( ( 𝐴 · 𝐸 ) + ( 𝐶 · 𝐷 ) ) ) + ( 𝐴 · 𝐷 ) ) ) )
55 16 20 addcld ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐷 ∈ ℂ ∧ 𝐸 ∈ ℂ ∧ 𝐹 ∈ ℂ ) ) → ( ( 𝐴 · 𝐹 ) + ( 𝐵 · 𝐷 ) ) ∈ ℂ )
56 13 55 subcld ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐷 ∈ ℂ ∧ 𝐸 ∈ ℂ ∧ 𝐹 ∈ ℂ ) ) → ( ( 𝐵 · 𝐹 ) − ( ( 𝐴 · 𝐹 ) + ( 𝐵 · 𝐷 ) ) ) ∈ ℂ )
57 43 46 addcld ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐷 ∈ ℂ ∧ 𝐸 ∈ ℂ ∧ 𝐹 ∈ ℂ ) ) → ( ( 𝐴 · 𝐸 ) + ( 𝐶 · 𝐷 ) ) ∈ ℂ )
58 41 57 subcld ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐷 ∈ ℂ ∧ 𝐸 ∈ ℂ ∧ 𝐹 ∈ ℂ ) ) → ( ( 𝐶 · 𝐸 ) − ( ( 𝐴 · 𝐸 ) + ( 𝐶 · 𝐷 ) ) ) ∈ ℂ )
59 56 58 22 addcan2d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐷 ∈ ℂ ∧ 𝐸 ∈ ℂ ∧ 𝐹 ∈ ℂ ) ) → ( ( ( ( 𝐵 · 𝐹 ) − ( ( 𝐴 · 𝐹 ) + ( 𝐵 · 𝐷 ) ) ) + ( 𝐴 · 𝐷 ) ) = ( ( ( 𝐶 · 𝐸 ) − ( ( 𝐴 · 𝐸 ) + ( 𝐶 · 𝐷 ) ) ) + ( 𝐴 · 𝐷 ) ) ↔ ( ( 𝐵 · 𝐹 ) − ( ( 𝐴 · 𝐹 ) + ( 𝐵 · 𝐷 ) ) ) = ( ( 𝐶 · 𝐸 ) − ( ( 𝐴 · 𝐸 ) + ( 𝐶 · 𝐷 ) ) ) ) )
60 54 59 bitrd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐷 ∈ ℂ ∧ 𝐸 ∈ ℂ ∧ 𝐹 ∈ ℂ ) ) → ( ( ( 𝐵 − 𝐴 ) · ( 𝐹 − 𝐷 ) ) = ( ( 𝐸 − 𝐷 ) · ( 𝐶 − 𝐴 ) ) ↔ ( ( 𝐵 · 𝐹 ) − ( ( 𝐴 · 𝐹 ) + ( 𝐵 · 𝐷 ) ) ) = ( ( 𝐶 · 𝐸 ) − ( ( 𝐴 · 𝐸 ) + ( 𝐶 · 𝐷 ) ) ) ) )