prlngmo

Description: Playfair's axiom. Given a line A and a point X not on A , at most one line parallel to A can be drawn through X . Theorem 12.11 of Schwabhauser p. 123. Note that this is the first instance of a theorem where the geometry is required to be Euclidean, as expressed by G e. TarskiGE . Theorem A10 of Schwabhauser p. 24 is used, in the form of axtgeucl , in the proof of prlngmolem1 . See prlngex for the corresponding existence theorem. (Contributed by Thierry Arnoux, 5-Jul-2026)

	Ref	Expression
Hypotheses	prlngeu.p	$⊢ P = {Base}_{G}$
	prlngeu.l	$⊢ L = {Line}_{𝒢} (G)$
	prlngeu.r	No typesetting found for \|- .\|\| = ( parlnG ` G ) with typecode \|-
	prlngeu.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	prlngeu.a	$⊢ φ \to A \in ran L$
	prlngeu.x	$⊢ φ \to X \in (P ∖ A)$
	prlngeu.1	$⊢ φ \to G \in 𝒢_{Tarski}^{E}$
Assertion	prlngmo	$⊢ φ \to \exists^{*} b \in ran L (A \underset{˙}{∥} b \land X \in b)$

Proof

Step	Hyp	Ref	Expression
1		prlngeu.p	$⊢ P = {Base}_{G}$
2		prlngeu.l	$⊢ L = {Line}_{𝒢} (G)$
3		prlngeu.r	Could not format .\|\| = ( parlnG ` G ) : No typesetting found for \|- .\|\| = ( parlnG ` G ) with typecode \|-
4		prlngeu.g	$⊢ φ \to G \in 𝒢_{Tarski}$
5		prlngeu.a	$⊢ φ \to A \in ran L$
6		prlngeu.x	$⊢ φ \to X \in (P ∖ A)$
7		prlngeu.1	$⊢ φ \to G \in 𝒢_{Tarski}^{E}$
8		eleq1w	$⊢ x = z \to (x \in (P ∖ b) \leftrightarrow z \in (P ∖ b))$
9		eleq1w	$⊢ y = w \to (y \in (P ∖ b) \leftrightarrow w \in (P ∖ b))$
10	8 9	bi2anan9	$⊢ (x = z \land y = w) \to ((x \in (P ∖ b) \land y \in (P ∖ b)) \leftrightarrow (z \in (P ∖ b) \land w \in (P ∖ b)))$
11		eleq1w	$⊢ s = t \to (s \in (x Itv (G) y) \leftrightarrow t \in (x Itv (G) y))$
12	11	cbvrexvw	$⊢ \exists s \in b s \in (x Itv (G) y) \leftrightarrow \exists t \in b t \in (x Itv (G) y)$
13		oveq12	$⊢ (x = z \land y = w) \to x Itv (G) y = z Itv (G) w$
14	13	eleq2d	$⊢ (x = z \land y = w) \to (t \in (x Itv (G) y) \leftrightarrow t \in (z Itv (G) w))$
15	14	rexbidv	$⊢ (x = z \land y = w) \to (\exists t \in b t \in (x Itv (G) y) \leftrightarrow \exists t \in b t \in (z Itv (G) w))$
16	12 15	bitrid	$⊢ (x = z \land y = w) \to (\exists s \in b s \in (x Itv (G) y) \leftrightarrow \exists t \in b t \in (z Itv (G) w))$
17	10 16	anbi12d	$⊢ (x = z \land y = w) \to (((x \in (P ∖ b) \land y \in (P ∖ b)) \land \exists s \in b s \in (x Itv (G) y)) \leftrightarrow ((z \in (P ∖ b) \land w \in (P ∖ b)) \land \exists t \in b t \in (z Itv (G) w)))$
18	17	cbvopabv	$⊢ \{⟨x, y⟩ \| ((x \in (P ∖ b) \land y \in (P ∖ b)) \land \exists s \in b s \in (x Itv (G) y))\} = \{⟨z, w⟩ \| ((z \in (P ∖ b) \land w \in (P ∖ b)) \land \exists t \in b t \in (z Itv (G) w))\}$
19		eleq1w	$⊢ x = z \to (x \in (P ∖ A) \leftrightarrow z \in (P ∖ A))$
20		eleq1w	$⊢ y = w \to (y \in (P ∖ A) \leftrightarrow w \in (P ∖ A))$
21	19 20	bi2anan9	$⊢ (x = z \land y = w) \to ((x \in (P ∖ A) \land y \in (P ∖ A)) \leftrightarrow (z \in (P ∖ A) \land w \in (P ∖ A)))$
22		eleq1w	$⊢ s = v \to (s \in (x Itv (G) y) \leftrightarrow v \in (x Itv (G) y))$
23	22	cbvrexvw	$⊢ \exists s \in A s \in (x Itv (G) y) \leftrightarrow \exists v \in A v \in (x Itv (G) y)$
24	13	eleq2d	$⊢ (x = z \land y = w) \to (v \in (x Itv (G) y) \leftrightarrow v \in (z Itv (G) w))$
25	24	rexbidv	$⊢ (x = z \land y = w) \to (\exists v \in A v \in (x Itv (G) y) \leftrightarrow \exists v \in A v \in (z Itv (G) w))$
26	23 25	bitrid	$⊢ (x = z \land y = w) \to (\exists s \in A s \in (x Itv (G) y) \leftrightarrow \exists v \in A v \in (z Itv (G) w))$
27	21 26	anbi12d	$⊢ (x = z \land y = w) \to (((x \in (P ∖ A) \land y \in (P ∖ A)) \land \exists s \in A s \in (x Itv (G) y)) \leftrightarrow ((z \in (P ∖ A) \land w \in (P ∖ A)) \land \exists v \in A v \in (z Itv (G) w)))$
28	27	cbvopabv	$⊢ \{⟨x, y⟩ \| ((x \in (P ∖ A) \land y \in (P ∖ A)) \land \exists s \in A s \in (x Itv (G) y))\} = \{⟨z, w⟩ \| ((z \in (P ∖ A) \land w \in (P ∖ A)) \land \exists v \in A v \in (z Itv (G) w))\}$
29	1 2 3 4 5 6 7 18 28	prlngmolem2	$⊢ φ \to \exists^{*} b \in ran L (A \underset{˙}{∥} b \land X \in b)$

Metamath Proof Explorer

Theorem prlngmo

Proof