Theorem prlngrcl1

Description: Reverse closure for parallelism. (Contributed by Thierry Arnoux, 5-Jul-2026)

	Ref	Expression
Hypotheses	prlngin0.l	|- L = ( LineG ` G )
	prlngin0.p	|- .|| = ( parlnG ` G )
	prlngin0.g	|- ( ph -> G e. V )
	prlngin0.1	|- ( ph -> A .|| B )
Assertion	prlngrcl1	|- ( ph -> A e. ran L )

Proof

Step	Hyp	Ref	Expression
1		prlngin0.l	|- L = ( LineG ` G )
2		prlngin0.p	|- .|| = ( parlnG ` G )
3		prlngin0.g	|- ( ph -> G e. V )
4		prlngin0.1	|- ( ph -> A .|| B )
5		eqid	|- ( PlnG ` G ) = ( PlnG ` G )
6	1 5 2 3	brprlng	|- ( ph -> ( A .|| B <-> ( ( A e. ran L /\ B e. ran L ) /\ ( A = B \/ ( E. h e. ran ( PlnG ` G ) ( A C_ h /\ B C_ h ) /\ ( A i^i B ) = (/) ) ) ) ) )
7	4 6	mpbid	|- ( ph -> ( ( A e. ran L /\ B e. ran L ) /\ ( A = B \/ ( E. h e. ran ( PlnG ` G ) ( A C_ h /\ B C_ h ) /\ ( A i^i B ) = (/) ) ) ) )
8	7	simplld	|- ( ph -> A e. ran L )