Metamath Proof Explorer


Theorem brcolinear

Description: The binary relation form of the colinearity predicate. (Contributed by Scott Fenton, 5-Oct-2013)

Ref Expression
Assertion brcolinear NA𝔼NB𝔼NC𝔼NAColinearBCABtwnBCBBtwnCACBtwnAB

Proof

Step Hyp Ref Expression
1 brcolinear2 B𝔼NC𝔼NAColinearBCnA𝔼nB𝔼nC𝔼nABtwnBCBBtwnCACBtwnAB
2 1 3adant1 A𝔼NB𝔼NC𝔼NAColinearBCnA𝔼nB𝔼nC𝔼nABtwnBCBBtwnCACBtwnAB
3 2 adantl NA𝔼NB𝔼NC𝔼NAColinearBCnA𝔼nB𝔼nC𝔼nABtwnBCBBtwnCACBtwnAB
4 simpr A𝔼nB𝔼nC𝔼nABtwnBCBBtwnCACBtwnABABtwnBCBBtwnCACBtwnAB
5 4 rexlimivw nA𝔼nB𝔼nC𝔼nABtwnBCBBtwnCACBtwnABABtwnBCBBtwnCACBtwnAB
6 fveq2 n=N𝔼n=𝔼N
7 6 eleq2d n=NA𝔼nA𝔼N
8 6 eleq2d n=NB𝔼nB𝔼N
9 6 eleq2d n=NC𝔼nC𝔼N
10 7 8 9 3anbi123d n=NA𝔼nB𝔼nC𝔼nA𝔼NB𝔼NC𝔼N
11 10 anbi1d n=NA𝔼nB𝔼nC𝔼nABtwnBCBBtwnCACBtwnABA𝔼NB𝔼NC𝔼NABtwnBCBBtwnCACBtwnAB
12 11 rspcev NA𝔼NB𝔼NC𝔼NABtwnBCBBtwnCACBtwnABnA𝔼nB𝔼nC𝔼nABtwnBCBBtwnCACBtwnAB
13 12 expr NA𝔼NB𝔼NC𝔼NABtwnBCBBtwnCACBtwnABnA𝔼nB𝔼nC𝔼nABtwnBCBBtwnCACBtwnAB
14 5 13 impbid2 NA𝔼NB𝔼NC𝔼NnA𝔼nB𝔼nC𝔼nABtwnBCBBtwnCACBtwnABABtwnBCBBtwnCACBtwnAB
15 3 14 bitrd NA𝔼NB𝔼NC𝔼NAColinearBCABtwnBCBBtwnCACBtwnAB