Theorem prlngeq

Description: Playfair's axiom, written as an equality: if two different lines are parallel to a given line at a given point, they are equal. (Contributed by Thierry Arnoux, 20-Jul-2026)

	Ref	Expression
Hypotheses	prlngeq.p	$$⊢P={\mathrm{Base}}_G$$
	prlngeq.r	No typesetting found for |- .|| = ( parlnG ` G ) with typecode |-
	prlngeq.g	$$⊢\phi \to G\in {𝒢}_{\mathrm{Tarski}}$$
	prlngeq.1	$$⊢\phi \to G\in {𝒢}_{\mathrm{Tarski}}^E$$
	prlngeq.b	$$⊢\phi \to A\underset{\dot{}}{\parallel }B$$
	prlngeq.c	$$⊢\phi \to A\underset{\dot{}}{\parallel }C$$
	prlngeq.2	$$⊢\phi \to X\in B$$
	prlngeq.3	$$⊢\phi \to X\in C$$
Assertion	prlngeq	$$⊢\phi \to B=C$$

Proof

Step	Hyp	Ref	Expression
1		prlngeq.p	$$⊢P={\mathrm{Base}}_G$$
2		prlngeq.r	Could not format .|| = ( parlnG ` G ) : No typesetting found for |- .|| = ( parlnG ` G ) with typecode |-
3		prlngeq.g	$$⊢\phi \to G\in {𝒢}_{\mathrm{Tarski}}$$
4		prlngeq.1	$$⊢\phi \to G\in {𝒢}_{\mathrm{Tarski}}^E$$
5		prlngeq.b	$$⊢\phi \to A\underset{\dot{}}{\parallel }B$$
6		prlngeq.c	$$⊢\phi \to A\underset{\dot{}}{\parallel }C$$
7		prlngeq.2	$$⊢\phi \to X\in B$$
8		prlngeq.3	$$⊢\phi \to X\in C$$
9		eqid	$$⊢{Line}_{𝒢}\left(G\right)={Line}_{𝒢}\left(G\right)$$
10	9 2 3 5	prlngrcl1	$$⊢\phi \to A\in \mathrm{ran}{Line}_{𝒢}\left(G\right)$$
11		eqid	$$⊢\mathrm{Itv}\left(G\right)=\mathrm{Itv}\left(G\right)$$
12	9 2 3 5	prlngrcl2	$$⊢\phi \to B\in \mathrm{ran}{Line}_{𝒢}\left(G\right)$$
13	1 9 11 3 12 7	tglnpt	$$⊢\phi \to X\in P$$
14	1 9 2 3 10 13 4	prlngmo2	$$⊢\phi \to {\exists }^{*}b\in \mathrm{ran}{Line}_{𝒢}\left(G\right)\left(A\underset{\dot{}}{\parallel }b\wedge X\in b\right)$$
15	5 7	jca	$$⊢\phi \to \left(A\underset{\dot{}}{\parallel }B\wedge X\in B\right)$$
16	9 2 3 6	prlngrcl2	$$⊢\phi \to C\in \mathrm{ran}{Line}_{𝒢}\left(G\right)$$
17	6 8	jca	$$⊢\phi \to \left(A\underset{\dot{}}{\parallel }C\wedge X\in C\right)$$
18		breq2	$$⊢b=B\to \left(A\underset{\dot{}}{\parallel }b\leftrightarrow A\underset{\dot{}}{\parallel }B\right)$$
19		eleq2	$$⊢b=B\to \left(X\in b\leftrightarrow X\in B\right)$$
20	18 19	anbi12d	$$⊢b=B\to \left(\left(A\underset{\dot{}}{\parallel }b\wedge X\in b\right)\leftrightarrow \left(A\underset{\dot{}}{\parallel }B\wedge X\in B\right)\right)$$
21		breq2	$$⊢b=C\to \left(A\underset{\dot{}}{\parallel }b\leftrightarrow A\underset{\dot{}}{\parallel }C\right)$$
22		eleq2	$$⊢b=C\to \left(X\in b\leftrightarrow X\in C\right)$$
23	21 22	anbi12d	$$⊢b=C\to \left(\left(A\underset{\dot{}}{\parallel }b\wedge X\in b\right)\leftrightarrow \left(A\underset{\dot{}}{\parallel }C\wedge X\in C\right)\right)$$
24	20 23	rmoi	$$⊢\left({\exists }^{*}b\in \mathrm{ran}{Line}_{𝒢}\left(G\right)\left(A\underset{\dot{}}{\parallel }b\wedge X\in b\right)\wedge \left(B\in \mathrm{ran}{Line}_{𝒢}\left(G\right)\wedge \left(A\underset{\dot{}}{\parallel }B\wedge X\in B\right)\right)\wedge \left(C\in \mathrm{ran}{Line}_{𝒢}\left(G\right)\wedge \left(A\underset{\dot{}}{\parallel }C\wedge X\in C\right)\right)\right)\to B=C$$
25	14 12 15 16 17 24	syl122anc	$$⊢\phi \to B=C$$