Metamath Proof Explorer

Theorem islnoppd

Description: Deduce that A and B lie on opposite sides of line L . (Contributed by Thierry Arnoux, 16-Aug-2020)

Ref Expression
Hypotheses hpg.p ⊢ P = Base G
hpg.d ⊢ - ˙ = dist ⁡ G
hpg.i ⊢ I = Itv ⁡ G
hpg.o ⊢ O = a b | a ∈ P ∖ D ∧ b ∈ P ∖ D ∧ ∃ t ∈ D t ∈ a I b
islnoppd.a ⊢ φ → A ∈ P
islnoppd.b ⊢ φ → B ∈ P
islnoppd.c ⊢ φ → C ∈ D
islnoppd.1 ⊢ φ → ¬ A ∈ D
islnoppd.2 ⊢ φ → ¬ B ∈ D
islnoppd.3 ⊢ φ → C ∈ A I B
Assertion islnoppd ⊢ φ → A O B

Proof

Step Hyp Ref Expression
1 hpg.p ⊢ P = Base G
2 hpg.d ⊢ - ˙ = dist ⁡ G
3 hpg.i ⊢ I = Itv ⁡ G
4 hpg.o ⊢ O = a b | a ∈ P ∖ D ∧ b ∈ P ∖ D ∧ ∃ t ∈ D t ∈ a I b
5 islnoppd.a ⊢ φ → A ∈ P
6 islnoppd.b ⊢ φ → B ∈ P
7 islnoppd.c ⊢ φ → C ∈ D
8 islnoppd.1 ⊢ φ → ¬ A ∈ D
9 islnoppd.2 ⊢ φ → ¬ B ∈ D
10 islnoppd.3 ⊢ φ → C ∈ A I B
11 simpr ⊢ φ ∧ t = C → t = C
12 11 eleq1d ⊢ φ ∧ t = C → t ∈ A I B ↔ C ∈ A I B
13 7 12 10 rspcedvd ⊢ φ → ∃ t ∈ D t ∈ A I B
14 8 9 13 jca31 ⊢ φ → ¬ A ∈ D ∧ ¬ B ∈ D ∧ ∃ t ∈ D t ∈ A I B
15 1 2 3 4 5 6 islnopp ⊢ φ → A O B ↔ ¬ A ∈ D ∧ ¬ B ∈ D ∧ ∃ t ∈ D t ∈ A I B
16 14 15 mpbird ⊢ φ → A O B