prlnghpg

Description: If two lines A and B are parallel, then any two points X and Y of B lie on the same half-plane limited by A . Theorem 12.6 of Schwabhauser p. 122. . (Contributed by Thierry Arnoux, 5-Jul-2026)

	Ref	Expression
Hypotheses	prlnghpg.l	$⊢ L = {Line}_{𝒢} (G)$
	prlnghpg.e	No typesetting found for \|- E = ( PlnG ` G ) with typecode \|-
	prlnghpg.p	No typesetting found for \|- .\|\| = ( parlnG ` G ) with typecode \|-
	prlnghpg.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	prlnghpg.1	$⊢ φ \to A \underset{˙}{∥} B$
	prlnghpg.2	$⊢ φ \to A \neq B$
	prlnghpg.x	$⊢ φ \to X \in B$
	prlnghpg.y	$⊢ φ \to Y \in B$
Assertion	prlnghpg	$⊢ φ \to X {hp}_{𝒢} (G) (A) Y$

Proof

Step	Hyp	Ref	Expression
1		prlnghpg.l	$⊢ L = {Line}_{𝒢} (G)$
2		prlnghpg.e	Could not format E = ( PlnG ` G ) : No typesetting found for \|- E = ( PlnG ` G ) with typecode \|-
3		prlnghpg.p	Could not format .\|\| = ( parlnG ` G ) : No typesetting found for \|- .\|\| = ( parlnG ` G ) with typecode \|-
4		prlnghpg.g	$⊢ φ \to G \in 𝒢_{Tarski}$
5		prlnghpg.1	$⊢ φ \to A \underset{˙}{∥} B$
6		prlnghpg.2	$⊢ φ \to A \neq B$
7		prlnghpg.x	$⊢ φ \to X \in B$
8		prlnghpg.y	$⊢ φ \to Y \in B$
9		eqid	$⊢ {Base}_{G} = {Base}_{G}$
10		eqid	$⊢ Itv (G) = Itv (G)$
11	1 2 3 4	brprlng	$⊢ φ \to (A \underset{˙}{∥} B \leftrightarrow ((A \in ran L \land B \in ran L) \land (A = B \lor (\exists h \in ran E (A \subseteq h \land B \subseteq h) \land A \cap B = \emptyset))))$
12	5 11	mpbid	$⊢ φ \to ((A \in ran L \land B \in ran L) \land (A = B \lor (\exists h \in ran E (A \subseteq h \land B \subseteq h) \land A \cap B = \emptyset)))$
13	12	simpld	$⊢ φ \to (A \in ran L \land B \in ran L)$
14	13	simpld	$⊢ φ \to A \in ran L$
15	13	simprd	$⊢ φ \to B \in ran L$
16	9 1 10 4 15 8	tglnpt	$⊢ φ \to Y \in {Base}_{G}$
17		eleq1w	$⊢ a = c \to (a \in ({Base}_{G} ∖ A) \leftrightarrow c \in ({Base}_{G} ∖ A))$
18		eleq1w	$⊢ b = d \to (b \in ({Base}_{G} ∖ A) \leftrightarrow d \in ({Base}_{G} ∖ A))$
19	17 18	bi2anan9	$⊢ (a = c \land b = d) \to ((a \in ({Base}_{G} ∖ A) \land b \in ({Base}_{G} ∖ A)) \leftrightarrow (c \in ({Base}_{G} ∖ A) \land d \in ({Base}_{G} ∖ A)))$
20		oveq12	$⊢ (a = c \land b = d) \to a Itv (G) b = c Itv (G) d$
21	20	eleq2d	$⊢ (a = c \land b = d) \to (s \in (a Itv (G) b) \leftrightarrow s \in (c Itv (G) d))$
22	21	rexbidv	$⊢ (a = c \land b = d) \to (\exists s \in A s \in (a Itv (G) b) \leftrightarrow \exists s \in A s \in (c Itv (G) d))$
23		eleq1w	$⊢ s = t \to (s \in (c Itv (G) d) \leftrightarrow t \in (c Itv (G) d))$
24	23	cbvrexvw	$⊢ \exists s \in A s \in (c Itv (G) d) \leftrightarrow \exists t \in A t \in (c Itv (G) d)$
25	22 24	bitrdi	$⊢ (a = c \land b = d) \to (\exists s \in A s \in (a Itv (G) b) \leftrightarrow \exists t \in A t \in (c Itv (G) d))$
26	19 25	anbi12d	$⊢ (a = c \land b = d) \to (((a \in ({Base}_{G} ∖ A) \land b \in ({Base}_{G} ∖ A)) \land \exists s \in A s \in (a Itv (G) b)) \leftrightarrow ((c \in ({Base}_{G} ∖ A) \land d \in ({Base}_{G} ∖ A)) \land \exists t \in A t \in (c Itv (G) d)))$
27	26	cbvopabv	$⊢ \{⟨a, b⟩ \| ((a \in ({Base}_{G} ∖ A) \land b \in ({Base}_{G} ∖ A)) \land \exists s \in A s \in (a Itv (G) b))\} = \{⟨c, d⟩ \| ((c \in ({Base}_{G} ∖ A) \land d \in ({Base}_{G} ∖ A)) \land \exists t \in A t \in (c Itv (G) d))\}$
28	9 1 10 4 15 7	tglnpt	$⊢ φ \to X \in {Base}_{G}$
29	4	adantr	$⊢ (φ \land Y = X) \to G \in 𝒢_{Tarski}$
30	14	adantr	$⊢ (φ \land Y = X) \to A \in ran L$
31	16	adantr	$⊢ (φ \land Y = X) \to Y \in {Base}_{G}$
32	12	simprd	$⊢ φ \to (A = B \lor (\exists h \in ran E (A \subseteq h \land B \subseteq h) \land A \cap B = \emptyset))$
33	6	neneqd	$⊢ φ \to \neg A = B$
34	32 33	orcnd	$⊢ φ \to (\exists h \in ran E (A \subseteq h \land B \subseteq h) \land A \cap B = \emptyset)$
35	34	simprd	$⊢ φ \to A \cap B = \emptyset$
36	35	adantr	$⊢ (φ \land Y \in A) \to A \cap B = \emptyset$
37		simpr	$⊢ (φ \land Y \in A) \to Y \in A$
38	8	adantr	$⊢ (φ \land Y \in A) \to Y \in B$
39		inelcm	$⊢ (Y \in A \land Y \in B) \to A \cap B \neq \emptyset$
40	37 38 39	syl2anc	$⊢ (φ \land Y \in A) \to A \cap B \neq \emptyset$
41	40	neneqd	$⊢ (φ \land Y \in A) \to \neg A \cap B = \emptyset$
42	36 41	pm2.65da	$⊢ φ \to \neg Y \in A$
43	42	adantr	$⊢ (φ \land Y = X) \to \neg Y \in A$
44	9 10 1 29 30 31 27 43	hpgid	$⊢ (φ \land Y = X) \to Y {hp}_{𝒢} (G) (A) Y$
45		simpr	$⊢ (φ \land Y = X) \to Y = X$
46	44 45	breqtrd	$⊢ (φ \land Y = X) \to Y {hp}_{𝒢} (G) (A) X$
47	42	adantr	$⊢ (φ \land Y \neq X) \to \neg Y \in A$
48	35	ad2antrr	$⊢ ((φ \land Y \neq X) \land Y \{⟨a, b⟩ \| ((a \in ({Base}_{G} ∖ A) \land b \in ({Base}_{G} ∖ A)) \land \exists s \in A s \in (a Itv (G) b))\} X) \to A \cap B = \emptyset$
49		simplr	$⊢ ((((φ \land Y \neq X) \land Y \{⟨a, b⟩ \| ((a \in ({Base}_{G} ∖ A) \land b \in ({Base}_{G} ∖ A)) \land \exists s \in A s \in (a Itv (G) b))\} X) \land t \in A) \land t \in (Y Itv (G) X)) \to t \in A$
50	4	ad4antr	$⊢ ((((φ \land Y \neq X) \land Y \{⟨a, b⟩ \| ((a \in ({Base}_{G} ∖ A) \land b \in ({Base}_{G} ∖ A)) \land \exists s \in A s \in (a Itv (G) b))\} X) \land t \in A) \land t \in (Y Itv (G) X)) \to G \in 𝒢_{Tarski}$
51	16	ad4antr	$⊢ ((((φ \land Y \neq X) \land Y \{⟨a, b⟩ \| ((a \in ({Base}_{G} ∖ A) \land b \in ({Base}_{G} ∖ A)) \land \exists s \in A s \in (a Itv (G) b))\} X) \land t \in A) \land t \in (Y Itv (G) X)) \to Y \in {Base}_{G}$
52	28	ad4antr	$⊢ ((((φ \land Y \neq X) \land Y \{⟨a, b⟩ \| ((a \in ({Base}_{G} ∖ A) \land b \in ({Base}_{G} ∖ A)) \land \exists s \in A s \in (a Itv (G) b))\} X) \land t \in A) \land t \in (Y Itv (G) X)) \to X \in {Base}_{G}$
53	14	ad4antr	$⊢ ((((φ \land Y \neq X) \land Y \{⟨a, b⟩ \| ((a \in ({Base}_{G} ∖ A) \land b \in ({Base}_{G} ∖ A)) \land \exists s \in A s \in (a Itv (G) b))\} X) \land t \in A) \land t \in (Y Itv (G) X)) \to A \in ran L$
54	9 1 10 50 53 49	tglnpt	$⊢ ((((φ \land Y \neq X) \land Y \{⟨a, b⟩ \| ((a \in ({Base}_{G} ∖ A) \land b \in ({Base}_{G} ∖ A)) \land \exists s \in A s \in (a Itv (G) b))\} X) \land t \in A) \land t \in (Y Itv (G) X)) \to t \in {Base}_{G}$
55		simp-4r	$⊢ ((((φ \land Y \neq X) \land Y \{⟨a, b⟩ \| ((a \in ({Base}_{G} ∖ A) \land b \in ({Base}_{G} ∖ A)) \land \exists s \in A s \in (a Itv (G) b))\} X) \land t \in A) \land t \in (Y Itv (G) X)) \to Y \neq X$
56		simpr	$⊢ ((((φ \land Y \neq X) \land Y \{⟨a, b⟩ \| ((a \in ({Base}_{G} ∖ A) \land b \in ({Base}_{G} ∖ A)) \land \exists s \in A s \in (a Itv (G) b))\} X) \land t \in A) \land t \in (Y Itv (G) X)) \to t \in (Y Itv (G) X)$
57	9 10 1 50 51 52 54 55 56	btwnlng1	$⊢ ((((φ \land Y \neq X) \land Y \{⟨a, b⟩ \| ((a \in ({Base}_{G} ∖ A) \land b \in ({Base}_{G} ∖ A)) \land \exists s \in A s \in (a Itv (G) b))\} X) \land t \in A) \land t \in (Y Itv (G) X)) \to t \in (Y L X)$
58	15	ad4antr	$⊢ ((((φ \land Y \neq X) \land Y \{⟨a, b⟩ \| ((a \in ({Base}_{G} ∖ A) \land b \in ({Base}_{G} ∖ A)) \land \exists s \in A s \in (a Itv (G) b))\} X) \land t \in A) \land t \in (Y Itv (G) X)) \to B \in ran L$
59	8	ad4antr	$⊢ ((((φ \land Y \neq X) \land Y \{⟨a, b⟩ \| ((a \in ({Base}_{G} ∖ A) \land b \in ({Base}_{G} ∖ A)) \land \exists s \in A s \in (a Itv (G) b))\} X) \land t \in A) \land t \in (Y Itv (G) X)) \to Y \in B$
60	7	ad4antr	$⊢ ((((φ \land Y \neq X) \land Y \{⟨a, b⟩ \| ((a \in ({Base}_{G} ∖ A) \land b \in ({Base}_{G} ∖ A)) \land \exists s \in A s \in (a Itv (G) b))\} X) \land t \in A) \land t \in (Y Itv (G) X)) \to X \in B$
61	9 10 1 50 51 52 55 55 58 59 60	tglinethru	$⊢ ((((φ \land Y \neq X) \land Y \{⟨a, b⟩ \| ((a \in ({Base}_{G} ∖ A) \land b \in ({Base}_{G} ∖ A)) \land \exists s \in A s \in (a Itv (G) b))\} X) \land t \in A) \land t \in (Y Itv (G) X)) \to B = Y L X$
62	57 61	eleqtrrd	$⊢ ((((φ \land Y \neq X) \land Y \{⟨a, b⟩ \| ((a \in ({Base}_{G} ∖ A) \land b \in ({Base}_{G} ∖ A)) \land \exists s \in A s \in (a Itv (G) b))\} X) \land t \in A) \land t \in (Y Itv (G) X)) \to t \in B$
63		inelcm	$⊢ (t \in A \land t \in B) \to A \cap B \neq \emptyset$
64	49 62 63	syl2anc	$⊢ ((((φ \land Y \neq X) \land Y \{⟨a, b⟩ \| ((a \in ({Base}_{G} ∖ A) \land b \in ({Base}_{G} ∖ A)) \land \exists s \in A s \in (a Itv (G) b))\} X) \land t \in A) \land t \in (Y Itv (G) X)) \to A \cap B \neq \emptyset$
65		eqid	$⊢ dist (G) = dist (G)$
66	9 65 10 27 16 28	islnopp	$⊢ φ \to (Y \{⟨a, b⟩ \| ((a \in ({Base}_{G} ∖ A) \land b \in ({Base}_{G} ∖ A)) \land \exists s \in A s \in (a Itv (G) b))\} X \leftrightarrow ((\neg Y \in A \land \neg X \in A) \land \exists t \in A t \in (Y Itv (G) X)))$
67	66	adantr	$⊢ (φ \land Y \neq X) \to (Y \{⟨a, b⟩ \| ((a \in ({Base}_{G} ∖ A) \land b \in ({Base}_{G} ∖ A)) \land \exists s \in A s \in (a Itv (G) b))\} X \leftrightarrow ((\neg Y \in A \land \neg X \in A) \land \exists t \in A t \in (Y Itv (G) X)))$
68	67	simplbda	$⊢ ((φ \land Y \neq X) \land Y \{⟨a, b⟩ \| ((a \in ({Base}_{G} ∖ A) \land b \in ({Base}_{G} ∖ A)) \land \exists s \in A s \in (a Itv (G) b))\} X) \to \exists t \in A t \in (Y Itv (G) X)$
69	64 68	r19.29a	$⊢ ((φ \land Y \neq X) \land Y \{⟨a, b⟩ \| ((a \in ({Base}_{G} ∖ A) \land b \in ({Base}_{G} ∖ A)) \land \exists s \in A s \in (a Itv (G) b))\} X) \to A \cap B \neq \emptyset$
70	69	neneqd	$⊢ ((φ \land Y \neq X) \land Y \{⟨a, b⟩ \| ((a \in ({Base}_{G} ∖ A) \land b \in ({Base}_{G} ∖ A)) \land \exists s \in A s \in (a Itv (G) b))\} X) \to \neg A \cap B = \emptyset$
71	48 70	pm2.65da	$⊢ (φ \land Y \neq X) \to \neg Y \{⟨a, b⟩ \| ((a \in ({Base}_{G} ∖ A) \land b \in ({Base}_{G} ∖ A)) \land \exists s \in A s \in (a Itv (G) b))\} X$
72		simpr	$⊢ (((φ \land h \in ran E) \land A \subseteq h) \land B \subseteq h) \to B \subseteq h$
73	4	ad3antrrr	$⊢ (((φ \land h \in ran E) \land A \subseteq h) \land B \subseteq h) \to G \in 𝒢_{Tarski}$
74		simpllr	$⊢ (((φ \land h \in ran E) \land A \subseteq h) \land B \subseteq h) \to h \in ran E$
75	14	ad3antrrr	$⊢ (((φ \land h \in ran E) \land A \subseteq h) \land B \subseteq h) \to A \in ran L$
76	7	ad3antrrr	$⊢ (((φ \land h \in ran E) \land A \subseteq h) \land B \subseteq h) \to X \in B$
77	72 76	sseldd	$⊢ (((φ \land h \in ran E) \land A \subseteq h) \land B \subseteq h) \to X \in h$
78	35	adantr	$⊢ (φ \land X \in A) \to A \cap B = \emptyset$
79		simpr	$⊢ (φ \land X \in A) \to X \in A$
80	7	adantr	$⊢ (φ \land X \in A) \to X \in B$
81		inelcm	$⊢ (X \in A \land X \in B) \to A \cap B \neq \emptyset$
82	79 80 81	syl2anc	$⊢ (φ \land X \in A) \to A \cap B \neq \emptyset$
83	82	neneqd	$⊢ (φ \land X \in A) \to \neg A \cap B = \emptyset$
84	78 83	pm2.65da	$⊢ φ \to \neg X \in A$
85	84	ad3antrrr	$⊢ (((φ \land h \in ran E) \land A \subseteq h) \land B \subseteq h) \to \neg X \in A$
86	77 85	eldifd	$⊢ (((φ \land h \in ran E) \land A \subseteq h) \land B \subseteq h) \to X \in (h ∖ A)$
87		simplr	$⊢ (((φ \land h \in ran E) \land A \subseteq h) \land B \subseteq h) \to A \subseteq h$
88	9 1 2 73 74 75 86 87	plng3p	$⊢ (((φ \land h \in ran E) \land A \subseteq h) \land B \subseteq h) \to h = A E X$
89	72 88	sseqtrd	$⊢ (((φ \land h \in ran E) \land A \subseteq h) \land B \subseteq h) \to B \subseteq A E X$
90	8	ad3antrrr	$⊢ (((φ \land h \in ran E) \land A \subseteq h) \land B \subseteq h) \to Y \in B$
91	89 90	sseldd	$⊢ (((φ \land h \in ran E) \land A \subseteq h) \land B \subseteq h) \to Y \in (A E X)$
92	91	anasss	$⊢ ((φ \land h \in ran E) \land (A \subseteq h \land B \subseteq h)) \to Y \in (A E X)$
93	34	simpld	$⊢ φ \to \exists h \in ran E (A \subseteq h \land B \subseteq h)$
94	92 93	r19.29a	$⊢ φ \to Y \in (A E X)$
95	28 84	eldifd	$⊢ φ \to X \in ({Base}_{G} ∖ A)$
96	9 10 1 2 4 14 95 27 16	elplng	$⊢ φ \to (Y \in (A E X) \leftrightarrow (Y \in A \lor Y {hp}_{𝒢} (G) (A) X \lor Y \{⟨a, b⟩ \| ((a \in ({Base}_{G} ∖ A) \land b \in ({Base}_{G} ∖ A)) \land \exists s \in A s \in (a Itv (G) b))\} X))$
97	94 96	mpbid	$⊢ φ \to (Y \in A \lor Y {hp}_{𝒢} (G) (A) X \lor Y \{⟨a, b⟩ \| ((a \in ({Base}_{G} ∖ A) \land b \in ({Base}_{G} ∖ A)) \land \exists s \in A s \in (a Itv (G) b))\} X)$
98	97	adantr	$⊢ (φ \land Y \neq X) \to (Y \in A \lor Y {hp}_{𝒢} (G) (A) X \lor Y \{⟨a, b⟩ \| ((a \in ({Base}_{G} ∖ A) \land b \in ({Base}_{G} ∖ A)) \land \exists s \in A s \in (a Itv (G) b))\} X)$
99	47 71 98	ecase13d	$⊢ (φ \land Y \neq X) \to Y {hp}_{𝒢} (G) (A) X$
100	46 99	pm2.61dane	$⊢ φ \to Y {hp}_{𝒢} (G) (A) X$
101	9 10 1 4 14 16 27 28 100	hpgcom	$⊢ φ \to X {hp}_{𝒢} (G) (A) Y$

Metamath Proof Explorer

Theorem prlnghpg

Proof