Metamath Proof Explorer

Theorem hpgbr

Description: Half-planes : property for points A and B to belong to the same open half plane delimited by line D . Definition 9.7 of Schwabhauser p. 71. (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
Assertion hpgbr ⊢ φ → A hp 𝒢 ⁡ G ⁡ D B ↔ ∃ c ∈ P A O c ∧ B O c

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 1 2 3 4 5 6 ishpg ⊢ φ → hp 𝒢 ⁡ G ⁡ D = a b | ∃ c ∈ P a O c ∧ b O c
10 simpl ⊢ a = u ∧ b = v → a = u
11 10 breq1d ⊢ a = u ∧ b = v → a O c ↔ u O c
12 simpr ⊢ a = u ∧ b = v → b = v
13 12 breq1d ⊢ a = u ∧ b = v → b O c ↔ v O c
14 11 13 anbi12d ⊢ a = u ∧ b = v → a O c ∧ b O c ↔ u O c ∧ v O c
15 14 rexbidv ⊢ a = u ∧ b = v → ∃ c ∈ P a O c ∧ b O c ↔ ∃ c ∈ P u O c ∧ v O c
16 15 cbvopabv ⊢ a b | ∃ c ∈ P a O c ∧ b O c = u v | ∃ c ∈ P u O c ∧ v O c
17 9 16 eqtrdi ⊢ φ → hp 𝒢 ⁡ G ⁡ D = u v | ∃ c ∈ P u O c ∧ v O c
18 17 breqd ⊢ φ → A hp 𝒢 ⁡ G ⁡ D B ↔ A u v | ∃ c ∈ P u O c ∧ v O c B
19 simpl ⊢ u = A ∧ v = B → u = A
20 19 breq1d ⊢ u = A ∧ v = B → u O c ↔ A O c
21 simpr ⊢ u = A ∧ v = B → v = B
22 21 breq1d ⊢ u = A ∧ v = B → v O c ↔ B O c
23 20 22 anbi12d ⊢ u = A ∧ v = B → u O c ∧ v O c ↔ A O c ∧ B O c
24 23 rexbidv ⊢ u = A ∧ v = B → ∃ c ∈ P u O c ∧ v O c ↔ ∃ c ∈ P A O c ∧ B O c
25 eqid ⊢ u v | ∃ c ∈ P u O c ∧ v O c = u v | ∃ c ∈ P u O c ∧ v O c
26 24 25 brabga ⊢ A ∈ P ∧ B ∈ P → A u v | ∃ c ∈ P u O c ∧ v O c B ↔ ∃ c ∈ P A O c ∧ B O c
27 7 8 26 syl2anc ⊢ φ → A u v | ∃ c ∈ P u O c ∧ v O c B ↔ ∃ c ∈ P A O c ∧ B O c
28 18 27 bitrd ⊢ φ → A hp 𝒢 ⁡ G ⁡ D B ↔ ∃ c ∈ P A O c ∧ B O c