Metamath Proof Explorer

Theorem colinearalglem2

Description: Lemma for colinearalg . Translate between two forms of the colinearity condition. (Contributed by Scott Fenton, 24-Jun-2013)

Ref Expression
Assertion colinearalglem2 
|- ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) -> ( A. i e. ( 1 ... N ) A. j e. ( 1 ... N ) ( ( ( B ` i ) - ( A ` i ) ) x. ( ( C ` j ) - ( A ` j ) ) ) = ( ( ( B ` j ) - ( A ` j ) ) x. ( ( C ` i ) - ( A ` i ) ) ) <-> A. i e. ( 1 ... N ) A. j e. ( 1 ... N ) ( ( ( C ` i ) - ( B ` i ) ) x. ( ( A ` j ) - ( B ` j ) ) ) = ( ( ( C ` j ) - ( B ` j ) ) x. ( ( A ` i ) - ( B ` i ) ) ) ) )

Proof

Step Hyp Ref Expression
1 simp1 
 |-  ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) -> A e. ( EE ` N ) )
2 simpl 
 |-  ( ( i e. ( 1 ... N ) /\ j e. ( 1 ... N ) ) -> i e. ( 1 ... N ) )
3 fveecn 
 |-  ( ( A e. ( EE ` N ) /\ i e. ( 1 ... N ) ) -> ( A ` i ) e. CC )
4 1 2 3 syl2an 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( i e. ( 1 ... N ) /\ j e. ( 1 ... N ) ) ) -> ( A ` i ) e. CC )
5 simp2 
 |-  ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) -> B e. ( EE ` N ) )
6 fveecn 
 |-  ( ( B e. ( EE ` N ) /\ i e. ( 1 ... N ) ) -> ( B ` i ) e. CC )
7 5 2 6 syl2an 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( i e. ( 1 ... N ) /\ j e. ( 1 ... N ) ) ) -> ( B ` i ) e. CC )
8 simp3 
 |-  ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) -> C e. ( EE ` N ) )
9 fveecn 
 |-  ( ( C e. ( EE ` N ) /\ i e. ( 1 ... N ) ) -> ( C ` i ) e. CC )
10 8 2 9 syl2an 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( i e. ( 1 ... N ) /\ j e. ( 1 ... N ) ) ) -> ( C ` i ) e. CC )
11 simpr 
 |-  ( ( i e. ( 1 ... N ) /\ j e. ( 1 ... N ) ) -> j e. ( 1 ... N ) )
12 fveecn 
 |-  ( ( A e. ( EE ` N ) /\ j e. ( 1 ... N ) ) -> ( A ` j ) e. CC )
13 1 11 12 syl2an 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( i e. ( 1 ... N ) /\ j e. ( 1 ... N ) ) ) -> ( A ` j ) e. CC )
14 fveecn 
 |-  ( ( B e. ( EE ` N ) /\ j e. ( 1 ... N ) ) -> ( B ` j ) e. CC )
15 5 11 14 syl2an 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( i e. ( 1 ... N ) /\ j e. ( 1 ... N ) ) ) -> ( B ` j ) e. CC )
16 fveecn 
 |-  ( ( C e. ( EE ` N ) /\ j e. ( 1 ... N ) ) -> ( C ` j ) e. CC )
17 8 11 16 syl2an 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( i e. ( 1 ... N ) /\ j e. ( 1 ... N ) ) ) -> ( C ` j ) e. CC )
18 simp1 
 |-  ( ( ( A ` i ) e. CC /\ ( B ` i ) e. CC /\ ( C ` i ) e. CC ) -> ( A ` i ) e. CC )
19 simp3 
 |-  ( ( ( A ` j ) e. CC /\ ( B ` j ) e. CC /\ ( C ` j ) e. CC ) -> ( C ` j ) e. CC )
20 mulcl 
 |-  ( ( ( A ` i ) e. CC /\ ( C ` j ) e. CC ) -> ( ( A ` i ) x. ( C ` j ) ) e. CC )
21 18 19 20 syl2an 
 |-  ( ( ( ( A ` i ) e. CC /\ ( B ` i ) e. CC /\ ( C ` i ) e. CC ) /\ ( ( A ` j ) e. CC /\ ( B ` j ) e. CC /\ ( C ` j ) e. CC ) ) -> ( ( A ` i ) x. ( C ` j ) ) e. CC )
22 simp2 
 |-  ( ( ( A ` i ) e. CC /\ ( B ` i ) e. CC /\ ( C ` i ) e. CC ) -> ( B ` i ) e. CC )
23 simp1 
 |-  ( ( ( A ` j ) e. CC /\ ( B ` j ) e. CC /\ ( C ` j ) e. CC ) -> ( A ` j ) e. CC )
24 mulcl 
 |-  ( ( ( B ` i ) e. CC /\ ( A ` j ) e. CC ) -> ( ( B ` i ) x. ( A ` j ) ) e. CC )
25 22 23 24 syl2an 
 |-  ( ( ( ( A ` i ) e. CC /\ ( B ` i ) e. CC /\ ( C ` i ) e. CC ) /\ ( ( A ` j ) e. CC /\ ( B ` j ) e. CC /\ ( C ` j ) e. CC ) ) -> ( ( B ` i ) x. ( A ` j ) ) e. CC )
26 21 25 addcld 
 |-  ( ( ( ( A ` i ) e. CC /\ ( B ` i ) e. CC /\ ( C ` i ) e. CC ) /\ ( ( A ` j ) e. CC /\ ( B ` j ) e. CC /\ ( C ` j ) e. CC ) ) -> ( ( ( A ` i ) x. ( C ` j ) ) + ( ( B ` i ) x. ( A ` j ) ) ) e. CC )
27 mulcl 
 |-  ( ( ( B ` i ) e. CC /\ ( C ` j ) e. CC ) -> ( ( B ` i ) x. ( C ` j ) ) e. CC )
28 22 19 27 syl2an 
 |-  ( ( ( ( A ` i ) e. CC /\ ( B ` i ) e. CC /\ ( C ` i ) e. CC ) /\ ( ( A ` j ) e. CC /\ ( B ` j ) e. CC /\ ( C ` j ) e. CC ) ) -> ( ( B ` i ) x. ( C ` j ) ) e. CC )
29 26 28 subcld 
 |-  ( ( ( ( A ` i ) e. CC /\ ( B ` i ) e. CC /\ ( C ` i ) e. CC ) /\ ( ( A ` j ) e. CC /\ ( B ` j ) e. CC /\ ( C ` j ) e. CC ) ) -> ( ( ( ( A ` i ) x. ( C ` j ) ) + ( ( B ` i ) x. ( A ` j ) ) ) - ( ( B ` i ) x. ( C ` j ) ) ) e. CC )
30 simp2 
 |-  ( ( ( A ` j ) e. CC /\ ( B ` j ) e. CC /\ ( C ` j ) e. CC ) -> ( B ` j ) e. CC )
31 mulcl 
 |-  ( ( ( A ` i ) e. CC /\ ( B ` j ) e. CC ) -> ( ( A ` i ) x. ( B ` j ) ) e. CC )
32 18 30 31 syl2an 
 |-  ( ( ( ( A ` i ) e. CC /\ ( B ` i ) e. CC /\ ( C ` i ) e. CC ) /\ ( ( A ` j ) e. CC /\ ( B ` j ) e. CC /\ ( C ` j ) e. CC ) ) -> ( ( A ` i ) x. ( B ` j ) ) e. CC )
33 simp3 
 |-  ( ( ( A ` i ) e. CC /\ ( B ` i ) e. CC /\ ( C ` i ) e. CC ) -> ( C ` i ) e. CC )
34 mulcl 
 |-  ( ( ( C ` i ) e. CC /\ ( A ` j ) e. CC ) -> ( ( C ` i ) x. ( A ` j ) ) e. CC )
35 33 23 34 syl2an 
 |-  ( ( ( ( A ` i ) e. CC /\ ( B ` i ) e. CC /\ ( C ` i ) e. CC ) /\ ( ( A ` j ) e. CC /\ ( B ` j ) e. CC /\ ( C ` j ) e. CC ) ) -> ( ( C ` i ) x. ( A ` j ) ) e. CC )
36 mulcl 
 |-  ( ( ( C ` i ) e. CC /\ ( B ` j ) e. CC ) -> ( ( C ` i ) x. ( B ` j ) ) e. CC )
37 33 30 36 syl2an 
 |-  ( ( ( ( A ` i ) e. CC /\ ( B ` i ) e. CC /\ ( C ` i ) e. CC ) /\ ( ( A ` j ) e. CC /\ ( B ` j ) e. CC /\ ( C ` j ) e. CC ) ) -> ( ( C ` i ) x. ( B ` j ) ) e. CC )
38 35 37 subcld 
 |-  ( ( ( ( A ` i ) e. CC /\ ( B ` i ) e. CC /\ ( C ` i ) e. CC ) /\ ( ( A ` j ) e. CC /\ ( B ` j ) e. CC /\ ( C ` j ) e. CC ) ) -> ( ( ( C ` i ) x. ( A ` j ) ) - ( ( C ` i ) x. ( B ` j ) ) ) e. CC )
39 29 32 38 subadd2d 
 |-  ( ( ( ( A ` i ) e. CC /\ ( B ` i ) e. CC /\ ( C ` i ) e. CC ) /\ ( ( A ` j ) e. CC /\ ( B ` j ) e. CC /\ ( C ` j ) e. CC ) ) -> ( ( ( ( ( ( A ` i ) x. ( C ` j ) ) + ( ( B ` i ) x. ( A ` j ) ) ) - ( ( B ` i ) x. ( C ` j ) ) ) - ( ( A ` i ) x. ( B ` j ) ) ) = ( ( ( C ` i ) x. ( A ` j ) ) - ( ( C ` i ) x. ( B ` j ) ) ) <-> ( ( ( ( C ` i ) x. ( A ` j ) ) - ( ( C ` i ) x. ( B ` j ) ) ) + ( ( A ` i ) x. ( B ` j ) ) ) = ( ( ( ( A ` i ) x. ( C ` j ) ) + ( ( B ` i ) x. ( A ` j ) ) ) - ( ( B ` i ) x. ( C ` j ) ) ) ) )
40 eqcom 
 |-  ( ( ( ( ( C ` i ) x. ( A ` j ) ) - ( ( C ` i ) x. ( B ` j ) ) ) + ( ( A ` i ) x. ( B ` j ) ) ) = ( ( ( ( A ` i ) x. ( C ` j ) ) + ( ( B ` i ) x. ( A ` j ) ) ) - ( ( B ` i ) x. ( C ` j ) ) ) <-> ( ( ( ( A ` i ) x. ( C ` j ) ) + ( ( B ` i ) x. ( A ` j ) ) ) - ( ( B ` i ) x. ( C ` j ) ) ) = ( ( ( ( C ` i ) x. ( A ` j ) ) - ( ( C ` i ) x. ( B ` j ) ) ) + ( ( A ` i ) x. ( B ` j ) ) ) )
41 39 40 bitrdi 
 |-  ( ( ( ( A ` i ) e. CC /\ ( B ` i ) e. CC /\ ( C ` i ) e. CC ) /\ ( ( A ` j ) e. CC /\ ( B ` j ) e. CC /\ ( C ` j ) e. CC ) ) -> ( ( ( ( ( ( A ` i ) x. ( C ` j ) ) + ( ( B ` i ) x. ( A ` j ) ) ) - ( ( B ` i ) x. ( C ` j ) ) ) - ( ( A ` i ) x. ( B ` j ) ) ) = ( ( ( C ` i ) x. ( A ` j ) ) - ( ( C ` i ) x. ( B ` j ) ) ) <-> ( ( ( ( A ` i ) x. ( C ` j ) ) + ( ( B ` i ) x. ( A ` j ) ) ) - ( ( B ` i ) x. ( C ` j ) ) ) = ( ( ( ( C ` i ) x. ( A ` j ) ) - ( ( C ` i ) x. ( B ` j ) ) ) + ( ( A ` i ) x. ( B ` j ) ) ) ) )
42 35 32 37 addsubd 
 |-  ( ( ( ( A ` i ) e. CC /\ ( B ` i ) e. CC /\ ( C ` i ) e. CC ) /\ ( ( A ` j ) e. CC /\ ( B ` j ) e. CC /\ ( C ` j ) e. CC ) ) -> ( ( ( ( C ` i ) x. ( A ` j ) ) + ( ( A ` i ) x. ( B ` j ) ) ) - ( ( C ` i ) x. ( B ` j ) ) ) = ( ( ( ( C ` i ) x. ( A ` j ) ) - ( ( C ` i ) x. ( B ` j ) ) ) + ( ( A ` i ) x. ( B ` j ) ) ) )
43 35 32 addcomd 
 |-  ( ( ( ( A ` i ) e. CC /\ ( B ` i ) e. CC /\ ( C ` i ) e. CC ) /\ ( ( A ` j ) e. CC /\ ( B ` j ) e. CC /\ ( C ` j ) e. CC ) ) -> ( ( ( C ` i ) x. ( A ` j ) ) + ( ( A ` i ) x. ( B ` j ) ) ) = ( ( ( A ` i ) x. ( B ` j ) ) + ( ( C ` i ) x. ( A ` j ) ) ) )
44 43 oveq1d 
 |-  ( ( ( ( A ` i ) e. CC /\ ( B ` i ) e. CC /\ ( C ` i ) e. CC ) /\ ( ( A ` j ) e. CC /\ ( B ` j ) e. CC /\ ( C ` j ) e. CC ) ) -> ( ( ( ( C ` i ) x. ( A ` j ) ) + ( ( A ` i ) x. ( B ` j ) ) ) - ( ( C ` i ) x. ( B ` j ) ) ) = ( ( ( ( A ` i ) x. ( B ` j ) ) + ( ( C ` i ) x. ( A ` j ) ) ) - ( ( C ` i ) x. ( B ` j ) ) ) )
45 42 44 eqtr3d 
 |-  ( ( ( ( A ` i ) e. CC /\ ( B ` i ) e. CC /\ ( C ` i ) e. CC ) /\ ( ( A ` j ) e. CC /\ ( B ` j ) e. CC /\ ( C ` j ) e. CC ) ) -> ( ( ( ( C ` i ) x. ( A ` j ) ) - ( ( C ` i ) x. ( B ` j ) ) ) + ( ( A ` i ) x. ( B ` j ) ) ) = ( ( ( ( A ` i ) x. ( B ` j ) ) + ( ( C ` i ) x. ( A ` j ) ) ) - ( ( C ` i ) x. ( B ` j ) ) ) )
46 45 eqeq2d 
 |-  ( ( ( ( A ` i ) e. CC /\ ( B ` i ) e. CC /\ ( C ` i ) e. CC ) /\ ( ( A ` j ) e. CC /\ ( B ` j ) e. CC /\ ( C ` j ) e. CC ) ) -> ( ( ( ( ( A ` i ) x. ( C ` j ) ) + ( ( B ` i ) x. ( A ` j ) ) ) - ( ( B ` i ) x. ( C ` j ) ) ) = ( ( ( ( C ` i ) x. ( A ` j ) ) - ( ( C ` i ) x. ( B ` j ) ) ) + ( ( A ` i ) x. ( B ` j ) ) ) <-> ( ( ( ( A ` i ) x. ( C ` j ) ) + ( ( B ` i ) x. ( A ` j ) ) ) - ( ( B ` i ) x. ( C ` j ) ) ) = ( ( ( ( A ` i ) x. ( B ` j ) ) + ( ( C ` i ) x. ( A ` j ) ) ) - ( ( C ` i ) x. ( B ` j ) ) ) ) )
47 41 46 bitrd 
 |-  ( ( ( ( A ` i ) e. CC /\ ( B ` i ) e. CC /\ ( C ` i ) e. CC ) /\ ( ( A ` j ) e. CC /\ ( B ` j ) e. CC /\ ( C ` j ) e. CC ) ) -> ( ( ( ( ( ( A ` i ) x. ( C ` j ) ) + ( ( B ` i ) x. ( A ` j ) ) ) - ( ( B ` i ) x. ( C ` j ) ) ) - ( ( A ` i ) x. ( B ` j ) ) ) = ( ( ( C ` i ) x. ( A ` j ) ) - ( ( C ` i ) x. ( B ` j ) ) ) <-> ( ( ( ( A ` i ) x. ( C ` j ) ) + ( ( B ` i ) x. ( A ` j ) ) ) - ( ( B ` i ) x. ( C ` j ) ) ) = ( ( ( ( A ` i ) x. ( B ` j ) ) + ( ( C ` i ) x. ( A ` j ) ) ) - ( ( C ` i ) x. ( B ` j ) ) ) ) )
48 26 28 32 subsub4d 
 |-  ( ( ( ( A ` i ) e. CC /\ ( B ` i ) e. CC /\ ( C ` i ) e. CC ) /\ ( ( A ` j ) e. CC /\ ( B ` j ) e. CC /\ ( C ` j ) e. CC ) ) -> ( ( ( ( ( A ` i ) x. ( C ` j ) ) + ( ( B ` i ) x. ( A ` j ) ) ) - ( ( B ` i ) x. ( C ` j ) ) ) - ( ( A ` i ) x. ( B ` j ) ) ) = ( ( ( ( A ` i ) x. ( C ` j ) ) + ( ( B ` i ) x. ( A ` j ) ) ) - ( ( ( B ` i ) x. ( C ` j ) ) + ( ( A ` i ) x. ( B ` j ) ) ) ) )
49 28 32 addcld 
 |-  ( ( ( ( A ` i ) e. CC /\ ( B ` i ) e. CC /\ ( C ` i ) e. CC ) /\ ( ( A ` j ) e. CC /\ ( B ` j ) e. CC /\ ( C ` j ) e. CC ) ) -> ( ( ( B ` i ) x. ( C ` j ) ) + ( ( A ` i ) x. ( B ` j ) ) ) e. CC )
50 21 49 25 subsub3d 
 |-  ( ( ( ( A ` i ) e. CC /\ ( B ` i ) e. CC /\ ( C ` i ) e. CC ) /\ ( ( A ` j ) e. CC /\ ( B ` j ) e. CC /\ ( C ` j ) e. CC ) ) -> ( ( ( A ` i ) x. ( C ` j ) ) - ( ( ( ( B ` i ) x. ( C ` j ) ) + ( ( A ` i ) x. ( B ` j ) ) ) - ( ( B ` i ) x. ( A ` j ) ) ) ) = ( ( ( ( A ` i ) x. ( C ` j ) ) + ( ( B ` i ) x. ( A ` j ) ) ) - ( ( ( B ` i ) x. ( C ` j ) ) + ( ( A ` i ) x. ( B ` j ) ) ) ) )
51 28 25 32 subsub3d 
 |-  ( ( ( ( A ` i ) e. CC /\ ( B ` i ) e. CC /\ ( C ` i ) e. CC ) /\ ( ( A ` j ) e. CC /\ ( B ` j ) e. CC /\ ( C ` j ) e. CC ) ) -> ( ( ( B ` i ) x. ( C ` j ) ) - ( ( ( B ` i ) x. ( A ` j ) ) - ( ( A ` i ) x. ( B ` j ) ) ) ) = ( ( ( ( B ` i ) x. ( C ` j ) ) + ( ( A ` i ) x. ( B ` j ) ) ) - ( ( B ` i ) x. ( A ` j ) ) ) )
52 51 eqcomd 
 |-  ( ( ( ( A ` i ) e. CC /\ ( B ` i ) e. CC /\ ( C ` i ) e. CC ) /\ ( ( A ` j ) e. CC /\ ( B ` j ) e. CC /\ ( C ` j ) e. CC ) ) -> ( ( ( ( B ` i ) x. ( C ` j ) ) + ( ( A ` i ) x. ( B ` j ) ) ) - ( ( B ` i ) x. ( A ` j ) ) ) = ( ( ( B ` i ) x. ( C ` j ) ) - ( ( ( B ` i ) x. ( A ` j ) ) - ( ( A ` i ) x. ( B ` j ) ) ) ) )
53 52 oveq2d 
 |-  ( ( ( ( A ` i ) e. CC /\ ( B ` i ) e. CC /\ ( C ` i ) e. CC ) /\ ( ( A ` j ) e. CC /\ ( B ` j ) e. CC /\ ( C ` j ) e. CC ) ) -> ( ( ( A ` i ) x. ( C ` j ) ) - ( ( ( ( B ` i ) x. ( C ` j ) ) + ( ( A ` i ) x. ( B ` j ) ) ) - ( ( B ` i ) x. ( A ` j ) ) ) ) = ( ( ( A ` i ) x. ( C ` j ) ) - ( ( ( B ` i ) x. ( C ` j ) ) - ( ( ( B ` i ) x. ( A ` j ) ) - ( ( A ` i ) x. ( B ` j ) ) ) ) ) )
54 25 32 subcld 
 |-  ( ( ( ( A ` i ) e. CC /\ ( B ` i ) e. CC /\ ( C ` i ) e. CC ) /\ ( ( A ` j ) e. CC /\ ( B ` j ) e. CC /\ ( C ` j ) e. CC ) ) -> ( ( ( B ` i ) x. ( A ` j ) ) - ( ( A ` i ) x. ( B ` j ) ) ) e. CC )
55 21 28 54 subsubd 
 |-  ( ( ( ( A ` i ) e. CC /\ ( B ` i ) e. CC /\ ( C ` i ) e. CC ) /\ ( ( A ` j ) e. CC /\ ( B ` j ) e. CC /\ ( C ` j ) e. CC ) ) -> ( ( ( A ` i ) x. ( C ` j ) ) - ( ( ( B ` i ) x. ( C ` j ) ) - ( ( ( B ` i ) x. ( A ` j ) ) - ( ( A ` i ) x. ( B ` j ) ) ) ) ) = ( ( ( ( A ` i ) x. ( C ` j ) ) - ( ( B ` i ) x. ( C ` j ) ) ) + ( ( ( B ` i ) x. ( A ` j ) ) - ( ( A ` i ) x. ( B ` j ) ) ) ) )
56 53 55 eqtrd 
 |-  ( ( ( ( A ` i ) e. CC /\ ( B ` i ) e. CC /\ ( C ` i ) e. CC ) /\ ( ( A ` j ) e. CC /\ ( B ` j ) e. CC /\ ( C ` j ) e. CC ) ) -> ( ( ( A ` i ) x. ( C ` j ) ) - ( ( ( ( B ` i ) x. ( C ` j ) ) + ( ( A ` i ) x. ( B ` j ) ) ) - ( ( B ` i ) x. ( A ` j ) ) ) ) = ( ( ( ( A ` i ) x. ( C ` j ) ) - ( ( B ` i ) x. ( C ` j ) ) ) + ( ( ( B ` i ) x. ( A ` j ) ) - ( ( A ` i ) x. ( B ` j ) ) ) ) )
57 48 50 56 3eqtr2d 
 |-  ( ( ( ( A ` i ) e. CC /\ ( B ` i ) e. CC /\ ( C ` i ) e. CC ) /\ ( ( A ` j ) e. CC /\ ( B ` j ) e. CC /\ ( C ` j ) e. CC ) ) -> ( ( ( ( ( A ` i ) x. ( C ` j ) ) + ( ( B ` i ) x. ( A ` j ) ) ) - ( ( B ` i ) x. ( C ` j ) ) ) - ( ( A ` i ) x. ( B ` j ) ) ) = ( ( ( ( A ` i ) x. ( C ` j ) ) - ( ( B ` i ) x. ( C ` j ) ) ) + ( ( ( B ` i ) x. ( A ` j ) ) - ( ( A ` i ) x. ( B ` j ) ) ) ) )
58 21 28 subcld 
 |-  ( ( ( ( A ` i ) e. CC /\ ( B ` i ) e. CC /\ ( C ` i ) e. CC ) /\ ( ( A ` j ) e. CC /\ ( B ` j ) e. CC /\ ( C ` j ) e. CC ) ) -> ( ( ( A ` i ) x. ( C ` j ) ) - ( ( B ` i ) x. ( C ` j ) ) ) e. CC )
59 58 25 32 addsub12d 
 |-  ( ( ( ( A ` i ) e. CC /\ ( B ` i ) e. CC /\ ( C ` i ) e. CC ) /\ ( ( A ` j ) e. CC /\ ( B ` j ) e. CC /\ ( C ` j ) e. CC ) ) -> ( ( ( ( A ` i ) x. ( C ` j ) ) - ( ( B ` i ) x. ( C ` j ) ) ) + ( ( ( B ` i ) x. ( A ` j ) ) - ( ( A ` i ) x. ( B ` j ) ) ) ) = ( ( ( B ` i ) x. ( A ` j ) ) + ( ( ( ( A ` i ) x. ( C ` j ) ) - ( ( B ` i ) x. ( C ` j ) ) ) - ( ( A ` i ) x. ( B ` j ) ) ) ) )
60 21 28 32 subsub4d 
 |-  ( ( ( ( A ` i ) e. CC /\ ( B ` i ) e. CC /\ ( C ` i ) e. CC ) /\ ( ( A ` j ) e. CC /\ ( B ` j ) e. CC /\ ( C ` j ) e. CC ) ) -> ( ( ( ( A ` i ) x. ( C ` j ) ) - ( ( B ` i ) x. ( C ` j ) ) ) - ( ( A ` i ) x. ( B ` j ) ) ) = ( ( ( A ` i ) x. ( C ` j ) ) - ( ( ( B ` i ) x. ( C ` j ) ) + ( ( A ` i ) x. ( B ` j ) ) ) ) )
61 60 oveq2d 
 |-  ( ( ( ( A ` i ) e. CC /\ ( B ` i ) e. CC /\ ( C ` i ) e. CC ) /\ ( ( A ` j ) e. CC /\ ( B ` j ) e. CC /\ ( C ` j ) e. CC ) ) -> ( ( ( B ` i ) x. ( A ` j ) ) + ( ( ( ( A ` i ) x. ( C ` j ) ) - ( ( B ` i ) x. ( C ` j ) ) ) - ( ( A ` i ) x. ( B ` j ) ) ) ) = ( ( ( B ` i ) x. ( A ` j ) ) + ( ( ( A ` i ) x. ( C ` j ) ) - ( ( ( B ` i ) x. ( C ` j ) ) + ( ( A ` i ) x. ( B ` j ) ) ) ) ) )
62 57 59 61 3eqtrd 
 |-  ( ( ( ( A ` i ) e. CC /\ ( B ` i ) e. CC /\ ( C ` i ) e. CC ) /\ ( ( A ` j ) e. CC /\ ( B ` j ) e. CC /\ ( C ` j ) e. CC ) ) -> ( ( ( ( ( A ` i ) x. ( C ` j ) ) + ( ( B ` i ) x. ( A ` j ) ) ) - ( ( B ` i ) x. ( C ` j ) ) ) - ( ( A ` i ) x. ( B ` j ) ) ) = ( ( ( B ` i ) x. ( A ` j ) ) + ( ( ( A ` i ) x. ( C ` j ) ) - ( ( ( B ` i ) x. ( C ` j ) ) + ( ( A ` i ) x. ( B ` j ) ) ) ) ) )
63 62 eqeq1d 
 |-  ( ( ( ( A ` i ) e. CC /\ ( B ` i ) e. CC /\ ( C ` i ) e. CC ) /\ ( ( A ` j ) e. CC /\ ( B ` j ) e. CC /\ ( C ` j ) e. CC ) ) -> ( ( ( ( ( ( A ` i ) x. ( C ` j ) ) + ( ( B ` i ) x. ( A ` j ) ) ) - ( ( B ` i ) x. ( C ` j ) ) ) - ( ( A ` i ) x. ( B ` j ) ) ) = ( ( ( C ` i ) x. ( A ` j ) ) - ( ( C ` i ) x. ( B ` j ) ) ) <-> ( ( ( B ` i ) x. ( A ` j ) ) + ( ( ( A ` i ) x. ( C ` j ) ) - ( ( ( B ` i ) x. ( C ` j ) ) + ( ( A ` i ) x. ( B ` j ) ) ) ) ) = ( ( ( C ` i ) x. ( A ` j ) ) - ( ( C ` i ) x. ( B ` j ) ) ) ) )
64 32 35 addcld 
 |-  ( ( ( ( A ` i ) e. CC /\ ( B ` i ) e. CC /\ ( C ` i ) e. CC ) /\ ( ( A ` j ) e. CC /\ ( B ` j ) e. CC /\ ( C ` j ) e. CC ) ) -> ( ( ( A ` i ) x. ( B ` j ) ) + ( ( C ` i ) x. ( A ` j ) ) ) e. CC )
65 subeqrev 
 |-  ( ( ( ( ( ( A ` i ) x. ( C ` j ) ) + ( ( B ` i ) x. ( A ` j ) ) ) e. CC /\ ( ( B ` i ) x. ( C ` j ) ) e. CC ) /\ ( ( ( ( A ` i ) x. ( B ` j ) ) + ( ( C ` i ) x. ( A ` j ) ) ) e. CC /\ ( ( C ` i ) x. ( B ` j ) ) e. CC ) ) -> ( ( ( ( ( A ` i ) x. ( C ` j ) ) + ( ( B ` i ) x. ( A ` j ) ) ) - ( ( B ` i ) x. ( C ` j ) ) ) = ( ( ( ( A ` i ) x. ( B ` j ) ) + ( ( C ` i ) x. ( A ` j ) ) ) - ( ( C ` i ) x. ( B ` j ) ) ) <-> ( ( ( B ` i ) x. ( C ` j ) ) - ( ( ( A ` i ) x. ( C ` j ) ) + ( ( B ` i ) x. ( A ` j ) ) ) ) = ( ( ( C ` i ) x. ( B ` j ) ) - ( ( ( A ` i ) x. ( B ` j ) ) + ( ( C ` i ) x. ( A ` j ) ) ) ) ) )
66 26 28 64 37 65 syl22anc 
 |-  ( ( ( ( A ` i ) e. CC /\ ( B ` i ) e. CC /\ ( C ` i ) e. CC ) /\ ( ( A ` j ) e. CC /\ ( B ` j ) e. CC /\ ( C ` j ) e. CC ) ) -> ( ( ( ( ( A ` i ) x. ( C ` j ) ) + ( ( B ` i ) x. ( A ` j ) ) ) - ( ( B ` i ) x. ( C ` j ) ) ) = ( ( ( ( A ` i ) x. ( B ` j ) ) + ( ( C ` i ) x. ( A ` j ) ) ) - ( ( C ` i ) x. ( B ` j ) ) ) <-> ( ( ( B ` i ) x. ( C ` j ) ) - ( ( ( A ` i ) x. ( C ` j ) ) + ( ( B ` i ) x. ( A ` j ) ) ) ) = ( ( ( C ` i ) x. ( B ` j ) ) - ( ( ( A ` i ) x. ( B ` j ) ) + ( ( C ` i ) x. ( A ` j ) ) ) ) ) )
67 47 63 66 3bitr3rd 
 |-  ( ( ( ( A ` i ) e. CC /\ ( B ` i ) e. CC /\ ( C ` i ) e. CC ) /\ ( ( A ` j ) e. CC /\ ( B ` j ) e. CC /\ ( C ` j ) e. CC ) ) -> ( ( ( ( B ` i ) x. ( C ` j ) ) - ( ( ( A ` i ) x. ( C ` j ) ) + ( ( B ` i ) x. ( A ` j ) ) ) ) = ( ( ( C ` i ) x. ( B ` j ) ) - ( ( ( A ` i ) x. ( B ` j ) ) + ( ( C ` i ) x. ( A ` j ) ) ) ) <-> ( ( ( B ` i ) x. ( A ` j ) ) + ( ( ( A ` i ) x. ( C ` j ) ) - ( ( ( B ` i ) x. ( C ` j ) ) + ( ( A ` i ) x. ( B ` j ) ) ) ) ) = ( ( ( C ` i ) x. ( A ` j ) ) - ( ( C ` i ) x. ( B ` j ) ) ) ) )
68 21 49 subcld 
 |-  ( ( ( ( A ` i ) e. CC /\ ( B ` i ) e. CC /\ ( C ` i ) e. CC ) /\ ( ( A ` j ) e. CC /\ ( B ` j ) e. CC /\ ( C ` j ) e. CC ) ) -> ( ( ( A ` i ) x. ( C ` j ) ) - ( ( ( B ` i ) x. ( C ` j ) ) + ( ( A ` i ) x. ( B ` j ) ) ) ) e. CC )
69 25 68 38 addrsub 
 |-  ( ( ( ( A ` i ) e. CC /\ ( B ` i ) e. CC /\ ( C ` i ) e. CC ) /\ ( ( A ` j ) e. CC /\ ( B ` j ) e. CC /\ ( C ` j ) e. CC ) ) -> ( ( ( ( B ` i ) x. ( A ` j ) ) + ( ( ( A ` i ) x. ( C ` j ) ) - ( ( ( B ` i ) x. ( C ` j ) ) + ( ( A ` i ) x. ( B ` j ) ) ) ) ) = ( ( ( C ` i ) x. ( A ` j ) ) - ( ( C ` i ) x. ( B ` j ) ) ) <-> ( ( ( A ` i ) x. ( C ` j ) ) - ( ( ( B ` i ) x. ( C ` j ) ) + ( ( A ` i ) x. ( B ` j ) ) ) ) = ( ( ( ( C ` i ) x. ( A ` j ) ) - ( ( C ` i ) x. ( B ` j ) ) ) - ( ( B ` i ) x. ( A ` j ) ) ) ) )
70 35 37 25 sub32d 
 |-  ( ( ( ( A ` i ) e. CC /\ ( B ` i ) e. CC /\ ( C ` i ) e. CC ) /\ ( ( A ` j ) e. CC /\ ( B ` j ) e. CC /\ ( C ` j ) e. CC ) ) -> ( ( ( ( C ` i ) x. ( A ` j ) ) - ( ( C ` i ) x. ( B ` j ) ) ) - ( ( B ` i ) x. ( A ` j ) ) ) = ( ( ( ( C ` i ) x. ( A ` j ) ) - ( ( B ` i ) x. ( A ` j ) ) ) - ( ( C ` i ) x. ( B ` j ) ) ) )
71 35 25 37 subsub4d 
 |-  ( ( ( ( A ` i ) e. CC /\ ( B ` i ) e. CC /\ ( C ` i ) e. CC ) /\ ( ( A ` j ) e. CC /\ ( B ` j ) e. CC /\ ( C ` j ) e. CC ) ) -> ( ( ( ( C ` i ) x. ( A ` j ) ) - ( ( B ` i ) x. ( A ` j ) ) ) - ( ( C ` i ) x. ( B ` j ) ) ) = ( ( ( C ` i ) x. ( A ` j ) ) - ( ( ( B ` i ) x. ( A ` j ) ) + ( ( C ` i ) x. ( B ` j ) ) ) ) )
72 70 71 eqtrd 
 |-  ( ( ( ( A ` i ) e. CC /\ ( B ` i ) e. CC /\ ( C ` i ) e. CC ) /\ ( ( A ` j ) e. CC /\ ( B ` j ) e. CC /\ ( C ` j ) e. CC ) ) -> ( ( ( ( C ` i ) x. ( A ` j ) ) - ( ( C ` i ) x. ( B ` j ) ) ) - ( ( B ` i ) x. ( A ` j ) ) ) = ( ( ( C ` i ) x. ( A ` j ) ) - ( ( ( B ` i ) x. ( A ` j ) ) + ( ( C ` i ) x. ( B ` j ) ) ) ) )
73 72 eqeq2d 
 |-  ( ( ( ( A ` i ) e. CC /\ ( B ` i ) e. CC /\ ( C ` i ) e. CC ) /\ ( ( A ` j ) e. CC /\ ( B ` j ) e. CC /\ ( C ` j ) e. CC ) ) -> ( ( ( ( A ` i ) x. ( C ` j ) ) - ( ( ( B ` i ) x. ( C ` j ) ) + ( ( A ` i ) x. ( B ` j ) ) ) ) = ( ( ( ( C ` i ) x. ( A ` j ) ) - ( ( C ` i ) x. ( B ` j ) ) ) - ( ( B ` i ) x. ( A ` j ) ) ) <-> ( ( ( A ` i ) x. ( C ` j ) ) - ( ( ( B ` i ) x. ( C ` j ) ) + ( ( A ` i ) x. ( B ` j ) ) ) ) = ( ( ( C ` i ) x. ( A ` j ) ) - ( ( ( B ` i ) x. ( A ` j ) ) + ( ( C ` i ) x. ( B ` j ) ) ) ) ) )
74 69 73 bitrd 
 |-  ( ( ( ( A ` i ) e. CC /\ ( B ` i ) e. CC /\ ( C ` i ) e. CC ) /\ ( ( A ` j ) e. CC /\ ( B ` j ) e. CC /\ ( C ` j ) e. CC ) ) -> ( ( ( ( B ` i ) x. ( A ` j ) ) + ( ( ( A ` i ) x. ( C ` j ) ) - ( ( ( B ` i ) x. ( C ` j ) ) + ( ( A ` i ) x. ( B ` j ) ) ) ) ) = ( ( ( C ` i ) x. ( A ` j ) ) - ( ( C ` i ) x. ( B ` j ) ) ) <-> ( ( ( A ` i ) x. ( C ` j ) ) - ( ( ( B ` i ) x. ( C ` j ) ) + ( ( A ` i ) x. ( B ` j ) ) ) ) = ( ( ( C ` i ) x. ( A ` j ) ) - ( ( ( B ` i ) x. ( A ` j ) ) + ( ( C ` i ) x. ( B ` j ) ) ) ) ) )
75 eqcom 
 |-  ( ( ( ( A ` i ) x. ( C ` j ) ) - ( ( ( B ` i ) x. ( C ` j ) ) + ( ( A ` i ) x. ( B ` j ) ) ) ) = ( ( ( C ` i ) x. ( A ` j ) ) - ( ( ( B ` i ) x. ( A ` j ) ) + ( ( C ` i ) x. ( B ` j ) ) ) ) <-> ( ( ( C ` i ) x. ( A ` j ) ) - ( ( ( B ` i ) x. ( A ` j ) ) + ( ( C ` i ) x. ( B ` j ) ) ) ) = ( ( ( A ` i ) x. ( C ` j ) ) - ( ( ( B ` i ) x. ( C ` j ) ) + ( ( A ` i ) x. ( B ` j ) ) ) ) )
76 74 75 bitrdi 
 |-  ( ( ( ( A ` i ) e. CC /\ ( B ` i ) e. CC /\ ( C ` i ) e. CC ) /\ ( ( A ` j ) e. CC /\ ( B ` j ) e. CC /\ ( C ` j ) e. CC ) ) -> ( ( ( ( B ` i ) x. ( A ` j ) ) + ( ( ( A ` i ) x. ( C ` j ) ) - ( ( ( B ` i ) x. ( C ` j ) ) + ( ( A ` i ) x. ( B ` j ) ) ) ) ) = ( ( ( C ` i ) x. ( A ` j ) ) - ( ( C ` i ) x. ( B ` j ) ) ) <-> ( ( ( C ` i ) x. ( A ` j ) ) - ( ( ( B ` i ) x. ( A ` j ) ) + ( ( C ` i ) x. ( B ` j ) ) ) ) = ( ( ( A ` i ) x. ( C ` j ) ) - ( ( ( B ` i ) x. ( C ` j ) ) + ( ( A ` i ) x. ( B ` j ) ) ) ) ) )
77 67 76 bitrd 
 |-  ( ( ( ( A ` i ) e. CC /\ ( B ` i ) e. CC /\ ( C ` i ) e. CC ) /\ ( ( A ` j ) e. CC /\ ( B ` j ) e. CC /\ ( C ` j ) e. CC ) ) -> ( ( ( ( B ` i ) x. ( C ` j ) ) - ( ( ( A ` i ) x. ( C ` j ) ) + ( ( B ` i ) x. ( A ` j ) ) ) ) = ( ( ( C ` i ) x. ( B ` j ) ) - ( ( ( A ` i ) x. ( B ` j ) ) + ( ( C ` i ) x. ( A ` j ) ) ) ) <-> ( ( ( C ` i ) x. ( A ` j ) ) - ( ( ( B ` i ) x. ( A ` j ) ) + ( ( C ` i ) x. ( B ` j ) ) ) ) = ( ( ( A ` i ) x. ( C ` j ) ) - ( ( ( B ` i ) x. ( C ` j ) ) + ( ( A ` i ) x. ( B ` j ) ) ) ) ) )
78 colinearalglem1 
 |-  ( ( ( ( A ` i ) e. CC /\ ( B ` i ) e. CC /\ ( C ` i ) e. CC ) /\ ( ( A ` j ) e. CC /\ ( B ` j ) e. CC /\ ( C ` j ) e. CC ) ) -> ( ( ( ( B ` i ) - ( A ` i ) ) x. ( ( C ` j ) - ( A ` j ) ) ) = ( ( ( B ` j ) - ( A ` j ) ) x. ( ( C ` i ) - ( A ` i ) ) ) <-> ( ( ( B ` i ) x. ( C ` j ) ) - ( ( ( A ` i ) x. ( C ` j ) ) + ( ( B ` i ) x. ( A ` j ) ) ) ) = ( ( ( C ` i ) x. ( B ` j ) ) - ( ( ( A ` i ) x. ( B ` j ) ) + ( ( C ` i ) x. ( A ` j ) ) ) ) ) )
79 3anrot 
 |-  ( ( ( A ` i ) e. CC /\ ( B ` i ) e. CC /\ ( C ` i ) e. CC ) <-> ( ( B ` i ) e. CC /\ ( C ` i ) e. CC /\ ( A ` i ) e. CC ) )
80 3anrot 
 |-  ( ( ( A ` j ) e. CC /\ ( B ` j ) e. CC /\ ( C ` j ) e. CC ) <-> ( ( B ` j ) e. CC /\ ( C ` j ) e. CC /\ ( A ` j ) e. CC ) )
81 colinearalglem1 
 |-  ( ( ( ( B ` i ) e. CC /\ ( C ` i ) e. CC /\ ( A ` i ) e. CC ) /\ ( ( B ` j ) e. CC /\ ( C ` j ) e. CC /\ ( A ` j ) e. CC ) ) -> ( ( ( ( C ` i ) - ( B ` i ) ) x. ( ( A ` j ) - ( B ` j ) ) ) = ( ( ( C ` j ) - ( B ` j ) ) x. ( ( A ` i ) - ( B ` i ) ) ) <-> ( ( ( C ` i ) x. ( A ` j ) ) - ( ( ( B ` i ) x. ( A ` j ) ) + ( ( C ` i ) x. ( B ` j ) ) ) ) = ( ( ( A ` i ) x. ( C ` j ) ) - ( ( ( B ` i ) x. ( C ` j ) ) + ( ( A ` i ) x. ( B ` j ) ) ) ) ) )
82 79 80 81 syl2anb 
 |-  ( ( ( ( A ` i ) e. CC /\ ( B ` i ) e. CC /\ ( C ` i ) e. CC ) /\ ( ( A ` j ) e. CC /\ ( B ` j ) e. CC /\ ( C ` j ) e. CC ) ) -> ( ( ( ( C ` i ) - ( B ` i ) ) x. ( ( A ` j ) - ( B ` j ) ) ) = ( ( ( C ` j ) - ( B ` j ) ) x. ( ( A ` i ) - ( B ` i ) ) ) <-> ( ( ( C ` i ) x. ( A ` j ) ) - ( ( ( B ` i ) x. ( A ` j ) ) + ( ( C ` i ) x. ( B ` j ) ) ) ) = ( ( ( A ` i ) x. ( C ` j ) ) - ( ( ( B ` i ) x. ( C ` j ) ) + ( ( A ` i ) x. ( B ` j ) ) ) ) ) )
83 77 78 82 3bitr4d 
 |-  ( ( ( ( A ` i ) e. CC /\ ( B ` i ) e. CC /\ ( C ` i ) e. CC ) /\ ( ( A ` j ) e. CC /\ ( B ` j ) e. CC /\ ( C ` j ) e. CC ) ) -> ( ( ( ( B ` i ) - ( A ` i ) ) x. ( ( C ` j ) - ( A ` j ) ) ) = ( ( ( B ` j ) - ( A ` j ) ) x. ( ( C ` i ) - ( A ` i ) ) ) <-> ( ( ( C ` i ) - ( B ` i ) ) x. ( ( A ` j ) - ( B ` j ) ) ) = ( ( ( C ` j ) - ( B ` j ) ) x. ( ( A ` i ) - ( B ` i ) ) ) ) )
84 4 7 10 13 15 17 83 syl33anc 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( i e. ( 1 ... N ) /\ j e. ( 1 ... N ) ) ) -> ( ( ( ( B ` i ) - ( A ` i ) ) x. ( ( C ` j ) - ( A ` j ) ) ) = ( ( ( B ` j ) - ( A ` j ) ) x. ( ( C ` i ) - ( A ` i ) ) ) <-> ( ( ( C ` i ) - ( B ` i ) ) x. ( ( A ` j ) - ( B ` j ) ) ) = ( ( ( C ` j ) - ( B ` j ) ) x. ( ( A ` i ) - ( B ` i ) ) ) ) )
85 84 2ralbidva 
 |-  ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) -> ( A. i e. ( 1 ... N ) A. j e. ( 1 ... N ) ( ( ( B ` i ) - ( A ` i ) ) x. ( ( C ` j ) - ( A ` j ) ) ) = ( ( ( B ` j ) - ( A ` j ) ) x. ( ( C ` i ) - ( A ` i ) ) ) <-> A. i e. ( 1 ... N ) A. j e. ( 1 ... N ) ( ( ( C ` i ) - ( B ` i ) ) x. ( ( A ` j ) - ( B ` j ) ) ) = ( ( ( C ` j ) - ( B ` j ) ) x. ( ( A ` i ) - ( B ` i ) ) ) ) )