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	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐷 ∈ ℂ ∧ 𝐸 ∈ ℂ ∧ 𝐹 ∈ ℂ ) ) → ( ( ( 𝐵 − 𝐴 ) · ( 𝐹 − 𝐷 ) ) = ( ( 𝐸 − 𝐷 ) · ( 𝐶 − 𝐴 ) ) ↔ ( ( 𝐵 · 𝐹 ) − ( ( 𝐴 · 𝐹 ) + ( 𝐵 · 𝐷 ) ) ) = ( ( 𝐶 · 𝐸 ) − ( ( 𝐴 · 𝐸 ) + ( 𝐶 · 𝐷 ) ) ) ) )