Metamath Proof Explorer

Theorem hpgcom

Description: The half-plane relation commutes. Theorem 9.12 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
Assertion hpgcom ⊢ φ → B 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 hpgcom.b ⊢ φ → B ∈ P
9 hpgcom.1 ⊢ φ → A hp 𝒢 ⁡ G ⁡ D B
10 ancom ⊢ A O c ∧ B O c ↔ B O c ∧ A O c
11 10 a1i ⊢ φ → A O c ∧ B O c ↔ B O c ∧ A O c
12 11 rexbidv ⊢ φ → ∃ c ∈ P A O c ∧ B O c ↔ ∃ c ∈ P B O c ∧ A O c
13 1 2 3 7 4 5 6 8 hpgbr ⊢ φ → A hp 𝒢 ⁡ G ⁡ D B ↔ ∃ c ∈ P A O c ∧ B O c
14 1 2 3 7 4 5 8 6 hpgbr ⊢ φ → B hp 𝒢 ⁡ G ⁡ D A ↔ ∃ c ∈ P B O c ∧ A O c
15 12 13 14 3bitr4d ⊢ φ → A hp 𝒢 ⁡ G ⁡ D B ↔ B hp 𝒢 ⁡ G ⁡ D A
16 9 15 mpbid ⊢ φ → B hp 𝒢 ⁡ G ⁡ D A