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 = {Base}_{G}$
	tgdim01.i	$⊢ I = Itv (G)$
	tgdim01.g	$⊢ φ \to G \in V$
	tgdim01.1	$⊢ φ \to \neg G {Dim}_{𝒢} \geq 2$
	tgdim01.x	$⊢ φ \to X \in P$
	tgdim01.y	$⊢ φ \to Y \in P$
	tgdim01.z	$⊢ φ \to Z \in P$
Assertion	tgdim01	$⊢ φ \to (Z \in (X I Y) \lor X \in (Z I Y) \lor Y \in (X I Z))$

Proof

Step	Hyp	Ref	Expression
1		tgdim01.p	$⊢ P = {Base}_{G}$
2		tgdim01.i	$⊢ I = Itv (G)$
3		tgdim01.g	$⊢ φ \to G \in V$
4		tgdim01.1	$⊢ φ \to \neg G {Dim}_{𝒢} \geq 2$
5		tgdim01.x	$⊢ φ \to X \in P$
6		tgdim01.y	$⊢ φ \to Y \in P$
7		tgdim01.z	$⊢ φ \to Z \in P$
8		eqid	$⊢ dist (G) = dist (G)$
9	1 8 2	istrkg2ld	$⊢ G \in V \to (G {Dim}_{𝒢} \geq 2 \leftrightarrow \exists x \in P \exists y \in P \exists z \in P \neg (z \in (x I y) \lor x \in (z I y) \lor y \in (x I z)))$
10	3 9	syl	$⊢ φ \to (G {Dim}_{𝒢} \geq 2 \leftrightarrow \exists x \in P \exists y \in P \exists z \in P \neg (z \in (x I y) \lor x \in (z I y) \lor y \in (x I z)))$
11	4 10	mtbid	$⊢ φ \to \neg \exists x \in P \exists y \in P \exists z \in P \neg (z \in (x I y) \lor x \in (z I y) \lor y \in (x I z))$
12		rexnal3	$⊢ \exists x \in P \exists y \in P \exists z \in P \neg (z \in (x I y) \lor x \in (z I y) \lor y \in (x I z)) \leftrightarrow \neg \forall x \in P \forall y \in P \forall z \in P (z \in (x I y) \lor x \in (z I y) \lor y \in (x I z))$
13	12	con2bii	$⊢ \forall x \in P \forall y \in P \forall z \in P (z \in (x I y) \lor x \in (z I y) \lor y \in (x I z)) \leftrightarrow \neg \exists x \in P \exists y \in P \exists z \in P \neg (z \in (x I y) \lor x \in (z I y) \lor y \in (x I z))$
14	11 13	sylibr	$⊢ φ \to \forall x \in P \forall y \in P \forall z \in P (z \in (x I y) \lor x \in (z I y) \lor y \in (x I z))$
15		oveq1	$⊢ x = X \to x I y = X I y$
16	15	eleq2d	$⊢ x = X \to (z \in (x I y) \leftrightarrow z \in (X I y))$
17		eleq1	$⊢ x = X \to (x \in (z I y) \leftrightarrow X \in (z I y))$
18		oveq1	$⊢ x = X \to x I z = X I z$
19	18	eleq2d	$⊢ x = X \to (y \in (x I z) \leftrightarrow y \in (X I z))$
20	16 17 19	3orbi123d	$⊢ x = X \to ((z \in (x I y) \lor x \in (z I y) \lor y \in (x I z)) \leftrightarrow (z \in (X I y) \lor X \in (z I y) \lor y \in (X I z)))$
21		oveq2	$⊢ y = Y \to X I y = X I Y$
22	21	eleq2d	$⊢ y = Y \to (z \in (X I y) \leftrightarrow z \in (X I Y))$
23		oveq2	$⊢ y = Y \to z I y = z I Y$
24	23	eleq2d	$⊢ y = Y \to (X \in (z I y) \leftrightarrow X \in (z I Y))$
25		eleq1	$⊢ y = Y \to (y \in (X I z) \leftrightarrow Y \in (X I z))$
26	22 24 25	3orbi123d	$⊢ y = Y \to ((z \in (X I y) \lor X \in (z I y) \lor y \in (X I z)) \leftrightarrow (z \in (X I Y) \lor X \in (z I Y) \lor Y \in (X I z)))$
27		eleq1	$⊢ z = Z \to (z \in (X I Y) \leftrightarrow Z \in (X I Y))$
28		oveq1	$⊢ z = Z \to z I Y = Z I Y$
29	28	eleq2d	$⊢ z = Z \to (X \in (z I Y) \leftrightarrow X \in (Z I Y))$
30		oveq2	$⊢ z = Z \to X I z = X I Z$
31	30	eleq2d	$⊢ z = Z \to (Y \in (X I z) \leftrightarrow Y \in (X I Z))$
32	27 29 31	3orbi123d	$⊢ z = Z \to ((z \in (X I Y) \lor X \in (z I Y) \lor Y \in (X I z)) \leftrightarrow (Z \in (X I Y) \lor X \in (Z I Y) \lor Y \in (X I Z)))$
33	20 26 32	rspc3v	$⊢ (X \in P \land Y \in P \land Z \in P) \to (\forall x \in P \forall y \in P \forall z \in P (z \in (x I y) \lor x \in (z I y) \lor y \in (x I z)) \to (Z \in (X I Y) \lor X \in (Z I Y) \lor Y \in (X I Z)))$
34	33	imp	$⊢ ((X \in P \land Y \in P \land Z \in P) \land \forall x \in P \forall y \in P \forall z \in P (z \in (x I y) \lor x \in (z I y) \lor y \in (x I z))) \to (Z \in (X I Y) \lor X \in (Z I Y) \lor Y \in (X I Z))$
35	5 6 7 14 34	syl31anc	$⊢ φ \to (Z \in (X I Y) \lor X \in (Z I Y) \lor Y \in (X I Z))$

Metamath Proof Explorer

Theorem tgdim01

Proof