Theorem hphl

Description: If two points are on the same half-line with endpoint on a line, they are on the same half-plane defined by this line. (Contributed by Thierry Arnoux, 9-Aug-2020)

	Ref	Expression
Hypotheses	hpgid.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
	hpgid.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
	hpgid.l	⊢ 𝐿 = ( LineG ‘ 𝐺 )
	hpgid.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
	hpgid.d	⊢ ( 𝜑 → 𝐷 ∈ ran 𝐿 )
	hpgid.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
	hpgid.o	⊢ 𝑂 = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝑃 ∖ 𝐷 ) ∧ 𝑏 ∈ ( 𝑃 ∖ 𝐷 ) ) ∧ ∃ 𝑡 ∈ 𝐷 𝑡 ∈ ( 𝑎 𝐼 𝑏 ) ) }
	hphl.k	⊢ 𝐾 = ( hlG ‘ 𝐺 )
	hphl.a	⊢ ( 𝜑 → 𝐴 ∈ 𝐷 )
	hphl.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
	hphl.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
	hphl.1	⊢ ( 𝜑 → ¬ 𝐵 ∈ 𝐷 )
	hphl.2	⊢ ( 𝜑 → 𝐵 ( 𝐾 ‘ 𝐴 ) 𝐶 )
Assertion	hphl	⊢ ( 𝜑 → 𝐵 ( ( hpG ‘ 𝐺 ) ‘ 𝐷 ) 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		hpgid.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
2		hpgid.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
3		hpgid.l	⊢ 𝐿 = ( LineG ‘ 𝐺 )
4		hpgid.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
5		hpgid.d	⊢ ( 𝜑 → 𝐷 ∈ ran 𝐿 )
6		hpgid.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
7		hpgid.o	⊢ 𝑂 = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝑃 ∖ 𝐷 ) ∧ 𝑏 ∈ ( 𝑃 ∖ 𝐷 ) ) ∧ ∃ 𝑡 ∈ 𝐷 𝑡 ∈ ( 𝑎 𝐼 𝑏 ) ) }
8		hphl.k	⊢ 𝐾 = ( hlG ‘ 𝐺 )
9		hphl.a	⊢ ( 𝜑 → 𝐴 ∈ 𝐷 )
10		hphl.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
11		hphl.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
12		hphl.1	⊢ ( 𝜑 → ¬ 𝐵 ∈ 𝐷 )
13		hphl.2	⊢ ( 𝜑 → 𝐵 ( 𝐾 ‘ 𝐴 ) 𝐶 )
14	1 2 8 10 11 6 4 3 13	hlln	⊢ ( 𝜑 → 𝐵 ∈ ( 𝐶 𝐿 𝐴 ) )
15	14	orcd	⊢ ( 𝜑 → ( 𝐵 ∈ ( 𝐶 𝐿 𝐴 ) ∨ 𝐶 = 𝐴 ) )
16	1 3 2 4 11 6 10 15	colrot2	⊢ ( 𝜑 → ( 𝐴 ∈ ( 𝐵 𝐿 𝐶 ) ∨ 𝐵 = 𝐶 ) )
17	1 2 3 4 5 10 7 11 9 16 8	colhp	⊢ ( 𝜑 → ( 𝐵 ( ( hpG ‘ 𝐺 ) ‘ 𝐷 ) 𝐶 ↔ ( 𝐵 ( 𝐾 ‘ 𝐴 ) 𝐶 ∧ ¬ 𝐵 ∈ 𝐷 ) ) )
18	13 12 17	mpbir2and	⊢ ( 𝜑 → 𝐵 ( ( hpG ‘ 𝐺 ) ‘ 𝐷 ) 𝐶 )