hpgne1

Description: Points on the open half plane cannot lie on its border. (Contributed by Thierry Arnoux, 4-Mar-2020)

	Ref	Expression
Hypotheses	ishpg.p	$⊢ P = {Base}_{G}$
	ishpg.i	$⊢ I = Itv (G)$
	ishpg.l	$⊢ L = {Line}_{𝒢} (G)$
	ishpg.o	$⊢ O = \{⟨a, b⟩ \| ((a \in (P ∖ D) \land b \in (P ∖ D)) \land \exists t \in D t \in (a I b))\}$
	ishpg.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	ishpg.d	$⊢ φ \to D \in ran L$
	hpgbr.a	$⊢ φ \to A \in P$
	hpgbr.b	$⊢ φ \to B \in P$
	hpgne1.1	$⊢ φ \to A {hp}_{𝒢} (G) (D) B$
Assertion	hpgne1	$⊢ φ \to \neg A \in D$

Step	Hyp	Ref	Expression
1		ishpg.p	$⊢ P = {Base}_{G}$
2		ishpg.i	$⊢ I = Itv (G)$
3		ishpg.l	$⊢ L = {Line}_{𝒢} (G)$
4		ishpg.o	$⊢ O = \{⟨a, b⟩ \| ((a \in (P ∖ D) \land b \in (P ∖ D)) \land \exists t \in D t \in (a I b))\}$
5		ishpg.g	$⊢ φ \to G \in 𝒢_{Tarski}$
6		ishpg.d	$⊢ φ \to D \in ran L$
7		hpgbr.a	$⊢ φ \to A \in P$
8		hpgbr.b	$⊢ φ \to B \in P$
9		hpgne1.1	$⊢ φ \to A {hp}_{𝒢} (G) (D) B$
10		eqid	$⊢ dist (G) = dist (G)$
11	6	ad2antrr	$⊢ ((φ \land c \in P) \land (A O c \land B O c)) \to D \in ran L$
12	5	ad2antrr	$⊢ ((φ \land c \in P) \land (A O c \land B O c)) \to G \in 𝒢_{Tarski}$
13	7	ad2antrr	$⊢ ((φ \land c \in P) \land (A O c \land B O c)) \to A \in P$
14		simplr	$⊢ ((φ \land c \in P) \land (A O c \land B O c)) \to c \in P$
15		simprl	$⊢ ((φ \land c \in P) \land (A O c \land B O c)) \to A O c$
16	1 10 2 4 3 11 12 13 14 15	oppne1	$⊢ ((φ \land c \in P) \land (A O c \land B O c)) \to \neg A \in D$
17	1 2 3 4 5 6 7 8	hpgbr	$⊢ φ \to (A {hp}_{𝒢} (G) (D) B \leftrightarrow \exists c \in P (A O c \land B O c))$
18	9 17	mpbid	$⊢ φ \to \exists c \in P (A O c \land B O c)$
19	16 18	r19.29a	$⊢ φ \to \neg A \in D$

Metamath Proof Explorer