Metamath Proof Explorer

Theorem colineardim1

Description: If A is colinear with B and C , then A is in the same space as B . (Contributed by Scott Fenton, 25-Oct-2013) (Revised by Mario Carneiro, 19-Apr-2014)

Ref Expression
Assertion colineardim1 
|- ( ( N e. NN /\ ( A e. V /\ B e. ( EE ` N ) /\ C e. W ) ) -> ( A Colinear <. B , C >. -> A e. ( EE ` N ) ) )

Proof

Step Hyp Ref Expression
1 df-colinear 
 |-  Colinear = `' { <. <. b , c >. , a >. | E. n e. NN ( ( a e. ( EE ` n ) /\ b e. ( EE ` n ) /\ c e. ( EE ` n ) ) /\ ( a Btwn <. b , c >. \/ b Btwn <. c , a >. \/ c Btwn <. a , b >. ) ) }
2 1 breqi 
 |-  ( A Colinear <. B , C >. <-> A `' { <. <. b , c >. , a >. | E. n e. NN ( ( a e. ( EE ` n ) /\ b e. ( EE ` n ) /\ c e. ( EE ` n ) ) /\ ( a Btwn <. b , c >. \/ b Btwn <. c , a >. \/ c Btwn <. a , b >. ) ) } <. B , C >. )
3 simpr1 
 |-  ( ( N e. NN /\ ( A e. V /\ B e. ( EE ` N ) /\ C e. W ) ) -> A e. V )
4 opex 
 |-  <. B , C >. e. _V
5 brcnvg 
 |-  ( ( A e. V /\ <. B , C >. e. _V ) -> ( A `' { <. <. b , c >. , a >. | E. n e. NN ( ( a e. ( EE ` n ) /\ b e. ( EE ` n ) /\ c e. ( EE ` n ) ) /\ ( a Btwn <. b , c >. \/ b Btwn <. c , a >. \/ c Btwn <. a , b >. ) ) } <. B , C >. <-> <. B , C >. { <. <. b , c >. , a >. | E. n e. NN ( ( a e. ( EE ` n ) /\ b e. ( EE ` n ) /\ c e. ( EE ` n ) ) /\ ( a Btwn <. b , c >. \/ b Btwn <. c , a >. \/ c Btwn <. a , b >. ) ) } A ) )
6 3 4 5 sylancl 
 |-  ( ( N e. NN /\ ( A e. V /\ B e. ( EE ` N ) /\ C e. W ) ) -> ( A `' { <. <. b , c >. , a >. | E. n e. NN ( ( a e. ( EE ` n ) /\ b e. ( EE ` n ) /\ c e. ( EE ` n ) ) /\ ( a Btwn <. b , c >. \/ b Btwn <. c , a >. \/ c Btwn <. a , b >. ) ) } <. B , C >. <-> <. B , C >. { <. <. b , c >. , a >. | E. n e. NN ( ( a e. ( EE ` n ) /\ b e. ( EE ` n ) /\ c e. ( EE ` n ) ) /\ ( a Btwn <. b , c >. \/ b Btwn <. c , a >. \/ c Btwn <. a , b >. ) ) } A ) )
7 df-br 
 |-  ( <. B , C >. { <. <. b , c >. , a >. | E. n e. NN ( ( a e. ( EE ` n ) /\ b e. ( EE ` n ) /\ c e. ( EE ` n ) ) /\ ( a Btwn <. b , c >. \/ b Btwn <. c , a >. \/ c Btwn <. a , b >. ) ) } A <-> <. <. B , C >. , A >. e. { <. <. b , c >. , a >. | E. n e. NN ( ( a e. ( EE ` n ) /\ b e. ( EE ` n ) /\ c e. ( EE ` n ) ) /\ ( a Btwn <. b , c >. \/ b Btwn <. c , a >. \/ c Btwn <. a , b >. ) ) } )
8 eleq1 
 |-  ( b = B -> ( b e. ( EE ` n ) <-> B e. ( EE ` n ) ) )
9 8 3anbi2d 
 |-  ( b = B -> ( ( a e. ( EE ` n ) /\ b e. ( EE ` n ) /\ c e. ( EE ` n ) ) <-> ( a e. ( EE ` n ) /\ B e. ( EE ` n ) /\ c e. ( EE ` n ) ) ) )
10 opeq1 
 |-  ( b = B -> <. b , c >. = <. B , c >. )
11 10 breq2d 
 |-  ( b = B -> ( a Btwn <. b , c >. <-> a Btwn <. B , c >. ) )
12 breq1 
 |-  ( b = B -> ( b Btwn <. c , a >. <-> B Btwn <. c , a >. ) )
13 opeq2 
 |-  ( b = B -> <. a , b >. = <. a , B >. )
14 13 breq2d 
 |-  ( b = B -> ( c Btwn <. a , b >. <-> c Btwn <. a , B >. ) )
15 11 12 14 3orbi123d 
 |-  ( b = B -> ( ( a Btwn <. b , c >. \/ b Btwn <. c , a >. \/ c Btwn <. a , b >. ) <-> ( a Btwn <. B , c >. \/ B Btwn <. c , a >. \/ c Btwn <. a , B >. ) ) )
16 9 15 anbi12d 
 |-  ( b = B -> ( ( ( a e. ( EE ` n ) /\ b e. ( EE ` n ) /\ c e. ( EE ` n ) ) /\ ( a Btwn <. b , c >. \/ b Btwn <. c , a >. \/ c Btwn <. a , b >. ) ) <-> ( ( a e. ( EE ` n ) /\ B e. ( EE ` n ) /\ c e. ( EE ` n ) ) /\ ( a Btwn <. B , c >. \/ B Btwn <. c , a >. \/ c Btwn <. a , B >. ) ) ) )
17 16 rexbidv 
 |-  ( b = B -> ( E. n e. NN ( ( a e. ( EE ` n ) /\ b e. ( EE ` n ) /\ c e. ( EE ` n ) ) /\ ( a Btwn <. b , c >. \/ b Btwn <. c , a >. \/ c Btwn <. a , b >. ) ) <-> E. n e. NN ( ( a e. ( EE ` n ) /\ B e. ( EE ` n ) /\ c e. ( EE ` n ) ) /\ ( a Btwn <. B , c >. \/ B Btwn <. c , a >. \/ c Btwn <. a , B >. ) ) ) )
18 eleq1 
 |-  ( c = C -> ( c e. ( EE ` n ) <-> C e. ( EE ` n ) ) )
19 18 3anbi3d 
 |-  ( c = C -> ( ( a e. ( EE ` n ) /\ B e. ( EE ` n ) /\ c e. ( EE ` n ) ) <-> ( a e. ( EE ` n ) /\ B e. ( EE ` n ) /\ C e. ( EE ` n ) ) ) )
20 opeq2 
 |-  ( c = C -> <. B , c >. = <. B , C >. )
21 20 breq2d 
 |-  ( c = C -> ( a Btwn <. B , c >. <-> a Btwn <. B , C >. ) )
22 opeq1 
 |-  ( c = C -> <. c , a >. = <. C , a >. )
23 22 breq2d 
 |-  ( c = C -> ( B Btwn <. c , a >. <-> B Btwn <. C , a >. ) )
24 breq1 
 |-  ( c = C -> ( c Btwn <. a , B >. <-> C Btwn <. a , B >. ) )
25 21 23 24 3orbi123d 
 |-  ( c = C -> ( ( a Btwn <. B , c >. \/ B Btwn <. c , a >. \/ c Btwn <. a , B >. ) <-> ( a Btwn <. B , C >. \/ B Btwn <. C , a >. \/ C Btwn <. a , B >. ) ) )
26 19 25 anbi12d 
 |-  ( c = C -> ( ( ( a e. ( EE ` n ) /\ B e. ( EE ` n ) /\ c e. ( EE ` n ) ) /\ ( a Btwn <. B , c >. \/ B Btwn <. c , a >. \/ c Btwn <. a , B >. ) ) <-> ( ( a e. ( EE ` n ) /\ B e. ( EE ` n ) /\ C e. ( EE ` n ) ) /\ ( a Btwn <. B , C >. \/ B Btwn <. C , a >. \/ C Btwn <. a , B >. ) ) ) )
27 26 rexbidv 
 |-  ( c = C -> ( E. n e. NN ( ( a e. ( EE ` n ) /\ B e. ( EE ` n ) /\ c e. ( EE ` n ) ) /\ ( a Btwn <. B , c >. \/ B Btwn <. c , a >. \/ c Btwn <. a , B >. ) ) <-> E. n e. NN ( ( a e. ( EE ` n ) /\ B e. ( EE ` n ) /\ C e. ( EE ` n ) ) /\ ( a Btwn <. B , C >. \/ B Btwn <. C , a >. \/ C Btwn <. a , B >. ) ) ) )
28 eleq1 
 |-  ( a = A -> ( a e. ( EE ` n ) <-> A e. ( EE ` n ) ) )
29 28 3anbi1d 
 |-  ( a = A -> ( ( a e. ( EE ` n ) /\ B e. ( EE ` n ) /\ C e. ( EE ` n ) ) <-> ( A e. ( EE ` n ) /\ B e. ( EE ` n ) /\ C e. ( EE ` n ) ) ) )
30 breq1 
 |-  ( a = A -> ( a Btwn <. B , C >. <-> A Btwn <. B , C >. ) )
31 opeq2 
 |-  ( a = A -> <. C , a >. = <. C , A >. )
32 31 breq2d 
 |-  ( a = A -> ( B Btwn <. C , a >. <-> B Btwn <. C , A >. ) )
33 opeq1 
 |-  ( a = A -> <. a , B >. = <. A , B >. )
34 33 breq2d 
 |-  ( a = A -> ( C Btwn <. a , B >. <-> C Btwn <. A , B >. ) )
35 30 32 34 3orbi123d 
 |-  ( a = A -> ( ( a Btwn <. B , C >. \/ B Btwn <. C , a >. \/ C Btwn <. a , B >. ) <-> ( A Btwn <. B , C >. \/ B Btwn <. C , A >. \/ C Btwn <. A , B >. ) ) )
36 29 35 anbi12d 
 |-  ( a = A -> ( ( ( a e. ( EE ` n ) /\ B e. ( EE ` n ) /\ C e. ( EE ` n ) ) /\ ( a Btwn <. B , C >. \/ B Btwn <. C , a >. \/ C Btwn <. a , B >. ) ) <-> ( ( A e. ( EE ` n ) /\ B e. ( EE ` n ) /\ C e. ( EE ` n ) ) /\ ( A Btwn <. B , C >. \/ B Btwn <. C , A >. \/ C Btwn <. A , B >. ) ) ) )
37 36 rexbidv 
 |-  ( a = A -> ( E. n e. NN ( ( a e. ( EE ` n ) /\ B e. ( EE ` n ) /\ C e. ( EE ` n ) ) /\ ( a Btwn <. B , C >. \/ B Btwn <. C , a >. \/ C Btwn <. a , B >. ) ) <-> E. n e. NN ( ( A e. ( EE ` n ) /\ B e. ( EE ` n ) /\ C e. ( EE ` n ) ) /\ ( A Btwn <. B , C >. \/ B Btwn <. C , A >. \/ C Btwn <. A , B >. ) ) ) )
38 17 27 37 eloprabg 
 |-  ( ( B e. ( EE ` N ) /\ C e. W /\ A e. V ) -> ( <. <. B , C >. , A >. e. { <. <. b , c >. , a >. | E. n e. NN ( ( a e. ( EE ` n ) /\ b e. ( EE ` n ) /\ c e. ( EE ` n ) ) /\ ( a Btwn <. b , c >. \/ b Btwn <. c , a >. \/ c Btwn <. a , b >. ) ) } <-> E. n e. NN ( ( A e. ( EE ` n ) /\ B e. ( EE ` n ) /\ C e. ( EE ` n ) ) /\ ( A Btwn <. B , C >. \/ B Btwn <. C , A >. \/ C Btwn <. A , B >. ) ) ) )
39 38 3comr 
 |-  ( ( A e. V /\ B e. ( EE ` N ) /\ C e. W ) -> ( <. <. B , C >. , A >. e. { <. <. b , c >. , a >. | E. n e. NN ( ( a e. ( EE ` n ) /\ b e. ( EE ` n ) /\ c e. ( EE ` n ) ) /\ ( a Btwn <. b , c >. \/ b Btwn <. c , a >. \/ c Btwn <. a , b >. ) ) } <-> E. n e. NN ( ( A e. ( EE ` n ) /\ B e. ( EE ` n ) /\ C e. ( EE ` n ) ) /\ ( A Btwn <. B , C >. \/ B Btwn <. C , A >. \/ C Btwn <. A , B >. ) ) ) )
40 39 adantl 
 |-  ( ( N e. NN /\ ( A e. V /\ B e. ( EE ` N ) /\ C e. W ) ) -> ( <. <. B , C >. , A >. e. { <. <. b , c >. , a >. | E. n e. NN ( ( a e. ( EE ` n ) /\ b e. ( EE ` n ) /\ c e. ( EE ` n ) ) /\ ( a Btwn <. b , c >. \/ b Btwn <. c , a >. \/ c Btwn <. a , b >. ) ) } <-> E. n e. NN ( ( A e. ( EE ` n ) /\ B e. ( EE ` n ) /\ C e. ( EE ` n ) ) /\ ( A Btwn <. B , C >. \/ B Btwn <. C , A >. \/ C Btwn <. A , B >. ) ) ) )
41 simpl 
 |-  ( ( ( A e. ( EE ` n ) /\ B e. ( EE ` n ) /\ C e. ( EE ` n ) ) /\ ( A Btwn <. B , C >. \/ B Btwn <. C , A >. \/ C Btwn <. A , B >. ) ) -> ( A e. ( EE ` n ) /\ B e. ( EE ` n ) /\ C e. ( EE ` n ) ) )
42 simp2 
 |-  ( ( A e. V /\ B e. ( EE ` N ) /\ C e. W ) -> B e. ( EE ` N ) )
43 42 anim2i 
 |-  ( ( N e. NN /\ ( A e. V /\ B e. ( EE ` N ) /\ C e. W ) ) -> ( N e. NN /\ B e. ( EE ` N ) ) )
44 3simpa 
 |-  ( ( A e. ( EE ` n ) /\ B e. ( EE ` n ) /\ C e. ( EE ` n ) ) -> ( A e. ( EE ` n ) /\ B e. ( EE ` n ) ) )
45 44 anim2i 
 |-  ( ( n e. NN /\ ( A e. ( EE ` n ) /\ B e. ( EE ` n ) /\ C e. ( EE ` n ) ) ) -> ( n e. NN /\ ( A e. ( EE ` n ) /\ B e. ( EE ` n ) ) ) )
46 axdimuniq 
 |-  ( ( ( N e. NN /\ B e. ( EE ` N ) ) /\ ( n e. NN /\ B e. ( EE ` n ) ) ) -> N = n )
47 46 adantrrl 
 |-  ( ( ( N e. NN /\ B e. ( EE ` N ) ) /\ ( n e. NN /\ ( A e. ( EE ` n ) /\ B e. ( EE ` n ) ) ) ) -> N = n )
48 simprrl 
 |-  ( ( ( N e. NN /\ B e. ( EE ` N ) ) /\ ( n e. NN /\ ( A e. ( EE ` n ) /\ B e. ( EE ` n ) ) ) ) -> A e. ( EE ` n ) )
49 fveq2 
 |-  ( N = n -> ( EE ` N ) = ( EE ` n ) )
50 49 eleq2d 
 |-  ( N = n -> ( A e. ( EE ` N ) <-> A e. ( EE ` n ) ) )
51 48 50 syl5ibrcom 
 |-  ( ( ( N e. NN /\ B e. ( EE ` N ) ) /\ ( n e. NN /\ ( A e. ( EE ` n ) /\ B e. ( EE ` n ) ) ) ) -> ( N = n -> A e. ( EE ` N ) ) )
52 47 51 mpd 
 |-  ( ( ( N e. NN /\ B e. ( EE ` N ) ) /\ ( n e. NN /\ ( A e. ( EE ` n ) /\ B e. ( EE ` n ) ) ) ) -> A e. ( EE ` N ) )
53 43 45 52 syl2an 
 |-  ( ( ( N e. NN /\ ( A e. V /\ B e. ( EE ` N ) /\ C e. W ) ) /\ ( n e. NN /\ ( A e. ( EE ` n ) /\ B e. ( EE ` n ) /\ C e. ( EE ` n ) ) ) ) -> A e. ( EE ` N ) )
54 53 exp32 
 |-  ( ( N e. NN /\ ( A e. V /\ B e. ( EE ` N ) /\ C e. W ) ) -> ( n e. NN -> ( ( A e. ( EE ` n ) /\ B e. ( EE ` n ) /\ C e. ( EE ` n ) ) -> A e. ( EE ` N ) ) ) )
55 41 54 syl7 
 |-  ( ( N e. NN /\ ( A e. V /\ B e. ( EE ` N ) /\ C e. W ) ) -> ( n e. NN -> ( ( ( A e. ( EE ` n ) /\ B e. ( EE ` n ) /\ C e. ( EE ` n ) ) /\ ( A Btwn <. B , C >. \/ B Btwn <. C , A >. \/ C Btwn <. A , B >. ) ) -> A e. ( EE ` N ) ) ) )
56 55 rexlimdv 
 |-  ( ( N e. NN /\ ( A e. V /\ B e. ( EE ` N ) /\ C e. W ) ) -> ( E. n e. NN ( ( A e. ( EE ` n ) /\ B e. ( EE ` n ) /\ C e. ( EE ` n ) ) /\ ( A Btwn <. B , C >. \/ B Btwn <. C , A >. \/ C Btwn <. A , B >. ) ) -> A e. ( EE ` N ) ) )
57 40 56 sylbid 
 |-  ( ( N e. NN /\ ( A e. V /\ B e. ( EE ` N ) /\ C e. W ) ) -> ( <. <. B , C >. , A >. e. { <. <. b , c >. , a >. | E. n e. NN ( ( a e. ( EE ` n ) /\ b e. ( EE ` n ) /\ c e. ( EE ` n ) ) /\ ( a Btwn <. b , c >. \/ b Btwn <. c , a >. \/ c Btwn <. a , b >. ) ) } -> A e. ( EE ` N ) ) )
58 7 57 syl5bi 
 |-  ( ( N e. NN /\ ( A e. V /\ B e. ( EE ` N ) /\ C e. W ) ) -> ( <. B , C >. { <. <. b , c >. , a >. | E. n e. NN ( ( a e. ( EE ` n ) /\ b e. ( EE ` n ) /\ c e. ( EE ` n ) ) /\ ( a Btwn <. b , c >. \/ b Btwn <. c , a >. \/ c Btwn <. a , b >. ) ) } A -> A e. ( EE ` N ) ) )
59 6 58 sylbid 
 |-  ( ( N e. NN /\ ( A e. V /\ B e. ( EE ` N ) /\ C e. W ) ) -> ( A `' { <. <. b , c >. , a >. | E. n e. NN ( ( a e. ( EE ` n ) /\ b e. ( EE ` n ) /\ c e. ( EE ` n ) ) /\ ( a Btwn <. b , c >. \/ b Btwn <. c , a >. \/ c Btwn <. a , b >. ) ) } <. B , C >. -> A e. ( EE ` N ) ) )
60 2 59 syl5bi 
 |-  ( ( N e. NN /\ ( A e. V /\ B e. ( EE ` N ) /\ C e. W ) ) -> ( A Colinear <. B , C >. -> A e. ( EE ` N ) ) )