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 = Line 𝒢 G
tglngval.i I = Itv G
tglngval.g φ G 𝒢 Tarski
tglngval.x φ X P
tglngval.y φ Y P
tgcolg.z φ Z P
ncoltgdim2.1 φ ¬ Z X L Y X = Y
Assertion ncoltgdim2 φ G Dim 𝒢 2

Proof

Step Hyp Ref Expression
1 tglngval.p P = Base G
2 tglngval.l L = Line 𝒢 G
3 tglngval.i I = Itv G
4 tglngval.g φ G 𝒢 Tarski
5 tglngval.x φ X P
6 tglngval.y φ Y P
7 tgcolg.z φ Z P
8 ncoltgdim2.1 φ ¬ Z X L Y X = Y
9 4 adantr φ ¬ G Dim 𝒢 2 G 𝒢 Tarski
10 5 adantr φ ¬ G Dim 𝒢 2 X P
11 6 adantr φ ¬ G Dim 𝒢 2 Y P
12 7 adantr φ ¬ G Dim 𝒢 2 Z P
13 simpr φ ¬ G Dim 𝒢 2 ¬ G Dim 𝒢 2
14 1 2 3 9 10 11 12 13 tgdim01ln φ ¬ G Dim 𝒢 2 Z X L Y X = Y
15 8 14 mtand φ ¬ ¬ G Dim 𝒢 2
16 15 notnotrd φ G Dim 𝒢 2