Description: Betweenness implies colinearity. (Contributed by Thierry Arnoux, 28-Mar-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 ) |
||
btwncolg3.z | |- ( ph -> Y e. ( X I Z ) ) |
||
Assertion | btwncolg3 | |- ( ph -> ( Z e. ( X L Y ) \/ X = Y ) ) |
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 | btwncolg3.z | |- ( ph -> Y e. ( X I Z ) ) |
|
9 | 8 | 3mix3d | |- ( ph -> ( Z e. ( X I Y ) \/ X e. ( Z I Y ) \/ Y e. ( X I Z ) ) ) |
10 | 1 2 3 4 5 6 7 | tgcolg | |- ( ph -> ( ( Z e. ( X L Y ) \/ X = Y ) <-> ( Z e. ( X I Y ) \/ X e. ( Z I Y ) \/ Y e. ( X I Z ) ) ) ) |
11 | 9 10 | mpbird | |- ( ph -> ( Z e. ( X L Y ) \/ X = Y ) ) |