Metamath Proof Explorer

Theorem 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 ⊢ φ → G ∈ 𝒢 Tarski
hpgid.d ⊢ φ → D ∈ ran ⁡ L
hpgid.a ⊢ φ → A ∈ P
hpgid.o ⊢ O = a b | a ∈ P ∖ D ∧ b ∈ P ∖ D ∧ ∃ t ∈ D t ∈ a I b
hpgid.1 ⊢ φ → ¬ A ∈ D
Assertion hpgid ⊢ φ → A hp 𝒢 ⁡ G ⁡ D A

Proof

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 ⊢ φ → G ∈ 𝒢 Tarski
5 hpgid.d ⊢ φ → D ∈ ran ⁡ L
6 hpgid.a ⊢ φ → A ∈ P
7 hpgid.o ⊢ O = a b | a ∈ P ∖ D ∧ b ∈ P ∖ D ∧ ∃ t ∈ D t ∈ a I b
8 hpgid.1 ⊢ φ → ¬ A ∈ D
9 simprr ⊢ φ ∧ c ∈ P ∧ A O c → A O c
10 9 9 jca ⊢ φ ∧ c ∈ P ∧ A O c → A O c ∧ A O c
11 1 2 3 4 5 6 7 8 hpgerlem ⊢ φ → ∃ c ∈ P A O c
12 10 11 reximddv ⊢ φ → ∃ c ∈ P A O c ∧ A O c
13 1 2 3 7 4 5 6 6 hpgbr ⊢ φ → A hp 𝒢 ⁡ G ⁡ D A ↔ ∃ c ∈ P A O c ∧ A O c
14 12 13 mpbird ⊢ φ → A hp 𝒢 ⁡ G ⁡ D A