Metamath Proof Explorer

Theorem colinearalglem1

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

Ref Expression
Assertion colinearalglem1 
|- ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( D e. CC /\ E e. CC /\ F e. CC ) ) -> ( ( ( B - A ) x. ( F - D ) ) = ( ( E - D ) x. ( C - A ) ) <-> ( ( B x. F ) - ( ( A x. F ) + ( B x. D ) ) ) = ( ( C x. E ) - ( ( A x. E ) + ( C x. D ) ) ) ) )

Proof

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