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 ∈ P ∖ D ∧ b ∈ P ∖ D ∧ ∃ t ∈ D t ∈ a I b
ishpg.g ⊢ φ → G ∈ 𝒢 Tarski
ishpg.d ⊢ φ → D ∈ ran ⁡ L
hpgbr.a ⊢ φ → A ∈ P
hpgbr.b ⊢ φ → B ∈ P
lnoppnhpg.1 ⊢ φ → A O B
Assertion lnoppnhpg ⊢ φ → ¬ 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 ∈ P ∖ D ∧ b ∈ P ∖ D ∧ ∃ t ∈ D t ∈ a I b
5 ishpg.g ⊢ φ → G ∈ 𝒢 Tarski
6 ishpg.d ⊢ φ → D ∈ ran ⁡ L
7 hpgbr.a ⊢ φ → A ∈ P
8 hpgbr.b ⊢ φ → B ∈ P
9 lnoppnhpg.1 ⊢ φ → A O B
10 eqid ⊢ dist ⁡ G = dist ⁡ G
11 1 10 2 4 3 6 5 8 oppnid ⊢ φ → ¬ B O B
12 1 2 3 4 5 6 7 8 8 9 lnopp2hpgb ⊢ φ → B O B ↔ A hp 𝒢 ⁡ G ⁡ D B
13 11 12 mtbid ⊢ φ → ¬ A hp 𝒢 ⁡ G ⁡ D B