tgdim01ln

Description: In geometries of dimension less than two, then any three points are colinear. (Contributed by Thierry Arnoux, 27-Aug-2019)

	Ref	Expression
Hypotheses	tglngval.p	$⊢ P = {Base}_{G}$
	tglngval.l	$⊢ L = {Line}_{𝒢} (G)$
	tglngval.i	$⊢ I = Itv (G)$
	tglngval.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	tglngval.x	$⊢ φ \to X \in P$
	tglngval.y	$⊢ φ \to Y \in P$
	tgcolg.z	$⊢ φ \to Z \in P$
	tgdim01ln.1	$⊢ φ \to \neg G {Dim}_{𝒢} \geq 2$
Assertion	tgdim01ln	$⊢ φ \to (Z \in (X L Y) \lor X = Y)$

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	$⊢ φ \to G \in 𝒢_{Tarski}$
5		tglngval.x	$⊢ φ \to X \in P$
6		tglngval.y	$⊢ φ \to Y \in P$
7		tgcolg.z	$⊢ φ \to Z \in P$
8		tgdim01ln.1	$⊢ φ \to \neg G {Dim}_{𝒢} \geq 2$
9	4	adantr	$⊢ (φ \land Z \in (X I Y)) \to G \in 𝒢_{Tarski}$
10	5	adantr	$⊢ (φ \land Z \in (X I Y)) \to X \in P$
11	6	adantr	$⊢ (φ \land Z \in (X I Y)) \to Y \in P$
12	7	adantr	$⊢ (φ \land Z \in (X I Y)) \to Z \in P$
13		simpr	$⊢ (φ \land Z \in (X I Y)) \to Z \in (X I Y)$
14	1 2 3 9 10 11 12 13	btwncolg1	$⊢ (φ \land Z \in (X I Y)) \to (Z \in (X L Y) \lor X = Y)$
15	4	adantr	$⊢ (φ \land X \in (Z I Y)) \to G \in 𝒢_{Tarski}$
16	5	adantr	$⊢ (φ \land X \in (Z I Y)) \to X \in P$
17	6	adantr	$⊢ (φ \land X \in (Z I Y)) \to Y \in P$
18	7	adantr	$⊢ (φ \land X \in (Z I Y)) \to Z \in P$
19		simpr	$⊢ (φ \land X \in (Z I Y)) \to X \in (Z I Y)$
20	1 2 3 15 16 17 18 19	btwncolg2	$⊢ (φ \land X \in (Z I Y)) \to (Z \in (X L Y) \lor X = Y)$
21	4	adantr	$⊢ (φ \land Y \in (X I Z)) \to G \in 𝒢_{Tarski}$
22	5	adantr	$⊢ (φ \land Y \in (X I Z)) \to X \in P$
23	6	adantr	$⊢ (φ \land Y \in (X I Z)) \to Y \in P$
24	7	adantr	$⊢ (φ \land Y \in (X I Z)) \to Z \in P$
25		simpr	$⊢ (φ \land Y \in (X I Z)) \to Y \in (X I Z)$
26	1 2 3 21 22 23 24 25	btwncolg3	$⊢ (φ \land Y \in (X I Z)) \to (Z \in (X L Y) \lor X = Y)$
27	1 3 4 8 5 6 7	tgdim01	$⊢ φ \to (Z \in (X I Y) \lor X \in (Z I Y) \lor Y \in (X I Z))$
28	14 20 26 27	mpjao3dan	$⊢ φ \to (Z \in (X L Y) \lor X = Y)$

Metamath Proof Explorer

Theorem tgdim01ln

Proof