hpgid

Description: The half-plane relation is reflexive. Theorem 9.11 of Schwabhauser p. 72. (Contributed by Thierry Arnoux, 4-Mar-2020)

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

Step	Hyp	Ref	Expression
1		hpgid.p	$⊢ P = {Base}_{G}$
2		hpgid.i	$⊢ I = Itv (G)$
3		hpgid.l	$⊢ L = {Line}_{𝒢} (G)$
4		hpgid.g	$⊢ φ \to G \in 𝒢_{Tarski}$
5		hpgid.d	$⊢ φ \to D \in ran L$
6		hpgid.a	$⊢ φ \to A \in P$
7		hpgid.o	$⊢ O = \{⟨a, b⟩ \| ((a \in (P ∖ D) \land b \in (P ∖ D)) \land \exists t \in D t \in (a I b))\}$
8		hpgid.1	$⊢ φ \to \neg A \in D$
9		simprr	$⊢ (φ \land (c \in P \land A O c)) \to A O c$
10	9 9	jca	$⊢ (φ \land (c \in P \land A O c)) \to (A O c \land A O c)$
11	1 2 3 4 5 6 7 8	hpgerlem	$⊢ φ \to \exists c \in P A O c$
12	10 11	reximddv	$⊢ φ \to \exists c \in P (A O c \land A O c)$
13	1 2 3 7 4 5 6 6	hpgbr	$⊢ φ \to (A {hp}_{𝒢} (G) (D) A \leftrightarrow \exists c \in P (A O c \land A O c))$
14	12 13	mpbird	$⊢ φ \to A {hp}_{𝒢} (G) (D) A$

Metamath Proof Explorer