Metamath Proof Explorer


Theorem ncoltgdim2

Description: If there are three non-colinear points, then the dimension is at least two. Converse of tglowdim2l . (Contributed by Thierry Arnoux, 23-Feb-2020)

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 )
ncoltgdim2.1
|- ( ph -> -. ( Z e. ( X L Y ) \/ X = Y ) )
Assertion ncoltgdim2
|- ( ph -> G TarskiGDim>= 2 )

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 ncoltgdim2.1
 |-  ( ph -> -. ( Z e. ( X L Y ) \/ X = Y ) )
9 4 adantr
 |-  ( ( ph /\ -. G TarskiGDim>= 2 ) -> G e. TarskiG )
10 5 adantr
 |-  ( ( ph /\ -. G TarskiGDim>= 2 ) -> X e. P )
11 6 adantr
 |-  ( ( ph /\ -. G TarskiGDim>= 2 ) -> Y e. P )
12 7 adantr
 |-  ( ( ph /\ -. G TarskiGDim>= 2 ) -> Z e. P )
13 simpr
 |-  ( ( ph /\ -. G TarskiGDim>= 2 ) -> -. G TarskiGDim>= 2 )
14 1 2 3 9 10 11 12 13 tgdim01ln
 |-  ( ( ph /\ -. G TarskiGDim>= 2 ) -> ( Z e. ( X L Y ) \/ X = Y ) )
15 8 14 mtand
 |-  ( ph -> -. -. G TarskiGDim>= 2 )
16 15 notnotrd
 |-  ( ph -> G TarskiGDim>= 2 )