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 𝑃 = ( Base ‘ 𝐺 )
hpg.d = ( dist ‘ 𝐺 )
hpg.i 𝐼 = ( Itv ‘ 𝐺 )
hpg.o 𝑂 = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝑃𝐷 ) ∧ 𝑏 ∈ ( 𝑃𝐷 ) ) ∧ ∃ 𝑡𝐷 𝑡 ∈ ( 𝑎 𝐼 𝑏 ) ) }
islnoppd.a ( 𝜑𝐴𝑃 )
islnoppd.b ( 𝜑𝐵𝑃 )
islnoppd.c ( 𝜑𝐶𝐷 )
islnoppd.1 ( 𝜑 → ¬ 𝐴𝐷 )
islnoppd.2 ( 𝜑 → ¬ 𝐵𝐷 )
islnoppd.3 ( 𝜑𝐶 ∈ ( 𝐴 𝐼 𝐵 ) )
Assertion islnoppd ( 𝜑𝐴 𝑂 𝐵 )

Proof

Step Hyp Ref Expression
1 hpg.p 𝑃 = ( Base ‘ 𝐺 )
2 hpg.d = ( dist ‘ 𝐺 )
3 hpg.i 𝐼 = ( Itv ‘ 𝐺 )
4 hpg.o 𝑂 = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝑃𝐷 ) ∧ 𝑏 ∈ ( 𝑃𝐷 ) ) ∧ ∃ 𝑡𝐷 𝑡 ∈ ( 𝑎 𝐼 𝑏 ) ) }
5 islnoppd.a ( 𝜑𝐴𝑃 )
6 islnoppd.b ( 𝜑𝐵𝑃 )
7 islnoppd.c ( 𝜑𝐶𝐷 )
8 islnoppd.1 ( 𝜑 → ¬ 𝐴𝐷 )
9 islnoppd.2 ( 𝜑 → ¬ 𝐵𝐷 )
10 islnoppd.3 ( 𝜑𝐶 ∈ ( 𝐴 𝐼 𝐵 ) )
11 simpr ( ( 𝜑𝑡 = 𝐶 ) → 𝑡 = 𝐶 )
12 11 eleq1d ( ( 𝜑𝑡 = 𝐶 ) → ( 𝑡 ∈ ( 𝐴 𝐼 𝐵 ) ↔ 𝐶 ∈ ( 𝐴 𝐼 𝐵 ) ) )
13 7 12 10 rspcedvd ( 𝜑 → ∃ 𝑡𝐷 𝑡 ∈ ( 𝐴 𝐼 𝐵 ) )
14 8 9 13 jca31 ( 𝜑 → ( ( ¬ 𝐴𝐷 ∧ ¬ 𝐵𝐷 ) ∧ ∃ 𝑡𝐷 𝑡 ∈ ( 𝐴 𝐼 𝐵 ) ) )
15 1 2 3 4 5 6 islnopp ( 𝜑 → ( 𝐴 𝑂 𝐵 ↔ ( ( ¬ 𝐴𝐷 ∧ ¬ 𝐵𝐷 ) ∧ ∃ 𝑡𝐷 𝑡 ∈ ( 𝐴 𝐼 𝐵 ) ) ) )
16 14 15 mpbird ( 𝜑𝐴 𝑂 𝐵 )