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 A V B 𝔼 N C W A Colinear B C A 𝔼 N

Proof

Step Hyp Ref Expression
1 df-colinear Colinear = b c a | n a 𝔼 n b 𝔼 n c 𝔼 n a Btwn b c b Btwn c a c Btwn a b -1
2 1 breqi A Colinear B C A b c a | n a 𝔼 n b 𝔼 n c 𝔼 n a Btwn b c b Btwn c a c Btwn a b -1 B C
3 simpr1 N A V B 𝔼 N C W A V
4 opex B C V
5 brcnvg A V B C V A b c a | n a 𝔼 n b 𝔼 n c 𝔼 n a Btwn b c b Btwn c a c Btwn a b -1 B C B C b c a | n a 𝔼 n b 𝔼 n c 𝔼 n a Btwn b c b Btwn c a c Btwn a b A
6 3 4 5 sylancl N A V B 𝔼 N C W A b c a | n a 𝔼 n b 𝔼 n c 𝔼 n a Btwn b c b Btwn c a c Btwn a b -1 B C B C b c a | n a 𝔼 n b 𝔼 n c 𝔼 n a Btwn b c b Btwn c a c Btwn a b A
7 df-br B C b c a | n a 𝔼 n b 𝔼 n c 𝔼 n a Btwn b c b Btwn c a c Btwn a b A B C A b c a | n a 𝔼 n b 𝔼 n c 𝔼 n a Btwn b c b Btwn c a c Btwn a b
8 eleq1 b = B b 𝔼 n B 𝔼 n
9 8 3anbi2d b = B a 𝔼 n b 𝔼 n c 𝔼 n a 𝔼 n B 𝔼 n c 𝔼 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 𝔼 n b 𝔼 n c 𝔼 n a Btwn b c b Btwn c a c Btwn a b a 𝔼 n B 𝔼 n c 𝔼 n a Btwn B c B Btwn c a c Btwn a B
17 16 rexbidv b = B n a 𝔼 n b 𝔼 n c 𝔼 n a Btwn b c b Btwn c a c Btwn a b n a 𝔼 n B 𝔼 n c 𝔼 n a Btwn B c B Btwn c a c Btwn a B
18 eleq1 c = C c 𝔼 n C 𝔼 n
19 18 3anbi3d c = C a 𝔼 n B 𝔼 n c 𝔼 n a 𝔼 n B 𝔼 n C 𝔼 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 𝔼 n B 𝔼 n c 𝔼 n a Btwn B c B Btwn c a c Btwn a B a 𝔼 n B 𝔼 n C 𝔼 n a Btwn B C B Btwn C a C Btwn a B
27 26 rexbidv c = C n a 𝔼 n B 𝔼 n c 𝔼 n a Btwn B c B Btwn c a c Btwn a B n a 𝔼 n B 𝔼 n C 𝔼 n a Btwn B C B Btwn C a C Btwn a B
28 eleq1 a = A a 𝔼 n A 𝔼 n
29 28 3anbi1d a = A a 𝔼 n B 𝔼 n C 𝔼 n A 𝔼 n B 𝔼 n C 𝔼 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 𝔼 n B 𝔼 n C 𝔼 n a Btwn B C B Btwn C a C Btwn a B A 𝔼 n B 𝔼 n C 𝔼 n A Btwn B C B Btwn C A C Btwn A B
37 36 rexbidv a = A n a 𝔼 n B 𝔼 n C 𝔼 n a Btwn B C B Btwn C a C Btwn a B n A 𝔼 n B 𝔼 n C 𝔼 n A Btwn B C B Btwn C A C Btwn A B
38 17 27 37 eloprabg B 𝔼 N C W A V B C A b c a | n a 𝔼 n b 𝔼 n c 𝔼 n a Btwn b c b Btwn c a c Btwn a b n A 𝔼 n B 𝔼 n C 𝔼 n A Btwn B C B Btwn C A C Btwn A B
39 38 3comr A V B 𝔼 N C W B C A b c a | n a 𝔼 n b 𝔼 n c 𝔼 n a Btwn b c b Btwn c a c Btwn a b n A 𝔼 n B 𝔼 n C 𝔼 n A Btwn B C B Btwn C A C Btwn A B
40 39 adantl N A V B 𝔼 N C W B C A b c a | n a 𝔼 n b 𝔼 n c 𝔼 n a Btwn b c b Btwn c a c Btwn a b n A 𝔼 n B 𝔼 n C 𝔼 n A Btwn B C B Btwn C A C Btwn A B
41 simpl A 𝔼 n B 𝔼 n C 𝔼 n A Btwn B C B Btwn C A C Btwn A B A 𝔼 n B 𝔼 n C 𝔼 n
42 simp2 A V B 𝔼 N C W B 𝔼 N
43 42 anim2i N A V B 𝔼 N C W N B 𝔼 N
44 3simpa A 𝔼 n B 𝔼 n C 𝔼 n A 𝔼 n B 𝔼 n
45 44 anim2i n A 𝔼 n B 𝔼 n C 𝔼 n n A 𝔼 n B 𝔼 n
46 axdimuniq N B 𝔼 N n B 𝔼 n N = n
47 46 adantrrl N B 𝔼 N n A 𝔼 n B 𝔼 n N = n
48 simprrl N B 𝔼 N n A 𝔼 n B 𝔼 n A 𝔼 n
49 fveq2 N = n 𝔼 N = 𝔼 n
50 49 eleq2d N = n A 𝔼 N A 𝔼 n
51 48 50 syl5ibrcom N B 𝔼 N n A 𝔼 n B 𝔼 n N = n A 𝔼 N
52 47 51 mpd N B 𝔼 N n A 𝔼 n B 𝔼 n A 𝔼 N
53 43 45 52 syl2an N A V B 𝔼 N C W n A 𝔼 n B 𝔼 n C 𝔼 n A 𝔼 N
54 53 exp32 N A V B 𝔼 N C W n A 𝔼 n B 𝔼 n C 𝔼 n A 𝔼 N
55 41 54 syl7 N A V B 𝔼 N C W n A 𝔼 n B 𝔼 n C 𝔼 n A Btwn B C B Btwn C A C Btwn A B A 𝔼 N
56 55 rexlimdv N A V B 𝔼 N C W n A 𝔼 n B 𝔼 n C 𝔼 n A Btwn B C B Btwn C A C Btwn A B A 𝔼 N
57 40 56 sylbid N A V B 𝔼 N C W B C A b c a | n a 𝔼 n b 𝔼 n c 𝔼 n a Btwn b c b Btwn c a c Btwn a b A 𝔼 N
58 7 57 syl5bi N A V B 𝔼 N C W B C b c a | n a 𝔼 n b 𝔼 n c 𝔼 n a Btwn b c b Btwn c a c Btwn a b A A 𝔼 N
59 6 58 sylbid N A V B 𝔼 N C W A b c a | n a 𝔼 n b 𝔼 n c 𝔼 n a Btwn b c b Btwn c a c Btwn a b -1 B C A 𝔼 N
60 2 59 syl5bi N A V B 𝔼 N C W A Colinear B C A 𝔼 N