Theorem prlngrcl2

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

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

Proof

Step	Hyp	Ref	Expression
1		prlngin0.l	$$⊢L={Line}_{𝒢}\left(G\right)$$
2		prlngin0.p	Could not format .|| = ( parlnG ` G ) : No typesetting found for |- .|| = ( parlnG ` G ) with typecode |-
3		prlngin0.g	$$⊢\phi \to G\in V$$
4		prlngin0.1	$$⊢\phi \to A\underset{\dot{}}{\parallel }B$$
5		eqid	Could not format ( PlnG ` G ) = ( PlnG ` G ) : No typesetting found for |- ( PlnG ` G ) = ( PlnG ` G ) with typecode |-
6	1 5 2 3	brprlng	Could not format ( 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 ) = (/) ) ) ) ) ) : No typesetting found for |- ( 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 ) = (/) ) ) ) ) ) with typecode |-
7	4 6	mpbid	Could not format ( 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 ) = (/) ) ) ) ) : No typesetting found for |- ( 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 ) = (/) ) ) ) ) with typecode |-
8	7	simplrd	$$⊢\phi \to B\in \mathrm{ran}L$$