Metamath Proof Explorer

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	$⊢ P = {Base}_{G}$
		hpgid.i	$⊢ I = Itv (G)$
		hpgid.l	$⊢ L = {Line}_{𝒢} (G)$
		hpgid.g	$⊢ φ \to G \in 𝒢_{Tarski}$
		hpgid.d	$⊢ φ \to D \in ran L$
		hpgid.a	$⊢ φ \to A \in P$
		hpgid.o	$⊢ O = \{⟨a, b⟩ \| ((a \in (P ∖ D) \land b \in (P ∖ D)) \land \exists t \in D t \in (a I b))\}$
		hphl.k	$⊢ K = {hl}_{𝒢} (G)$
		hphl.a	$⊢ φ \to A \in D$
		hphl.b	$⊢ φ \to B \in P$
		hphl.c	$⊢ φ \to C \in P$
		hphl.1	$⊢ φ \to \neg B \in D$
		hphl.2	$⊢ φ \to B K (A) C$
	Assertion	hphl	$⊢ φ \to B {hp}_{𝒢} (G) (D) C$

Proof

Step	Hyp	Ref	Expression
1		hpgid.p	$⊢ P = {Base}_{G}$
2		hpgid.i	$⊢ I = Itv (G)$
3		hpgid.l	$⊢ L = {Line}_{𝒢} (G)$
4		hpgid.g	$⊢ φ \to G \in 𝒢_{Tarski}$
5		hpgid.d	$⊢ φ \to D \in ran L$
6		hpgid.a	$⊢ φ \to A \in P$
7		hpgid.o	$⊢ O = \{⟨a, b⟩ \| ((a \in (P ∖ D) \land b \in (P ∖ D)) \land \exists t \in D t \in (a I b))\}$
8		hphl.k	$⊢ K = {hl}_{𝒢} (G)$
9		hphl.a	$⊢ φ \to A \in D$
10		hphl.b	$⊢ φ \to B \in P$
11		hphl.c	$⊢ φ \to C \in P$
12		hphl.1	$⊢ φ \to \neg B \in D$
13		hphl.2	$⊢ φ \to B K (A) C$
14	1 2 8 10 11 6 4 3 13	hlln	$⊢ φ \to B \in (C L A)$
15	14	orcd	$⊢ φ \to (B \in (C L A) \lor C = A)$
16	1 3 2 4 11 6 10 15	colrot2	$⊢ φ \to (A \in (B L C) \lor B = C)$
17	1 2 3 4 5 10 7 11 9 16 8	colhp	$⊢ φ \to (B {hp}_{𝒢} (G) (D) C \leftrightarrow (B K (A) C \land \neg B \in D))$
18	13 12 17	mpbir2and	$⊢ φ \to B {hp}_{𝒢} (G) (D) C$