Metamath Proof Explorer

Theorem hphl

Description: If two points are on the same half-line with endpoint on a line, they are on the same half-plane defined by this line. (Contributed by Thierry Arnoux, 9-Aug-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
hphl.k ⊢ K = hl 𝒢 ⁡ G
hphl.a ⊢ φ → A ∈ D
hphl.b ⊢ φ → B ∈ P
hphl.c ⊢ φ → C ∈ P
hphl.1 ⊢ φ → ¬ B ∈ D
hphl.2 ⊢ φ → B K ⁡ A C
Assertion hphl ⊢ φ → B hp 𝒢 ⁡ G ⁡ D C

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 hphl.k ⊢ K = hl 𝒢 ⁡ G
9 hphl.a ⊢ φ → A ∈ D
10 hphl.b ⊢ φ → B ∈ P
11 hphl.c ⊢ φ → C ∈ P
12 hphl.1 ⊢ φ → ¬ B ∈ D
13 hphl.2 ⊢ φ → B K ⁡ A C
14 1 2 8 10 11 6 4 3 13 hlln ⊢ φ → B ∈ C L A
15 14 orcd ⊢ φ → B ∈ C L A ∨ C = A
16 1 3 2 4 11 6 10 15 colrot2 ⊢ φ → A ∈ B L C ∨ B = C
17 1 2 3 4 5 10 7 11 9 16 8 colhp ⊢ φ → B hp 𝒢 ⁡ G ⁡ D C ↔ B K ⁡ A C ∧ ¬ B ∈ D
18 13 12 17 mpbir2and ⊢ φ → B hp 𝒢 ⁡ G ⁡ D C