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 )