Theorem prlngref

Description: Parallelism is reflexive. Theorem 12.4 of Schwabhauser p. 122. (Contributed by Thierry Arnoux, 18-Jun-2026)

	Ref	Expression
Hypotheses	brprlng.l	$$⊢L={Line}_{𝒢}\left(G\right)$$
	brprlng.e	No typesetting found for |- E = ( PlnG ` G ) with typecode |-
	brprlng.p	No typesetting found for |- .|| = ( parlnG ` G ) with typecode |-
	brprlng.g	$$⊢\phi \to G\in V$$
	prlngref.1	$$⊢\phi \to A\in \mathrm{ran}L$$
Assertion	prlngref	$$⊢\phi \to A\underset{\dot{}}{\parallel }A$$

Proof

Step	Hyp	Ref	Expression
1		brprlng.l	$$⊢L={Line}_{𝒢}\left(G\right)$$
2		brprlng.e	Could not format E = ( PlnG ` G ) : No typesetting found for |- E = ( PlnG ` G ) with typecode |-
3		brprlng.p	Could not format .|| = ( parlnG ` G ) : No typesetting found for |- .|| = ( parlnG ` G ) with typecode |-
4		brprlng.g	$$⊢\phi \to G\in V$$
5		prlngref.1	$$⊢\phi \to A\in \mathrm{ran}L$$
6	5 5	jca	$$⊢\phi \to \left(A\in \mathrm{ran}L\wedge A\in \mathrm{ran}L\right)$$
7		eqidd	$$⊢\phi \to A=A$$
8	7	orcd	$$⊢\phi \to \left(A=A\vee \left(\exists h\in \mathrm{ran}E\left(A\subseteq h\wedge A\subseteq h\right)\wedge A\cap A=\varnothing \right)\right)$$
9	1 2 3 4	brprlng	$$⊢\phi \to \left(A\underset{\dot{}}{\parallel }A\leftrightarrow \left(\left(A\in \mathrm{ran}L\wedge A\in \mathrm{ran}L\right)\wedge \left(A=A\vee \left(\exists h\in \mathrm{ran}E\left(A\subseteq h\wedge A\subseteq h\right)\wedge A\cap A=\varnothing \right)\right)\right)\right)$$
10	6 8 9	mpbir2and	$$⊢\phi \to A\underset{\dot{}}{\parallel }A$$