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