Metamath Proof Explorer

Theorem tgdim01

Description: In geometries of dimension less than 2, all points are colinear. (Contributed by Thierry Arnoux, 27-Aug-2019)

Ref Expression
Hypotheses tgdim01.p ⊢P=BaseG
tgdim01.i ⊢I=Itv⁡G
tgdim01.g ⊢φ→G∈V
tgdim01.1 ⊢φ→¬GDim𝒢≥2
tgdim01.x ⊢φ→X∈P
tgdim01.y ⊢φ→Y∈P
tgdim01.z ⊢φ→Z∈P
Assertion tgdim01 ⊢φ→Z∈XIY∨X∈ZIY∨Y∈XIZ

Proof

Step Hyp Ref Expression
1 tgdim01.p ⊢P=BaseG
2 tgdim01.i ⊢I=Itv⁡G
3 tgdim01.g ⊢φ→G∈V
4 tgdim01.1 ⊢φ→¬GDim𝒢≥2
5 tgdim01.x ⊢φ→X∈P
6 tgdim01.y ⊢φ→Y∈P
7 tgdim01.z ⊢φ→Z∈P
8 eqid ⊢dist⁡G=dist⁡G
9 1 8 2 istrkg2ld ⊢G∈V→GDim𝒢≥2↔∃x∈P∃y∈P∃z∈P¬z∈xIy∨x∈zIy∨y∈xIz
10 3 9 syl ⊢φ→GDim𝒢≥2↔∃x∈P∃y∈P∃z∈P¬z∈xIy∨x∈zIy∨y∈xIz
11 4 10 mtbid ⊢φ→¬∃x∈P∃y∈P∃z∈P¬z∈xIy∨x∈zIy∨y∈xIz
12 rexnal3 ⊢∃x∈P∃y∈P∃z∈P¬z∈xIy∨x∈zIy∨y∈xIz↔¬∀x∈P∀y∈P∀z∈Pz∈xIy∨x∈zIy∨y∈xIz
13 12 con2bii ⊢∀x∈P∀y∈P∀z∈Pz∈xIy∨x∈zIy∨y∈xIz↔¬∃x∈P∃y∈P∃z∈P¬z∈xIy∨x∈zIy∨y∈xIz
14 11 13 sylibr ⊢φ→∀x∈P∀y∈P∀z∈Pz∈xIy∨x∈zIy∨y∈xIz
15 oveq1 ⊢x=X→xIy=XIy
16 15 eleq2d ⊢x=X→z∈xIy↔z∈XIy
17 eleq1 ⊢x=X→x∈zIy↔X∈zIy
18 oveq1 ⊢x=X→xIz=XIz
19 18 eleq2d ⊢x=X→y∈xIz↔y∈XIz
20 16 17 19 3orbi123d ⊢x=X→z∈xIy∨x∈zIy∨y∈xIz↔z∈XIy∨X∈zIy∨y∈XIz
21 oveq2 ⊢y=Y→XIy=XIY
22 21 eleq2d ⊢y=Y→z∈XIy↔z∈XIY
23 oveq2 ⊢y=Y→zIy=zIY
24 23 eleq2d ⊢y=Y→X∈zIy↔X∈zIY
25 eleq1 ⊢y=Y→y∈XIz↔Y∈XIz
26 22 24 25 3orbi123d ⊢y=Y→z∈XIy∨X∈zIy∨y∈XIz↔z∈XIY∨X∈zIY∨Y∈XIz
27 eleq1 ⊢z=Z→z∈XIY↔Z∈XIY
28 oveq1 ⊢z=Z→zIY=ZIY
29 28 eleq2d ⊢z=Z→X∈zIY↔X∈ZIY
30 oveq2 ⊢z=Z→XIz=XIZ
31 30 eleq2d ⊢z=Z→Y∈XIz↔Y∈XIZ
32 27 29 31 3orbi123d ⊢z=Z→z∈XIY∨X∈zIY∨Y∈XIz↔Z∈XIY∨X∈ZIY∨Y∈XIZ
33 20 26 32 rspc3v ⊢X∈P∧Y∈P∧Z∈P→∀x∈P∀y∈P∀z∈Pz∈xIy∨x∈zIy∨y∈xIz→Z∈XIY∨X∈ZIY∨Y∈XIZ
34 33 imp ⊢X∈P∧Y∈P∧Z∈P∧∀x∈P∀y∈P∀z∈Pz∈xIy∨x∈zIy∨y∈xIz→Z∈XIY∨X∈ZIY∨Y∈XIZ
35 5 6 7 14 34 syl31anc ⊢φ→Z∈XIY∨X∈ZIY∨Y∈XIZ