Metamath Proof Explorer

Theorem hpgtr

Description: The half-plane relation is transitive. Theorem 9.13 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
hpgcom.b ⊢ φ → B ∈ P
hpgcom.1 ⊢ φ → A hp 𝒢 ⁡ G ⁡ D B
hpgtr.c ⊢ φ → C ∈ P
hpgtr.1 ⊢ φ → B hp 𝒢 ⁡ G ⁡ D C
Assertion hpgtr ⊢ φ → A 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 hpgcom.b ⊢ φ → B ∈ P
9 hpgcom.1 ⊢ φ → A hp 𝒢 ⁡ G ⁡ D B
10 hpgtr.c ⊢ φ → C ∈ P
11 hpgtr.1 ⊢ φ → B hp 𝒢 ⁡ G ⁡ D C
12 1 2 3 7 4 5 6 8 hpgbr ⊢ φ → A hp 𝒢 ⁡ G ⁡ D B ↔ ∃ c ∈ P A O c ∧ B O c
13 9 12 mpbid ⊢ φ → ∃ c ∈ P A O c ∧ B O c
14 simprl ⊢ φ ∧ c ∈ P ∧ A O c ∧ B O c → A O c
15 11 ad2antrr ⊢ φ ∧ c ∈ P ∧ A O c ∧ B O c → B hp 𝒢 ⁡ G ⁡ D C
16 4 ad2antrr ⊢ φ ∧ c ∈ P ∧ A O c ∧ B O c → G ∈ 𝒢 Tarski
17 5 ad2antrr ⊢ φ ∧ c ∈ P ∧ A O c ∧ B O c → D ∈ ran ⁡ L
18 8 ad2antrr ⊢ φ ∧ c ∈ P ∧ A O c ∧ B O c → B ∈ P
19 10 ad2antrr ⊢ φ ∧ c ∈ P ∧ A O c ∧ B O c → C ∈ P
20 simplr ⊢ φ ∧ c ∈ P ∧ A O c ∧ B O c → c ∈ P
21 simprr ⊢ φ ∧ c ∈ P ∧ A O c ∧ B O c → B O c
22 1 2 3 7 16 17 18 19 20 21 lnopp2hpgb ⊢ φ ∧ c ∈ P ∧ A O c ∧ B O c → C O c ↔ B hp 𝒢 ⁡ G ⁡ D C
23 15 22 mpbird ⊢ φ ∧ c ∈ P ∧ A O c ∧ B O c → C O c
24 14 23 jca ⊢ φ ∧ c ∈ P ∧ A O c ∧ B O c → A O c ∧ C O c
25 24 ex ⊢ φ ∧ c ∈ P → A O c ∧ B O c → A O c ∧ C O c
26 25 reximdva ⊢ φ → ∃ c ∈ P A O c ∧ B O c → ∃ c ∈ P A O c ∧ C O c
27 13 26 mpd ⊢ φ → ∃ c ∈ P A O c ∧ C O c
28 1 2 3 7 4 5 6 10 hpgbr ⊢ φ → A hp 𝒢 ⁡ G ⁡ D C ↔ ∃ c ∈ P A O c ∧ C O c
29 27 28 mpbird ⊢ φ → A hp 𝒢 ⁡ G ⁡ D C