opptgdim2

Description: If two points opposite to a line exist, dimension must be 2 or more. (Contributed by Thierry Arnoux, 3-Mar-2020)

	Ref	Expression
Hypotheses	hpg.p	$⊢ P = {Base}_{G}$
	hpg.d	$⊢ \underset{˙}{-} = dist (G)$
	hpg.i	$⊢ I = Itv (G)$
	hpg.o	$⊢ O = \{⟨a, b⟩ \| ((a \in (P ∖ D) \land b \in (P ∖ D)) \land \exists t \in D t \in (a I b))\}$
	opphl.l	$⊢ L = {Line}_{𝒢} (G)$
	opphl.d	$⊢ φ \to D \in ran L$
	opphl.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	oppcom.a	$⊢ φ \to A \in P$
	oppcom.b	$⊢ φ \to B \in P$
	oppcom.o	$⊢ φ \to A O B$
Assertion	opptgdim2	$⊢ φ \to G {Dim}_{𝒢} \geq 2$

Proof

Step	Hyp	Ref	Expression
1		hpg.p	$⊢ P = {Base}_{G}$
2		hpg.d	$⊢ \underset{˙}{-} = dist (G)$
3		hpg.i	$⊢ I = Itv (G)$
4		hpg.o	$⊢ O = \{⟨a, b⟩ \| ((a \in (P ∖ D) \land b \in (P ∖ D)) \land \exists t \in D t \in (a I b))\}$
5		opphl.l	$⊢ L = {Line}_{𝒢} (G)$
6		opphl.d	$⊢ φ \to D \in ran L$
7		opphl.g	$⊢ φ \to G \in 𝒢_{Tarski}$
8		oppcom.a	$⊢ φ \to A \in P$
9		oppcom.b	$⊢ φ \to B \in P$
10		oppcom.o	$⊢ φ \to A O B$
11	7	ad3antrrr	$⊢ (((φ \land x \in P) \land y \in P) \land (D = x L y \land x \neq y)) \to G \in 𝒢_{Tarski}$
12		simpllr	$⊢ (((φ \land x \in P) \land y \in P) \land (D = x L y \land x \neq y)) \to x \in P$
13		simplr	$⊢ (((φ \land x \in P) \land y \in P) \land (D = x L y \land x \neq y)) \to y \in P$
14	8	ad3antrrr	$⊢ (((φ \land x \in P) \land y \in P) \land (D = x L y \land x \neq y)) \to A \in P$
15	1 2 3 4 5 6 7 8 9 10	oppne1	$⊢ φ \to \neg A \in D$
16	15	ad3antrrr	$⊢ (((φ \land x \in P) \land y \in P) \land (D = x L y \land x \neq y)) \to \neg A \in D$
17		simprl	$⊢ (((φ \land x \in P) \land y \in P) \land (D = x L y \land x \neq y)) \to D = x L y$
18	16 17	neleqtrd	$⊢ (((φ \land x \in P) \land y \in P) \land (D = x L y \land x \neq y)) \to \neg A \in (x L y)$
19		simprr	$⊢ (((φ \land x \in P) \land y \in P) \land (D = x L y \land x \neq y)) \to x \neq y$
20	19	neneqd	$⊢ (((φ \land x \in P) \land y \in P) \land (D = x L y \land x \neq y)) \to \neg x = y$
21		ioran	$⊢ \neg (A \in (x L y) \lor x = y) \leftrightarrow (\neg A \in (x L y) \land \neg x = y)$
22	18 20 21	sylanbrc	$⊢ (((φ \land x \in P) \land y \in P) \land (D = x L y \land x \neq y)) \to \neg (A \in (x L y) \lor x = y)$
23	1 5 3 11 12 13 14 22	ncoltgdim2	$⊢ (((φ \land x \in P) \land y \in P) \land (D = x L y \land x \neq y)) \to G {Dim}_{𝒢} \geq 2$
24	1 3 5 7 6	tgisline	$⊢ φ \to \exists x \in P \exists y \in P (D = x L y \land x \neq y)$
25	23 24	r19.29vva	$⊢ φ \to G {Dim}_{𝒢} \geq 2$

Metamath Proof Explorer

Theorem opptgdim2

Proof