colinearalglem1

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

		Ref	Expression
	Assertion	colinearalglem1	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land (D \in ℂ \land E \in ℂ \land F \in ℂ)) \to ((B - A) (F - D) = (E - D) (C - A) \leftrightarrow B F - (A F + B D) = C E - (A E + C D))$

Proof

Step	Hyp	Ref	Expression
1		simpl2	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land (D \in ℂ \land E \in ℂ \land F \in ℂ)) \to B \in ℂ$
2		simpl1	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land (D \in ℂ \land E \in ℂ \land F \in ℂ)) \to A \in ℂ$
3	1 2	subcld	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land (D \in ℂ \land E \in ℂ \land F \in ℂ)) \to B - A \in ℂ$
4		simpr3	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land (D \in ℂ \land E \in ℂ \land F \in ℂ)) \to F \in ℂ$
5		simpr1	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land (D \in ℂ \land E \in ℂ \land F \in ℂ)) \to D \in ℂ$
6	3 4 5	subdid	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land (D \in ℂ \land E \in ℂ \land F \in ℂ)) \to (B - A) (F - D) = (B - A) F - (B - A) D$
7	1 2 4	subdird	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land (D \in ℂ \land E \in ℂ \land F \in ℂ)) \to (B - A) F = B F - A F$
8	1 2 5	subdird	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land (D \in ℂ \land E \in ℂ \land F \in ℂ)) \to (B - A) D = B D - A D$
9	7 8	oveq12d	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land (D \in ℂ \land E \in ℂ \land F \in ℂ)) \to (B - A) F - (B - A) D = B F - A F - (B D - A D)$
10		simp2	$⊢ (A \in ℂ \land B \in ℂ \land C \in ℂ) \to B \in ℂ$
11		simp3	$⊢ (D \in ℂ \land E \in ℂ \land F \in ℂ) \to F \in ℂ$
12		mulcl	$⊢ (B \in ℂ \land F \in ℂ) \to B F \in ℂ$
13	10 11 12	syl2an	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land (D \in ℂ \land E \in ℂ \land F \in ℂ)) \to B F \in ℂ$
14		simp1	$⊢ (A \in ℂ \land B \in ℂ \land C \in ℂ) \to A \in ℂ$
15		mulcl	$⊢ (A \in ℂ \land F \in ℂ) \to A F \in ℂ$
16	14 11 15	syl2an	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land (D \in ℂ \land E \in ℂ \land F \in ℂ)) \to A F \in ℂ$
17	13 16	subcld	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land (D \in ℂ \land E \in ℂ \land F \in ℂ)) \to B F - A F \in ℂ$
18		simp1	$⊢ (D \in ℂ \land E \in ℂ \land F \in ℂ) \to D \in ℂ$
19		mulcl	$⊢ (B \in ℂ \land D \in ℂ) \to B D \in ℂ$
20	10 18 19	syl2an	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land (D \in ℂ \land E \in ℂ \land F \in ℂ)) \to B D \in ℂ$
21		mulcl	$⊢ (A \in ℂ \land D \in ℂ) \to A D \in ℂ$
22	14 18 21	syl2an	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land (D \in ℂ \land E \in ℂ \land F \in ℂ)) \to A D \in ℂ$
23	17 20 22	subsub3d	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land (D \in ℂ \land E \in ℂ \land F \in ℂ)) \to B F - A F - (B D - A D) = (B F - A F) + A D - B D$
24	17 22 20	addsubd	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land (D \in ℂ \land E \in ℂ \land F \in ℂ)) \to (B F - A F) + A D - B D = (B F - A F) - B D + A D$
25	9 23 24	3eqtrrd	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land (D \in ℂ \land E \in ℂ \land F \in ℂ)) \to (B F - A F) - B D + A D = (B - A) F - (B - A) D$
26	13 16 20	subsub4d	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land (D \in ℂ \land E \in ℂ \land F \in ℂ)) \to B F - A F - B D = B F - (A F + B D)$
27	26	oveq1d	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land (D \in ℂ \land E \in ℂ \land F \in ℂ)) \to (B F - A F) - B D + A D = B F - (A F + B D) + A D$
28	6 25 27	3eqtr2d	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land (D \in ℂ \land E \in ℂ \land F \in ℂ)) \to (B - A) (F - D) = B F - (A F + B D) + A D$
29		simpr2	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land (D \in ℂ \land E \in ℂ \land F \in ℂ)) \to E \in ℂ$
30	29 5	subcld	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land (D \in ℂ \land E \in ℂ \land F \in ℂ)) \to E - D \in ℂ$
31		simpl3	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land (D \in ℂ \land E \in ℂ \land F \in ℂ)) \to C \in ℂ$
32	31 2	subcld	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land (D \in ℂ \land E \in ℂ \land F \in ℂ)) \to C - A \in ℂ$
33	30 32	mulcomd	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land (D \in ℂ \land E \in ℂ \land F \in ℂ)) \to (E - D) (C - A) = (C - A) (E - D)$
34	32 29 5	subdid	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land (D \in ℂ \land E \in ℂ \land F \in ℂ)) \to (C - A) (E - D) = (C - A) E - (C - A) D$
35	31 2 29	subdird	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land (D \in ℂ \land E \in ℂ \land F \in ℂ)) \to (C - A) E = C E - A E$
36	31 2 5	subdird	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land (D \in ℂ \land E \in ℂ \land F \in ℂ)) \to (C - A) D = C D - A D$
37	35 36	oveq12d	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land (D \in ℂ \land E \in ℂ \land F \in ℂ)) \to (C - A) E - (C - A) D = C E - A E - (C D - A D)$
38		simp3	$⊢ (A \in ℂ \land B \in ℂ \land C \in ℂ) \to C \in ℂ$
39		simp2	$⊢ (D \in ℂ \land E \in ℂ \land F \in ℂ) \to E \in ℂ$
40		mulcl	$⊢ (C \in ℂ \land E \in ℂ) \to C E \in ℂ$
41	38 39 40	syl2an	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land (D \in ℂ \land E \in ℂ \land F \in ℂ)) \to C E \in ℂ$
42		mulcl	$⊢ (A \in ℂ \land E \in ℂ) \to A E \in ℂ$
43	14 39 42	syl2an	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land (D \in ℂ \land E \in ℂ \land F \in ℂ)) \to A E \in ℂ$
44	41 43	subcld	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land (D \in ℂ \land E \in ℂ \land F \in ℂ)) \to C E - A E \in ℂ$
45		mulcl	$⊢ (C \in ℂ \land D \in ℂ) \to C D \in ℂ$
46	38 18 45	syl2an	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land (D \in ℂ \land E \in ℂ \land F \in ℂ)) \to C D \in ℂ$
47	44 46 22	subsub3d	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land (D \in ℂ \land E \in ℂ \land F \in ℂ)) \to C E - A E - (C D - A D) = (C E - A E) + A D - C D$
48	44 22 46	addsubd	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land (D \in ℂ \land E \in ℂ \land F \in ℂ)) \to (C E - A E) + A D - C D = (C E - A E) - C D + A D$
49	37 47 48	3eqtrrd	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land (D \in ℂ \land E \in ℂ \land F \in ℂ)) \to (C E - A E) - C D + A D = (C - A) E - (C - A) D$
50	41 43 46	subsub4d	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land (D \in ℂ \land E \in ℂ \land F \in ℂ)) \to C E - A E - C D = C E - (A E + C D)$
51	50	oveq1d	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land (D \in ℂ \land E \in ℂ \land F \in ℂ)) \to (C E - A E) - C D + A D = C E - (A E + C D) + A D$
52	49 51	eqtr3d	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land (D \in ℂ \land E \in ℂ \land F \in ℂ)) \to (C - A) E - (C - A) D = C E - (A E + C D) + A D$
53	33 34 52	3eqtrd	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land (D \in ℂ \land E \in ℂ \land F \in ℂ)) \to (E - D) (C - A) = C E - (A E + C D) + A D$
54	28 53	eqeq12d	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land (D \in ℂ \land E \in ℂ \land F \in ℂ)) \to ((B - A) (F - D) = (E - D) (C - A) \leftrightarrow B F - (A F + B D) + A D = C E - (A E + C D) + A D)$
55	16 20	addcld	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land (D \in ℂ \land E \in ℂ \land F \in ℂ)) \to A F + B D \in ℂ$
56	13 55	subcld	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land (D \in ℂ \land E \in ℂ \land F \in ℂ)) \to B F - (A F + B D) \in ℂ$
57	43 46	addcld	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land (D \in ℂ \land E \in ℂ \land F \in ℂ)) \to A E + C D \in ℂ$
58	41 57	subcld	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land (D \in ℂ \land E \in ℂ \land F \in ℂ)) \to C E - (A E + C D) \in ℂ$
59	56 58 22	addcan2d	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land (D \in ℂ \land E \in ℂ \land F \in ℂ)) \to (B F - (A F + B D) + A D = C E - (A E + C D) + A D \leftrightarrow B F - (A F + B D) = C E - (A E + C D))$
60	54 59	bitrd	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land (D \in ℂ \land E \in ℂ \land F \in ℂ)) \to ((B - A) (F - D) = (E - D) (C - A) \leftrightarrow B F - (A F + B D) = C E - (A E + C D))$

Metamath Proof Explorer

Theorem colinearalglem1

Proof