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	⊢ ( 𝜑 → 𝐴 𝑂 𝐵 )