Metamath Proof Explorer

Theorem lnoppnhpg

Description: If two points lie on the opposite side of a line D , they are not on the same half-plane. Theorem 9.9 of Schwabhauser p. 72. (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$
		lnoppnhpg.1	$⊢ φ \to A O B$
	Assertion	lnoppnhpg	$⊢ φ \to \neg A {hp}_{𝒢} (G) (D) B$

Proof

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		lnoppnhpg.1	$⊢ φ \to A O B$
10		eqid	$⊢ dist (G) = dist (G)$
11	1 10 2 4 3 6 5 8	oppnid	$⊢ φ \to \neg B O B$
12	1 2 3 4 5 6 7 8 8 9	lnopp2hpgb	$⊢ φ \to (B O B \leftrightarrow A {hp}_{𝒢} (G) (D) B)$
13	11 12	mtbid	$⊢ φ \to \neg A {hp}_{𝒢} (G) (D) B$