Metamath Proof Explorer

Theorem tgdim01

Description: In geometries of dimension less than 2, all points are colinear. (Contributed by Thierry Arnoux, 27-Aug-2019)

Ref Expression
Hypotheses tgdim01.p 
|- P = ( Base ` G )
tgdim01.i 
|- I = ( Itv ` G )
tgdim01.g 
|- ( ph -> G e. V )
tgdim01.1 
|- ( ph -> -. G TarskiGDim>= 2 )
tgdim01.x 
|- ( ph -> X e. P )
tgdim01.y 
|- ( ph -> Y e. P )
tgdim01.z 
|- ( ph -> Z e. P )
Assertion tgdim01 
|- ( ph -> ( Z e. ( X I Y ) \/ X e. ( Z I Y ) \/ Y e. ( X I Z ) ) )

Proof

Step Hyp Ref Expression
1 tgdim01.p 
 |-  P = ( Base ` G )
2 tgdim01.i 
 |-  I = ( Itv ` G )
3 tgdim01.g 
 |-  ( ph -> G e. V )
4 tgdim01.1 
 |-  ( ph -> -. G TarskiGDim>= 2 )
5 tgdim01.x 
 |-  ( ph -> X e. P )
6 tgdim01.y 
 |-  ( ph -> Y e. P )
7 tgdim01.z 
 |-  ( ph -> Z e. P )
8 eqid 
 |-  ( dist ` G ) = ( dist ` G )
9 1 8 2 istrkg2ld 
 |-  ( G e. V -> ( G TarskiGDim>= 2 <-> E. x e. P E. y e. P E. z e. P -. ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) ) )
10 3 9 syl 
 |-  ( ph -> ( G TarskiGDim>= 2 <-> E. x e. P E. y e. P E. z e. P -. ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) ) )
11 4 10 mtbid 
 |-  ( ph -> -. E. x e. P E. y e. P E. z e. P -. ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) )
12 rexnal3 
 |-  ( E. x e. P E. y e. P E. z e. P -. ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) <-> -. A. x e. P A. y e. P A. z e. P ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) )
13 12 con2bii 
 |-  ( A. x e. P A. y e. P A. z e. P ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) <-> -. E. x e. P E. y e. P E. z e. P -. ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) )
14 11 13 sylibr 
 |-  ( ph -> A. x e. P A. y e. P A. z e. P ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) )
15 oveq1 
 |-  ( x = X -> ( x I y ) = ( X I y ) )
16 15 eleq2d 
 |-  ( x = X -> ( z e. ( x I y ) <-> z e. ( X I y ) ) )
17 eleq1 
 |-  ( x = X -> ( x e. ( z I y ) <-> X e. ( z I y ) ) )
18 oveq1 
 |-  ( x = X -> ( x I z ) = ( X I z ) )
19 18 eleq2d 
 |-  ( x = X -> ( y e. ( x I z ) <-> y e. ( X I z ) ) )
20 16 17 19 3orbi123d 
 |-  ( x = X -> ( ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) <-> ( z e. ( X I y ) \/ X e. ( z I y ) \/ y e. ( X I z ) ) ) )
21 oveq2 
 |-  ( y = Y -> ( X I y ) = ( X I Y ) )
22 21 eleq2d 
 |-  ( y = Y -> ( z e. ( X I y ) <-> z e. ( X I Y ) ) )
23 oveq2 
 |-  ( y = Y -> ( z I y ) = ( z I Y ) )
24 23 eleq2d 
 |-  ( y = Y -> ( X e. ( z I y ) <-> X e. ( z I Y ) ) )
25 eleq1 
 |-  ( y = Y -> ( y e. ( X I z ) <-> Y e. ( X I z ) ) )
26 22 24 25 3orbi123d 
 |-  ( y = Y -> ( ( z e. ( X I y ) \/ X e. ( z I y ) \/ y e. ( X I z ) ) <-> ( z e. ( X I Y ) \/ X e. ( z I Y ) \/ Y e. ( X I z ) ) ) )
27 eleq1 
 |-  ( z = Z -> ( z e. ( X I Y ) <-> Z e. ( X I Y ) ) )
28 oveq1 
 |-  ( z = Z -> ( z I Y ) = ( Z I Y ) )
29 28 eleq2d 
 |-  ( z = Z -> ( X e. ( z I Y ) <-> X e. ( Z I Y ) ) )
30 oveq2 
 |-  ( z = Z -> ( X I z ) = ( X I Z ) )
31 30 eleq2d 
 |-  ( z = Z -> ( Y e. ( X I z ) <-> Y e. ( X I Z ) ) )
32 27 29 31 3orbi123d 
 |-  ( z = Z -> ( ( z e. ( X I Y ) \/ X e. ( z I Y ) \/ Y e. ( X I z ) ) <-> ( Z e. ( X I Y ) \/ X e. ( Z I Y ) \/ Y e. ( X I Z ) ) ) )
33 20 26 32 rspc3v 
 |-  ( ( X e. P /\ Y e. P /\ Z e. P ) -> ( A. x e. P A. y e. P A. z e. P ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) -> ( Z e. ( X I Y ) \/ X e. ( Z I Y ) \/ Y e. ( X I Z ) ) ) )
34 33 imp 
 |-  ( ( ( X e. P /\ Y e. P /\ Z e. P ) /\ A. x e. P A. y e. P A. z e. P ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) ) -> ( Z e. ( X I Y ) \/ X e. ( Z I Y ) \/ Y e. ( X I Z ) ) )
35 5 6 7 14 34 syl31anc 
 |-  ( ph -> ( Z e. ( X I Y ) \/ X e. ( Z I Y ) \/ Y e. ( X I Z ) ) )