Metamath Proof Explorer

Theorem colline

Description: Three points are colinear iff there is a line through all three of them. Theorem 6.23 of Schwabhauser p. 46. (Contributed by Thierry Arnoux, 28-May-2019)

Ref Expression
Hypotheses tglineintmo.p 
|- P = ( Base ` G )
tglineintmo.i 
|- I = ( Itv ` G )
tglineintmo.l 
|- L = ( LineG ` G )
tglineintmo.g 
|- ( ph -> G e. TarskiG )
colline.1 
|- ( ph -> X e. P )
colline.2 
|- ( ph -> Y e. P )
colline.3 
|- ( ph -> Z e. P )
colline.4 
|- ( ph -> 2 <_ ( # ` P ) )
Assertion colline 
|- ( ph -> ( ( X e. ( Y L Z ) \/ Y = Z ) <-> E. a e. ran L ( X e. a /\ Y e. a /\ Z e. a ) ) )

Proof

Step Hyp Ref Expression
1 tglineintmo.p 
 |-  P = ( Base ` G )
2 tglineintmo.i 
 |-  I = ( Itv ` G )
3 tglineintmo.l 
 |-  L = ( LineG ` G )
4 tglineintmo.g 
 |-  ( ph -> G e. TarskiG )
5 colline.1 
 |-  ( ph -> X e. P )
6 colline.2 
 |-  ( ph -> Y e. P )
7 colline.3 
 |-  ( ph -> Z e. P )
8 colline.4 
 |-  ( ph -> 2 <_ ( # ` P ) )
9 4 ad4antr 
 |-  ( ( ( ( ( ph /\ Y = Z ) /\ X = Z ) /\ x e. P ) /\ X =/= x ) -> G e. TarskiG )
10 5 ad4antr 
 |-  ( ( ( ( ( ph /\ Y = Z ) /\ X = Z ) /\ x e. P ) /\ X =/= x ) -> X e. P )
11 simplr 
 |-  ( ( ( ( ( ph /\ Y = Z ) /\ X = Z ) /\ x e. P ) /\ X =/= x ) -> x e. P )
12 simpr 
 |-  ( ( ( ( ( ph /\ Y = Z ) /\ X = Z ) /\ x e. P ) /\ X =/= x ) -> X =/= x )
13 1 2 3 9 10 11 12 tgelrnln 
 |-  ( ( ( ( ( ph /\ Y = Z ) /\ X = Z ) /\ x e. P ) /\ X =/= x ) -> ( X L x ) e. ran L )
14 1 2 3 9 10 11 12 tglinerflx1 
 |-  ( ( ( ( ( ph /\ Y = Z ) /\ X = Z ) /\ x e. P ) /\ X =/= x ) -> X e. ( X L x ) )
15 simp-4r 
 |-  ( ( ( ( ( ph /\ Y = Z ) /\ X = Z ) /\ x e. P ) /\ X =/= x ) -> Y = Z )
16 simpllr 
 |-  ( ( ( ( ( ph /\ Y = Z ) /\ X = Z ) /\ x e. P ) /\ X =/= x ) -> X = Z )
17 16 14 eqeltrrd 
 |-  ( ( ( ( ( ph /\ Y = Z ) /\ X = Z ) /\ x e. P ) /\ X =/= x ) -> Z e. ( X L x ) )
18 15 17 eqeltrd 
 |-  ( ( ( ( ( ph /\ Y = Z ) /\ X = Z ) /\ x e. P ) /\ X =/= x ) -> Y e. ( X L x ) )
19 eleq2 
 |-  ( a = ( X L x ) -> ( X e. a <-> X e. ( X L x ) ) )
20 eleq2 
 |-  ( a = ( X L x ) -> ( Y e. a <-> Y e. ( X L x ) ) )
21 eleq2 
 |-  ( a = ( X L x ) -> ( Z e. a <-> Z e. ( X L x ) ) )
22 19 20 21 3anbi123d 
 |-  ( a = ( X L x ) -> ( ( X e. a /\ Y e. a /\ Z e. a ) <-> ( X e. ( X L x ) /\ Y e. ( X L x ) /\ Z e. ( X L x ) ) ) )
23 22 rspcev 
 |-  ( ( ( X L x ) e. ran L /\ ( X e. ( X L x ) /\ Y e. ( X L x ) /\ Z e. ( X L x ) ) ) -> E. a e. ran L ( X e. a /\ Y e. a /\ Z e. a ) )
24 13 14 18 17 23 syl13anc 
 |-  ( ( ( ( ( ph /\ Y = Z ) /\ X = Z ) /\ x e. P ) /\ X =/= x ) -> E. a e. ran L ( X e. a /\ Y e. a /\ Z e. a ) )
25 eqid 
 |-  ( dist ` G ) = ( dist ` G )
26 1 25 2 4 8 5 tglowdim1i 
 |-  ( ph -> E. x e. P X =/= x )
27 26 ad2antrr 
 |-  ( ( ( ph /\ Y = Z ) /\ X = Z ) -> E. x e. P X =/= x )
28 24 27 r19.29a 
 |-  ( ( ( ph /\ Y = Z ) /\ X = Z ) -> E. a e. ran L ( X e. a /\ Y e. a /\ Z e. a ) )
29 4 ad2antrr 
 |-  ( ( ( ph /\ Y = Z ) /\ X =/= Z ) -> G e. TarskiG )
30 5 ad2antrr 
 |-  ( ( ( ph /\ Y = Z ) /\ X =/= Z ) -> X e. P )
31 7 ad2antrr 
 |-  ( ( ( ph /\ Y = Z ) /\ X =/= Z ) -> Z e. P )
32 simpr 
 |-  ( ( ( ph /\ Y = Z ) /\ X =/= Z ) -> X =/= Z )
33 1 2 3 29 30 31 32 tgelrnln 
 |-  ( ( ( ph /\ Y = Z ) /\ X =/= Z ) -> ( X L Z ) e. ran L )
34 1 2 3 29 30 31 32 tglinerflx1 
 |-  ( ( ( ph /\ Y = Z ) /\ X =/= Z ) -> X e. ( X L Z ) )
35 simplr 
 |-  ( ( ( ph /\ Y = Z ) /\ X =/= Z ) -> Y = Z )
36 1 2 3 29 30 31 32 tglinerflx2 
 |-  ( ( ( ph /\ Y = Z ) /\ X =/= Z ) -> Z e. ( X L Z ) )
37 35 36 eqeltrd 
 |-  ( ( ( ph /\ Y = Z ) /\ X =/= Z ) -> Y e. ( X L Z ) )
38 eleq2 
 |-  ( a = ( X L Z ) -> ( X e. a <-> X e. ( X L Z ) ) )
39 eleq2 
 |-  ( a = ( X L Z ) -> ( Y e. a <-> Y e. ( X L Z ) ) )
40 eleq2 
 |-  ( a = ( X L Z ) -> ( Z e. a <-> Z e. ( X L Z ) ) )
41 38 39 40 3anbi123d 
 |-  ( a = ( X L Z ) -> ( ( X e. a /\ Y e. a /\ Z e. a ) <-> ( X e. ( X L Z ) /\ Y e. ( X L Z ) /\ Z e. ( X L Z ) ) ) )
42 41 rspcev 
 |-  ( ( ( X L Z ) e. ran L /\ ( X e. ( X L Z ) /\ Y e. ( X L Z ) /\ Z e. ( X L Z ) ) ) -> E. a e. ran L ( X e. a /\ Y e. a /\ Z e. a ) )
43 33 34 37 36 42 syl13anc 
 |-  ( ( ( ph /\ Y = Z ) /\ X =/= Z ) -> E. a e. ran L ( X e. a /\ Y e. a /\ Z e. a ) )
44 28 43 pm2.61dane 
 |-  ( ( ph /\ Y = Z ) -> E. a e. ran L ( X e. a /\ Y e. a /\ Z e. a ) )
45 44 adantlr 
 |-  ( ( ( ph /\ ( X e. ( Y L Z ) \/ Y = Z ) ) /\ Y = Z ) -> E. a e. ran L ( X e. a /\ Y e. a /\ Z e. a ) )
46 simpll 
 |-  ( ( ( ph /\ ( X e. ( Y L Z ) \/ Y = Z ) ) /\ Y =/= Z ) -> ph )
47 simpr 
 |-  ( ( ( ph /\ ( X e. ( Y L Z ) \/ Y = Z ) ) /\ Y =/= Z ) -> Y =/= Z )
48 47 neneqd 
 |-  ( ( ( ph /\ ( X e. ( Y L Z ) \/ Y = Z ) ) /\ Y =/= Z ) -> -. Y = Z )
49 simplr 
 |-  ( ( ( ph /\ ( X e. ( Y L Z ) \/ Y = Z ) ) /\ Y =/= Z ) -> ( X e. ( Y L Z ) \/ Y = Z ) )
50 orel2 
 |-  ( -. Y = Z -> ( ( X e. ( Y L Z ) \/ Y = Z ) -> X e. ( Y L Z ) ) )
51 48 49 50 sylc 
 |-  ( ( ( ph /\ ( X e. ( Y L Z ) \/ Y = Z ) ) /\ Y =/= Z ) -> X e. ( Y L Z ) )
52 4 ad2antrr 
 |-  ( ( ( ph /\ X e. ( Y L Z ) ) /\ Y =/= Z ) -> G e. TarskiG )
53 6 ad2antrr 
 |-  ( ( ( ph /\ X e. ( Y L Z ) ) /\ Y =/= Z ) -> Y e. P )
54 7 ad2antrr 
 |-  ( ( ( ph /\ X e. ( Y L Z ) ) /\ Y =/= Z ) -> Z e. P )
55 simpr 
 |-  ( ( ( ph /\ X e. ( Y L Z ) ) /\ Y =/= Z ) -> Y =/= Z )
56 1 2 3 52 53 54 55 tgelrnln 
 |-  ( ( ( ph /\ X e. ( Y L Z ) ) /\ Y =/= Z ) -> ( Y L Z ) e. ran L )
57 46 51 47 56 syl21anc 
 |-  ( ( ( ph /\ ( X e. ( Y L Z ) \/ Y = Z ) ) /\ Y =/= Z ) -> ( Y L Z ) e. ran L )
58 1 2 3 52 53 54 55 tglinerflx1 
 |-  ( ( ( ph /\ X e. ( Y L Z ) ) /\ Y =/= Z ) -> Y e. ( Y L Z ) )
59 46 51 47 58 syl21anc 
 |-  ( ( ( ph /\ ( X e. ( Y L Z ) \/ Y = Z ) ) /\ Y =/= Z ) -> Y e. ( Y L Z ) )
60 1 2 3 52 53 54 55 tglinerflx2 
 |-  ( ( ( ph /\ X e. ( Y L Z ) ) /\ Y =/= Z ) -> Z e. ( Y L Z ) )
61 46 51 47 60 syl21anc 
 |-  ( ( ( ph /\ ( X e. ( Y L Z ) \/ Y = Z ) ) /\ Y =/= Z ) -> Z e. ( Y L Z ) )
62 eleq2 
 |-  ( a = ( Y L Z ) -> ( X e. a <-> X e. ( Y L Z ) ) )
63 eleq2 
 |-  ( a = ( Y L Z ) -> ( Y e. a <-> Y e. ( Y L Z ) ) )
64 eleq2 
 |-  ( a = ( Y L Z ) -> ( Z e. a <-> Z e. ( Y L Z ) ) )
65 62 63 64 3anbi123d 
 |-  ( a = ( Y L Z ) -> ( ( X e. a /\ Y e. a /\ Z e. a ) <-> ( X e. ( Y L Z ) /\ Y e. ( Y L Z ) /\ Z e. ( Y L Z ) ) ) )
66 65 rspcev 
 |-  ( ( ( Y L Z ) e. ran L /\ ( X e. ( Y L Z ) /\ Y e. ( Y L Z ) /\ Z e. ( Y L Z ) ) ) -> E. a e. ran L ( X e. a /\ Y e. a /\ Z e. a ) )
67 57 51 59 61 66 syl13anc 
 |-  ( ( ( ph /\ ( X e. ( Y L Z ) \/ Y = Z ) ) /\ Y =/= Z ) -> E. a e. ran L ( X e. a /\ Y e. a /\ Z e. a ) )
68 45 67 pm2.61dane 
 |-  ( ( ph /\ ( X e. ( Y L Z ) \/ Y = Z ) ) -> E. a e. ran L ( X e. a /\ Y e. a /\ Z e. a ) )
69 df-ne 
 |-  ( Y =/= Z <-> -. Y = Z )
70 simplr1 
 |-  ( ( ( ( ph /\ a e. ran L ) /\ ( X e. a /\ Y e. a /\ Z e. a ) ) /\ Y =/= Z ) -> X e. a )
71 4 ad3antrrr 
 |-  ( ( ( ( ph /\ a e. ran L ) /\ ( X e. a /\ Y e. a /\ Z e. a ) ) /\ Y =/= Z ) -> G e. TarskiG )
72 6 ad3antrrr 
 |-  ( ( ( ( ph /\ a e. ran L ) /\ ( X e. a /\ Y e. a /\ Z e. a ) ) /\ Y =/= Z ) -> Y e. P )
73 7 ad3antrrr 
 |-  ( ( ( ( ph /\ a e. ran L ) /\ ( X e. a /\ Y e. a /\ Z e. a ) ) /\ Y =/= Z ) -> Z e. P )
74 simpr 
 |-  ( ( ( ( ph /\ a e. ran L ) /\ ( X e. a /\ Y e. a /\ Z e. a ) ) /\ Y =/= Z ) -> Y =/= Z )
75 simpllr 
 |-  ( ( ( ( ph /\ a e. ran L ) /\ ( X e. a /\ Y e. a /\ Z e. a ) ) /\ Y =/= Z ) -> a e. ran L )
76 simplr2 
 |-  ( ( ( ( ph /\ a e. ran L ) /\ ( X e. a /\ Y e. a /\ Z e. a ) ) /\ Y =/= Z ) -> Y e. a )
77 simplr3 
 |-  ( ( ( ( ph /\ a e. ran L ) /\ ( X e. a /\ Y e. a /\ Z e. a ) ) /\ Y =/= Z ) -> Z e. a )
78 1 2 3 71 72 73 74 74 75 76 77 tglinethru 
 |-  ( ( ( ( ph /\ a e. ran L ) /\ ( X e. a /\ Y e. a /\ Z e. a ) ) /\ Y =/= Z ) -> a = ( Y L Z ) )
79 70 78 eleqtrd 
 |-  ( ( ( ( ph /\ a e. ran L ) /\ ( X e. a /\ Y e. a /\ Z e. a ) ) /\ Y =/= Z ) -> X e. ( Y L Z ) )
80 79 ex 
 |-  ( ( ( ph /\ a e. ran L ) /\ ( X e. a /\ Y e. a /\ Z e. a ) ) -> ( Y =/= Z -> X e. ( Y L Z ) ) )
81 69 80 syl5bir 
 |-  ( ( ( ph /\ a e. ran L ) /\ ( X e. a /\ Y e. a /\ Z e. a ) ) -> ( -. Y = Z -> X e. ( Y L Z ) ) )
82 81 orrd 
 |-  ( ( ( ph /\ a e. ran L ) /\ ( X e. a /\ Y e. a /\ Z e. a ) ) -> ( Y = Z \/ X e. ( Y L Z ) ) )
83 82 orcomd 
 |-  ( ( ( ph /\ a e. ran L ) /\ ( X e. a /\ Y e. a /\ Z e. a ) ) -> ( X e. ( Y L Z ) \/ Y = Z ) )
84 83 r19.29an 
 |-  ( ( ph /\ E. a e. ran L ( X e. a /\ Y e. a /\ Z e. a ) ) -> ( X e. ( Y L Z ) \/ Y = Z ) )
85 68 84 impbida 
 |-  ( ph -> ( ( X e. ( Y L Z ) \/ Y = Z ) <-> E. a e. ran L ( X e. a /\ Y e. a /\ Z e. a ) ) )