Metamath Proof Explorer

Theorem tgdim01ln

Description: In geometries of dimension less than two, then any three points are colinear. (Contributed by Thierry Arnoux, 27-Aug-2019)

Ref Expression
Hypotheses tglngval.p 
|- P = ( Base ` G )
tglngval.l 
|- L = ( LineG ` G )
tglngval.i 
|- I = ( Itv ` G )
tglngval.g 
|- ( ph -> G e. TarskiG )
tglngval.x 
|- ( ph -> X e. P )
tglngval.y 
|- ( ph -> Y e. P )
tgcolg.z 
|- ( ph -> Z e. P )
tgdim01ln.1 
|- ( ph -> -. G TarskiGDim>= 2 )
Assertion tgdim01ln 
|- ( ph -> ( Z e. ( X L Y ) \/ X = Y ) )

Proof

Step Hyp Ref Expression
1 tglngval.p 
 |-  P = ( Base ` G )
2 tglngval.l 
 |-  L = ( LineG ` G )
3 tglngval.i 
 |-  I = ( Itv ` G )
4 tglngval.g 
 |-  ( ph -> G e. TarskiG )
5 tglngval.x 
 |-  ( ph -> X e. P )
6 tglngval.y 
 |-  ( ph -> Y e. P )
7 tgcolg.z 
 |-  ( ph -> Z e. P )
8 tgdim01ln.1 
 |-  ( ph -> -. G TarskiGDim>= 2 )
9 4 adantr 
 |-  ( ( ph /\ Z e. ( X I Y ) ) -> G e. TarskiG )
10 5 adantr 
 |-  ( ( ph /\ Z e. ( X I Y ) ) -> X e. P )
11 6 adantr 
 |-  ( ( ph /\ Z e. ( X I Y ) ) -> Y e. P )
12 7 adantr 
 |-  ( ( ph /\ Z e. ( X I Y ) ) -> Z e. P )
13 simpr 
 |-  ( ( ph /\ Z e. ( X I Y ) ) -> Z e. ( X I Y ) )
14 1 2 3 9 10 11 12 13 btwncolg1 
 |-  ( ( ph /\ Z e. ( X I Y ) ) -> ( Z e. ( X L Y ) \/ X = Y ) )
15 4 adantr 
 |-  ( ( ph /\ X e. ( Z I Y ) ) -> G e. TarskiG )
16 5 adantr 
 |-  ( ( ph /\ X e. ( Z I Y ) ) -> X e. P )
17 6 adantr 
 |-  ( ( ph /\ X e. ( Z I Y ) ) -> Y e. P )
18 7 adantr 
 |-  ( ( ph /\ X e. ( Z I Y ) ) -> Z e. P )
19 simpr 
 |-  ( ( ph /\ X e. ( Z I Y ) ) -> X e. ( Z I Y ) )
20 1 2 3 15 16 17 18 19 btwncolg2 
 |-  ( ( ph /\ X e. ( Z I Y ) ) -> ( Z e. ( X L Y ) \/ X = Y ) )
21 4 adantr 
 |-  ( ( ph /\ Y e. ( X I Z ) ) -> G e. TarskiG )
22 5 adantr 
 |-  ( ( ph /\ Y e. ( X I Z ) ) -> X e. P )
23 6 adantr 
 |-  ( ( ph /\ Y e. ( X I Z ) ) -> Y e. P )
24 7 adantr 
 |-  ( ( ph /\ Y e. ( X I Z ) ) -> Z e. P )
25 simpr 
 |-  ( ( ph /\ Y e. ( X I Z ) ) -> Y e. ( X I Z ) )
26 1 2 3 21 22 23 24 25 btwncolg3 
 |-  ( ( ph /\ Y e. ( X I Z ) ) -> ( Z e. ( X L Y ) \/ X = Y ) )
27 1 3 4 8 5 6 7 tgdim01 
 |-  ( ph -> ( Z e. ( X I Y ) \/ X e. ( Z I Y ) \/ Y e. ( X I Z ) ) )
28 14 20 26 27 mpjao3dan 
 |-  ( ph -> ( Z e. ( X L Y ) \/ X = Y ) )