Theorem prlngeu

Description: Given a line A and a point X not on A , a unique line parallel to A can be drawn through X . Theorem 12.13 of Schwabhauser p. 124. (Contributed by Thierry Arnoux, 5-Jul-2026)

	Ref	Expression
Hypotheses	prlngeu.p	$$⊢P={\mathrm{Base}}_G$$
	prlngeu.l	$$⊢L={Line}_{𝒢}\left(G\right)$$
	prlngeu.r	No typesetting found for |- .|| = ( parlnG ` G ) with typecode |-
	prlngeu.g	$$⊢\phi \to G\in {𝒢}_{\mathrm{Tarski}}$$
	prlngeu.a	$$⊢\phi \to A\in \mathrm{ran}L$$
	prlngeu.x	$$⊢\phi \to X\in \left(P\setminus A\right)$$
	prlngeu.1	$$⊢\phi \to G\in {𝒢}_{\mathrm{Tarski}}^E$$
Assertion	prlngeu	$$⊢\phi \to \exists !b\in \mathrm{ran}L\left(A\underset{\dot{}}{\parallel }b\wedge X\in b\right)$$

Proof

Step	Hyp	Ref	Expression
1		prlngeu.p	$$⊢P={\mathrm{Base}}_G$$
2		prlngeu.l	$$⊢L={Line}_{𝒢}\left(G\right)$$
3		prlngeu.r	Could not format .|| = ( parlnG ` G ) : No typesetting found for |- .|| = ( parlnG ` G ) with typecode |-
4		prlngeu.g	$$⊢\phi \to G\in {𝒢}_{\mathrm{Tarski}}$$
5		prlngeu.a	$$⊢\phi \to A\in \mathrm{ran}L$$
6		prlngeu.x	$$⊢\phi \to X\in \left(P\setminus A\right)$$
7		prlngeu.1	$$⊢\phi \to G\in {𝒢}_{\mathrm{Tarski}}^E$$
8	6	eldifad	$$⊢\phi \to X\in P$$
9	1 2 3 4 5 8	prlngex	$$⊢\phi \to \exists b\in \mathrm{ran}L\left(A\underset{\dot{}}{\parallel }b\wedge X\in b\right)$$
10	1 2 3 4 5 6 7	prlngmo	$$⊢\phi \to {\exists }^{*}b\in \mathrm{ran}L\left(A\underset{\dot{}}{\parallel }b\wedge X\in b\right)$$
11		reu5	$$⊢\exists !b\in \mathrm{ran}L\left(A\underset{\dot{}}{\parallel }b\wedge X\in b\right)\leftrightarrow \left(\exists b\in \mathrm{ran}L\left(A\underset{\dot{}}{\parallel }b\wedge X\in b\right)\wedge {\exists }^{*}b\in \mathrm{ran}L\left(A\underset{\dot{}}{\parallel }b\wedge X\in b\right)\right)$$
12	9 10 11	sylanbrc	$$⊢\phi \to \exists !b\in \mathrm{ran}L\left(A\underset{\dot{}}{\parallel }b\wedge X\in b\right)$$