Metamath Proof Explorer

Theorem colinearalglem3

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

Ref Expression
Assertion colinearalglem3 
|- ( ( 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 ) ( ( ( A ` i ) - ( C ` i ) ) x. ( ( B ` j ) - ( C ` j ) ) ) = ( ( ( A ` j ) - ( C ` j ) ) x. ( ( B ` i ) - ( C ` i ) ) ) ) )

Proof

Step Hyp Ref Expression
1 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 ) ) ) ) )
2 colinearalglem2 
 |-  ( ( B e. ( EE ` N ) /\ C e. ( EE ` N ) /\ A e. ( EE ` N ) ) -> ( 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 ) ) ) <-> A. i e. ( 1 ... N ) A. j e. ( 1 ... N ) ( ( ( A ` i ) - ( C ` i ) ) x. ( ( B ` j ) - ( C ` j ) ) ) = ( ( ( A ` j ) - ( C ` j ) ) x. ( ( B ` i ) - ( C ` i ) ) ) ) )
3 2 3comr 
 |-  ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) -> ( 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 ) ) ) <-> A. i e. ( 1 ... N ) A. j e. ( 1 ... N ) ( ( ( A ` i ) - ( C ` i ) ) x. ( ( B ` j ) - ( C ` j ) ) ) = ( ( ( A ` j ) - ( C ` j ) ) x. ( ( B ` i ) - ( C ` i ) ) ) ) )
4 1 3 bitrd 
 |-  ( ( 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 ) ( ( ( A ` i ) - ( C ` i ) ) x. ( ( B ` j ) - ( C ` j ) ) ) = ( ( ( A ` j ) - ( C ` j ) ) x. ( ( B ` i ) - ( C ` i ) ) ) ) )