Description: Non-colinear points are different. (Contributed by Thierry Arnoux, 8-Aug-2019) TODO (NM): maybe ncolne2 could be simplified out and deleted, replaced by ncolcom .
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | tglineelsb2.p | |- B = ( Base ` G ) |
|
| tglineelsb2.i | |- I = ( Itv ` G ) |
||
| tglineelsb2.l | |- L = ( LineG ` G ) |
||
| tglineelsb2.g | |- ( ph -> G e. TarskiG ) |
||
| ncolne.x | |- ( ph -> X e. B ) |
||
| ncolne.y | |- ( ph -> Y e. B ) |
||
| ncolne.z | |- ( ph -> Z e. B ) |
||
| ncolne.2 | |- ( ph -> -. ( X e. ( Y L Z ) \/ Y = Z ) ) |
||
| Assertion | ncolne2 | |- ( ph -> X =/= Z ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | tglineelsb2.p | |- B = ( Base ` G ) |
|
| 2 | tglineelsb2.i | |- I = ( Itv ` G ) |
|
| 3 | tglineelsb2.l | |- L = ( LineG ` G ) |
|
| 4 | tglineelsb2.g | |- ( ph -> G e. TarskiG ) |
|
| 5 | ncolne.x | |- ( ph -> X e. B ) |
|
| 6 | ncolne.y | |- ( ph -> Y e. B ) |
|
| 7 | ncolne.z | |- ( ph -> Z e. B ) |
|
| 8 | ncolne.2 | |- ( ph -> -. ( X e. ( Y L Z ) \/ Y = Z ) ) |
|
| 9 | 1 3 2 4 6 7 5 8 | ncolcom | |- ( ph -> -. ( X e. ( Z L Y ) \/ Z = Y ) ) |
| 10 | 1 2 3 4 5 7 6 9 | ncolne1 | |- ( ph -> X =/= Z ) |