Theorem prlngrcl1

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

	Ref	Expression
Hypotheses	prlngin0.l	⊢ 𝐿 = ( LineG ‘ 𝐺 )
	prlngin0.p	⊢ ∥ = ( parlnG ‘ 𝐺 )
	prlngin0.g	⊢ ( 𝜑 → 𝐺 ∈ 𝑉 )
	prlngin0.1	⊢ ( 𝜑 → 𝐴 ∥ 𝐵 )
Assertion	prlngrcl1	⊢ ( 𝜑 → 𝐴 ∈ ran 𝐿 )

Proof

Step	Hyp	Ref	Expression
1		prlngin0.l	⊢ 𝐿 = ( LineG ‘ 𝐺 )
2		prlngin0.p	⊢ ∥ = ( parlnG ‘ 𝐺 )
3		prlngin0.g	⊢ ( 𝜑 → 𝐺 ∈ 𝑉 )
4		prlngin0.1	⊢ ( 𝜑 → 𝐴 ∥ 𝐵 )
5		eqid	⊢ ( hlG ‘ 𝐺 ) = ( hlG ‘ 𝐺 )
6	1 5 2 3	brprlng	⊢ ( 𝜑 → ( 𝐴 ∥ 𝐵 ↔ ( ( 𝐴 ∈ ran 𝐿 ∧ 𝐵 ∈ ran 𝐿 ) ∧ ( 𝐴 = 𝐵 ∨ ( ∃ ℎ ∈ ran ( hlG ‘ 𝐺 ) ( 𝐴 ⊆ ℎ ∧ 𝐵 ⊆ ℎ ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) ) ) ) )
7	4 6	mpbid	⊢ ( 𝜑 → ( ( 𝐴 ∈ ran 𝐿 ∧ 𝐵 ∈ ran 𝐿 ) ∧ ( 𝐴 = 𝐵 ∨ ( ∃ ℎ ∈ ran ( hlG ‘ 𝐺 ) ( 𝐴 ⊆ ℎ ∧ 𝐵 ⊆ ℎ ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) ) ) )
8	7	simplld	⊢ ( 𝜑 → 𝐴 ∈ ran 𝐿 )